From: Anders Date: Tue, 21 Apr 2015 12:38:16 +0000 (+0200) Subject: Improve printing of lambdas and paths X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9766157e93a1e6826e2e5df7b1ce6ac3165ea541;p=cubicaltt.git Improve printing of lambdas and paths --- diff --git a/CTT.hs b/CTT.hs index b9dfb0b..27be0be 100644 --- a/CTT.hs +++ b/CTT.hs @@ -382,19 +382,18 @@ showVal v = case v of <+> (hsep $ map ((char '@' <+>) . showFormula) phis) VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b - | otherwise -> parens (text x <+> colon <+> showVal t) <+> text "->" <+> showVal b + | otherwise -> char '(' <> showLam v VPi a b -> text "Pi" <+> showVals [a,b] VPair u v -> parens (showVal u <> comma <> showVal v) VSigma u v -> text "Sigma" <+> showVals [u,v] VApp u v -> showVal u <+> showVal1 v - VLam x t e -> char '\\' <> parens (text x <+> colon <+> showVal t) <+> - text "->" <+> showVal e + VLam{} -> text "\\(" <> showLam v + VPath{} -> char '<' <> showPath v VSplit u v -> showVal u <+> showVal1 v VVar x _ -> text x VFst u -> showVal1 u <> text ".1" VSnd u -> showVal1 u <> text ".2" VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] - VPath i v -> char '<' <> text (show i) <> char '>' <+> showVal v VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) VTrans v0 v1 -> text "trans" <+> showVals [v0,v1] @@ -405,6 +404,27 @@ showVal v = case v of VElimComp a es t -> text "elimComp" <+> showVal1 a <+> text (showSystem es) <+> showVal1 t +showPath :: Val -> Doc +showPath e = case e of + VPath i a@VPath{} -> text (show i) <+> showPath a + VPath i a -> text (show i) <> char '>' <+> showVal a + _ -> showVal e + +-- Merge lambdas of the same type +showLam :: Val -> Doc +showLam e = case e of + VLam x t a@(VLam _ t' _) + | t == t' -> text x <+> showLam a + | otherwise -> text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a + VPi _ (VLam x t a@(VPi _ (VLam _ t' _))) + | t == t' -> text x <+> showLam a + | otherwise -> text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a + VLam x t e -> + text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal e + VPi _ (VLam x t e) -> + text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal e + _ -> showVal e + showVal1 :: Val -> Doc showVal1 v = case v of VU -> showVal v @@ -416,3 +436,4 @@ showVal1 v = case v of showVals :: [Val] -> Doc showVals = hsep . map showVal1 + diff --git a/examples/prop.ctt b/examples/prop.ctt index cb6d02c..f9af4ed 100644 --- a/examples/prop.ctt +++ b/examples/prop.ctt @@ -8,19 +8,28 @@ lemProp (A B : U) (f : A -> B) (g : B -> A) \ (b0 b1:B) -> subst U prop A B (isoId A B f g s t) pA b0 b1 {- normal form -\(A : U) -> \(B : U) -> \(f : A -> B) -> \(g : B -> A) -> - \(s : \(y : B) -> IdP ( B) (f (g y)) y) -> - \(t : \(x : A) -> IdP ( A) (g (f x)) x) -> - \(pA : \(a : A) -> \(b : A) -> IdP ( A) a b) -> - \(b0 : B) -> \(b1 : B) -> - comp B (f (pA (g b0) (g b1) @ j)) - [ (j = 0) -> comp B b0 - [ (i = 0) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) - [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] - ] - , (j = 1) -> comp B b1 [ (i = 0) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) - [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ] - ] + +\(A B : U) -> \(f : A -> B) -> \(g : B -> A) -> + \(s : (y : B) -> IdP ( B) (f (g y)) y) -> + \(t : (x : A) -> IdP ( A) (g (f x)) x) -> + \(pA : (a : A) -> (b : A) -> IdP ( A) a b) -> + \(b0 b1 : B) -> + comp B (f (pA (g b0) (g b1) @ !1)) + [ (!1 = 0) -> comp B b0 + [ (!2 = 0) -> comp B (f (comp A (g b0) + [ (!3 = 1) -> t (g b0) @ -!4 ])) + [ (!3 = 0) -> s b0 @ !4, (!3 = 1) -> s (f (g b0)) @ !4 ] + ] + , (!1 = 1) -> comp B b1 [ (!2 = 0) -> comp B (f (comp A (g b1) [ (!3 = 1) -> t (g b1) @ -!4 ])) + [ (!3 = 0) -> s b1 @ !4, (!3 = 1) -> s (f (g b1)) @ !4 ] ] ] + +\(A B : U) -> \(f : A -> B) -> \(g : B -> A) -> + \(s : (y : B) -> IdP ( B) (f (g y)) y) -> + \(t : (x : A) -> IdP ( A) (g (f x)) x) -> + \(pA : (a b : A) -> IdP ( A) a b) -> + \(b0 b1 : B) -> + comp B (f (pA (g b0) (g b1) @ !1)) [ (!1 = 0) -> comp B b0 [ (!2 = 0) -> comp B (f (comp A (g b0) [ (!3 = 1) -> t (g b0) @ -!4 ])) [ (!3 = 0) -> s b0 @ !4, (!3 = 1) -> s (f (g b0)) @ !4 ] ], (!1 = 1) -> comp B b1 [ (!2 = 0) -> comp B (f (comp A (g b1) [ (!3 = 1) -> t (g b1) @ -!4 ])) [ (!3 = 0) -> s b1 @ !4, (!3 = 1) -> s (f (g b1)) @ !4 ] ] ] + -} lemSet (A B : U) (f : A -> B) (g : B -> A) @@ -29,10 +38,13 @@ lemSet (A B : U) (f : A -> B) (g : B -> A) \ (b0 b1:B) (p q : Id B b0 b1) -> subst U set A B (isoId A B f g s t) sA b0 b1 p q {- normal form -\(A : U) -> \(B : U) -> - \(f : A -> B) -> \(g : B -> A) -> - \(s : \(y : B) -> IdP ( B) (f (g y)) y) -> - \(t : \(x : A) -> IdP ( A) (g (f x)) x) -> - \(sA : \(a : A) -> \(b : A) -> \(a0 : IdP ( A) a b) -> \(b0 : IdP ( A) a b) -> IdP ( IdP ( A) a b) a0 b0) -> \(b0 : B) -> \(b1 : B) -> \(p : IdP ( B) b0 b1) -> \(q : IdP ( B) b0 b1) -> - comp B (comp B (f (sA (g b0) (g b1) ( comp A (g (p @ j)) [ (j = 0) -> comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ], (j = 1) -> comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ] ]) ( comp A (g (q @ j)) [ (j = 0) -> comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ], (j = 1) -> comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ] ]) @ j @ k)) [ (k = 0) -> comp B b0 [ (i = 0) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ], (k = 1) -> comp B b1 [ (i = 0) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ] ]) [ (j = 0) -> comp B (comp B (comp B (comp B (p @ k) [ (i = 0) -> comp B (f (comp A (g (p @ k)) [ (j = 1) -> t (g (p @ k)) @ -i ])) [ (j = 0) -> s (p @ k) @ i, (j = 1) -> s (f (g (p @ k))) @ i ] ]) [ (k = 0) -> comp B (comp B b0 [ (i = 0)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ (k /\ i) ]) [ (j = 1) -> t (g b0) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b0)) @ i, (k = 0) -> s (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ])) @ i ] ], (k = 1) -> comp B (comp B b1 [ (i = 0)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ (k /\ i) ]) [ (j = 1) -> t (g b1) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b1)) @ i, (k = 0) -> s (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ])) @ i ] ] ]) [ (i = 0) -> comp B (f (g (p @ k))) [ (j = 0) -> comp B (f (g (p @ k))) [ (k = 0) -> f (comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ]) ], (j = 1) -> f (comp A (g (p @ k)) [ (k = 0) -> comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ], (k = 1) -> comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ] ]), (k = 0) -> f (comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ]) ] ]) [ (k = 0) -> comp B b0 [ (i = 0)(j = 0) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ], (k = 1) -> comp B b1 [ (i = 0)(j = 0) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ] ], (j = 1) -> comp B (comp B (comp B (comp B (q @ k) [ (i = 0) -> comp B (f (comp A (g (q @ k)) [ (j = 1) -> t (g (q @ k)) @ -i ])) [ (j = 0) -> s (q @ k) @ i, (j = 1) -> s (f (g (q @ k))) @ i ] ]) [ (k = 0) -> comp B (comp B b0 [ (i = 0)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ (k /\ i) ]) [ (j = 1) -> t (g b0) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b0)) @ i, (k = 0) -> s (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b0 [ (j = 1) -> comp B (f (comp A (g b0) [ (i = 1) -> t (g b0) @ -j ])) [ (i = 0) -> s b0 @ j, (i = 1) -> s (f (g b0)) @ j ] ])) [ (j = 1) -> t (g b0) @ i ])) @ i ] ], (k = 1) -> comp B (comp B b1 [ (i = 0)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ]) [ (i = 0) -> comp B (f (comp A (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ (k /\ i) ]) [ (j = 1) -> t (g b1) @ (k /\ -i), (k = 1) -> t (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ]) @ -i ])) [ (j = 1) -> s (f (g b1)) @ i, (k = 0) -> s (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ]) @ i, (k = 1) -> s (f (comp A (g (comp B b1 [ (j = 1) -> comp B (f (comp A (g b1) [ (i = 1) -> t (g b1) @ -j ])) [ (i = 0) -> s b1 @ j, (i = 1) -> s (f (g b1)) @ j ] ])) [ (j = 1) -> t (g b1) @ i ])) @ i ] ] ]) [ (i = 0) -> comp B (f (g (q @ k))) [ (j = 0) -> comp B (f (g (q @ k))) [ (k = 0) -> f (comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ]) ], (j = 1) -> f (comp A (g (q @ k)) [ (k = 0) -> comp A (g (comp B b0 [ (i = 1)(j = 1) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b0) @ k ], (k = 1) -> comp A (g (comp B b1 [ (i = 1)(j = 1) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1)(j = 1) -> t (g b1) @ k ] ]), (k = 0) -> f (comp A (g (comp B b0 [ (i = 1) -> comp B (f (comp A (g b0) [ (j = 1) -> t (g b0) @ -i ])) [ (j = 0) -> s b0 @ i, (j = 1) -> s (f (g b0)) @ i ] ])) [ (i = 1) -> t (g b0) @ j ]), (k = 1) -> f (comp A (g (comp B b1 [ (i = 1) -> comp B (f (comp A (g b1) [ (j = 1) -> t (g b1) @ -i ])) [ (j = 0) -> s b1 @ i, (j = 1) -> s (f (g b1)) @ i ] ])) [ (i = 1) -> t (g b1) @ j ]) ] ]) [ (k = 0) -> comp B b0 [ (i = 0)(j = 0) -> comp B (f (comp A (g b0) [ (k = 1) -> t (g b0) @ -i ])) [ (k = 0) -> s b0 @ i, (k = 1) -> s (f (g b0)) @ i ] ], (k = 1) -> comp B b1 [ (i = 0)(j = 0) -> comp B (f (comp A (g b1) [ (k = 1) -> t (g b1) @ -i ])) [ (k = 0) -> s b1 @ i, (k = 1) -> s (f (g b1)) @ i ] ] ] ] + +\(A B : U) -> \(f : A -> B) -> \(g : B -> A) -> + \(s : (y : B) -> IdP ( B) (f (g y)) y) -> + \(t : (x : A) -> IdP ( A) (g (f x)) x) -> + \(sA : (a b : A) -> (a0 b0 : IdP ( A) a b) -> IdP ( IdP ( A) a b) a0 b0) -> + \(b0 b1 : B) -> + \(p q : IdP ( B) b0 b1) -> + comp B (comp B (f (sA (g b0) (g b1) ( comp A (g (p @ !1)) [ (!1 = 0) -> comp A (g (comp B b0 [ (!2 = 1) -> comp B (f (comp A (g b0) [ (!3 = 1) -> t (g b0) @ -!4 ])) [ (!3 = 0) -> s b0 @ !4, (!3 = 1) -> s (f (g b0)) @ !4 ] ])) [ (!2 = 1) -> t (g b0) @ !3 ], (!1 = 1) -> comp A (g (comp B b1 [ (!2 = 1) -> comp B (f (comp A (g b1) [ (!3 = 1) -> t (g b1) @ -!4 ])) [ (!3 = 0) -> s b1 @ !4, (!3 = 1) -> s (f (g b1)) @ !4 ] ])) [ (!2 = 1) -> t (g b1) @ !3 ] ]) ( comp A (g (q @ !1)) [ (!1 = 0) -> comp A (g (comp B b0 [ (!2 = 1) -> comp B (f (comp A (g b0) [ (!3 = 1) -> t (g b0) @ -!4 ])) [ (!3 = 0) -> s b0 @ !4, (!3 = 1) -> s (f (g b0)) @ !4 ] ])) [ (!2 = 1) -> t (g b0) @ !3 ], (!1 = 1) -> comp A (g (comp B b1 [ (!2 = 1) -> comp B (f (comp A (g b1) [ (!3 = 1) -> t (g b1) @ -!4 ])) [ (!3 = 0) -> s b1 @ !4, (!3 = 1) -> s (f (g b1)) @ !4 ] ])) [ (!2 = 1) -> t (g b1) @ !3 ] ]) @ !1 @ !2)) [ (!2 = 0) -> comp B b0 [ (!3 = 0) -> comp B (f (comp A (g b0) [ (!4 = 1) -> t (g b0) @ -!5 ])) [ (!4 = 0) -> s b0 @ !5, (!4 = 1) -> s (f (g b0)) @ !5 ] ], (!2 = 1) -> comp B b1 [ (!3 = 0) -> comp B (f (comp A (g b1) [ (!4 = 1) -> t (g b1) @ -!5 ])) [ (!4 = 0) -> s b1 @ !5, (!4 = 1) -> s (f (g b1)) @ !5 ] ] ]) [ (!1 = 0) -> comp B (comp B (comp B (comp B (p @ !2) [ (!3 = 0) -> comp B (f (comp A (g (p @ !2)) [ (!4 = 1) -> t (g (p @ !2)) @ -!5 ])) [ (!4 = 0) -> s (p @ !2) @ !5, (!4 = 1) -> s (f (g (p @ !2))) @ !5 ] ]) [ (!2 = 0) -> comp B (comp B b0 [ (!3 = 0)(!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ]) [ (!3 = 0) -> comp B (f (comp A (comp A (g (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> t (g b0) @ (!5 /\ !6) ]) [ (!4 = 1) -> t (g b0) @ (!5 /\ -!6), (!5 = 1) -> t (comp A (g (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> t (g b0) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> s (f (g b0)) @ !6, (!5 = 0) -> s (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ]) @ !6, (!5 = 1) -> s (f (comp A (g (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> t (g b0) @ !5 ])) @ !6 ] ], (!2 = 1) -> comp B (comp B b1 [ (!3 = 0)(!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ]) [ (!3 = 0) -> comp B (f (comp A (comp A (g (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> t (g b1) @ (!5 /\ !6) ]) [ (!4 = 1) -> t (g b1) @ (!5 /\ -!6), (!5 = 1) -> t (comp A (g (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> t (g b1) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> s (f (g b1)) @ !6, (!5 = 0) -> s (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ]) @ !6, (!5 = 1) -> s (f (comp A (g (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> t (g b1) @ !5 ])) @ !6 ] ] ]) [ (!3 = 0) -> comp B (f (g (p @ !2))) [ (!2 = 0) -> f (comp A (g (comp B b0 [ (!5 = 1) -> comp B (f (comp A (g b0) [ (!6 = 1) -> t (g b0) @ -!7 ])) [ (!6 = 0) -> s b0 @ !7, (!6 = 1) -> s (f (g b0)) @ !7 ] ])) [ (!5 = 1) -> t (g b0) @ !6 ]), (!2 = 1) -> f (comp A (g (comp B b1 [ (!5 = 1) -> comp B (f (comp A (g b1) [ (!6 = 1) -> t (g b1) @ -!7 ])) [ (!6 = 0) -> s b1 @ !7, (!6 = 1) -> s (f (g b1)) @ !7 ] ])) [ (!5 = 1) -> t (g b1) @ !6 ]), (!4 = 0) -> comp B (f (g (p @ !2))) [ (!2 = 0) -> f (comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b0) [ (!7 = 1) -> t (g b0) @ -!8 ])) [ (!7 = 0) -> s b0 @ !8, (!7 = 1) -> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b0) @ !7 ]), (!2 = 1) -> f (comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b1) [ (!7 = 1) -> t (g b1) @ -!8 ])) [ (!7 = 0) -> s b1 @ !8, (!7 = 1) -> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b1) @ !7 ]) ], (!4 = 1) -> f (comp A (g (p @ !2)) [ (!2 = 0) -> comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b0) [ (!7 = 1) -> t (g b0) @ -!8 ])) [ (!7 = 0) -> s b0 @ !8, (!7 = 1) -> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b0) @ !7 ], (!2 = 1) -> comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b1) [ (!7 = 1) -> t (g b1) @ -!8 ])) [ (!7 = 0) -> s b1 @ !8, (!7 = 1) -> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b1) @ !7 ] ]) ] ]) [ (!2 = 0) -> comp B b0 [ (!3 = 0)(!4 = 0) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ], (!2 = 1) -> comp B b1 [ (!3 = 0)(!4 = 0) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ] ], (!1 = 1) -> comp B (comp B (comp B (comp B (q @ !2) [ (!3 = 0) -> comp B (f (comp A (g (q @ !2)) [ (!4 = 1) -> t (g (q @ !2)) @ -!5 ])) [ (!4 = 0) -> s (q @ !2) @ !5, (!4 = 1) -> s (f (g (q @ !2))) @ !5 ] ]) [ (!2 = 0) -> comp B (comp B b0 [ (!3 = 0)(!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ]) [ (!3 = 0) -> comp B (f (comp A (comp A (g (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> t (g b0) @ (!5 /\ !6) ]) [ (!4 = 1) -> t (g b0) @ (!5 /\ -!6), (!5 = 1) -> t (comp A (g (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> t (g b0) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> s (f (g b0)) @ !6, (!5 = 0) -> s (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ]) @ !6, (!5 = 1) -> s (f (comp A (g (comp B b0 [ (!4 = 1) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ])) [ (!4 = 1) -> t (g b0) @ !5 ])) @ !6 ] ], (!2 = 1) -> comp B (comp B b1 [ (!3 = 0)(!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ]) [ (!3 = 0) -> comp B (f (comp A (comp A (g (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> t (g b1) @ (!5 /\ !6) ]) [ (!4 = 1) -> t (g b1) @ (!5 /\ -!6), (!5 = 1) -> t (comp A (g (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> t (g b1) @ !5 ]) @ -!6 ])) [ (!4 = 1) -> s (f (g b1)) @ !6, (!5 = 0) -> s (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ]) @ !6, (!5 = 1) -> s (f (comp A (g (comp B b1 [ (!4 = 1) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ])) [ (!4 = 1) -> t (g b1) @ !5 ])) @ !6 ] ] ]) [ (!3 = 0) -> comp B (f (g (q @ !2))) [ (!2 = 0) -> f (comp A (g (comp B b0 [ (!5 = 1) -> comp B (f (comp A (g b0) [ (!6 = 1) -> t (g b0) @ -!7 ])) [ (!6 = 0) -> s b0 @ !7, (!6 = 1) -> s (f (g b0)) @ !7 ] ])) [ (!5 = 1) -> t (g b0) @ !6 ]), (!2 = 1) -> f (comp A (g (comp B b1 [ (!5 = 1) -> comp B (f (comp A (g b1) [ (!6 = 1) -> t (g b1) @ -!7 ])) [ (!6 = 0) -> s b1 @ !7, (!6 = 1) -> s (f (g b1)) @ !7 ] ])) [ (!5 = 1) -> t (g b1) @ !6 ]), (!4 = 0) -> comp B (f (g (q @ !2))) [ (!2 = 0) -> f (comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b0) [ (!7 = 1) -> t (g b0) @ -!8 ])) [ (!7 = 0) -> s b0 @ !8, (!7 = 1) -> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b0) @ !7 ]), (!2 = 1) -> f (comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b1) [ (!7 = 1) -> t (g b1) @ -!8 ])) [ (!7 = 0) -> s b1 @ !8, (!7 = 1) -> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b1) @ !7 ]) ], (!4 = 1) -> f (comp A (g (q @ !2)) [ (!2 = 0) -> comp A (g (comp B b0 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b0) [ (!7 = 1) -> t (g b0) @ -!8 ])) [ (!7 = 0) -> s b0 @ !8, (!7 = 1) -> s (f (g b0)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b0) @ !7 ], (!2 = 1) -> comp A (g (comp B b1 [ (!5 = 1)(!6 = 1) -> comp B (f (comp A (g b1) [ (!7 = 1) -> t (g b1) @ -!8 ])) [ (!7 = 0) -> s b1 @ !8, (!7 = 1) -> s (f (g b1)) @ !8 ] ])) [ (!5 = 1)(!6 = 1) -> t (g b1) @ !7 ] ]) ] ]) [ (!2 = 0) -> comp B b0 [ (!3 = 0)(!4 = 0) -> comp B (f (comp A (g b0) [ (!5 = 1) -> t (g b0) @ -!6 ])) [ (!5 = 0) -> s b0 @ !6, (!5 = 1) -> s (f (g b0)) @ !6 ] ], (!2 = 1) -> comp B b1 [ (!3 = 0)(!4 = 0) -> comp B (f (comp A (g b1) [ (!5 = 1) -> t (g b1) @ -!6 ])) [ (!5 = 0) -> s b1 @ !6, (!5 = 1) -> s (f (g b1)) @ !6 ] ] ] ] + -}