From: Anders Mörtberg <mortberg@chalmers.se>
Date: Thu, 4 Jun 2015 20:34:47 +0000 (+0200)
Subject: Update squeezeHIT
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d5d1c9d8cccddafb79c1e424a0fcfd740ab0bfac;p=cubicaltt.git

Update squeezeHIT
---

diff --git a/Eval.hs b/Eval.hs
index 3144eef..1ff94cc 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -408,17 +408,21 @@ transpHIT i a u = squeezeHIT i a u `face` (i ~> 0)
 -- given u(i) of type a(i) "squeezeHIT i a u" connects in the direction i
 -- transHIT i a u(i=0) to u(i=1) in a(1)
 squeezeHIT :: Name -> Val -> Val -> Val
-squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of
+squeezeHIT i a@(Ter (HSum _ _ nass) env) u =
+ let j = fresh (a,u)
+     aij = swap a (i,j)
+ in
+ case u of
   VCon n us -> case lookupLabel n nass of
     Just as -> VCon n (squeezes i as env us)
     Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n
   VPCon c _ ws0 phis -> case lookupLabel c nass of
-    Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) (phis `face` (i ~> 1))
+    Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) phis
     Nothing -> error $ "squeezeHIT: missing path constructor " ++ c
   VHComp _ v vs ->
-    hComp (a `face` (i ~> 1)) (transpHIT i a v) $
+    hComp (a `face` (i ~> 1)) (squeezeHIT i a v) $
       mapWithKey (\alpha vAlpha ->
-                   VPath i $ squeezeHIT i (a `face` alpha) (vAlpha @@ i)) vs
+                   VPath j $ squeezeHIT j (aij `face` alpha) (vAlpha @@ j)) vs
   _ -> error $ "squeezeHIT: neutral " ++ show u
 
 hComp :: Val -> Val -> System Val -> Val
diff --git a/examples/integer.ctt b/examples/integer.ctt
index 8caa322..e100089 100644
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -63,21 +63,4 @@ test0 : Id (Id Z (inr zero) (inr zero)) (refl Z (inr zero)) (refl Z (inr zero))
 test1 : Id T p0 p1 = intSet (pos zero) (pos zero) p0 p1
 test2 : Id T p0 p0 = intSet (pos zero) (pos zero) p0 p0
 
-test3 : Id T p0 p1 = <i1 i2> comp (int) (comp (int) (comp (int) (pos zero) [ (i1 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i1 = 1) -> <i3> comp (int) (comp (int) (comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ] ], (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]
-
---test3 : 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) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i1 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> 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 ]
-
--- test2 : Id T p0 p1 =
---  <i j> comp int (pos zero)
---     [ (i = 1) ->
---   <k> comp int
---           (comp int (zeroP {int} @ j)
---           [ (j = 1) -> <l> zeroP {int} @ -l ])
---        [ (k = 0) -> <l> comp int (pos zero)
---                            [ (l = 0) -> <m> comp int (comp int (zeroP {int} @ (j /\ m))
---                                                           [ (m = 1) -> <n> comp int (zeroP {int} @ j)
---                                                                    [ (j = 1) -> <p> zeroP {int} @ (-n \/ -p) ] ])
---                                                [ (j = 1) -> <n> comp int (zeroP {int} @ (-n /\ m))
---                                                                    [ (m = 1) -> <p> zeroP {int} @ (-n /\ -p) ] ]]]]
-
--- test2 : Id T p0 p1 = <i1 i2> comp int (comp int (comp int (pos zero) [ (i1 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i1 = 1) -> <i3> comp int (comp int (comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ]) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ]) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ]) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ] ], (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]
+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 ]