Make bool, circle and integer compile

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 9dcc6ba72ab07bfcba9182f2d2634b21d55a3267..299ba60b4fe781ee678a4221f581a01263cf1256 100644 (file)
--- 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 f12b45dfa18ece4f65e7aa9bbef86fd7225ee360..ea3895719f0a509e888f90c0879eb59cbea2b8a6 100644 (file)
--- 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 e100089d8cadcfb77ef335c15ea267aea4ed6a48..fdf55a5816ac542a746878a4d16a5735d60048e3 100644 (file)
--- 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 36dc6ae54d90a1a75350d791214c4dd0d193d1e5..50adb42c46ce4682b4ed14dc9e2f28cce9833be6 100644 (file)
--- 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 03bb539a1dedc46b39ea1fb6205a5584700b788a..158660ec8155ae888938a3a0878ea39c08254816 100644 (file)
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -4,15 +4,20 @@ import prelude
 \r
 hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :\r
             Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = \r
- 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)))\r
-    (<i>(f a (refl A a)))\r
+ comp (<i> Square A a a (<_> a) a (p @ i) (<j> p @ i /\ j)\r
+                 (f a (<_> a)) (f (p @ i) (<j> p @ i /\ j)))\r
+      (<i> f a (<_> a)) []\r
 \r
-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 =\r
- <j i>comp (<_> A) a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j]\r
+hedberg (A : U) (a b : A) (h : (x : A) -> stable (Id A a x))\r
+        (p q : Id A a b) : Id (Id A a b) p q =\r
+ <j i> comp (<_> A) a [ (j = 0) -> rem2 @ i\r
+                      , (j = 1) -> rem3 @ i\r
+                      , (i = 0) -> r\r
+                      , (i = 1) -> rem4 @ j]\r
  where \r
-   ra : Id A a a = refl A a \r
-   rem1 (x:A) : exConst (Id A a x) = stableConst (Id A a x) (h x)\r
-   f (x:A) : Id A a x -> Id A a x  = (rem1 x).1\r
+   ra : Id A a a = <_> a \r
+   rem1 (x : A) : exConst (Id A a x) = stableConst (Id A a x) (h x)\r
+   f (x : A) : Id A a x -> Id A a x  = (rem1 x).1\r
    fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2\r
    rem4 : Square A a a ra b b (refl A b) (f b p) (f b q)  = fIsConst b p q\r
    r : Id A a a = f a ra\r
@@ -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\r
 \r
 hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A =\r
- \ (a b:A) -> hedberg A a b (h a)\r
+ \(a b : A) -> hedberg A a b (h a)\r
 \r
-{- normal form\r
- \(A : U) -> \r
- \(h : (a x : A) -> (((IdP (<!0> A) a x) -> N0) -> N0) -> (IdP (<!0> A) a x)) -> \r
- \(a b : A) -> \r
- \(p q : IdP (<!0> A) a b) ->\r
- <!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 ]\r
--}\r
-\r
-corrhedberg (A:U) (h : discrete A) : set A =\r
- \ (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 =\r
+ \(a b : A) -> hedberg A a b (\(b : A) -> decStable (Id A a b) (h a b))
\ No newline at end of file