From: Anders Mörtberg 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 = comp (int) (comp (int) (comp (int) (pos zero) [ (i1 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i1 = 1) -> comp (int) (comp (int) (comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ] ], (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ], (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ], (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ] - ---test3 : Id T p0 p0 = comp (int) (comp (int) (comp (int) (pos zero) [ (i1 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i1 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp (int) (pos zero) [ (i2 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 0) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp (int) (comp (int) (comp (int) (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> comp (int) (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp (int) (comp (int) (pos zero) [ ]) [ (i3 = 0) -> comp (int) (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> pos zero, (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> pos zero, (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ] - --- test2 : Id T p0 p1 = --- comp int (pos zero) --- [ (i = 1) -> --- comp int --- (comp int (zeroP {int} @ j) --- [ (j = 1) -> zeroP {int} @ -l ]) --- [ (k = 0) -> comp int (pos zero) --- [ (l = 0) -> comp int (comp int (zeroP {int} @ (j /\ m)) --- [ (m = 1) -> comp int (zeroP {int} @ j) --- [ (j = 1) ->

zeroP {int} @ (-n \/ -p) ] ]) --- [ (j = 1) -> comp int (zeroP {int} @ (-n /\ m)) --- [ (m = 1) ->

zeroP {int} @ (-n /\ -p) ] ]]]] - --- test2 : Id T p0 p1 = comp int (comp int (comp int (pos zero) [ (i1 = 0) -> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i1 = 1) -> comp int (comp int (comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ -i3 ]) [ (i2 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ -i3 ]) [ (i2 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i3 = 0) -> comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ -i3 ]) [ (i2 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ], (i2 = 1) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ] ] ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> comp int (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ -i3 ] ], (i2 = 0) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ ]) [ ]) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> comp int (pos zero) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (comp int (pos zero) [ ]) [ (i3 = 0) -> comp int (pos zero) [ ] ] ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> comp int (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ -i3 ], (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> comp int (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ -i3 ], (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ] +ntest2 : Id T p0 p0 = comp int (comp int (comp int (pos zero) [ (i1 = 0) -> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i4 = 0) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i6 = 0) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i1 = 1) -> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i4 = 0) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int(pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i6 = 0) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> pos zero, (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> pos zero, (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]