From: Anders <mortberg@chalmers.se>
Date: Mon, 8 Jun 2015 12:42:23 +0000 (+0200)
Subject: Make bool, circle and integer compile
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=8607a41482d90f917d435a9eff3fa49f751b9ac9;p=cubicaltt.git

Make bool, circle and integer compile
---

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 9dcc6ba..299ba60 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -13,9 +13,9 @@ negBoolK : (b : bool) -> Id bool (negBool (negBool b)) b = split
   true -> refl bool true
 
 negBoolEq : Id U bool bool =
-  <i> glue bool [ (i = 0) -> (bool,negBool,negBool,negBoolK,negBoolK) ]
+  isoId bool bool negBool negBool negBoolK negBoolK
 
-test : bool = transport negBoolEq true
+test : bool = trans bool bool negBoolEq true
 
 data F2 = zeroF2 | oneF2
 
@@ -53,12 +53,12 @@ negBool' : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2
 F2EqBoolComp : Id U F2 bool =
   compId U F2 bool bool F2EqBool negBoolEq
 
-test2 : bool = transport F2EqBoolComp oneF2
+test2 : bool = trans F2 bool F2EqBoolComp oneF2
 
 negNegEq : Id U bool bool =
   compId U bool bool bool negBoolEq negBoolEq
 
-test3 : bool = transport negNegEq true
+test3 : bool = trans bool bool negNegEq true
 test4 : Id U bool bool = <i> negNegEq @ i
 
 kanBool : Id U bool bool =
@@ -69,10 +69,10 @@ squareBoolF2 : Square U bool bool (refl U bool) bool F2
   <i j> boolEqF2 @ i /\ j
 
 test5 : IdP boolEqF2 true oneF2 = 
-  <i> transport (<j> boolEqF2 @ i /\ j) true
+  <i> comp (<j> boolEqF2 @ i /\ j) true []
 
 test6 : Id bool true true =
-  <i> transport (<j> F2EqBool @ i \/ j) (test5 @ - i)
+  <i> comp (<j> F2EqBool @ i \/ j) (test5 @ - i) []
 
 test7 : Id U F2 F2 =
   subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 negNegEq
@@ -81,7 +81,7 @@ test8 : Id U F2 F2 =
   subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 (refl U bool)
 
 test9 : Id U F2 F2 =
-  transport (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool)
+  comp (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) []
 
-p : Id U F2 bool = <i> comp (<_>U) bool [ (i = 0) -> boolEqF2 ]
+p : Id U F2 bool = <i> comp (<_> U) bool [ (i = 0) -> boolEqF2, (i = 1) -> <_> bool]
 q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file
diff --git a/examples/circle.ctt b/examples/circle.ctt
index f12b45d..ea38957 100644
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -20,7 +20,7 @@ helix : S1 -> U = split
   base -> Z
   loop @ i -> sucIdZ @ i
 
-winding (p : loopS1) : Z = transport rem zeroZ
+winding (p : loopS1) : Z = trans Z Z rem zeroZ
   where
     rem : Id U Z Z = <i> helix (p @ i)
 
diff --git a/examples/integer.ctt b/examples/integer.ctt
index e100089..fdf55a5 100644
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -60,7 +60,12 @@ p1 : T = compId int (pos zero) (neg zero) (pos zero) zeroP' (<i>zeroP'@-i)
 
 test0 : Id (Id Z (inr zero) (inr zero)) (refl Z (inr zero)) (refl Z (inr zero)) =
   ZSet (inr zero) (inr zero) (refl Z (inr zero)) (refl Z (inr zero))
+
+-- Tests for normal forms:
 test1 : Id T p0 p1 = intSet (pos zero) (pos zero) p0 p1
 test2 : Id T p0 p0 = intSet (pos zero) (pos zero) p0 p0
 
