non-trivial homotopy in the loop space of stwo

diff --git a/examples/pi1S2output.ctt b/examples/pi1S2output.ctt
new file mode 100644 (file)
index 0000000..a268409
--- /dev/null
+++ b/examples/pi1S2output.ctt
@@ -0,0 +1,17 @@
+module pi1S2output where
+
+import pi1S2
+
+loopSpace : U = Id stwo north north
+
+aLoop1 : loopSpace = refl stwo north
+aLoop2 : loopSpace = compId stwo north south north meridNstwo (<i>meridSstwo@-i)
+
+
+
+test2Normal : Id pi1stwo trivstwo loopstwo =
+  <i1> inc (<i2> comp stwo (comp stwo (comp stwo north [ (i2 = 1) -> <i3> comp stwo north [ (i1 = 1) -> <i4> comp stwo north [ (i4 = 1) -> <i5> comp stwo north [ (i5 = 1) -> <i6> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> merid {stwo} north @ -i4 ]) [ (i6 = 0) -> <i7> comp stwo north [ (i7 = 0) -> <i8> comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i9> comp stwo south [ (i8 = 0) -> <i10> comp stwo north [ (i10 = 0) -> <i11> comp stwo south [ (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ], (i9 = 0) -> <i11> comp stwo south [ (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i8 = 0) -> <i9> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> <i10> comp stwo north [ (i9 = 0) -> <i11> comp stwo south [ (i10 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ], (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ]) [ (i9 = 0) -> <i10> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i11> comp stwo south [ (i10 = 0) -> <i12> comp stwo north [ (i11 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ], (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ], (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0)(i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> comp stwo north [ (i4 = 0) -> <i5> comp stwo north [ (i5 = 1) -> <i6> merid {stwo} north @ i6 ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ], (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 0)(i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0) -> <i13> comp stwo north [ (i12 = 1)(i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 1) -> <i14> merid {stwo} north @ (i13 /\ i14) ] ]) [ (i12 = 1) -> <i13> comp stwo (merid {stwo} north @ (i13 /\ i3)) [ (i3 = 1) -> <i14> merid {stwo} north @ (i13 \/ i14) ] ]) [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 1) -> <i14> merid {stwo} north @ i14, (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0)(i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ]) [ (i3 = 1) -> <i11> comp stwo south [ (i10 = 0)(i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ]) [ (i3 = 1) -> <i10> comp stwo north [ (i10 = 0)(i9 = 0) -> <i11> comp stwo south [ (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i3 = 1) -> <i9> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i10> comp stwo south [ (i8 = 0) -> <i11> comp stwo north [ (i10 = 0) -> <i12> comp stwo south [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ], (i11 = 0) -> <i12> comp stwo south [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ] ]) [ (i8 = 0) -> <i10> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> <i11> comp stwo north [ (i10 = 0) -> <i12> comp stwo south [ (i11 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ], (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i12> comp stwo south [ (i11 = 0) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ], (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ], (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0)(i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i10> comp stwo north [ (i10 = 0) -> <i11> comp stwo north [ (i11 = 1) -> <i12> merid {stwo} north @ i12 ] ] ]) [ (i12 = 0) -> <i13> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 0) -> <i15> comp stwo north [ (i15 = 1) -> <i16> merid {stwo} north @ i16 ], (i14 = 0) -> <i15> comp stwo north [ (i15 = 1) -> <i16> merid {stwo} north @ i16 ] ] ]) [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 0)(i14 = 0) -> <i15> comp stwo north [ (i15 = 1) -> <i16> merid {stwo} north @ i16 ] ] ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i13 = 1)(i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i12 = 0) -> <i13> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 1) -> <i15> merid {stwo} north @ (i14 /\ i15) ] ]) [ (i13 = 1) -> <i14> comp stwo (merid {stwo} north @ (i14 /\ -i9)) [ (i9 = 0) -> <i15> merid {stwo} north @ (i14 \/ i15) ] ]) [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 1) -> <i15> merid {stwo} north @ i15, (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0)(i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ]) [ (i9 = 0) -> <i12> comp stwo south [ (i11 = 0)(i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ]) [ (i9 = 0) -> <i11> comp stwo north [ (i10 = 0)(i11 = 0) -> <i12> comp stwo south [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ] ] ]) [ (i8 = 1) -> <i9> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i9 = 0) -> <i10> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i11> merid {stwo} north @ (-i10 \/ -i11) ], (i9 = 1) -> <i10> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i11> merid {stwo} north @ (-i10 \/ -i11) ] ]) [ (i3 = 1) -> <i10> comp stwo (merid {stwo} north @ -i10) [ (i9 = 0) -> <i11> merid {stwo} north @ (-i10 /\ -i11), (i9 = 1) -> <i11> merid {stwo} north @ (-i10 /\ -i11) ] ] ] ] ] ] ] ] ]) [ (i1 = 1) -> <i3> comp stwo (comp stwo north [ (i2 = 1) -> <i3> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> merid {stwo} north @ -i4 ] ]) [ (i3 = 1) -> <i4> comp stwo (comp stwo north [ (i2 = 1) -> <i3> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> merid {stwo} north @ -i4 ] ]) [ (i4 = 0) -> <i5> comp stwo (comp stwo north [ (i2 = 1) -> <i6> comp stwo (merid {stwo} north @ (i5 /\ i6)) [ (i5 = 1)(i6 = 1) -> <i7> merid {stwo} north @ -i7 ] ]) [ (i2 = 1) -> <i6> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> <i7> merid {stwo} north @ -i7, (i6 = 1) -> <i7> merid {stwo} north @ -i7 ] ], (i4 = 1) -> <i5> comp stwo (comp stwo (merid {stwo} north @ (i5 /\ i2)) [ (i2 = 1)(i5 = 1) -> <i6> merid {stwo} north @ -i6 ]) [ (i2 = 1) -> <i6> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> <i7> merid {stwo} north @ -i7, (i6 = 1) -> <i7> merid {stwo} north @ -i7 ] ] ] ] ]) [ (i1 = 1) -> <i0> comp stwo (merid {stwo} north @ i2) [ (i2 = 1) -> <i3> merid {stwo} (comp sone north [ (i0 = 1) -> <i1> merid {sone} true @ i1 ]) @ -i3 ] ])
+
+
+test2loop : Id loopSpace aLoop1 aLoop2 =
+  <i1 i2> comp stwo (comp stwo (comp stwo north [ (i2 = 1) -> <i3> comp stwo north [ (i1 = 1) -> <i4> comp stwo north [ (i4 = 1) -> <i5> comp stwo north [ (i5 = 1) -> <i6> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> merid {stwo} north @ -i4 ]) [ (i6 = 0) -> <i7> comp stwo north [ (i7 = 0) -> <i8> comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i9> comp stwo south [ (i8 = 0) -> <i10> comp stwo north [ (i10 = 0) -> <i11> comp stwo south [ (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ], (i9 = 0) -> <i11> comp stwo south [ (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i8 = 0) -> <i9> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> <i10> comp stwo north [ (i9 = 0) -> <i11> comp stwo south [ (i10 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ], (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ]) [ (i9 = 0) -> <i10> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i11> comp stwo south [ (i10 = 0) -> <i12> comp stwo north [ (i11 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ], (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ], (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0)(i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> comp stwo north [ (i4 = 0) -> <i5> comp stwo north [ (i5 = 1) -> <i6> merid {stwo} north @ i6 ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ], (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 0)(i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0) -> <i13> comp stwo north [ (i12 = 1)(i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 1) -> <i14> merid {stwo} north @ (i13 /\ i14) ] ]) [ (i12 = 1) -> <i13> comp stwo (merid {stwo} north @ (i13 /\ i3)) [ (i3 = 1) -> <i14> merid {stwo} north @ (i13 \/ i14) ] ]) [ (i3 = 1) -> <i13> comp stwo north [ (i12 = 1) -> <i14> merid {stwo} north @ i14, (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> <i12> comp stwo north [ (i11 = 0)(i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ]) [ (i3 = 1) -> <i11> comp stwo south [ (i10 = 0)(i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ]) [ (i3 = 1) -> <i10> comp stwo north [ (i10 = 0)(i9 = 0) -> <i11> comp stwo south [ (i11 = 0) -> <i12> comp stwo north [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 1) -> <i14> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i3 = 1) -> <i9> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i10> comp stwo south [ (i8 = 0) -> <i11> comp stwo north [ (i10 = 0) -> <i12> comp stwo south [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ], (i11 = 0) -> <i12> comp stwo south [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ] ]) [ (i8 = 0) -> <i10> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> <i11> comp stwo north [ (i10 = 0) -> <i12> comp stwo south [ (i11 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ], (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> <i11> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i12> comp stwo south [ (i11 = 0) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ], (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ], (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0)(i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i10> comp stwo north [ (i10 = 0) -> <i11> comp stwo north [ (i11 = 1) -> <i12> merid {stwo} north @ i12 ] ] ]) [ (i12 = 0) -> <i13> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 0) -> <i15> comp stwo north [ (i15 = 1) -> <i16> merid {stwo} north @ i16 ], (i14 = 0) -> <i15> comp stwo north [ (i15 = 1) -> <i16> merid {stwo} north @ i16 ] ] ]) [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 0)(i14 = 0) -> <i15> comp stwo north [ (i15 = 1) -> <i16> merid {stwo} north @ i16 ] ] ] ] ]) [ (i11 = 0) -> <i12> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0) -> <i14> comp stwo north [ (i13 = 1)(i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i12 = 0) -> <i13> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 1) -> <i15> merid {stwo} north @ (i14 /\ i15) ] ]) [ (i13 = 1) -> <i14> comp stwo (merid {stwo} north @ (i14 /\ -i9)) [ (i9 = 0) -> <i15> merid {stwo} north @ (i14 \/ i15) ] ]) [ (i9 = 0) -> <i14> comp stwo north [ (i13 = 1) -> <i15> merid {stwo} north @ i15, (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> <i13> comp stwo north [ (i12 = 0)(i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ]) [ (i9 = 0) -> <i12> comp stwo south [ (i11 = 0)(i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ]) [ (i9 = 0) -> <i11> comp stwo north [ (i10 = 0)(i11 = 0) -> <i12> comp stwo south [ (i12 = 0) -> <i13> comp stwo north [ (i13 = 0) -> <i14> comp stwo north [ (i14 = 1) -> <i15> merid {stwo} north @ i15 ] ] ] ] ] ] ]) [ (i8 = 1) -> <i9> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i9 = 0) -> <i10> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i11> merid {stwo} north @ (-i10 \/ -i11) ], (i9 = 1) -> <i10> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i11> merid {stwo} north @ (-i10 \/ -i11) ] ]) [ (i3 = 1) -> <i10> comp stwo (merid {stwo} north @ -i10) [ (i9 = 0) -> <i11> merid {stwo} north @ (-i10 /\ -i11), (i9 = 1) -> <i11> merid {stwo} north @ (-i10 /\ -i11) ] ] ] ] ] ] ] ] ]) [ (i1 = 1) -> <i3> comp stwo (comp stwo north [ (i2 = 1) -> <i3> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> merid {stwo} north @ -i4 ] ]) [ (i3 = 1) -> <i4> comp stwo (comp stwo north [ (i2 = 1) -> <i3> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> <i4> merid {stwo} north @ -i4 ] ]) [ (i4 = 0) -> <i5> comp stwo (comp stwo north [ (i2 = 1) -> <i6> comp stwo (merid {stwo} north @ (i5 /\ i6)) [ (i5 = 1)(i6 = 1) -> <i7> merid {stwo} north @ -i7 ] ]) [ (i2 = 1) -> <i6> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> <i7> merid {stwo} north @ -i7, (i6 = 1) -> <i7> merid {stwo} north @ -i7 ] ], (i4 = 1) -> <i5> comp stwo (comp stwo (merid {stwo} north @ (i5 /\ i2)) [ (i2 = 1)(i5 = 1) -> <i6> merid {stwo} north @ -i6 ]) [ (i2 = 1) -> <i6> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> <i7> merid {stwo} north @ -i7, (i6 = 1) -> <i7> merid {stwo} north @ -i7 ] ] ] ] ]) [ (i1 = 1) -> <i0> comp stwo (merid {stwo} north @ i2) [ (i2 = 1) -> <i3> merid {stwo} (comp sone north [ (i0 = 1) -> <i1> merid {sone} true @ i1 ]) @ -i3 ] ]