-ntest2 : Id T p0 p0 = <i1 i2> comp int (comp int (comp int (pos zero) [ (i1 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 0)(i4 = 1) -> <i5> comp int (pos zero) [ (i5 = 0) -> <i6> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i7 = 0) -> <i8> pos zero ] ]) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (comp int (pos zero) [  ]) [ (i7 = 0) -> <i8> comp int (pos zero) [  ] ] ], (i5 = 1) -> <i6> pos zero ], (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ], (i2 = 1) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 0)(i4 = 1) -> <i5> comp int (pos zero) [ (i5 = 0) -> <i6> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i7 = 0) -> <i8> pos zero ] ]) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (comp int (pos zero) [  ]) [ (i7 = 0) -> <i8> comp int (pos zero) [  ] ] ], (i5 = 1) -> <i6> pos zero ], (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ]) [ (i2 = 0) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i2 = 1) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i3 = 1) -> <i4> pos zero ]) [ (i2 = 0) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i2 = 1) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i3 = 0) -> <i4> comp int (pos zero) [ (i2 = 0) -> <i5> pos zero, (i2 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i2 = 0) -> <i6> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i7 = 1)(i8 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ] ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i5 = 0) -> <i8> pos zero, (i5 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> pos zero ], (i7 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> pos zero ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ] ]) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i9 = 0) -> <i10> pos zero ] ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i9 = 0) -> <i10> pos zero ] ] ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ] ] ], (i7 = 1) -> <i8> pos zero ] ], (i2 = 1) -> <i6> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i7 = 1)(i8 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ] ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i5 = 0) -> <i8> pos zero, (i5 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> pos zero ], (i7 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> pos zero ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ] ]) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i9 = 0) -> <i10> pos zero ] ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i9 = 0) -> <i10> pos zero ] ] ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ] ] ], (i7 = 1) -> <i8> pos zero ] ], (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i2 = 0) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1)(i7 = 1) -> <i8> comp int (pos zero) [ (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i8 = 1) -> <i9> pos zero ], (i7 = 0) -> <i8> pos zero ], (i2 = 1) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1)(i7 = 1) -> <i8> comp int (pos zero) [ (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i8 = 1) -> <i9> pos zero ], (i7 = 0) -> <i8> pos zero ], (i6 = 0) -> <i7> pos zero ] ]) [ (i2 = 0) -> <i6> pos zero, (i2 = 1) -> <i6> pos zero, (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ] ]) [ (i2 = 0) -> <i7> pos zero, (i2 = 1) -> <i7> pos zero, (i6 = 0) -> <i7> comp int (pos zero) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ] ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i1 = 1) -> <i3> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 0)(i4 = 1) -> <i5> comp int (pos zero) [ (i5 = 0) -> <i6> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i7 = 0) -> <i8> pos zero ] ]) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (comp int (pos zero) [  ]) [ (i7 = 0) -> <i8> comp int (pos zero) [  ] ] ], (i5 = 1) -> <i6> pos zero ], (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ], (i2 = 1) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ]) [ (i3 = 0)(i4 = 1) -> <i5> comp int (pos zero) [ (i5 = 0) -> <i6> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i7 = 0) -> <i8> pos zero ] ]) [ (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (comp int (pos zero) [  ]) [ (i7 = 0) -> <i8> comp int (pos zero) [  ] ] ], (i5 = 1) -> <i6> pos zero ], (i3 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ]) [ (i2 = 0) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i2 = 1) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i3 = 1) -> <i4> pos zero ]) [ (i2 = 0) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i2 = 1) -> <i4> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i3 = 0) -> <i4> comp int (pos zero) [ (i2 = 0) -> <i5> pos zero, (i2 = 1) -> <i5> pos zero, (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i2 = 0) -> <i6> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i7 = 1)(i8 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ] ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i5 = 0) -> <i8> pos zero, (i5 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> pos zero ], (i7 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> pos zero ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ] ]) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int(pos zero) [ (i9 = 0) -> <i10> pos zero ] ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i9 = 0) -> <i10> pos zero ] ] ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ] ] ], (i7 = 1) -> <i8> pos zero ] ], (i2 = 1) -> <i6> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero ]) [ (i5 = 0) -> <i7> pos zero, (i5 = 1) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i7 = 1)(i8 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ] ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ]) [ (i6 = 0) -> <i7> pos zero ] ], (i6 = 0) -> <i7> pos zero, (i6 = 1) -> <i7> comp int (pos zero) [ (i5 = 0) -> <i8> pos zero, (i5 = 1) -> <i8> comp int (pos zero) [ (i7 = 0) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1)(i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> pos zero ], (i7 = 1) -> <i9> pos zero, (i8 = 0) -> <i9> pos zero ], (i7 = 0) -> <i8> comp int (comp int (pos zero) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (pos zero) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero, (i9 = 0) -> <i11> pos zero ], (i9 = 0) -> <i10> pos zero ] ]) [ (i5 = 0) -> <i9> pos zero, (i5 = 1) -> <i9> comp int (comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i9 = 0) -> <i10> pos zero ] ]) [ (i8 = 0) -> <i10> pos zero, (i8 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (pos zero) [ (i9 = 0) -> <i10> pos zero ] ] ], (i8 = 0) -> <i9> pos zero, (i8 = 1) -> <i9> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i10> pos zero, (i5 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ], (i9 = 0) -> <i11> comp int (pos zero) [  ] ], (i9 = 0) -> <i10> comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ] ] ], (i7 = 1) -> <i8> pos zero ] ], (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i2 = 0) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1)(i7 = 1) -> <i8> comp int (pos zero) [ (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i8 = 1) -> <i9> pos zero ], (i7 = 0) -> <i8> pos zero ], (i2 = 1) -> <i7> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i7 = 0) -> <i8> pos zero ]) [ (i6 = 0) -> <i8> pos zero, (i6 = 1)(i7 = 1) -> <i8> comp int (pos zero) [ (i8 = 0) -> <i9> comp int (comp int (pos zero) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (pos zero) [ (i10 = 0) -> <i11> pos zero ] ]) [ (i9 = 0) -> <i10> pos zero, (i9 = 1) -> <i10> comp int (comp int (pos zero) [  ]) [ (i10 = 0) -> <i11> comp int (pos zero) [  ] ] ], (i8 = 1) -> <i9> pos zero ], (i7 = 0) -> <i8> pos zero ], (i6 = 0) -> <i7> pos zero ] ]) [ (i2 = 0) -> <i6> pos zero, (i2 = 1) -> <i6> pos zero, (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ] ]) [ (i2 = 0) -> <i7> pos zero, (i2 = 1) -> <i7> pos zero, (i6 = 0) -> <i7> comp int (pos zero) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ] ] ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 1) -> <i4> pos zero ]) [ (i3 = 0) -> <i4> comp int (pos zero) [ (i4 = 0) -> <i5> comp int (comp int (pos zero) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (pos zero) [ (i6 = 0) -> <i7> pos zero ] ]) [ (i5 = 0) -> <i6> pos zero, (i5 = 1) -> <i6> comp int (comp int (pos zero) [  ]) [ (i6 = 0) -> <i7> comp int (pos zero) [  ] ] ], (i4 = 1) -> <i5> pos zero ], (i3 = 1) -> <i4> pos zero ] ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> pos zero, (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> pos zero, (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]
+ntest1 : Id T p0 p1 = <i1 i2> comp (<_> int) (pos zero) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp (<_> int) (zeroP {int} @ (i2 /\ i3)) [ (i2 = 0) -> <i4> pos zero, (i2 = 1) -> <i4> zeroP {int} @ (-i4 /\ i3), (i3 = 0) -> <i4> pos zero, (i3 = 1) -> <i4> comp (<_> int) (zeroP {int} @ i2) [ (i2 = 0) -> <i5> pos zero, (i2 = 1) -> <i5> zeroP {int} @ (-i4 \/ -i5), (i4 = 0) -> <i5> zeroP {int} @ i2 ] ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]
+
+ntest2 : Id T p0 p0 = <i1 i2> comp (<_> int) (pos zero) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> pos zero, (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]
+
diff --git a/examples/interval.ctt b/examples/interval.ctt
index 36dc6ae..50adb42 100644
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -35,49 +35,12 @@ propI : prop I = subst U prop Unit I unitEqI propUnit
 
 setI : set I = subst U set Unit I unitEqI setUnit
 
-foo (X : U) : U = (x : X) -> Id X x x
-
 T : U = Id I zero zero
 p0 : T = refl I zero
 test : T = propI zero zero
 
-fooI : foo I = subst U foo Unit I unitEqI (\(x : Unit) -> <i> x)
-test2 : T = fooI zero
-
--- ntest2 : T = <i1> comp I (comp I (comp I zero [ (i1 = 0) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ], (i1 = 1) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ] ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]
-
--- test1 : T = <i1> comp I (comp I (comp I zero [ (i1 = 0) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ], (i1 = 1) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ] ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]
-
-
--- [ (i2 = 0) -> <i2> zero
--- , (i2 = 1) -> <i2> comp (<_> I) (comp (<_> I) zero [])
---                                 [ (i2 = 0) -> <i2> comp (<_> I) zero []]]
-
--- with zero
-
 
-test : Unit = transport (<i> unitEqI @ -i) zero
-test' : IdP (<i> unitEqI @ -i) zero tt =
-  <i> genComp (<k> unitEqI @ -i \/ -k) zero [(i = 0) -> <_> zero]
 
-test'' : Id I zero zero = <i0> comp I
-             (comp I
-               (comp I zero [ (i0 = 0) -> <i1> zero ])
-                 [ (i0 = 0) -> <i1> zero ])
-             [ (i0 = 0) -> <i1> zero, (i0 = 1) -> <i1> comp I zero [ (i1 = 0) -> <i1> comp I zero [ (i1 = 0) -> <i1> zero, (i1 = 1) -> <i1> comp I (comp I zero [  ]) [ (i1 = 0) -> <i1> comp I zero [  ] ] ], (i1 = 1) -> <i1> zero ] ]
 
--- -- <i0> glueElem
---            (comp I
---              (comp I
---                (comp I zero [ (i0 = 0) -> <i1> zero ])
---                  [ (i0 = 0) -> <i1> zero ])
---              [ (i0 = 0) -> <i1> zero, (i0 = 1) -> <i1> comp I zero [ (i1 = 0) -> <i1> comp I zero [ (i1 = 0) -> <i1> zero, (i1 = 1) -> <i1> comp I (comp I zero [  ]) [ (i1 = 0) -> <i1> comp I zero [  ] ] ], (i1 = 1) -> <i1> zero ] ])
---            [ (i0 = 1) -> tt ]
 
--- test : I = transport unitEqI tt
--- eqttzero : IdP unitEqI tt zero =
---   <i> genComp (<j> unitEqI @ -i \/ -j) zero [(i=1) -> <_>zero]
---  <i> transport (<j> unitEqI @ -i \/ -j) zero
---  <i> genComp (<j> unitEqI @ i /\ j) tt [(i=0) -> tt]
 
--- Type checking failed: path endpoints don't match for comp (<j> unitEqI @ (i /\ j)) tt [  ], got (tt,comp I (comp I (comp I zero [  ]) [  ]) [  ]), but expected (tt,zero)
diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
index 03bb539..158660e 100644
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -4,15 +4,20 @@ import prelude
 
 hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :
             Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = 
- transport (<i>Square A a a (refl A a) a (p@i) (<j>p@i/\j) (f a (refl A a)) (f (p@i) (<j>p@i/\j)))
-    (<i>(f a (refl A a)))
+ comp (<i> Square A a a (<_> a) a (p @ i) (<j> p @ i /\ j)
+                 (f a (<_> a)) (f (p @ i) (<j> p @ i /\ j)))
+      (<i> f a (<_> a)) []
 
-hedberg (A:U) (a b:A) (h: (x:A) -> stable (Id A a x)) (p q : Id A a b) : Id (Id A a b) p q =
- <j i>comp (<_> A) a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j]
+hedberg (A : U) (a b : A) (h : (x : A) -> stable (Id A a x))
+        (p q : Id A a b) : Id (Id A a b) p q =
+ <j i> comp (<_> A) a [ (j = 0) -> rem2 @ i
+                      , (j = 1) -> rem3 @ i
+                      , (i = 0) -> r
+                      , (i = 1) -> rem4 @ j]
  where 
-   ra : Id A a a = refl A a 
-   rem1 (x:A) : exConst (Id A a x) = stableConst (Id A a x) (h x)
-   f (x:A) : Id A a x -> Id A a x  = (rem1 x).1
+   ra : Id A a a = <_> a 
+   rem1 (x : A) : exConst (Id A a x) = stableConst (Id A a x) (h x)
+   f (x : A) : Id A a x -> Id A a x  = (rem1 x).1
    fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2
    rem4 : Square A a a ra b b (refl A b) (f b p) (f b q)  = fIsConst b p q
    r : Id A a a = f a ra
@@ -20,15 +25,7 @@ hedberg (A:U) (a b:A) (h: (x:A) -> stable (Id A a x)) (p q : Id A a b) : Id (Id
    rem3 : Square A a a ra a b q r (f b q) = hedbergLemma A a b f q
 
 hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A =
- \ (a b:A) -> hedberg A a b (h a)
+ \(a b : A) -> hedberg A a b (h a)
 
-{- normal form
- \(A : U) -> 
- \(h : (a x : A) -> (((IdP (<!0> A) a x) -> N0) -> N0) -> (IdP (<!0> A) a x)) -> 
- \(a b : A) -> 
- \(p q : IdP (<!0> A) a b) ->
- <!0 !1> comp A a [ (!0 = 0) -> <!2> comp A (comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !2) [ (!2 = 1) -> <!3> p @ (!3 /\ !1) ]) [ (!1 = 1) -> <!3> comp A (h a (p @ !3) (\(h0 : (IdP (<!1> A) a (p @ !3)) -> N0) -> h0 (<!1> p @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> <!4> p @ (!3 \/ !4) ] ], (!0 = 1) -> <!2> comp A (comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !2) [ (!2 = 1) -> <!3> q @ (!3 /\ !1) ]) [ (!1 = 1) -> <!3> comp A (h a (q @ !3) (\(h0 : (IdP (<!1> A) a (q @ !3)) -> N0) -> h0 (<!1> q @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> <!4> q @ (!3 \/ !4) ] ], (!1 = 0) -> <!2> h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !2, (!1 = 1) -> <!2> h a b (\(x : (IdP (<!0> A) a b) -> N0) -> efq (IdP (<!0> N0) (x p) (x q)) (x p) @ !0) @ !2 ]
--}
-
-corrhedberg (A:U) (h : discrete A) : set A =
- \ (a b :A) -> hedberg A a b (\ (b:A) -> decStable (Id A a b) (h a b))
\ No newline at end of file
+corrhedberg (A : U) (h : discrete A) : set A =
+ \(a b : A) -> hedberg A a b (\(b : A) -> decStable (Id A a b) (h a b))
\ No newline at end of file