diff --git a/BadRefl.idr b/BadRefl.idr deleted file mode 100644 index 9ac12a3..0000000 --- a/BadRefl.idr +++ /dev/null @@ -1,18 +0,0 @@ -module BadRefl - -import IdrisPrelude - -plus = - natElim - ( \ _ -> Nat -> Nat ) -- motive - ( \ n -> n ) -- case for Zero - ( \ p rec n -> Succ (rec n) ) -- case for Succ - --- the other direction requires induction on N: -postulate pNPlus0isN : (n : Nat) -> Eq Nat (plus n Zero) n - - --- the other direction requires induction on N: -succPlus : (n : Nat) -> Eq Nat (Succ n) (plus (Succ n) Zero) -succPlus = - (\n -> pNPlus0isN (Succ n)) diff --git a/badSubNames.txt b/badSubNames.txt deleted file mode 100644 index a23d974..0000000 --- a/badSubNames.txt +++ /dev/null @@ -1,27 +0,0 @@ -Initial context: -α_25_20__ ? : * -α_25_13__1 ? : ?α_25_20__ -> * -??_25_13_2 ?? : (forall (arg :: *) . (arg -> arg -> arg -> Nat -> arg) : *) === (?α_25_20__ -> (?α_25_13__1) : *) <= ACTIVE -α_25_20__3 ? : * -β_25_20 ? : ?α_25_20__3 -??_25_20_4 ?? : (?α_25_20__3 : *) === (?α_25_20__ : *) <= ACTIVE -α_25_22__5 ? : * -α_25_13__6 ? : ?α_25_22__5 -> * -??_25_13_7 ?? : (?α_25_13__1 ?β_25_20 : *) === (?α_25_22__5 -> (?α_25_13__6) : *) <= ACTIVE -??_25_22_10 ?? : (Nat : *) === (?α_25_22__5 : *) <= ACTIVE -α_25_24__11 ? : * -α_25_13__12 ? : ?α_25_24__11 -> * -??_25_13_13 ?? : (?α_25_13__6 Succ Zero : *) === (?α_25_24__11 -> (?α_25_13__12) : *) <= ACTIVE -α_25_29__14 ? : * -α_25_25__15 ? : ?α_25_29__14 -> * -??_25_25_16 ?? : (forall (a :: *) . (Vec (a) Zero) : *) === (?α_25_29__14 -> (?α_25_25__15) : *) <= ACTIVE -??_25_29_17 ?? : (* : *) === (?α_25_29__14 : *) <= ACTIVE -??_25_24_18 ?? : (?α_25_25__15 * : *) === (?α_25_24__11 : *) <= ACTIVE -α_25_32__20 ? : * -α_25_13__21 ? : ?α_25_32__20 -> * -??_25_13_22 ?? : (?α_25_13__12 Nil * : *) === (?α_25_32__20 -> (?α_25_13__21) : *) <= ACTIVE -??_25_32_27 ?? : (Nat : *) === (?α_25_32__20 : *) <= ACTIVE -α_25_34__28 ? : * -α_25_13__29 ? : ?α_25_34__28 -> * -??_25_13_30 ?? : (?α_25_13__21 Succ ((Succ ((Succ Zero)))) : *) === (?α_25_34__28 -> (?α_25_13__29) : *) <= ACTIVE -??_25_34_32 ?? : (Nat : *) === (?α_25_34__28 : *) <= ACTIVE diff --git a/chinterJunk.txt b/chinterJunk.txt deleted file mode 100644 index 92fcaea..0000000 --- a/chinterJunk.txt +++ /dev/null @@ -1,5 +0,0 @@ -((chInter8947-x8909),ConstraintInfo {edgeType = ChoiceEdge RightChoice α_11_5__148 (L ( C CEq [C CNat [],N (Var 0@0 Only) [],N (Var 0@0 Only) []]),N (Meta x8909) []), edgeEqnInfo = EqnInfo {creationInfo = CreatedBy (ProbId {probIdToName = x8870}), infoRegion = SourceRegion {regionFile = "thesisExamples/PlusReverse.lp", regionLine = 11, regionColumn = 5}, isCF = Factual, programContext = AppRetType (SourceRegion {regionFile = "thesisExamples/PlusReverse.lp", regionLine = 11, regionColumn = 5}) (N (Meta α_11_5__148) [Elim CA [N (Var xx_8884 Only) []]]), typeOfString = "result of application Refl Nat [Free_ (Local 0)]", initialCreatorId = Just (ProbId {probIdToName = ??_11_5_155})}, edgeEqn = (N (Meta x8909) [],N (Meta chInter8947) []), typeOfValues = C Pi [VChoice (ChoiceId {choiceIdToName = x4535, choiceRegion = SourceRegion {regionFile = "thesisExamples/PlusReverse.lp", regionLine = 10, regionColumn = 4}}) (CUID {cuidNom = CUID4536}) α_10_4__140 (C CNat []) (N (Meta x4534) []),L ( C Set [])], maybeHint = Nothing}) - - - - ((chInter8947-α_11_5__148),ConstraintInfo {edgeType = ChoiceEdge LeftChoice α_11_5__148 (L ( C CEq [C CNat [],N (Var 0@0 Only) [],N (Var 0@0 Only) []]),N (Meta x8909) []), edgeEqnInfo = EqnInfo {creationInfo = CreatedBy (ProbId {probIdToName = x8870}), infoRegion = SourceRegion {regionFile = "thesisExamples/PlusReverse.lp", regionLine = 11, regionColumn = 5}, isCF = Factual, programContext = AppRetType (SourceRegion {regionFile = "thesisExamples/PlusReverse.lp", regionLine = 11, regionColumn = 5}) (N (Meta α_11_5__148) [Elim CA [N (Var xx_8884 Only) []]]), typeOfString = "result of application Refl Nat [Free_ (Local 0)]", initialCreatorId = Just (ProbId {probIdToName = ??_11_5_155})}, edgeEqn = (N (Meta α_11_5__148) [],N (Meta chInter8947) []), typeOfValues = C Pi [VChoice (ChoiceId {choiceIdToName = x4535, choiceRegion = SourceRegion {regionFile = "thesisExamples/PlusReverse.lp", regionLine = 10, regionColumn = 4}}) (CUID {cuidNom = CUID4536}) α_10_4__140 (C CNat []) (N (Meta x4534) []),L ( C Set [])], maybeHint = Nothing}) diff --git a/elimTypes.txt b/elimTypes.txt deleted file mode 100644 index 7a2712e..0000000 --- a/elimTypes.txt +++ /dev/null @@ -1,28 +0,0 @@ -natElim :: - forall (m :: Nat -> *) . - m Zero -> - (forall (l :: Nat) . (m l -> m (Succ l))) -> - forall (n :: Nat) . (m n) - - -vecElim :: - forall (a :: *) . - forall (m :: forall (n :: Nat) . (Vec a n -> *)) . - m Zero (Nil a) -> - (forall (k :: Nat) (x :: a) (xs :: Vec a k) . m k xs -> m (Succ k) (Cons a k x xs)) -> - forall (n :: Nat) . - forall (xs :: Vec a n) . (m n xs) - - -finElim :: - forall (m :: forall (n :: Nat) . (Fin n -> *)) . - (forall (n :: Nat) . (m (Succ n) (FZero n))) -> - (forall (n :: Nat) (f :: Fin n) . m n f -> m (Succ n) (FSucc n f)) -> - forall (n :: Nat) (f :: Fin n) . (m n f) - - -eqElim :: - forall (a :: *) . - forall (m :: forall (x :: a) (y :: a) . Eq a x y -> *) . - (forall (x :: a) . m x x (Refl a x)) -> - forall (x :: a) (y :: a) (eq :: Eq a x y) . (m x y eq) diff --git a/implicit.lp b/implicit.lp deleted file mode 100644 index 09b8675..0000000 --- a/implicit.lp +++ /dev/null @@ -1,385 +0,0 @@ - --- identity and const -let id = (\ a x -> x) :: forall (a :: *) . a -> a -let const = (\ a b x y -> x) :: forall (a :: *) (b :: *) . a -> b -> a - --- addition of natural numbers -let plus = - (\n -> - natElim - _ -- motive - ( \ n -> n ) -- case for Zero - ( \ p rec n -> Succ (rec n) ) - n ) -- case for Succ - :: Nat -> Nat -> Nat - --- predecessor, mapping 0 to 0 -let pred = - (natElim - _ - Zero - ( \ n' _rec -> n' )) :: Nat -> Nat - --- a simpler elimination scheme for natural numbers -let natFold = - ( \ m mz ms -> natElim - _ - mz - ( \ n' rec -> ms rec ) ) - :: forall (m :: *) . m -> (m -> m) -> Nat -> m - --- an eliminator for natural numbers that has special --- cases for 0 and 1 -let nat1Elim = - ( \ m m0 m1 ms -> natElim _ m0 - (\ p rec -> natElim _ m1 ms p) ) - :: forall (m :: Nat -> *) . m 0 -> m 1 -> - (forall n :: Nat . m (Succ n) -> m (Succ (Succ n))) -> - forall (n :: Nat) . m n - - --- an eliminator for natural numbers that has special --- cases for 0, 1 and 2 -let nat2Elim = - ( \ m m0 m1 m2 ms -> nat1Elim _ m0 m1 - (\ p rec -> natElim _ m2 ms p) ) - :: forall (m :: Nat -> *) . m 0 -> m 1 -> m 2 -> - (forall n :: Nat . m (Succ (Succ n)) -> m (Succ (Succ (Succ n)))) -> - forall (n :: Nat) . m n - - --- increment by one -let inc = natFold _ (Succ Zero) Succ - - - -let myFinElim = finElim - --- embed Fin into Nat -let finNat = finElim _ - (\ _ -> Zero) - (\ _ _ rec -> Succ rec) - --- unit type -let Unit = Fin 1 --- constructor -let U = FZero 0 - --- eliminator -let unitElim = - ( \ m mu -> finElim ( nat1Elim _ - (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) ) - ( natElim _ - mu - (\ _ _ -> U) ) - ( \ n f _ -> finElim (\ n f -> natElim (\ n -> Fin (Succ n) -> *) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc n f)) - (\ _ -> U) - (\ _ _ _ -> U) - n f ) - 1 ) - :: forall (m :: Unit -> *) . m U -> forall (u :: Unit) . m u - --- empty type -let Void = Fin 0 - --- eliminator -let voidElim = - ( \ m -> finElim (natElim _ - (\ x -> m x) - (\ _ _ _ -> Unit)) - (\ _ -> U) - (\ _ _ _ -> U) - 0 ) - :: forall (m :: Void -> *) (v :: Void) . m v - - --- type of booleans -let Bool = Fin 2 - --- constructors -let False = FZero 1 -let True = FSucc 1 (FZero 0) - --- eliminator -let boolElim = - ( \ m mf mt -> finElim ( nat2Elim (\ n -> Fin n -> *) - (\ _ -> Unit) (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) ) - ( nat1Elim ( \ n -> nat1Elim (\ n -> Fin (Succ n) -> *) - (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FZero n)) - U mf (\ _ _ -> U) ) - ( \ n f _ -> finElim ( \ n f -> nat1Elim (\ n -> Fin (Succ n) -> *) - (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc n f) ) - ( natElim - ( \ n -> natElim - (\ n -> Fin (Succ (Succ n)) -> *) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc (Succ n) (FZero n)) ) - mt (\ _ _ -> U) ) - ( \ n f _ -> finElim - (\ n f -> natElim - (\ n -> Fin (Succ (Succ n)) -> *) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc (Succ n) (FSucc n f))) - (\ _ -> U) - (\ _ _ _ -> U) - n f ) - n f ) - 2 ) - :: forall (m :: Bool -> *) . m False -> m True -> forall (b :: Bool) . m b - -{- --- boolean not, and, or, equivalence, xor -let not = boolElim (\ _ -> Bool) True False -let and = boolElim (\ _ -> Bool -> Bool) (\ _ -> False) (id Bool) -let or = boolElim (\ _ -> Bool -> Bool) (id Bool) (\ _ -> True) -let iff = boolElim (\ _ -> Bool -> Bool) not (id Bool) -let xor = boolElim (\ _ -> Bool -> Bool) (id Bool) not - --- even, odd, isZero, isSucc -let even = natFold Bool True not -let odd = natFold Bool False not -let isZero = natFold Bool True (\ _ -> False) -let isSucc = natFold Bool False (\ _ -> True) - - - --- equality on natural numbers -let natEq = - natElim - ( \ _ -> Nat -> Bool ) - ( natElim - ( \ _ -> Bool ) - True - ( \ n' _ -> False ) ) - ( \ m' rec_m' -> natElim - ( \ _ -> Bool ) - False - ( \ n' _ -> rec_m' n' )) - --- "oh so true" -let Prop = boolElim (\ _ -> *) Void Unit - --- reflexivity of equality on natural numbers -let pNatEqRefl = - natElim - (\ n -> Prop (natEq n n)) - U - (\ n' rec -> rec) - :: forall (n :: Nat) . Prop (natEq n n) - --- alias for type-level negation -let Not = (\ a -> a -> Void) :: * -> * - --- Leibniz prinicple (look at the type signature) -let leibniz = - ( \ a b f -> eqElim a - (\ x y eq_x_y -> Eq b (f x) (f y)) - (\ x -> Refl b (f x)) ) - :: forall (a :: *) (b :: *) (f :: a -> b) (x :: a) (y :: a) . - Eq a x y -> Eq b (f x) (f y) - --- symmetry of (general) equality -let symm = - ( \ a -> eqElim a - (\ x y eq_x_y -> Eq a y x) - (\ x -> Refl a x) ) - :: forall (a :: *) (x :: a) (y :: a) . - Eq a x y -> Eq a y x - --- transitivity of (general) equality -let tran = - ( \ a x y z eq_x_y -> eqElim a - (\ x y eq_x_y -> forall (z :: a) . Eq a y z -> Eq a x z) - (\ x z eq_x_z -> eq_x_z) - x y eq_x_y z ) - :: forall (a :: *) (x :: a) (y :: a) (z :: a) . - Eq a x y -> Eq a y z -> Eq a x z - --- apply an equality proof on two types -let apply = - eqElim * (\ a b _ -> a -> b) (\ _ x -> x) - :: forall (a :: *) (b :: *) (p :: Eq * a b) . a -> b - --- proof that 1 is not 0 -let p1IsNot0 = - (\ p -> apply Unit Void - (leibniz Nat * - (natElim (\ _ -> *) Void (\ _ _ -> Unit)) - 1 0 p) - U) - :: Not (Eq Nat 1 0) - --- proof that 0 is not 1 -let p0IsNot1 = - (\ p -> p1IsNot0 (symm Nat 0 1 p)) - :: Not (Eq Nat 0 1) - --- proof that zero is not a successor -let p0IsNoSucc = - natElim - ( \ n -> Not (Eq Nat 0 (Succ n)) ) - p0IsNot1 - ( \ n' rec_n' eq_0_SSn' -> - rec_n' (leibniz Nat Nat pred Zero (Succ (Succ n')) eq_0_SSn') ) - --- generate a vector of given length from a specified element (replicate) -let replicate = - ( natElim - ( \ n -> forall (a :: *) . a -> Vec a n ) - ( \ a _ -> Nil a ) - ( \ n' rec_n' a x -> Cons a n' x (rec_n' a x) ) ) - :: forall (n :: Nat) . forall (a :: *) . a -> Vec a n - --- alternative definition of replicate -let replicate' = - (\ a n x -> natElim (Vec a) - (Nil a) - (\ n' rec_n' -> Cons a n' x rec_n') n) - :: forall (a :: *) (n :: Nat) . a -> Vec a n - --- generate a vector of given length n, containing the natural numbers smaller than n -let fromto = - natElim - ( \ n -> Vec Nat n ) - ( Nil Nat ) - ( \ n' rec_n' -> Cons Nat n' n' rec_n' ) - --- append two vectors -let append = - ( \ a -> vecElim a - (\ m _ -> forall (n :: Nat) . Vec a n -> Vec a (plus m n)) - (\ _ v -> v) - (\ m v vs rec n w -> Cons a (plus m n) v (rec n w))) - :: forall (a :: *) (m :: Nat) (v :: Vec a m) (n :: Nat) (w :: Vec a n). - Vec a (plus m n) - --- helper function for tail, see below -let tail' = - (\ a -> vecElim a ( \ m v -> forall (n :: Nat) . Eq Nat m (Succ n) -> Vec a n ) - ( \ n eq_0_SuccN -> voidElim ( \ _ -> Vec a n ) - ( p0IsNoSucc n eq_0_SuccN ) ) - ( \ m' v vs rec_m' n eq_SuccM'_SuccN -> - eqElim Nat - (\ m' n e -> Vec a m' -> Vec a n) - (\ _ v -> v) - m' n - (leibniz Nat Nat pred (Succ m') (Succ n) eq_SuccM'_SuccN) vs)) - :: forall (a :: *) (m :: Nat) . Vec a m -> forall (n :: Nat) . Eq Nat m (Succ n) -> Vec a n - --- compute the tail of a vector -let tail = - (\ a n v -> tail' a (Succ n) v n (Refl Nat (Succ n))) - :: forall (a :: *) (n :: Nat) . Vec a (Succ n) -> Vec a n - --- projection out of a vector -let at = - (\ a -> vecElim a ( \ n v -> Fin n -> a ) - ( \ f -> voidElim (\ _ -> a) f ) - ( \ n' v vs rec_n' f_SuccN' -> - finElim ( \ n _ -> Eq Nat n (Succ n') -> a ) - ( \ n e -> v ) - ( \ n f_N _ eq_SuccN_SuccN' -> - rec_n' (eqElim Nat - (\ x y e -> Fin x -> Fin y) - (\ _ f -> f) - n n' - (leibniz Nat Nat pred - (Succ n) (Succ n') eq_SuccN_SuccN') - f_N)) - (Succ n') - f_SuccN' - (Refl Nat (Succ n')))) - :: forall (a :: *) (n :: Nat) . Vec a n -> Fin n -> a - --- head of a vector -let head = - (\ a n v -> at a (Succ n) v (FZero n)) - :: forall (a :: *) (n :: Nat) . Vec a (Succ n) -> a - --- vector map -let map = - (\ a b f -> vecElim a ( \ n _ -> Vec b n ) - ( Nil b ) - ( \ n x _ rec -> Cons b n (f x) rec )) - :: forall (a :: *) (b :: *) (f :: a -> b) (n :: Nat) . Vec a n -> Vec b n - --- proofs that 0 is the neutral element of addition --- one direction is trivial by definition of plus: -let p0PlusNisN = - Refl Nat - :: forall n :: Nat . Eq Nat (plus 0 n) n - --- the other direction requires induction on N: -let pNPlus0isN = - natElim ( \ n -> Eq Nat (plus n 0) n ) - ( Refl Nat 0 ) - ( \ n' rec -> leibniz Nat Nat Succ (plus n' 0) n' rec ) - :: forall n :: Nat . Eq Nat (plus n 0) n - - --------------------------------------------------- --- Product / Sigma types proofs and utilities --------------------------------------------------- - - -let Prod = - (\s t -> exists (x :: s) . t ) - :: * -> * -> * - ---fst and snd as functions -let getFst = - (\ _ _ x -> fst x) - :: forall (s :: *) (t :: s -> *) . (exists (x :: s) . (t x)) -> s - - -let zeroes = ( 0 , 0 ) :: Prod Nat Nat - -let v1 = (fst zeroes) :: Nat - -let v2 = (snd zeroes) :: Nat - -let geq = (\ x y -> exists (z :: Nat) . Eq Nat x (plus y z) ) :: Nat -> Nat -> * - -let gt = - (\ x y -> geq x (Succ y)) - :: Nat -> Nat -> * - -let leq = (\ x y -> geq y x) :: Nat -> Nat -> * - -let lt = (\ x y -> gt y x) :: Nat -> Nat -> * - - -let geq0 = - (\n -> (n , p0PlusNisN n) ) - :: forall (n :: Nat ) . geq n 0 - -let natsAreInf = - (\n -> (Succ n, (0, symm Nat (plus (Succ n) 0) (Succ n) (pNPlus0isN (Succ n))) ) ) - :: forall (n :: Nat) . exists (m :: Nat) . gt m n - ------- We can build binary sums out of Bools and Products -let sum = - (\ s t -> exists (b :: Bool) . boolElim (\_ -> *) s t b ) - :: * -> * -> * - -let sumElim = - (\ m s t fs ft pair -> - boolElim (\_ -> m) (fs (snd pair)) (ft (snd pair)) (fst pair) - ) - :: forall (m :: *) (s :: *) (t :: *) . (s -> m) -> (t -> m) -> sum s t -> m --} diff --git a/lambda-pi-plus.prof.html b/lambda-pi-plus.prof.html deleted file mode 100644 index 65089e0..0000000 --- a/lambda-pi-plus.prof.html +++ /dev/null @@ -1,957 +0,0 @@ - - - - - lambda-pi-plus - - - - - - - - - - - - - - - - - - -
-
-
-
- -
- - diff --git a/nat3_init.txt b/nat3_init.txt deleted file mode 100644 index c0cdb2f..0000000 --- a/nat3_init.txt +++ /dev/null @@ -1,50 +0,0 @@ -α_23_20__ ? : * -α_23_13__1 ? : ?α_23_20__ -> * -??_23_13_2 ?? : (forall (arg :: *) . (arg -> arg -> arg -> Nat -> arg) : *) === (?α_23_20__ -> (?α_23_13__1) : *) <= ACTIVE -α_23_20__3 ? : * -β_23_20 ? : ?α_23_20__3 -??_23_20_4 ?? : (?α_23_20__3 : *) === (?α_23_20__ : *) <= ACTIVE -α_23_22__5 ? : * -α_23_13__6 ? : ?α_23_22__5 -> * -??_23_13_7 ?? : (?α_23_13__1 ?β_23_20 : *) === (?α_23_22__5 -> (?α_23_13__6) : *) <= ACTIVE -α_23_27__8 ? : * -α_23_23__9 ? : ?α_23_27__8 -> * -??_23_23_10 ?? : (forall (a :: *) . (Vec (a) Zero) : *) === (?α_23_27__8 -> (?α_23_23__9) : *) <= ACTIVE -??_23_27_11 ?? : (* : *) === (?α_23_27__8 : *) <= ACTIVE -??_23_22_12 ?? : (?α_23_23__9 Nat : *) === (?α_23_22__5 : *) <= ACTIVE -α_23_32__14 ? : * -α_23_13__15 ? : ?α_23_32__14 -> * -??_23_13_16 ?? : (?α_23_13__6 Nil Nat : *) === (?α_23_32__14 -> (?α_23_13__15) : *) <= ACTIVE -??_23_32_20 ?? : (Nat : *) === (?α_23_32__14 : *) <= ACTIVE -α_23_34__21 ? : * -α_23_13__22 ? : ?α_23_34__21 -> * -??_23_13_23 ?? : (?α_23_13__15 Succ ((Succ Zero)) : *) === (?α_23_34__21 -> (?α_23_13__22) : *) <= ACTIVE -??_23_34_28 ?? : (Nat : *) === (?α_23_34__21 : *) <= ACTIVE -α_23_36__29 ? : * -α_23_13__30 ? : ?α_23_36__29 -> * -??_23_13_31 ?? : (?α_23_13__22 Succ ((Succ ((Succ Zero)))) : *) === (?α_23_36__29 -> (?α_23_13__30) : *) <= ACTIVE -??_23_36_33 ?? : (Nat : *) === (?α_23_36__29 : *) <= ACTIVE -topLevel34 ? : * -??_0_0_115 ?? : (?α_23_13__30 Zero : *) === (?topLevel34 : *) <= ACTIVE - - - - - - - - - -??_23_13_2 ?? : (forall (arg :: *) . (arg -> arg -> arg -> Nat -> arg) : *) === (?α_23_20__ -> (?α_23_13__1) : *) <= ACTIVE -??_23_20_4 ?? : (?α_23_20__3 : *) === (?α_23_20__ : *) <= ACTIVE -??_23_13_7 ?? : (?α_23_13__1 ?β_23_20 : *) === (?α_23_22__5 -> (?α_23_13__6) : *) <= ACTIVE -??_23_23_10 ?? : (forall (a :: *) . (Vec (a) Zero) : *) === (?α_23_27__8 -> (?α_23_23__9) : *) <= ACTIVE -??_23_27_11 ?? : (* : *) === (?α_23_27__8 : *) <= ACTIVE -??_23_22_12 ?? : (?α_23_23__9 Nat : *) === (?α_23_22__5 : *) <= ACTIVE -??_23_13_16 ?? : (?α_23_13__6 Nil Nat : *) === (?α_23_32__14 -> (?α_23_13__15) : *) <= ACTIVE -??_23_32_20 ?? : (Nat : *) === (?α_23_32__14 : *) <= ACTIVE -??_23_13_23 ?? : (?α_23_13__15 Succ ((Succ Zero)) : *) === (?α_23_34__21 -> (?α_23_13__22) : *) <= ACTIVE -??_23_34_28 ?? : (Nat : *) === (?α_23_34__21 : *) <= ACTIVE -??_23_13_31 ?? : (?α_23_13__22 Succ ((Succ ((Succ Zero)))) : *) === (?α_23_36__29 -> (?α_23_13__30) : *) <= ACTIVE -??_23_36_33 ?? : (Nat : *) === (?α_23_36__29 : *) <= ACTIVE -??_0_0_115 ?? : (?α_23_13__30 Zero : *) === (?topLevel34 : *) <= ACTIVE diff --git a/natIf3_b b/natIf3_b deleted file mode 100644 index 36c6eb4..0000000 --- a/natIf3_b +++ /dev/null @@ -1,37 +0,0 @@ -α_25_20__ ? : * -α_25_13__1 ? : ?α_25_20__ -> * -??_25_13_2 ?? : (forall (arg :: *) . (arg -> arg -> arg -> Nat -> arg) : *) === (?α_25_20__ -> (?α_25_13__1) : *) <= ACTIVE -α_25_20__3 ? : * -β_25_20 ? : ?α_25_20__3 -??_25_20_4 ?? : (?α_25_20__3 : *) === (?α_25_20__ : *) <= ACTIVE -α_25_22__5 ? : * -α_25_13__6 ? : ?α_25_22__5 -> * -??_25_13_7 ?? : (?α_25_13__1 ?β_25_20 : *) === (?α_25_22__5 -> (?α_25_13__6) : *) <= ACTIVE -??_25_22_8 ?? : (Vec Nat Zero : *) === (?α_25_22__5 : *) <= ACTIVE -α_25_29__9 ? : * -α_25_13__10 ? : ?α_25_29__9 -> * -??_25_13_11 ?? : (?α_25_13__6 Nil Nat : *) === (?α_25_29__9 -> (?α_25_13__10) : *) <= ACTIVE -??_25_29_15 ?? : (Nat : *) === (?α_25_29__9 : *) <= ACTIVE -α_25_31__16 ? : * -α_25_13__17 ? : ?α_25_31__16 -> * -??_25_13_18 ?? : (?α_25_13__10 Succ ((Succ Zero)) : *) === (?α_25_31__16 -> (?α_25_13__17) : *) <= ACTIVE -??_25_31_23 ?? : (Nat : *) === (?α_25_31__16 : *) <= ACTIVE -α_25_33__24 ? : * -α_25_13__25 ? : ?α_25_33__24 -> * -??_25_13_26 ?? : (?α_25_13__17 Succ ((Succ ((Succ Zero)))) : *) === (?α_25_33__24 -> (?α_25_13__25) : *) <= ACTIVE -??_25_33_28 ?? : (Nat : *) === (?α_25_33__24 : *) <= ACTIVE -topLevel29 ? : * -??_0_0_109 ?? : (?α_25_13__25 Zero : *) === (?topLevel29 : *) <= ACTIVE - - - -??_25_13_2 ?? : (forall (arg :: *) . (arg -> arg -> arg -> Nat -> arg) : *) === (?α_25_20__ -> (?α_25_13__1) : *) <= ACTIVE -??_25_20_4 ?? : (?α_25_20__3 : *) === (?α_25_20__ : *) <= ACTIVE -??_25_13_7 ?? : (?α_25_13__1 ?β_25_20 : *) === (?α_25_22__5 -> (?α_25_13__6) : *) <= ACTIVE -??_25_22_8 ?? : (Vec Nat Zero : *) === (?α_25_22__5 : *) <= ACTIVE -??_25_13_11 ?? : (?α_25_13__6 Nil Nat : *) === (?α_25_29__9 -> (?α_25_13__10) : *) <= ACTIVE -??_25_29_15 ?? : (Nat : *) === (?α_25_29__9 : *) <= ACTIVE -??_25_13_18 ?? : (?α_25_13__10 Succ ((Succ Zero)) : *) === (?α_25_31__16 -> (?α_25_13__17) : *) <= ACTIVE -??_25_31_23 ?? : (Nat : *) === (?α_25_31__16 : *) <= ACTIVE -??_25_13_26 ?? : (?α_25_13__17 Succ ((Succ ((Succ Zero)))) : *) === (?α_25_33__24 -> (?α_25_13__25) : *) <= ACTIVE -??_25_33_28 ?? : (Nat : *) === (?α_25_33__24 : *) <= ACTIVE diff --git a/out.dot.png b/out.dot.png deleted file mode 100644 index cdf8dbc..0000000 Binary files a/out.dot.png and /dev/null differ diff --git a/out.dot.ps b/out.dot.ps deleted file mode 100644 index 6f1b5ca..0000000 Binary files a/out.dot.ps and /dev/null differ diff --git a/out.dot.svg b/out.dot.svg deleted file mode 100644 index 63e1f9a..0000000 --- a/out.dot.svg +++ /dev/null @@ -1,12428 +0,0 @@ - - - - - - -G - - -theNode15 - -theNode15: Con Pi - - -theNode17 - -theNode17: BoundVar arg13 - - -theNode18 - -theNode18: App theNode18 arg13 -> arg13 -> arg13 -> Nat -> arg13 - - -theNode18->theNode15 - - -L - - -theNode18->theNode17 - - -R - - -theNode21 - -theNode21: Con Pi - - -theNode23 - -theNode23: BoundVar arg13 - - -theNode24 - -theNode24: App theNode24 arg13 -> arg13 -> Nat -> arg13 - - -theNode24->theNode21 - - -L - - -theNode24->theNode23 - - -R - - -theNode27 - -theNode27: Con Pi - - -theNode29 - -theNode29: BoundVar arg13 - - -theNode30 - -theNode30: App theNode30 arg13 -> Nat -> arg13 - - -theNode30->theNode27 - - -L - - -theNode30->theNode29 - - -R - - -theNode33 - -theNode33: Con Pi - - -theNode35 - -theNode35: Con CNat - - -theNode36 - -theNode36: App theNode36 Nat -> arg13 - - -theNode36->theNode33 - - -L - - -theNode36->theNode35 - - -R - - -theNode39 - -theNode39: BoundVar arg13 - - -theNode41 - -theNode41: BoundVar arg37 - - -theNode42 - -theNode42: Lam theNode42  arg . arg13 - - -theNode42->theNode39 - - -R - - -theNode42->theNode41 - - -L - - -theNode43 - -theNode43: App theNode43 Nat -> arg13 - - -theNode43->theNode36 - - -L - - -theNode43->theNode42 - - -R - - -theNode45 - -theNode45: BoundVar arg31 - - -theNode46 - -theNode46: Lam theNode46  arg . Nat -> arg13 - - -theNode46->theNode43 - - -R - - -theNode46->theNode45 - - -L - - -theNode47 - -theNode47: App theNode47 arg13 -> Nat -> arg13 - - -theNode47->theNode30 - - -L - - -theNode47->theNode46 - - -R - - -theNode49 - -theNode49: BoundVar arg25 - - -theNode50 - -theNode50: Lam theNode50  arg . arg13 -> Nat -> arg13 - - -theNode50->theNode47 - - -R - - -theNode50->theNode49 - - -L - - -theNode51 - -theNode51: App theNode51 arg13 -> arg13 -> Nat -> arg13 - - -theNode51->theNode24 - - -L - - -theNode51->theNode50 - - -R - - -theNode53 - -theNode53: BoundVar arg19 - - -theNode54 - -theNode54: Lam theNode54  arg . arg13 -> arg13 -> Nat -> arg13 - - -theNode54->theNode51 - - -R - - -theNode54->theNode53 - - -L - - -theNode55 - -theNode55: App theNode55 arg13 -> arg13 -> arg13 -> Nat -> arg13 - - -theNode55->theNode18 - - -L - - -theNode55->theNode54 - - -R - - -theNode57 - -theNode57: BoundVar arg13 - - -theNode59 - -theNode59: App theNode59 forall (arg :: *)  .  (arg -> arg -> arg -> Nat -> arg) - - -theNode65 - -theNode65: App theNode65 ?α_19_19__ -> (?α_19_12__1) - - -theNode59->theNode65 - - - -theNode12 - -theNode12: App theNode12 forall (arg :: *)  .  (arg -> arg -> arg -> Nat -> arg) - - -theNode59->theNode12 - - -L - - -theNode58 - -theNode58: Lam theNode58  arg . arg -> arg -> arg -> Nat -> arg - - -theNode59->theNode58 - - -R - - -theNode63 - -theNode63: App theNode63 ?α_19_19__ -> (?α_19_12__1) - - -theNode65->theNode63 - - -L - - -α_19_12__1 - -α_19_12__1: Meta α_19_12__1 - - -theNode65->α_19_12__1 - - -R - - -theNode9 - -theNode9: Con Pi - - -theNode12->theNode9 - - -L - - -theNode11 - -theNode11: Con Set - - -theNode12->theNode11 - - -R - - -theNode61 - -theNode61: Con Pi - - -theNode63->theNode61 - - -L - - -α_19_19__ - -α_19_19__: Meta α_19_19__ - - -theNode63->α_19_19__ - - -R - - -theNode88 - -theNode88: Con Set - - -α_19_19__->theNode88 - - - -theNode833 - -theNode833: Con Set - - -α_19_19__->theNode833 - - - -theNode101 - -theNode101: Con Pi - - -theNode103 - -theNode103: BoundVar arg99 - - -theNode104 - -theNode104: App theNode104 arg99 -> arg99 -> arg99 -> Nat -> arg99 - - -theNode104->theNode101 - - -L - - -theNode104->theNode103 - - -R - - -theNode107 - -theNode107: Con Pi - - -theNode109 - -theNode109: BoundVar arg99 - - -theNode110 - -theNode110: App theNode110 arg99 -> arg99 -> Nat -> arg99 - - -theNode110->theNode107 - - -L - - -theNode110->theNode109 - - -R - - -theNode113 - -theNode113: Con Pi - - -theNode115 - -theNode115: BoundVar arg99 - - -theNode116 - -theNode116: App theNode116 arg99 -> Nat -> arg99 - - -theNode116->theNode113 - - -L - - -theNode116->theNode115 - - -R - - -theNode119 - -theNode119: Con Pi - - -theNode121 - -theNode121: Con CNat - - -theNode122 - -theNode122: App theNode122 Nat -> arg99 - - -theNode122->theNode119 - - -L - - -theNode122->theNode121 - - -R - - -theNode125 - -theNode125: BoundVar arg99 - - -theNode127 - -theNode127: BoundVar arg123 - - -theNode128 - -theNode128: Lam theNode128  arg . arg99 - - -theNode128->theNode125 - - -R - - -theNode128->theNode127 - - -L - - -theNode129 - -theNode129: App theNode129 Nat -> arg99 - - -theNode129->theNode122 - - -L - - -theNode129->theNode128 - - -R - - -theNode131 - -theNode131: BoundVar arg117 - - -theNode132 - -theNode132: Lam theNode132  arg . Nat -> arg99 - - -theNode132->theNode129 - - -R - - -theNode132->theNode131 - - -L - - -theNode133 - -theNode133: App theNode133 arg99 -> Nat -> arg99 - - -theNode133->theNode116 - - -L - - -theNode133->theNode132 - - -R - - -theNode135 - -theNode135: BoundVar arg111 - - -theNode136 - -theNode136: Lam theNode136  arg . arg99 -> Nat -> arg99 - - -theNode136->theNode133 - - -R - - -theNode136->theNode135 - - -L - - -theNode137 - -theNode137: App theNode137 arg99 -> arg99 -> Nat -> arg99 - - -theNode137->theNode110 - - -L - - -theNode137->theNode136 - - -R - - -theNode139 - -theNode139: BoundVar arg105 - - -theNode140 - -theNode140: Lam theNode140  arg . arg99 -> arg99 -> Nat -> arg99 - - -theNode140->theNode137 - - -R - - -theNode140->theNode139 - - -L - - -theNode141 - -theNode141: App theNode141 arg99 -> arg99 -> arg99 -> Nat -> arg99 - - -theNode141->theNode104 - - -L - - -theNode141->theNode140 - - -R - - -theNode143 - -theNode143: BoundVar arg99 - - -theNode443 - -theNode443: Lam theNode443  arg . arg -> arg -> arg -> Nat -> arg - - -α_19_12__1->theNode443 - - - -theNode770 - -theNode770: Lam theNode770  arg . arg -> arg -> arg -> Nat -> arg - - -α_19_12__1->theNode770 - - - -theNode185 - -theNode185: Con Pi - - -theNode187 - -theNode187: BoundVar x179 - - -theNode188 - -theNode188: App theNode188 x179 -> x179 -> x179 -> Nat -> x179 - - -theNode188->theNode185 - - -L - - -theNode188->theNode187 - - -R - - -theNode191 - -theNode191: Con Pi - - -theNode193 - -theNode193: BoundVar x179 - - -theNode194 - -theNode194: App theNode194 x179 -> x179 -> Nat -> x179 - - -theNode194->theNode191 - - -L - - -theNode194->theNode193 - - -R - - -theNode197 - -theNode197: Con Pi - - -theNode199 - -theNode199: BoundVar x179 - - -theNode200 - -theNode200: App theNode200 x179 -> Nat -> x179 - - -theNode200->theNode197 - - -L - - -theNode200->theNode199 - - -R - - -theNode203 - -theNode203: Con Pi - - -theNode205 - -theNode205: Con CNat - - -theNode206 - -theNode206: App theNode206 Nat -> x179 - - -theNode206->theNode203 - - -L - - -theNode206->theNode205 - - -R - - -theNode209 - -theNode209: BoundVar x179 - - -theNode211 - -theNode211: BoundVar arg207 - - -theNode212 - -theNode212: Lam theNode212  arg . x179 - - -theNode212->theNode209 - - -R - - -theNode212->theNode211 - - -L - - -theNode213 - -theNode213: App theNode213 Nat -> x179 - - -theNode213->theNode206 - - -L - - -theNode213->theNode212 - - -R - - -theNode215 - -theNode215: BoundVar arg201 - - -theNode216 - -theNode216: Lam theNode216  arg . Nat -> x179 - - -theNode216->theNode213 - - -R - - -theNode216->theNode215 - - -L - - -theNode217 - -theNode217: App theNode217 x179 -> Nat -> x179 - - -theNode217->theNode200 - - -L - - -theNode217->theNode216 - - -R - - -theNode219 - -theNode219: BoundVar arg195 - - -theNode220 - -theNode220: Lam theNode220  arg . x179 -> Nat -> x179 - - -theNode220->theNode217 - - -R - - -theNode220->theNode219 - - -L - - -theNode221 - -theNode221: App theNode221 x179 -> x179 -> Nat -> x179 - - -theNode221->theNode194 - - -L - - -theNode221->theNode220 - - -R - - -theNode223 - -theNode223: BoundVar arg189 - - -theNode224 - -theNode224: Lam theNode224  arg . x179 -> x179 -> Nat -> x179 - - -theNode224->theNode221 - - -R - - -theNode224->theNode223 - - -L - - -theNode - -theNode: ConElim CA - - -theNode228 - -theNode228: BoundVar x179 - - -theNode229 - -theNode229: App theNode229 ?α_19_12__1 x179 - - -theNode229->theNode - - -L - - -theNode229->theNode228 - - -R - - -theNode225 - -theNode225: App theNode225 x179 -> x179 -> x179 -> Nat -> x179 - - -theNode225->theNode188 - - -L - - -theNode225->theNode224 - - -R - - -theNode230 - -theNode230: Elim theNode230 ?α_19_12__1 x179 - - -theNode225->theNode230 - - - -theNode230->α_19_12__1 - - -L - - -theNode230->theNode229 - - -R - - -theNode400 - -theNode400: Con Pi - - -theNode402 - -theNode402: BoundVar arg398 - - -theNode403 - -theNode403: App theNode403 arg398 -> arg398 -> arg398 -> Nat -> arg398 - - -theNode403->theNode400 - - -L - - -theNode403->theNode402 - - -R - - -theNode406 - -theNode406: Con Pi - - -theNode408 - -theNode408: BoundVar arg398 - - -theNode409 - -theNode409: App theNode409 arg398 -> arg398 -> Nat -> arg398 - - -theNode409->theNode406 - - -L - - -theNode409->theNode408 - - -R - - -theNode412 - -theNode412: Con Pi - - -theNode414 - -theNode414: BoundVar arg398 - - -theNode415 - -theNode415: App theNode415 arg398 -> Nat -> arg398 - - -theNode415->theNode412 - - -L - - -theNode415->theNode414 - - -R - - -theNode418 - -theNode418: Con Pi - - -theNode420 - -theNode420: Con CNat - - -theNode421 - -theNode421: App theNode421 Nat -> arg398 - - -theNode421->theNode418 - - -L - - -theNode421->theNode420 - - -R - - -theNode424 - -theNode424: BoundVar arg398 - - -theNode426 - -theNode426: BoundVar arg422 - - -theNode427 - -theNode427: Lam theNode427  arg . arg398 - - -theNode427->theNode424 - - -R - - -theNode427->theNode426 - - -L - - -theNode428 - -theNode428: App theNode428 Nat -> arg398 - - -theNode428->theNode421 - - -L - - -theNode428->theNode427 - - -R - - -theNode430 - -theNode430: BoundVar arg416 - - -theNode431 - -theNode431: Lam theNode431  arg . Nat -> arg398 - - -theNode431->theNode428 - - -R - - -theNode431->theNode430 - - -L - - -theNode432 - -theNode432: App theNode432 arg398 -> Nat -> arg398 - - -theNode432->theNode415 - - -L - - -theNode432->theNode431 - - -R - - -theNode434 - -theNode434: BoundVar arg410 - - -theNode435 - -theNode435: Lam theNode435  arg . arg398 -> Nat -> arg398 - - -theNode435->theNode432 - - -R - - -theNode435->theNode434 - - -L - - -theNode436 - -theNode436: App theNode436 arg398 -> arg398 -> Nat -> arg398 - - -theNode436->theNode409 - - -L - - -theNode436->theNode435 - - -R - - -theNode438 - -theNode438: BoundVar arg404 - - -theNode439 - -theNode439: Lam theNode439  arg . arg398 -> arg398 -> Nat -> arg398 - - -theNode439->theNode436 - - -R - - -theNode439->theNode438 - - -L - - -theNode440 - -theNode440: App theNode440 arg398 -> arg398 -> arg398 -> Nat -> arg398 - - -theNode440->theNode403 - - -L - - -theNode440->theNode439 - - -R - - -theNode442 - -theNode442: BoundVar arg398 - - -theNode727 - -theNode727: Con Pi - - -theNode729 - -theNode729: BoundVar arg725 - - -theNode730 - -theNode730: App theNode730 arg725 -> arg725 -> arg725 -> Nat -> arg725 - - -theNode730->theNode727 - - -L - - -theNode730->theNode729 - - -R - - -theNode733 - -theNode733: Con Pi - - -theNode735 - -theNode735: BoundVar arg725 - - -theNode736 - -theNode736: App theNode736 arg725 -> arg725 -> Nat -> arg725 - - -theNode736->theNode733 - - -L - - -theNode736->theNode735 - - -R - - -theNode739 - -theNode739: Con Pi - - -theNode741 - -theNode741: BoundVar arg725 - - -theNode742 - -theNode742: App theNode742 arg725 -> Nat -> arg725 - - -theNode742->theNode739 - - -L - - -theNode742->theNode741 - - -R - - -theNode745 - -theNode745: Con Pi - - -theNode747 - -theNode747: Con CNat - - -theNode748 - -theNode748: App theNode748 Nat -> arg725 - - -theNode748->theNode745 - - -L - - -theNode748->theNode747 - - -R - - -theNode751 - -theNode751: BoundVar arg725 - - -theNode753 - -theNode753: BoundVar arg749 - - -theNode754 - -theNode754: Lam theNode754  arg . arg725 - - -theNode754->theNode751 - - -R - - -theNode754->theNode753 - - -L - - -theNode755 - -theNode755: App theNode755 Nat -> arg725 - - -theNode755->theNode748 - - -L - - -theNode755->theNode754 - - -R - - -theNode757 - -theNode757: BoundVar arg743 - - -theNode758 - -theNode758: Lam theNode758  arg . Nat -> arg725 - - -theNode758->theNode755 - - -R - - -theNode758->theNode757 - - -L - - -theNode759 - -theNode759: App theNode759 arg725 -> Nat -> arg725 - - -theNode759->theNode742 - - -L - - -theNode759->theNode758 - - -R - - -theNode761 - -theNode761: BoundVar arg737 - - -theNode762 - -theNode762: Lam theNode762  arg . arg725 -> Nat -> arg725 - - -theNode762->theNode759 - - -R - - -theNode762->theNode761 - - -L - - -theNode763 - -theNode763: App theNode763 arg725 -> arg725 -> Nat -> arg725 - - -theNode763->theNode736 - - -L - - -theNode763->theNode762 - - -R - - -theNode765 - -theNode765: BoundVar arg731 - - -theNode766 - -theNode766: Lam theNode766  arg . arg725 -> arg725 -> Nat -> arg725 - - -theNode766->theNode763 - - -R - - -theNode766->theNode765 - - -L - - -theNode767 - -theNode767: App theNode767 arg725 -> arg725 -> arg725 -> Nat -> arg725 - - -theNode767->theNode730 - - -L - - -theNode767->theNode766 - - -R - - -theNode769 - -theNode769: BoundVar arg725 - - -theNode785 - -theNode785: Con Pi - - -theNode787 - -theNode787: BoundVar arg783 - - -theNode788 - -theNode788: App theNode788 arg783 -> arg783 -> arg783 -> Nat -> arg783 - - -theNode788->theNode785 - - -L - - -theNode788->theNode787 - - -R - - -theNode791 - -theNode791: Con Pi - - -theNode793 - -theNode793: BoundVar arg783 - - -theNode794 - -theNode794: App theNode794 arg783 -> arg783 -> Nat -> arg783 - - -theNode794->theNode791 - - -L - - -theNode794->theNode793 - - -R - - -theNode797 - -theNode797: Con Pi - - -theNode799 - -theNode799: BoundVar arg783 - - -theNode800 - -theNode800: App theNode800 arg783 -> Nat -> arg783 - - -theNode800->theNode797 - - -L - - -theNode800->theNode799 - - -R - - -theNode803 - -theNode803: Con Pi - - -theNode805 - -theNode805: Con CNat - - -theNode806 - -theNode806: App theNode806 Nat -> arg783 - - -theNode806->theNode803 - - -L - - -theNode806->theNode805 - - -R - - -theNode809 - -theNode809: BoundVar arg783 - - -theNode811 - -theNode811: BoundVar arg807 - - -theNode812 - -theNode812: Lam theNode812  arg . arg783 - - -theNode812->theNode809 - - -R - - -theNode812->theNode811 - - -L - - -theNode813 - -theNode813: App theNode813 Nat -> arg783 - - -theNode813->theNode806 - - -L - - -theNode813->theNode812 - - -R - - -theNode815 - -theNode815: BoundVar arg801 - - -theNode816 - -theNode816: Lam theNode816  arg . Nat -> arg783 - - -theNode816->theNode813 - - -R - - -theNode816->theNode815 - - -L - - -theNode817 - -theNode817: App theNode817 arg783 -> Nat -> arg783 - - -theNode817->theNode800 - - -L - - -theNode817->theNode816 - - -R - - -theNode819 - -theNode819: BoundVar arg795 - - -theNode820 - -theNode820: Lam theNode820  arg . arg783 -> Nat -> arg783 - - -theNode820->theNode817 - - -R - - -theNode820->theNode819 - - -L - - -theNode821 - -theNode821: App theNode821 arg783 -> arg783 -> Nat -> arg783 - - -theNode821->theNode794 - - -L - - -theNode821->theNode820 - - -R - - -theNode823 - -theNode823: BoundVar arg789 - - -theNode824 - -theNode824: Lam theNode824  arg . arg783 -> arg783 -> Nat -> arg783 - - -theNode824->theNode821 - - -R - - -theNode824->theNode823 - - -L - - -theNode825 - -theNode825: App theNode825 arg783 -> arg783 -> arg783 -> Nat -> arg783 - - -theNode825->theNode788 - - -L - - -theNode825->theNode824 - - -R - - -theNode827 - -theNode827: BoundVar arg783 - - -theNode777 - -theNode777: App theNode777 ?α_19_19__ -> (?α_19_12__1) - - -theNode777->α_19_12__1 - - -R - - -theNode829 - -theNode829: App theNode829 forall (arg :: *)  .  (arg -> arg -> arg -> Nat -> arg) - - -theNode777->theNode829 - - - -theNode775 - -theNode775: App theNode775 ?α_19_19__ -> (?α_19_12__1) - - -theNode777->theNode775 - - -L - - -theNode782 - -theNode782: App theNode782 forall (arg :: *)  .  (arg -> arg -> arg -> Nat -> arg) - - -theNode829->theNode782 - - -L - - -theNode828 - -theNode828: Lam theNode828  arg . arg -> arg -> arg -> Nat -> arg - - -theNode829->theNode828 - - -R - - -theNode775->α_19_19__ - - -R - - -theNode773 - -theNode773: Con Pi - - -theNode775->theNode773 - - -L - - -theNode779 - -theNode779: Con Pi - - -theNode782->theNode779 - - -L - - -theNode781 - -theNode781: Con Set - - -theNode782->theNode781 - - -R - - -theNode828->theNode825 - - -R - - -theNode828->theNode827 - - -L - - -theNode144 - -theNode144: Lam theNode144  arg . arg -> arg -> arg -> Nat -> arg - - -theNode144->theNode141 - - -R - - -theNode144->theNode143 - - -L - - -theNode144->α_19_12__1 - - - -theNode58->theNode55 - - -R - - -theNode58->theNode57 - - -L - - -theNode443->theNode440 - - -R - - -theNode443->theNode442 - - -L - - -theNode770->theNode767 - - -R - - -theNode770->theNode769 - - -L - - -theNode81 - -theNode81: Con Set - - -theNode81->α_19_19__ - - - -α_19_19__3 - -α_19_19__3: Meta α_19_19__3 - - -theNode837 - -theNode837: Con Set - - -α_19_19__3->theNode837 - - - -theNode843 - -theNode843: Con Set - - -α_19_19__3->theNode843 - - - -theNode849 - -theNode849: App theNode849 ?α_19_12__1 ?β_19_19 - - -theNode849->theNode - - -L - - -β_19_19 - -β_19_19: Meta β_19_19 - - -theNode849->β_19_19 - - -R - - -theNode852 - -theNode852: Con Pi - - -α_19_22__5 - -α_19_22__5: Meta α_19_22__5 - - -β_19_19->α_19_22__5 - - - -theNode1513 - -theNode1513: App theNode1513 Prod ?α_19_22__8 (?α_19_26__9) - - -β_19_19->theNode1513 - - - -theNode1569 - -theNode1569: App theNode1569 Prod ?α_19_22__8 (?α_19_26__9) - - -β_19_19->theNode1569 - - - -theNode1669 - -theNode1669: App theNode1669 Prod ?α_19_22__8 (?α_19_26__9) - - -β_19_19->theNode1669 - - - -theNode854 - -theNode854: App theNode854 ?β_19_19 -> ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode854->theNode852 - - -L - - -theNode854->β_19_19 - - -R - - -theNode857 - -theNode857: Con Pi - - -theNode859 - -theNode859: App theNode859 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode859->β_19_19 - - -R - - -theNode859->theNode857 - - -L - - -theNode862 - -theNode862: Con Pi - - -theNode864 - -theNode864: App theNode864 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode864->β_19_19 - - -R - - -theNode864->theNode862 - - -L - - -theNode867 - -theNode867: Con Pi - - -theNode869 - -theNode869: Con CNat - - -theNode870 - -theNode870: App theNode870 Nat -> ?β_19_19 - - -theNode870->theNode867 - - -L - - -theNode870->theNode869 - - -R - - -theNode874 - -theNode874: BoundVar arg871 - - -theNode875 - -theNode875: Lam theNode875  arg . ?β_19_19 - - -theNode875->β_19_19 - - -R - - -theNode875->theNode874 - - -L - - -theNode876 - -theNode876: App theNode876 Nat -> ?β_19_19 - - -theNode876->theNode870 - - -L - - -theNode876->theNode875 - - -R - - -theNode878 - -theNode878: BoundVar arg865 - - -theNode879 - -theNode879: Lam theNode879  arg . Nat -> ?β_19_19 - - -theNode879->theNode876 - - -R - - -theNode879->theNode878 - - -L - - -theNode880 - -theNode880: App theNode880 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode880->theNode864 - - -L - - -theNode880->theNode879 - - -R - - -theNode882 - -theNode882: BoundVar arg860 - - -theNode883 - -theNode883: Lam theNode883  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode883->theNode880 - - -R - - -theNode883->theNode882 - - -L - - -theNode884 - -theNode884: App theNode884 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode884->theNode859 - - -L - - -theNode884->theNode883 - - -R - - -theNode886 - -theNode886: BoundVar arg855 - - -theNode887 - -theNode887: Lam theNode887  arg . ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode887->theNode884 - - -R - - -theNode887->theNode886 - - -L - - -theNode850 - -theNode850: Elim theNode850 ?α_19_12__1 ?β_19_19 - - -theNode850->α_19_12__1 - - -L - - -theNode850->theNode849 - - -R - - -theNode888 - -theNode888: App theNode888 ?β_19_19 -> ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode850->theNode888 - - - -theNode888->theNode854 - - -L - - -theNode888->theNode887 - - -R - - -theNode900 - -theNode900: Con Pi - - -theNode902 - -theNode902: App theNode902 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode902->β_19_19 - - -R - - -theNode902->theNode900 - - -L - - -theNode905 - -theNode905: Con Pi - - -theNode907 - -theNode907: App theNode907 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode907->β_19_19 - - -R - - -theNode907->theNode905 - - -L - - -theNode910 - -theNode910: Con Pi - - -theNode912 - -theNode912: Con CNat - - -theNode913 - -theNode913: App theNode913 Nat -> ?β_19_19 - - -theNode913->theNode910 - - -L - - -theNode913->theNode912 - - -R - - -theNode917 - -theNode917: BoundVar arg914 - - -theNode918 - -theNode918: Lam theNode918  arg . ?β_19_19 - - -theNode918->β_19_19 - - -R - - -theNode918->theNode917 - - -L - - -theNode919 - -theNode919: App theNode919 Nat -> ?β_19_19 - - -theNode919->theNode913 - - -L - - -theNode919->theNode918 - - -R - - -theNode921 - -theNode921: BoundVar arg908 - - -theNode922 - -theNode922: Lam theNode922  arg . Nat -> ?β_19_19 - - -theNode922->theNode919 - - -R - - -theNode922->theNode921 - - -L - - -theNode923 - -theNode923: App theNode923 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode923->theNode907 - - -L - - -theNode923->theNode922 - - -R - - -theNode925 - -theNode925: BoundVar arg903 - - -theNode926 - -theNode926: Lam theNode926  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode926->theNode923 - - -R - - -theNode926->theNode925 - - -L - - -theNode927 - -theNode927: App theNode927 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode927->theNode902 - - -L - - -theNode927->theNode926 - - -R - - -theNode929 - -theNode929: BoundVar arg898 - - -theNode931 - -theNode931: App theNode931 ?β_19_19 -> ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode937 - -theNode937: App theNode937 ?α_19_22__5 -> (?α_19_12__6) - - -theNode931->theNode937 - - - -theNode897 - -theNode897: App theNode897 ?β_19_19 -> ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode931->theNode897 - - -L - - -theNode930 - -theNode930: Lam theNode930  arg . ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode931->theNode930 - - -R - - -theNode935 - -theNode935: App theNode935 ?α_19_22__5 -> (?α_19_12__6) - - -theNode937->theNode935 - - -L - - -α_19_12__6 - -α_19_12__6: Meta α_19_12__6 - - -theNode937->α_19_12__6 - - -R - - -theNode897->β_19_19 - - -R - - -theNode895 - -theNode895: Con Pi - - -theNode897->theNode895 - - -L - - -theNode933 - -theNode933: Con Pi - - -theNode935->theNode933 - - -L - - -theNode935->α_19_22__5 - - -R - - -α_19_22__5->β_19_19 - - - -α_19_22__5->β_19_19 - - - -theNode969 - -theNode969: Con Pi - - -theNode971 - -theNode971: App theNode971 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode971->β_19_19 - - -R - - -theNode971->theNode969 - - -L - - -theNode974 - -theNode974: Con Pi - - -theNode976 - -theNode976: App theNode976 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode976->β_19_19 - - -R - - -theNode976->theNode974 - - -L - - -theNode979 - -theNode979: Con Pi - - -theNode981 - -theNode981: Con CNat - - -theNode982 - -theNode982: App theNode982 Nat -> ?β_19_19 - - -theNode982->theNode979 - - -L - - -theNode982->theNode981 - - -R - - -theNode986 - -theNode986: BoundVar arg983 - - -theNode987 - -theNode987: Lam theNode987  arg . ?β_19_19 - - -theNode987->β_19_19 - - -R - - -theNode987->theNode986 - - -L - - -theNode988 - -theNode988: App theNode988 Nat -> ?β_19_19 - - -theNode988->theNode982 - - -L - - -theNode988->theNode987 - - -R - - -theNode990 - -theNode990: BoundVar arg977 - - -theNode991 - -theNode991: Lam theNode991  arg . Nat -> ?β_19_19 - - -theNode991->theNode988 - - -R - - -theNode991->theNode990 - - -L - - -theNode992 - -theNode992: App theNode992 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode992->theNode976 - - -L - - -theNode992->theNode991 - - -R - - -theNode994 - -theNode994: BoundVar arg972 - - -theNode995 - -theNode995: Lam theNode995  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode995->theNode992 - - -R - - -theNode995->theNode994 - - -L - - -theNode996 - -theNode996: App theNode996 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode996->theNode971 - - -L - - -theNode996->theNode995 - - -R - - -theNode998 - -theNode998: BoundVar arg967 - - -theNode1226 - -theNode1226: Lam theNode1226  arg . ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -α_19_12__6->theNode1226 - - - -theNode1455 - -theNode1455: Lam theNode1455  arg . ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -α_19_12__6->theNode1455 - - - -theNode1037 - -theNode1037: Con Pi - - -theNode1039 - -theNode1039: App theNode1039 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1039->β_19_19 - - -R - - -theNode1039->theNode1037 - - -L - - -theNode1042 - -theNode1042: Con Pi - - -theNode1044 - -theNode1044: App theNode1044 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1044->β_19_19 - - -R - - -theNode1044->theNode1042 - - -L - - -theNode1047 - -theNode1047: Con Pi - - -theNode1049 - -theNode1049: Con CNat - - -theNode1050 - -theNode1050: App theNode1050 Nat -> ?β_19_19 - - -theNode1050->theNode1047 - - -L - - -theNode1050->theNode1049 - - -R - - -theNode1054 - -theNode1054: BoundVar arg1051 - - -theNode1055 - -theNode1055: Lam theNode1055  arg . ?β_19_19 - - -theNode1055->β_19_19 - - -R - - -theNode1055->theNode1054 - - -L - - -theNode1056 - -theNode1056: App theNode1056 Nat -> ?β_19_19 - - -theNode1056->theNode1050 - - -L - - -theNode1056->theNode1055 - - -R - - -theNode1058 - -theNode1058: BoundVar arg1045 - - -theNode1059 - -theNode1059: Lam theNode1059  arg . Nat -> ?β_19_19 - - -theNode1059->theNode1056 - - -R - - -theNode1059->theNode1058 - - -L - - -theNode1060 - -theNode1060: App theNode1060 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1060->theNode1044 - - -L - - -theNode1060->theNode1059 - - -R - - -theNode1062 - -theNode1062: BoundVar arg1040 - - -theNode1063 - -theNode1063: Lam theNode1063  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1063->theNode1060 - - -R - - -theNode1063->theNode1062 - - -L - - -theNode1067 - -theNode1067: BoundVar x1032 - - -theNode1068 - -theNode1068: App theNode1068 ?α_19_12__6 x1032 - - -theNode1068->theNode - - -L - - -theNode1068->theNode1067 - - -R - - -theNode1064 - -theNode1064: App theNode1064 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1064->theNode1039 - - -L - - -theNode1064->theNode1063 - - -R - - -theNode1069 - -theNode1069: Elim theNode1069 ?α_19_12__6 x1032 - - -theNode1064->theNode1069 - - - -theNode1069->α_19_12__6 - - -L - - -theNode1069->theNode1068 - - -R - - -theNode1196 - -theNode1196: Con Pi - - -theNode1198 - -theNode1198: App theNode1198 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1198->β_19_19 - - -R - - -theNode1198->theNode1196 - - -L - - -theNode1201 - -theNode1201: Con Pi - - -theNode1203 - -theNode1203: App theNode1203 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1203->β_19_19 - - -R - - -theNode1203->theNode1201 - - -L - - -theNode1206 - -theNode1206: Con Pi - - -theNode1208 - -theNode1208: Con CNat - - -theNode1209 - -theNode1209: App theNode1209 Nat -> ?β_19_19 - - -theNode1209->theNode1206 - - -L - - -theNode1209->theNode1208 - - -R - - -theNode1213 - -theNode1213: BoundVar arg1210 - - -theNode1214 - -theNode1214: Lam theNode1214  arg . ?β_19_19 - - -theNode1214->β_19_19 - - -R - - -theNode1214->theNode1213 - - -L - - -theNode1215 - -theNode1215: App theNode1215 Nat -> ?β_19_19 - - -theNode1215->theNode1209 - - -L - - -theNode1215->theNode1214 - - -R - - -theNode1217 - -theNode1217: BoundVar arg1204 - - -theNode1218 - -theNode1218: Lam theNode1218  arg . Nat -> ?β_19_19 - - -theNode1218->theNode1215 - - -R - - -theNode1218->theNode1217 - - -L - - -theNode1219 - -theNode1219: App theNode1219 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1219->theNode1203 - - -L - - -theNode1219->theNode1218 - - -R - - -theNode1221 - -theNode1221: BoundVar arg1199 - - -theNode1222 - -theNode1222: Lam theNode1222  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1222->theNode1219 - - -R - - -theNode1222->theNode1221 - - -L - - -theNode1223 - -theNode1223: App theNode1223 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1223->theNode1198 - - -L - - -theNode1223->theNode1222 - - -R - - -theNode1225 - -theNode1225: BoundVar arg1194 - - -theNode1425 - -theNode1425: Con Pi - - -theNode1427 - -theNode1427: App theNode1427 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1427->β_19_19 - - -R - - -theNode1427->theNode1425 - - -L - - -theNode1430 - -theNode1430: Con Pi - - -theNode1432 - -theNode1432: App theNode1432 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1432->β_19_19 - - -R - - -theNode1432->theNode1430 - - -L - - -theNode1435 - -theNode1435: Con Pi - - -theNode1437 - -theNode1437: Con CNat - - -theNode1438 - -theNode1438: App theNode1438 Nat -> ?β_19_19 - - -theNode1438->theNode1435 - - -L - - -theNode1438->theNode1437 - - -R - - -theNode1442 - -theNode1442: BoundVar arg1439 - - -theNode1443 - -theNode1443: Lam theNode1443  arg . ?β_19_19 - - -theNode1443->β_19_19 - - -R - - -theNode1443->theNode1442 - - -L - - -theNode1444 - -theNode1444: App theNode1444 Nat -> ?β_19_19 - - -theNode1444->theNode1438 - - -L - - -theNode1444->theNode1443 - - -R - - -theNode1446 - -theNode1446: BoundVar arg1433 - - -theNode1447 - -theNode1447: Lam theNode1447  arg . Nat -> ?β_19_19 - - -theNode1447->theNode1444 - - -R - - -theNode1447->theNode1446 - - -L - - -theNode1448 - -theNode1448: App theNode1448 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1448->theNode1432 - - -L - - -theNode1448->theNode1447 - - -R - - -theNode1450 - -theNode1450: BoundVar arg1428 - - -theNode1451 - -theNode1451: Lam theNode1451  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1451->theNode1448 - - -R - - -theNode1451->theNode1450 - - -L - - -theNode1452 - -theNode1452: App theNode1452 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1452->theNode1427 - - -L - - -theNode1452->theNode1451 - - -R - - -theNode1454 - -theNode1454: BoundVar arg1423 - - -theNode1469 - -theNode1469: Con Pi - - -theNode1471 - -theNode1471: App theNode1471 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1471->β_19_19 - - -R - - -theNode1471->theNode1469 - - -L - - -theNode1474 - -theNode1474: Con Pi - - -theNode1476 - -theNode1476: App theNode1476 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1476->β_19_19 - - -R - - -theNode1476->theNode1474 - - -L - - -theNode1479 - -theNode1479: Con Pi - - -theNode1481 - -theNode1481: Con CNat - - -theNode1482 - -theNode1482: App theNode1482 Nat -> ?β_19_19 - - -theNode1482->theNode1479 - - -L - - -theNode1482->theNode1481 - - -R - - -theNode1486 - -theNode1486: BoundVar arg1483 - - -theNode1487 - -theNode1487: Lam theNode1487  arg . ?β_19_19 - - -theNode1487->β_19_19 - - -R - - -theNode1487->theNode1486 - - -L - - -theNode1488 - -theNode1488: App theNode1488 Nat -> ?β_19_19 - - -theNode1488->theNode1482 - - -L - - -theNode1488->theNode1487 - - -R - - -theNode1490 - -theNode1490: BoundVar arg1477 - - -theNode1491 - -theNode1491: Lam theNode1491  arg . Nat -> ?β_19_19 - - -theNode1491->theNode1488 - - -R - - -theNode1491->theNode1490 - - -L - - -theNode1492 - -theNode1492: App theNode1492 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1492->theNode1476 - - -L - - -theNode1492->theNode1491 - - -R - - -theNode1494 - -theNode1494: BoundVar arg1472 - - -theNode1495 - -theNode1495: Lam theNode1495  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1495->theNode1492 - - -R - - -theNode1495->theNode1494 - - -L - - -theNode1496 - -theNode1496: App theNode1496 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1496->theNode1471 - - -L - - -theNode1496->theNode1495 - - -R - - -theNode1498 - -theNode1498: BoundVar arg1467 - - -theNode1462 - -theNode1462: App theNode1462 ?α_19_22__5 -> (?α_19_12__6) - - -theNode1462->α_19_12__6 - - -R - - -theNode1500 - -theNode1500: App theNode1500 ?β_19_19 -> ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1462->theNode1500 - - - -theNode1460 - -theNode1460: App theNode1460 ?α_19_22__5 -> (?α_19_12__6) - - -theNode1462->theNode1460 - - -L - - -theNode1466 - -theNode1466: App theNode1466 ?β_19_19 -> ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1500->theNode1466 - - -L - - -theNode1499 - -theNode1499: Lam theNode1499  arg . ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode1500->theNode1499 - - -R - - -theNode1460->α_19_22__5 - - -R - - -theNode1458 - -theNode1458: Con Pi - - -theNode1460->theNode1458 - - -L - - -theNode1466->β_19_19 - - -R - - -theNode1464 - -theNode1464: Con Pi - - -theNode1466->theNode1464 - - -L - - -theNode1499->theNode1496 - - -R - - -theNode1499->theNode1498 - - -L - - -theNode999 - -theNode999: Lam theNode999  arg . ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode999->theNode996 - - -R - - -theNode999->theNode998 - - -L - - -theNode999->α_19_12__6 - - - -theNode930->theNode927 - - -R - - -theNode930->theNode929 - - -L - - -theNode1226->theNode1223 - - -R - - -theNode1226->theNode1225 - - -L - - -theNode1455->theNode1452 - - -R - - -theNode1455->theNode1454 - - -L - - -α_19_26__9 - -α_19_26__9: Meta α_19_26__9 - - -α_19_22__8 - -α_19_22__8: Meta α_19_22__8 - - -theNode2385 - -theNode2385: Con CNat - - -α_19_22__8->theNode2385 - - - -theNode1513->α_19_26__9 - - -R - - -theNode1511 - -theNode1511: App theNode1511 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode1513->theNode1511 - - -L - - -theNode1569->α_19_26__9 - - -R - - -theNode1567 - -theNode1567: App theNode1567 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode1569->theNode1567 - - -L - - -theNode1669->α_19_26__9 - - -R - - -theNode1667 - -theNode1667: App theNode1667 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode1669->theNode1667 - - -L - - -theNode1511->α_19_22__8 - - -R - - -theNode1509 - -theNode1509: Con Sig - - -theNode1511->theNode1509 - - -L - - -theNode1567->α_19_22__8 - - -R - - -theNode1565 - -theNode1565: Con Sig - - -theNode1567->theNode1565 - - -L - - -theNode1667->α_19_22__8 - - -R - - -theNode1665 - -theNode1665: Con Sig - - -theNode1667->theNode1665 - - -L - - -x1735 - -x1735: Meta x1735 - - -theNode2275 - -theNode2275: BoundVar arg2272 - - -theNode2276 - -theNode2276: Elim theNode2276 (fst) arg2272 - - -theNode2276->theNode - - -R - - -theNode2276->theNode2275 - - -L - - -theNode2277 - -theNode2277: App theNode2277 ?x1735 (fst) arg2272 (snd) arg2272 - - -theNode2277->theNode - - -L - - -theNode2277->theNode2276 - - -R - - -theNode2278 - -theNode2278: Elim theNode2278 ?x1735 (fst) arg2272 (snd) arg2272 - - -theNode2278->x1735 - - -L - - -theNode2278->theNode2277 - - -R - - -theNode2280 - -theNode2280: BoundVar arg2272 - - -theNode2281 - -theNode2281: Elim theNode2281 (snd) arg2272 - - -theNode2281->theNode - - -R - - -theNode2281->theNode2280 - - -L - - -theNode2282 - -theNode2282: App theNode2282 ?x1735 (fst) arg2272 (snd) arg2272 - - -theNode2282->theNode - - -L - - -theNode2282->theNode2281 - - -R - - -theNode2283 - -theNode2283: Elim theNode2283 ?x1735 (fst) arg2272 (snd) arg2272 - - -theNode2283->theNode2278 - - -L - - -theNode2283->theNode2282 - - -R - - -theNode2285 - -theNode2285: BoundVar arg2272 - - -x1143 - -x1143: Meta x1143 - - -theNode2286 - -theNode2286: Lam theNode2286  arg . ?x1735 (fst) arg (snd) arg - - -x1143->theNode2286 - - - -theNode2286->theNode2283 - - -R - - -theNode2286->theNode2285 - - -L - - -theNode2295 - -theNode2295: Con Pi - - -theNode2297 - -theNode2297: App theNode2297 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode2297->β_19_19 - - -R - - -theNode2297->theNode2295 - - -L - - -theNode2300 - -theNode2300: Con Pi - - -theNode2302 - -theNode2302: App theNode2302 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode2302->β_19_19 - - -R - - -theNode2302->theNode2300 - - -L - - -theNode2305 - -theNode2305: Con Pi - - -theNode2307 - -theNode2307: Con CNat - - -theNode2308 - -theNode2308: App theNode2308 Nat -> ?β_19_19 - - -theNode2308->theNode2305 - - -L - - -theNode2308->theNode2307 - - -R - - -theNode2312 - -theNode2312: BoundVar arg2309 - - -theNode2313 - -theNode2313: Lam theNode2313  arg . ?β_19_19 - - -theNode2313->β_19_19 - - -R - - -theNode2313->theNode2312 - - -L - - -theNode2314 - -theNode2314: App theNode2314 Nat -> ?β_19_19 - - -theNode2314->theNode2308 - - -L - - -theNode2314->theNode2313 - - -R - - -theNode2316 - -theNode2316: BoundVar arg2303 - - -theNode2317 - -theNode2317: Lam theNode2317  arg . Nat -> ?β_19_19 - - -theNode2317->theNode2314 - - -R - - -theNode2317->theNode2316 - - -L - - -theNode2318 - -theNode2318: App theNode2318 ?β_19_19 -> Nat -> ?β_19_19 - - -theNode2318->theNode2302 - - -L - - -theNode2318->theNode2317 - - -R - - -theNode2320 - -theNode2320: BoundVar arg2298 - - -theNode2321 - -theNode2321: Lam theNode2321  arg . ?β_19_19 -> Nat -> ?β_19_19 - - -theNode2321->theNode2318 - - -R - - -theNode2321->theNode2320 - - -L - - -theNode2322 - -theNode2322: App theNode2322 ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode2322->theNode2297 - - -L - - -theNode2322->theNode2321 - - -R - - -theNode2324 - -theNode2324: BoundVar arg2293 - - -theNode2328 - -theNode2328: Con Pi - - -theNode2330 - -theNode2330: Con Sig - - -theNode2332 - -theNode2332: App theNode2332 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2332->α_19_22__8 - - -R - - -theNode2332->theNode2330 - - -L - - -theNode2334 - -theNode2334: App theNode2334 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2334->α_19_26__9 - - -R - - -theNode2334->theNode2332 - - -L - - -theNode2335 - -theNode2335: App theNode2335 (Prod ?α_19_22__8 (?α_19_26__9)) -> (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2335->theNode2328 - - -L - - -theNode2335->theNode2334 - - -R - - -theNode2338 - -theNode2338: Con Pi - - -theNode2340 - -theNode2340: Con Sig - - -theNode2342 - -theNode2342: App theNode2342 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2342->α_19_22__8 - - -R - - -theNode2342->theNode2340 - - -L - - -theNode2344 - -theNode2344: App theNode2344 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2344->α_19_26__9 - - -R - - -theNode2344->theNode2342 - - -L - - -theNode2345 - -theNode2345: App theNode2345 (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2345->theNode2338 - - -L - - -theNode2345->theNode2344 - - -R - - -theNode2348 - -theNode2348: Con Pi - - -theNode2350 - -theNode2350: Con CNat - - -theNode2351 - -theNode2351: App theNode2351 Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2351->theNode2348 - - -L - - -theNode2351->theNode2350 - - -R - - -theNode2354 - -theNode2354: Con Sig - - -theNode2356 - -theNode2356: App theNode2356 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2356->α_19_22__8 - - -R - - -theNode2356->theNode2354 - - -L - - -theNode2358 - -theNode2358: App theNode2358 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2358->α_19_26__9 - - -R - - -theNode2358->theNode2356 - - -L - - -theNode2360 - -theNode2360: BoundVar arg2352 - - -theNode2361 - -theNode2361: Lam theNode2361  arg . Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2361->theNode2358 - - -R - - -theNode2361->theNode2360 - - -L - - -theNode2362 - -theNode2362: App theNode2362 Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2362->theNode2351 - - -L - - -theNode2362->theNode2361 - - -R - - -theNode2364 - -theNode2364: BoundVar arg2346 - - -theNode2365 - -theNode2365: Lam theNode2365  arg . Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2365->theNode2362 - - -R - - -theNode2365->theNode2364 - - -L - - -theNode2366 - -theNode2366: App theNode2366 (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2366->theNode2345 - - -L - - -theNode2366->theNode2365 - - -R - - -theNode2368 - -theNode2368: BoundVar arg2336 - - -theNode2369 - -theNode2369: Lam theNode2369  arg . (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2369->theNode2366 - - -R - - -theNode2369->theNode2368 - - -L - - -theNode2370 - -theNode2370: App theNode2370 (Prod ?α_19_22__8 (?α_19_26__9)) -> (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2370->theNode2335 - - -L - - -theNode2370->theNode2369 - - -R - - -theNode2372 - -theNode2372: BoundVar arg2326 - - -theNode2325 - -theNode2325: Lam theNode2325  arg . ?β_19_19 -> ?β_19_19 -> Nat -> ?β_19_19 - - -theNode2325->theNode2322 - - -R - - -theNode2325->theNode2324 - - -L - - -theNode2373 - -theNode2373: Lam theNode2373  arg . (Prod ?α_19_22__8 (?α_19_26__9)) -> (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2325->theNode2373 - - - -theNode2373->theNode2370 - - -R - - -theNode2373->theNode2372 - - -L - - -theNode2394 - -theNode2394: App theNode2394 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2394->α_19_26__9 - - -R - - -theNode2401 - -theNode2401: App theNode2401 Prod Nat (?α_19_26__9) - - -theNode2394->theNode2401 - - - -theNode2392 - -theNode2392: App theNode2392 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2394->theNode2392 - - -L - - -theNode2401->α_19_26__9 - - -R - - -theNode2399 - -theNode2399: App theNode2399 Prod Nat (?α_19_26__9) - - -theNode2401->theNode2399 - - -L - - -theNode2392->α_19_22__8 - - -R - - -theNode2390 - -theNode2390: Con Sig - - -theNode2392->theNode2390 - - -L - - -theNode2396 - -theNode2396: Con Sig - - -theNode2399->theNode2396 - - -L - - -theNode2398 - -theNode2398: Con CNat - - -theNode2399->theNode2398 - - -R - - -theNode2408 - -theNode2408: App theNode2408 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2408->α_19_26__9 - - -R - - -theNode2415 - -theNode2415: App theNode2415 Prod Nat (?α_19_26__9) - - -theNode2408->theNode2415 - - - -theNode2406 - -theNode2406: App theNode2406 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2408->theNode2406 - - -L - - -theNode2415->α_19_26__9 - - -R - - -theNode2413 - -theNode2413: App theNode2413 Prod Nat (?α_19_26__9) - - -theNode2415->theNode2413 - - -L - - -theNode2406->α_19_22__8 - - -R - - -theNode2404 - -theNode2404: Con Sig - - -theNode2406->theNode2404 - - -L - - -theNode2410 - -theNode2410: Con Sig - - -theNode2413->theNode2410 - - -L - - -theNode2412 - -theNode2412: Con CNat - - -theNode2413->theNode2412 - - -R - - -theNode2378 - -theNode2378: Con CNat - - -theNode2378->α_19_22__8 - - - -theNode2424 - -theNode2424: Con Pi - - -theNode2426 - -theNode2426: Con Sig - - -theNode2428 - -theNode2428: App theNode2428 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2428->α_19_22__8 - - -R - - -theNode2428->theNode2426 - - -L - - -theNode2430 - -theNode2430: App theNode2430 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2430->α_19_26__9 - - -R - - -theNode2430->theNode2428 - - -L - - -theNode2431 - -theNode2431: App theNode2431 (Prod ?α_19_22__8 (?α_19_26__9)) -> (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2431->theNode2424 - - -L - - -theNode2431->theNode2430 - - -R - - -theNode2434 - -theNode2434: Con Pi - - -theNode2436 - -theNode2436: Con Sig - - -theNode2438 - -theNode2438: App theNode2438 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2438->α_19_22__8 - - -R - - -theNode2438->theNode2436 - - -L - - -theNode2440 - -theNode2440: App theNode2440 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2440->α_19_26__9 - - -R - - -theNode2440->theNode2438 - - -L - - -theNode2441 - -theNode2441: App theNode2441 (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2441->theNode2434 - - -L - - -theNode2441->theNode2440 - - -R - - -theNode2444 - -theNode2444: Con Pi - - -theNode2446 - -theNode2446: Con CNat - - -theNode2447 - -theNode2447: App theNode2447 Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2447->theNode2444 - - -L - - -theNode2447->theNode2446 - - -R - - -theNode2450 - -theNode2450: Con Sig - - -theNode2452 - -theNode2452: App theNode2452 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2452->α_19_22__8 - - -R - - -theNode2452->theNode2450 - - -L - - -theNode2454 - -theNode2454: App theNode2454 Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2454->α_19_26__9 - - -R - - -theNode2454->theNode2452 - - -L - - -theNode2456 - -theNode2456: BoundVar arg2448 - - -theNode2457 - -theNode2457: Lam theNode2457  arg . Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2457->theNode2454 - - -R - - -theNode2457->theNode2456 - - -L - - -theNode2458 - -theNode2458: App theNode2458 Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2458->theNode2447 - - -L - - -theNode2458->theNode2457 - - -R - - -theNode2460 - -theNode2460: BoundVar arg2442 - - -theNode2461 - -theNode2461: Lam theNode2461  arg . Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2461->theNode2458 - - -R - - -theNode2461->theNode2460 - - -L - - -theNode2462 - -theNode2462: App theNode2462 (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2462->theNode2441 - - -L - - -theNode2462->theNode2461 - - -R - - -theNode2464 - -theNode2464: BoundVar arg2432 - - -theNode2465 - -theNode2465: Lam theNode2465  arg . (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2465->theNode2462 - - -R - - -theNode2465->theNode2464 - - -L - - -theNode2466 - -theNode2466: App theNode2466 (Prod ?α_19_22__8 (?α_19_26__9)) -> (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2466->theNode2431 - - -L - - -theNode2466->theNode2465 - - -R - - -theNode2468 - -theNode2468: BoundVar arg2422 - - -theNode2472 - -theNode2472: Con Pi - - -theNode2474 - -theNode2474: Con Sig - - -theNode2476 - -theNode2476: Con CNat - - -theNode2477 - -theNode2477: App theNode2477 Prod Nat (?α_19_26__9) - - -theNode2477->theNode2474 - - -L - - -theNode2477->theNode2476 - - -R - - -theNode2479 - -theNode2479: App theNode2479 Prod Nat (?α_19_26__9) - - -theNode2479->α_19_26__9 - - -R - - -theNode2479->theNode2477 - - -L - - -theNode2480 - -theNode2480: App theNode2480 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2480->theNode2472 - - -L - - -theNode2480->theNode2479 - - -R - - -theNode2483 - -theNode2483: Con Pi - - -theNode2485 - -theNode2485: Con Sig - - -theNode2487 - -theNode2487: Con CNat - - -theNode2488 - -theNode2488: App theNode2488 Prod Nat (?α_19_26__9) - - -theNode2488->theNode2485 - - -L - - -theNode2488->theNode2487 - - -R - - -theNode2490 - -theNode2490: App theNode2490 Prod Nat (?α_19_26__9) - - -theNode2490->α_19_26__9 - - -R - - -theNode2490->theNode2488 - - -L - - -theNode2491 - -theNode2491: App theNode2491 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2491->theNode2483 - - -L - - -theNode2491->theNode2490 - - -R - - -theNode2494 - -theNode2494: Con Pi - - -theNode2496 - -theNode2496: Con CNat - - -theNode2497 - -theNode2497: App theNode2497 Nat -> Prod Nat (?α_19_26__9) - - -theNode2497->theNode2494 - - -L - - -theNode2497->theNode2496 - - -R - - -theNode2500 - -theNode2500: Con Sig - - -theNode2502 - -theNode2502: Con CNat - - -theNode2503 - -theNode2503: App theNode2503 Prod Nat (?α_19_26__9) - - -theNode2503->theNode2500 - - -L - - -theNode2503->theNode2502 - - -R - - -theNode2505 - -theNode2505: App theNode2505 Prod Nat (?α_19_26__9) - - -theNode2505->α_19_26__9 - - -R - - -theNode2505->theNode2503 - - -L - - -theNode2507 - -theNode2507: BoundVar arg2498 - - -theNode2508 - -theNode2508: Lam theNode2508  arg . Prod Nat (?α_19_26__9) - - -theNode2508->theNode2505 - - -R - - -theNode2508->theNode2507 - - -L - - -theNode2509 - -theNode2509: App theNode2509 Nat -> Prod Nat (?α_19_26__9) - - -theNode2509->theNode2497 - - -L - - -theNode2509->theNode2508 - - -R - - -theNode2511 - -theNode2511: BoundVar arg2492 - - -theNode2512 - -theNode2512: Lam theNode2512  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode2512->theNode2509 - - -R - - -theNode2512->theNode2511 - - -L - - -theNode2513 - -theNode2513: App theNode2513 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2513->theNode2491 - - -L - - -theNode2513->theNode2512 - - -R - - -theNode2515 - -theNode2515: BoundVar arg2481 - - -theNode2516 - -theNode2516: Lam theNode2516  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2516->theNode2513 - - -R - - -theNode2516->theNode2515 - - -L - - -theNode2517 - -theNode2517: App theNode2517 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2517->theNode2480 - - -L - - -theNode2517->theNode2516 - - -R - - -theNode2519 - -theNode2519: BoundVar arg2470 - - -theNode2469 - -theNode2469: Lam theNode2469  arg . (Prod ?α_19_22__8 (?α_19_26__9)) -> (Prod ?α_19_22__8 (?α_19_26__9)) -> Nat -> Prod ?α_19_22__8 (?α_19_26__9) - - -theNode2469->theNode2466 - - -R - - -theNode2469->theNode2468 - - -L - - -theNode2520 - -theNode2520: Lam theNode2520  arg . (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2469->theNode2520 - - - -theNode2520->theNode2517 - - -R - - -theNode2520->theNode2519 - - -L - - -theNode2528 - -theNode2528: Con CSucc - - -theNode2530 - -theNode2530: Con CZero - - -theNode2531 - -theNode2531: App theNode2531 Succ Zero - - -theNode2531->theNode2528 - - -L - - -theNode2531->theNode2530 - - -R - - -theNode2532 - -theNode2532: App theNode2532 ?α_19_26__9 Succ Zero - - -theNode2532->theNode - - -L - - -theNode2532->theNode2531 - - -R - - -theNode2525 - -theNode2525: Con CNat - - -theNode2533 - -theNode2533: Elim theNode2533 ?α_19_26__9 Succ Zero - - -theNode2525->theNode2533 - - - -theNode2533->α_19_26__9 - - -L - - -theNode2533->theNode2532 - - -R - - -theNode2546 - -theNode2546: Con Pair - - -theNode2548 - -theNode2548: Con CSucc - - -theNode2550 - -theNode2550: Con CZero - - -theNode2551 - -theNode2551: App theNode2551 Succ Zero - - -theNode2551->theNode2548 - - -L - - -theNode2551->theNode2550 - - -R - - -theNode2552 - -theNode2552: App theNode2552 Pair ((Succ Zero)) ((Succ Zero)) - - -theNode2552->theNode2546 - - -L - - -theNode2552->theNode2551 - - -R - - -theNode2554 - -theNode2554: Con CSucc - - -theNode2556 - -theNode2556: Con CZero - - -theNode2557 - -theNode2557: App theNode2557 Succ Zero - - -theNode2557->theNode2554 - - -L - - -theNode2557->theNode2556 - - -R - - -theNode2558 - -theNode2558: App theNode2558 Pair ((Succ Zero)) ((Succ Zero)) - - -theNode2558->theNode2552 - - -L - - -theNode2558->theNode2557 - - -R - - -theNode2559 - -theNode2559: App theNode2559 ?α_19_12__6 Pair ((Succ Zero)) ((Succ Zero)) - - -theNode2559->theNode - - -L - - -theNode2559->theNode2558 - - -R - - -theNode2562 - -theNode2562: Con Pi - - -theNode2564 - -theNode2564: Con Sig - - -theNode2566 - -theNode2566: Con CNat - - -theNode2567 - -theNode2567: App theNode2567 Prod Nat (?α_19_26__9) - - -theNode2567->theNode2564 - - -L - - -theNode2567->theNode2566 - - -R - - -theNode2569 - -theNode2569: App theNode2569 Prod Nat (?α_19_26__9) - - -theNode2569->α_19_26__9 - - -R - - -theNode2569->theNode2567 - - -L - - -theNode2570 - -theNode2570: App theNode2570 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2570->theNode2562 - - -L - - -theNode2570->theNode2569 - - -R - - -theNode2573 - -theNode2573: Con Pi - - -theNode2575 - -theNode2575: Con Sig - - -theNode2577 - -theNode2577: Con CNat - - -theNode2578 - -theNode2578: App theNode2578 Prod Nat (?α_19_26__9) - - -theNode2578->theNode2575 - - -L - - -theNode2578->theNode2577 - - -R - - -theNode2580 - -theNode2580: App theNode2580 Prod Nat (?α_19_26__9) - - -theNode2580->α_19_26__9 - - -R - - -theNode2580->theNode2578 - - -L - - -theNode2581 - -theNode2581: App theNode2581 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2581->theNode2573 - - -L - - -theNode2581->theNode2580 - - -R - - -theNode2584 - -theNode2584: Con Pi - - -theNode2586 - -theNode2586: Con CNat - - -theNode2587 - -theNode2587: App theNode2587 Nat -> Prod Nat (?α_19_26__9) - - -theNode2587->theNode2584 - - -L - - -theNode2587->theNode2586 - - -R - - -theNode2590 - -theNode2590: Con Sig - - -theNode2592 - -theNode2592: Con CNat - - -theNode2593 - -theNode2593: App theNode2593 Prod Nat (?α_19_26__9) - - -theNode2593->theNode2590 - - -L - - -theNode2593->theNode2592 - - -R - - -theNode2595 - -theNode2595: App theNode2595 Prod Nat (?α_19_26__9) - - -theNode2595->α_19_26__9 - - -R - - -theNode2595->theNode2593 - - -L - - -theNode2597 - -theNode2597: BoundVar arg2588 - - -theNode2598 - -theNode2598: Lam theNode2598  arg . Prod Nat (?α_19_26__9) - - -theNode2598->theNode2595 - - -R - - -theNode2598->theNode2597 - - -L - - -theNode2599 - -theNode2599: App theNode2599 Nat -> Prod Nat (?α_19_26__9) - - -theNode2599->theNode2587 - - -L - - -theNode2599->theNode2598 - - -R - - -theNode2601 - -theNode2601: BoundVar arg2582 - - -theNode2602 - -theNode2602: Lam theNode2602  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode2602->theNode2599 - - -R - - -theNode2602->theNode2601 - - -L - - -theNode2603 - -theNode2603: App theNode2603 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2603->theNode2581 - - -L - - -theNode2603->theNode2602 - - -R - - -theNode2605 - -theNode2605: BoundVar arg2571 - - -theNode2606 - -theNode2606: Lam theNode2606  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2606->theNode2603 - - -R - - -theNode2606->theNode2605 - - -L - - -theNode2560 - -theNode2560: Elim theNode2560 ?α_19_12__6 Pair ((Succ Zero)) ((Succ Zero)) - - -theNode2560->α_19_12__6 - - -L - - -theNode2560->theNode2559 - - -R - - -theNode2607 - -theNode2607: App theNode2607 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2560->theNode2607 - - - -theNode2607->theNode2570 - - -L - - -theNode2607->theNode2606 - - -R - - -theNode2624 - -theNode2624: Con Pi - - -theNode2626 - -theNode2626: Con Sig - - -theNode2628 - -theNode2628: Con CNat - - -theNode2629 - -theNode2629: App theNode2629 Prod Nat (?α_19_26__9) - - -theNode2629->theNode2626 - - -L - - -theNode2629->theNode2628 - - -R - - -theNode2631 - -theNode2631: App theNode2631 Prod Nat (?α_19_26__9) - - -theNode2631->α_19_26__9 - - -R - - -theNode2631->theNode2629 - - -L - - -theNode2632 - -theNode2632: App theNode2632 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2632->theNode2624 - - -L - - -theNode2632->theNode2631 - - -R - - -theNode2635 - -theNode2635: Con Pi - - -theNode2637 - -theNode2637: Con CNat - - -theNode2638 - -theNode2638: App theNode2638 Nat -> Prod Nat (?α_19_26__9) - - -theNode2638->theNode2635 - - -L - - -theNode2638->theNode2637 - - -R - - -theNode2641 - -theNode2641: Con Sig - - -theNode2643 - -theNode2643: Con CNat - - -theNode2644 - -theNode2644: App theNode2644 Prod Nat (?α_19_26__9) - - -theNode2644->theNode2641 - - -L - - -theNode2644->theNode2643 - - -R - - -theNode2646 - -theNode2646: App theNode2646 Prod Nat (?α_19_26__9) - - -theNode2646->α_19_26__9 - - -R - - -theNode2646->theNode2644 - - -L - - -theNode2648 - -theNode2648: BoundVar arg2639 - - -theNode2649 - -theNode2649: Lam theNode2649  arg . Prod Nat (?α_19_26__9) - - -theNode2649->theNode2646 - - -R - - -theNode2649->theNode2648 - - -L - - -theNode2650 - -theNode2650: App theNode2650 Nat -> Prod Nat (?α_19_26__9) - - -theNode2650->theNode2638 - - -L - - -theNode2650->theNode2649 - - -R - - -theNode2652 - -theNode2652: BoundVar arg2633 - - -theNode2653 - -theNode2653: Lam theNode2653  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode2653->theNode2650 - - -R - - -theNode2653->theNode2652 - - -L - - -theNode2654 - -theNode2654: App theNode2654 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2654->theNode2632 - - -L - - -theNode2654->theNode2653 - - -R - - -theNode2656 - -theNode2656: BoundVar arg2622 - - -theNode2658 - -theNode2658: App theNode2658 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2664 - -theNode2664: App theNode2664 ?α_19_29__17 -> (?α_19_12__18) - - -theNode2658->theNode2664 - - - -theNode2621 - -theNode2621: App theNode2621 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2658->theNode2621 - - -L - - -theNode2657 - -theNode2657: Lam theNode2657  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode2658->theNode2657 - - -R - - -theNode2662 - -theNode2662: App theNode2662 ?α_19_29__17 -> (?α_19_12__18) - - -theNode2664->theNode2662 - - -L - - -α_19_12__18 - -α_19_12__18: Meta α_19_12__18 - - -theNode2664->α_19_12__18 - - -R - - -theNode2613 - -theNode2613: Con Pi - - -theNode2621->theNode2613 - - -L - - -theNode2620 - -theNode2620: App theNode2620 Prod Nat (?α_19_26__9) - - -theNode2621->theNode2620 - - -R - - -theNode2660 - -theNode2660: Con Pi - - -theNode2662->theNode2660 - - -L - - -α_19_29__17 - -α_19_29__17: Meta α_19_29__17 - - -theNode2662->α_19_29__17 - - -R - - -theNode2741 - -theNode2741: App theNode2741 Prod Nat (?α_19_26__9) - - -α_19_29__17->theNode2741 - - - -theNode4528 - -theNode4528: App theNode4528 Prod Nat (?α_19_26__9) - - -α_19_29__17->theNode4528 - - - -theNode3450 - -theNode3450: Lam theNode3450  arg . ?x2899 (fst) arg (snd) arg - - -α_19_12__18->theNode3450 - - - -theNode3472 - -theNode3472: Lam theNode3472  arg . ?x2899 (fst) arg (snd) arg - - -α_19_12__18->theNode3472 - - - -theNode3439 - -theNode3439: BoundVar arg3436 - - -theNode3440 - -theNode3440: Elim theNode3440 (fst) arg3436 - - -theNode3440->theNode - - -R - - -theNode3440->theNode3439 - - -L - - -theNode3441 - -theNode3441: App theNode3441 ?x2899 (fst) arg3436 (snd) arg3436 - - -theNode3441->theNode - - -L - - -theNode3441->theNode3440 - - -R - - -theNode3442 - -theNode3442: Elim theNode3442 ?x2899 (fst) arg3436 (snd) arg3436 - - -theNode3442->theNode3441 - - -R - - -x2899 - -x2899: Meta x2899 - - -theNode3442->x2899 - - -L - - -theNode3444 - -theNode3444: BoundVar arg3436 - - -theNode3445 - -theNode3445: Elim theNode3445 (snd) arg3436 - - -theNode3445->theNode - - -R - - -theNode3445->theNode3444 - - -L - - -theNode3446 - -theNode3446: App theNode3446 ?x2899 (fst) arg3436 (snd) arg3436 - - -theNode3446->theNode - - -L - - -theNode3446->theNode3445 - - -R - - -theNode3447 - -theNode3447: Elim theNode3447 ?x2899 (fst) arg3436 (snd) arg3436 - - -theNode3447->theNode3442 - - -L - - -theNode3447->theNode3446 - - -R - - -theNode3449 - -theNode3449: BoundVar arg3436 - - -theNode4043 - -theNode4043: Lam theNode4043  arg arg1 . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -x2899->theNode4043 - - - -theNode3461 - -theNode3461: BoundVar arg3458 - - -theNode3462 - -theNode3462: Elim theNode3462 (fst) arg3458 - - -theNode3462->theNode - - -R - - -theNode3462->theNode3461 - - -L - - -theNode3463 - -theNode3463: App theNode3463 ?x2899 (fst) arg3458 (snd) arg3458 - - -theNode3463->theNode - - -L - - -theNode3463->theNode3462 - - -R - - -theNode3464 - -theNode3464: Elim theNode3464 ?x2899 (fst) arg3458 (snd) arg3458 - - -theNode3464->x2899 - - -L - - -theNode3464->theNode3463 - - -R - - -theNode3466 - -theNode3466: BoundVar arg3458 - - -theNode3467 - -theNode3467: Elim theNode3467 (snd) arg3458 - - -theNode3467->theNode - - -R - - -theNode3467->theNode3466 - - -L - - -theNode3468 - -theNode3468: App theNode3468 ?x2899 (fst) arg3458 (snd) arg3458 - - -theNode3468->theNode - - -L - - -theNode3468->theNode3467 - - -R - - -theNode3469 - -theNode3469: Elim theNode3469 ?x2899 (fst) arg3458 (snd) arg3458 - - -theNode3469->theNode3464 - - -L - - -theNode3469->theNode3468 - - -R - - -theNode3471 - -theNode3471: BoundVar arg3458 - - -theNode3482 - -theNode3482: Con Pi - - -theNode3484 - -theNode3484: Con Sig - - -theNode3486 - -theNode3486: Con CNat - - -theNode3487 - -theNode3487: App theNode3487 Prod Nat (?α_19_26__9) - - -theNode3487->theNode3484 - - -L - - -theNode3487->theNode3486 - - -R - - -theNode3489 - -theNode3489: App theNode3489 Prod Nat (?α_19_26__9) - - -theNode3489->α_19_26__9 - - -R - - -theNode3489->theNode3487 - - -L - - -theNode3490 - -theNode3490: App theNode3490 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode3490->theNode3482 - - -L - - -theNode3490->theNode3489 - - -R - - -theNode3493 - -theNode3493: Con Pi - - -theNode3495 - -theNode3495: Con CNat - - -theNode3496 - -theNode3496: App theNode3496 Nat -> Prod Nat (?α_19_26__9) - - -theNode3496->theNode3493 - - -L - - -theNode3496->theNode3495 - - -R - - -theNode3499 - -theNode3499: Con Sig - - -theNode3501 - -theNode3501: Con CNat - - -theNode3502 - -theNode3502: App theNode3502 Prod Nat (?α_19_26__9) - - -theNode3502->theNode3499 - - -L - - -theNode3502->theNode3501 - - -R - - -theNode3504 - -theNode3504: App theNode3504 Prod Nat (?α_19_26__9) - - -theNode3504->α_19_26__9 - - -R - - -theNode3504->theNode3502 - - -L - - -theNode3506 - -theNode3506: BoundVar arg3497 - - -theNode3507 - -theNode3507: Lam theNode3507  arg . Prod Nat (?α_19_26__9) - - -theNode3507->theNode3504 - - -R - - -theNode3507->theNode3506 - - -L - - -theNode3508 - -theNode3508: App theNode3508 Nat -> Prod Nat (?α_19_26__9) - - -theNode3508->theNode3496 - - -L - - -theNode3508->theNode3507 - - -R - - -theNode3510 - -theNode3510: BoundVar arg3491 - - -theNode3511 - -theNode3511: Lam theNode3511  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode3511->theNode3508 - - -R - - -theNode3511->theNode3510 - - -L - - -theNode3512 - -theNode3512: App theNode3512 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode3512->theNode3490 - - -L - - -theNode3512->theNode3511 - - -R - - -theNode3514 - -theNode3514: BoundVar arg3480 - - -theNode3519 - -theNode3519: BoundVar arg3516 - - -theNode3520 - -theNode3520: Elim theNode3520 (fst) arg3516 - - -theNode3520->theNode - - -R - - -theNode3520->theNode3519 - - -L - - -theNode3521 - -theNode3521: App theNode3521 ?x2899 (fst) arg3516 (snd) arg3516 - - -theNode3521->theNode - - -L - - -theNode3521->theNode3520 - - -R - - -theNode3522 - -theNode3522: Elim theNode3522 ?x2899 (fst) arg3516 (snd) arg3516 - - -theNode3522->x2899 - - -L - - -theNode3522->theNode3521 - - -R - - -theNode3524 - -theNode3524: BoundVar arg3516 - - -theNode3525 - -theNode3525: Elim theNode3525 (snd) arg3516 - - -theNode3525->theNode - - -R - - -theNode3525->theNode3524 - - -L - - -theNode3526 - -theNode3526: App theNode3526 ?x2899 (fst) arg3516 (snd) arg3516 - - -theNode3526->theNode - - -L - - -theNode3526->theNode3525 - - -R - - -theNode3527 - -theNode3527: Elim theNode3527 ?x2899 (fst) arg3516 (snd) arg3516 - - -theNode3527->theNode3522 - - -L - - -theNode3527->theNode3526 - - -R - - -theNode3529 - -theNode3529: BoundVar arg3516 - - -theNode3515 - -theNode3515: Lam theNode3515  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode3515->theNode3512 - - -R - - -theNode3515->theNode3514 - - -L - - -theNode3530 - -theNode3530: Lam theNode3530  arg . ?x2899 (fst) arg (snd) arg - - -theNode3515->theNode3530 - - - -theNode3530->theNode3527 - - -R - - -theNode3530->theNode3529 - - -L - - -theNode3709 - -theNode3709: Con Pi - - -theNode3711 - -theNode3711: Con Sig - - -theNode3713 - -theNode3713: Con CNat - - -theNode3714 - -theNode3714: App theNode3714 Prod Nat (?α_19_26__9) - - -theNode3714->theNode3711 - - -L - - -theNode3714->theNode3713 - - -R - - -theNode3716 - -theNode3716: App theNode3716 Prod Nat (?α_19_26__9) - - -theNode3716->α_19_26__9 - - -R - - -theNode3716->theNode3714 - - -L - - -theNode3717 - -theNode3717: App theNode3717 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode3717->theNode3709 - - -L - - -theNode3717->theNode3716 - - -R - - -theNode3720 - -theNode3720: Con Pi - - -theNode3722 - -theNode3722: Con CNat - - -theNode3723 - -theNode3723: App theNode3723 Nat -> Prod Nat (?α_19_26__9) - - -theNode3723->theNode3720 - - -L - - -theNode3723->theNode3722 - - -R - - -theNode3726 - -theNode3726: Con Sig - - -theNode3728 - -theNode3728: Con CNat - - -theNode3729 - -theNode3729: App theNode3729 Prod Nat (?α_19_26__9) - - -theNode3729->theNode3726 - - -L - - -theNode3729->theNode3728 - - -R - - -theNode3731 - -theNode3731: App theNode3731 Prod Nat (?α_19_26__9) - - -theNode3731->α_19_26__9 - - -R - - -theNode3731->theNode3729 - - -L - - -theNode3733 - -theNode3733: BoundVar arg3724 - - -theNode3734 - -theNode3734: Lam theNode3734  arg . Prod Nat (?α_19_26__9) - - -theNode3734->theNode3731 - - -R - - -theNode3734->theNode3733 - - -L - - -theNode3735 - -theNode3735: App theNode3735 Nat -> Prod Nat (?α_19_26__9) - - -theNode3735->theNode3723 - - -L - - -theNode3735->theNode3734 - - -R - - -theNode3737 - -theNode3737: BoundVar arg3718 - - -theNode3738 - -theNode3738: Lam theNode3738  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode3738->theNode3735 - - -R - - -theNode3738->theNode3737 - - -L - - -theNode3742 - -theNode3742: BoundVar x3704 - - -theNode3743 - -theNode3743: App theNode3743 ?x2899 x3704 x3705 - - -theNode3743->theNode - - -L - - -theNode3743->theNode3742 - - -R - - -theNode3744 - -theNode3744: Elim theNode3744 ?x2899 x3704 x3705 - - -theNode3744->x2899 - - -L - - -theNode3744->theNode3743 - - -R - - -theNode3746 - -theNode3746: BoundVar x3705 - - -theNode3747 - -theNode3747: App theNode3747 ?x2899 x3704 x3705 - - -theNode3747->theNode - - -L - - -theNode3747->theNode3746 - - -R - - -theNode3739 - -theNode3739: App theNode3739 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode3739->theNode3717 - - -L - - -theNode3739->theNode3738 - - -R - - -theNode3748 - -theNode3748: Elim theNode3748 ?x2899 x3704 x3705 - - -theNode3739->theNode3748 - - - -theNode3748->theNode3744 - - -L - - -theNode3748->theNode3747 - - -R - - -theNode4007 - -theNode4007: Con Pi - - -theNode4009 - -theNode4009: Con Sig - - -theNode4011 - -theNode4011: Con CNat - - -theNode4012 - -theNode4012: App theNode4012 Prod Nat (?α_19_26__9) - - -theNode4012->theNode4009 - - -L - - -theNode4012->theNode4011 - - -R - - -theNode4014 - -theNode4014: App theNode4014 Prod Nat (?α_19_26__9) - - -theNode4014->α_19_26__9 - - -R - - -theNode4014->theNode4012 - - -L - - -theNode4015 - -theNode4015: App theNode4015 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4015->theNode4007 - - -L - - -theNode4015->theNode4014 - - -R - - -theNode4018 - -theNode4018: Con Pi - - -theNode4020 - -theNode4020: Con CNat - - -theNode4021 - -theNode4021: App theNode4021 Nat -> Prod Nat (?α_19_26__9) - - -theNode4021->theNode4018 - - -L - - -theNode4021->theNode4020 - - -R - - -theNode4024 - -theNode4024: Con Sig - - -theNode4026 - -theNode4026: Con CNat - - -theNode4027 - -theNode4027: App theNode4027 Prod Nat (?α_19_26__9) - - -theNode4027->theNode4024 - - -L - - -theNode4027->theNode4026 - - -R - - -theNode4029 - -theNode4029: App theNode4029 Prod Nat (?α_19_26__9) - - -theNode4029->α_19_26__9 - - -R - - -theNode4029->theNode4027 - - -L - - -theNode4031 - -theNode4031: BoundVar arg4022 - - -theNode4032 - -theNode4032: Lam theNode4032  arg . Prod Nat (?α_19_26__9) - - -theNode4032->theNode4029 - - -R - - -theNode4032->theNode4031 - - -L - - -theNode4033 - -theNode4033: App theNode4033 Nat -> Prod Nat (?α_19_26__9) - - -theNode4033->theNode4021 - - -L - - -theNode4033->theNode4032 - - -R - - -theNode4035 - -theNode4035: BoundVar arg4016 - - -theNode4036 - -theNode4036: Lam theNode4036  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode4036->theNode4033 - - -R - - -theNode4036->theNode4035 - - -L - - -theNode4037 - -theNode4037: App theNode4037 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4037->theNode4015 - - -L - - -theNode4037->theNode4036 - - -R - - -theNode4039 - -theNode4039: BoundVar arg4005 - - -theNode4040 - -theNode4040: Lam theNode4040  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4040->theNode4037 - - -R - - -theNode4040->theNode4039 - - -L - - -theNode4042 - -theNode4042: BoundVar arg4004 - - -theNode4043->theNode4040 - - -R - - -theNode4043->theNode4042 - - -L - - -theNode4366 - -theNode4366: BoundVar arg4363 - - -theNode4367 - -theNode4367: Elim theNode4367 (fst) arg4363 - - -theNode4367->theNode - - -R - - -theNode4367->theNode4366 - - -L - - -theNode4368 - -theNode4368: App theNode4368 ?x2899 (fst) arg4363 (snd) arg4363 - - -theNode4368->theNode - - -L - - -theNode4368->theNode4367 - - -R - - -theNode4369 - -theNode4369: Elim theNode4369 ?x2899 (fst) arg4363 (snd) arg4363 - - -theNode4369->x2899 - - -L - - -theNode4369->theNode4368 - - -R - - -theNode4371 - -theNode4371: BoundVar arg4363 - - -theNode4372 - -theNode4372: Elim theNode4372 (snd) arg4363 - - -theNode4372->theNode - - -R - - -theNode4372->theNode4371 - - -L - - -theNode4373 - -theNode4373: App theNode4373 ?x2899 (fst) arg4363 (snd) arg4363 - - -theNode4373->theNode - - -L - - -theNode4373->theNode4372 - - -R - - -theNode4374 - -theNode4374: Elim theNode4374 ?x2899 (fst) arg4363 (snd) arg4363 - - -theNode4374->theNode4369 - - -L - - -theNode4374->theNode4373 - - -R - - -theNode4376 - -theNode4376: BoundVar arg4363 - - -theNode4380 - -theNode4380: Con Pi - - -theNode4382 - -theNode4382: Con Sig - - -theNode4384 - -theNode4384: Con CNat - - -theNode4385 - -theNode4385: App theNode4385 Prod Nat (?α_19_26__9) - - -theNode4385->theNode4382 - - -L - - -theNode4385->theNode4384 - - -R - - -theNode4387 - -theNode4387: App theNode4387 Prod Nat (?α_19_26__9) - - -theNode4387->α_19_26__9 - - -R - - -theNode4387->theNode4385 - - -L - - -theNode4388 - -theNode4388: App theNode4388 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4388->theNode4380 - - -L - - -theNode4388->theNode4387 - - -R - - -theNode4391 - -theNode4391: Con Pi - - -theNode4393 - -theNode4393: Con CNat - - -theNode4394 - -theNode4394: App theNode4394 Nat -> Prod Nat (?α_19_26__9) - - -theNode4394->theNode4391 - - -L - - -theNode4394->theNode4393 - - -R - - -theNode4397 - -theNode4397: Con Sig - - -theNode4399 - -theNode4399: Con CNat - - -theNode4400 - -theNode4400: App theNode4400 Prod Nat (?α_19_26__9) - - -theNode4400->theNode4397 - - -L - - -theNode4400->theNode4399 - - -R - - -theNode4402 - -theNode4402: App theNode4402 Prod Nat (?α_19_26__9) - - -theNode4402->α_19_26__9 - - -R - - -theNode4402->theNode4400 - - -L - - -theNode4404 - -theNode4404: BoundVar arg4395 - - -theNode4405 - -theNode4405: Lam theNode4405  arg . Prod Nat (?α_19_26__9) - - -theNode4405->theNode4402 - - -R - - -theNode4405->theNode4404 - - -L - - -theNode4406 - -theNode4406: App theNode4406 Nat -> Prod Nat (?α_19_26__9) - - -theNode4406->theNode4394 - - -L - - -theNode4406->theNode4405 - - -R - - -theNode4408 - -theNode4408: BoundVar arg4389 - - -theNode4409 - -theNode4409: Lam theNode4409  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode4409->theNode4406 - - -R - - -theNode4409->theNode4408 - - -L - - -theNode4410 - -theNode4410: App theNode4410 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4410->theNode4388 - - -L - - -theNode4410->theNode4409 - - -R - - -theNode4412 - -theNode4412: BoundVar arg4378 - - -theNode4377 - -theNode4377: Lam theNode4377  arg . ?x2899 (fst) arg (snd) arg - - -theNode4377->theNode4374 - - -R - - -theNode4377->theNode4376 - - -L - - -theNode4413 - -theNode4413: Lam theNode4413  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4377->theNode4413 - - - -theNode4413->theNode4410 - - -R - - -theNode4413->theNode4412 - - -L - - -theNode4418 - -theNode4418: BoundVar arg4415 - - -theNode4419 - -theNode4419: Elim theNode4419 (fst) arg4415 - - -theNode4419->theNode - - -R - - -theNode4419->theNode4418 - - -L - - -theNode4420 - -theNode4420: App theNode4420 ?x2899 (fst) arg4415 (snd) arg4415 - - -theNode4420->theNode - - -L - - -theNode4420->theNode4419 - - -R - - -theNode4421 - -theNode4421: Elim theNode4421 ?x2899 (fst) arg4415 (snd) arg4415 - - -theNode4421->x2899 - - -L - - -theNode4421->theNode4420 - - -R - - -theNode4423 - -theNode4423: BoundVar arg4415 - - -theNode4424 - -theNode4424: Elim theNode4424 (snd) arg4415 - - -theNode4424->theNode - - -R - - -theNode4424->theNode4423 - - -L - - -theNode4425 - -theNode4425: App theNode4425 ?x2899 (fst) arg4415 (snd) arg4415 - - -theNode4425->theNode - - -L - - -theNode4425->theNode4424 - - -R - - -theNode4426 - -theNode4426: Elim theNode4426 ?x2899 (fst) arg4415 (snd) arg4415 - - -theNode4426->theNode4421 - - -L - - -theNode4426->theNode4425 - - -R - - -theNode4428 - -theNode4428: BoundVar arg4415 - - -theNode4432 - -theNode4432: Con Pi - - -theNode4434 - -theNode4434: Con Sig - - -theNode4436 - -theNode4436: Con CNat - - -theNode4437 - -theNode4437: App theNode4437 Prod Nat (?α_19_26__9) - - -theNode4437->theNode4434 - - -L - - -theNode4437->theNode4436 - - -R - - -theNode4439 - -theNode4439: App theNode4439 Prod Nat (?α_19_26__9) - - -theNode4439->α_19_26__9 - - -R - - -theNode4439->theNode4437 - - -L - - -theNode4440 - -theNode4440: App theNode4440 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4440->theNode4432 - - -L - - -theNode4440->theNode4439 - - -R - - -theNode4443 - -theNode4443: Con Pi - - -theNode4445 - -theNode4445: Con CNat - - -theNode4446 - -theNode4446: App theNode4446 Nat -> Prod Nat (?α_19_26__9) - - -theNode4446->theNode4443 - - -L - - -theNode4446->theNode4445 - - -R - - -theNode4449 - -theNode4449: Con Sig - - -theNode4451 - -theNode4451: Con CNat - - -theNode4452 - -theNode4452: App theNode4452 Prod Nat (?α_19_26__9) - - -theNode4452->theNode4449 - - -L - - -theNode4452->theNode4451 - - -R - - -theNode4454 - -theNode4454: App theNode4454 Prod Nat (?α_19_26__9) - - -theNode4454->α_19_26__9 - - -R - - -theNode4454->theNode4452 - - -L - - -theNode4456 - -theNode4456: BoundVar arg4447 - - -theNode4457 - -theNode4457: Lam theNode4457  arg . Prod Nat (?α_19_26__9) - - -theNode4457->theNode4454 - - -R - - -theNode4457->theNode4456 - - -L - - -theNode4458 - -theNode4458: App theNode4458 Nat -> Prod Nat (?α_19_26__9) - - -theNode4458->theNode4446 - - -L - - -theNode4458->theNode4457 - - -R - - -theNode4460 - -theNode4460: BoundVar arg4441 - - -theNode4461 - -theNode4461: Lam theNode4461  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode4461->theNode4458 - - -R - - -theNode4461->theNode4460 - - -L - - -theNode4462 - -theNode4462: App theNode4462 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4462->theNode4440 - - -L - - -theNode4462->theNode4461 - - -R - - -theNode4464 - -theNode4464: BoundVar arg4430 - - -theNode4429 - -theNode4429: Lam theNode4429  arg . ?x2899 (fst) arg (snd) arg - - -theNode4429->theNode4426 - - -R - - -theNode4429->theNode4428 - - -L - - -theNode4465 - -theNode4465: Lam theNode4465  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4429->theNode4465 - - - -theNode4465->theNode4462 - - -R - - -theNode4465->theNode4464 - - -L - - -theNode4485 - -theNode4485: Con Pi - - -theNode4487 - -theNode4487: Con Sig - - -theNode4489 - -theNode4489: Con CNat - - -theNode4490 - -theNode4490: App theNode4490 Prod Nat (?α_19_26__9) - - -theNode4490->theNode4487 - - -L - - -theNode4490->theNode4489 - - -R - - -theNode4492 - -theNode4492: App theNode4492 Prod Nat (?α_19_26__9) - - -theNode4492->α_19_26__9 - - -R - - -theNode4492->theNode4490 - - -L - - -theNode4493 - -theNode4493: App theNode4493 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4493->theNode4485 - - -L - - -theNode4493->theNode4492 - - -R - - -theNode4496 - -theNode4496: Con Pi - - -theNode4498 - -theNode4498: Con CNat - - -theNode4499 - -theNode4499: App theNode4499 Nat -> Prod Nat (?α_19_26__9) - - -theNode4499->theNode4496 - - -L - - -theNode4499->theNode4498 - - -R - - -theNode4502 - -theNode4502: Con Sig - - -theNode4504 - -theNode4504: Con CNat - - -theNode4505 - -theNode4505: App theNode4505 Prod Nat (?α_19_26__9) - - -theNode4505->theNode4502 - - -L - - -theNode4505->theNode4504 - - -R - - -theNode4507 - -theNode4507: App theNode4507 Prod Nat (?α_19_26__9) - - -theNode4507->α_19_26__9 - - -R - - -theNode4507->theNode4505 - - -L - - -theNode4509 - -theNode4509: BoundVar arg4500 - - -theNode4510 - -theNode4510: Lam theNode4510  arg . Prod Nat (?α_19_26__9) - - -theNode4510->theNode4507 - - -R - - -theNode4510->theNode4509 - - -L - - -theNode4511 - -theNode4511: App theNode4511 Nat -> Prod Nat (?α_19_26__9) - - -theNode4511->theNode4499 - - -L - - -theNode4511->theNode4510 - - -R - - -theNode4513 - -theNode4513: BoundVar arg4494 - - -theNode4514 - -theNode4514: Lam theNode4514  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode4514->theNode4511 - - -R - - -theNode4514->theNode4513 - - -L - - -theNode4515 - -theNode4515: App theNode4515 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4515->theNode4493 - - -L - - -theNode4515->theNode4514 - - -R - - -theNode4517 - -theNode4517: BoundVar arg4483 - - -theNode4472 - -theNode4472: App theNode4472 ?α_19_29__17 -> (?α_19_12__18) - - -theNode4472->α_19_12__18 - - -R - - -theNode4519 - -theNode4519: App theNode4519 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4472->theNode4519 - - - -theNode4470 - -theNode4470: App theNode4470 ?α_19_29__17 -> (?α_19_12__18) - - -theNode4472->theNode4470 - - -L - - -theNode4482 - -theNode4482: App theNode4482 (Prod Nat (?α_19_26__9)) -> (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4519->theNode4482 - - -L - - -theNode4518 - -theNode4518: Lam theNode4518  arg . (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4519->theNode4518 - - -R - - -theNode4470->α_19_29__17 - - -R - - -theNode4468 - -theNode4468: Con Pi - - -theNode4470->theNode4468 - - -L - - -theNode4474 - -theNode4474: Con Pi - - -theNode4482->theNode4474 - - -L - - -theNode4481 - -theNode4481: App theNode4481 Prod Nat (?α_19_26__9) - - -theNode4482->theNode4481 - - -R - - -theNode4518->theNode4515 - - -R - - -theNode4518->theNode4517 - - -L - - -theNode2657->theNode2654 - - -R - - -theNode2657->theNode2656 - - -L - - -theNode3450->theNode3447 - - -R - - -theNode3450->theNode3449 - - -L - - -theNode3472->theNode3469 - - -R - - -theNode3472->theNode3471 - - -L - - -theNode4481->α_19_26__9 - - -R - - -theNode4479 - -theNode4479: App theNode4479 Prod Nat (?α_19_26__9) - - -theNode4481->theNode4479 - - -L - - -theNode2683 - -theNode2683: App theNode2683 Prod Nat (?α_19_26__9) - - -theNode2683->α_19_26__9 - - -R - - -theNode2683->α_19_29__17 - - - -theNode2681 - -theNode2681: App theNode2681 Prod Nat (?α_19_26__9) - - -theNode2683->theNode2681 - - -L - - -theNode2620->α_19_26__9 - - -R - - -theNode2618 - -theNode2618: App theNode2618 Prod Nat (?α_19_26__9) - - -theNode2620->theNode2618 - - -L - - -theNode2741->α_19_26__9 - - -R - - -theNode2739 - -theNode2739: App theNode2739 Prod Nat (?α_19_26__9) - - -theNode2741->theNode2739 - - -L - - -theNode4528->α_19_26__9 - - -R - - -theNode4526 - -theNode4526: App theNode4526 Prod Nat (?α_19_26__9) - - -theNode4528->theNode4526 - - -L - - -theNode2615 - -theNode2615: Con Sig - - -theNode2618->theNode2615 - - -L - - -theNode2617 - -theNode2617: Con CNat - - -theNode2618->theNode2617 - - -R - - -theNode2678 - -theNode2678: Con Sig - - -theNode2681->theNode2678 - - -L - - -theNode2680 - -theNode2680: Con CNat - - -theNode2681->theNode2680 - - -R - - -theNode2736 - -theNode2736: Con Sig - - -theNode2739->theNode2736 - - -L - - -theNode2738 - -theNode2738: Con CNat - - -theNode2739->theNode2738 - - -R - - -theNode4476 - -theNode4476: Con Sig - - -theNode4479->theNode4476 - - -L - - -theNode4478 - -theNode4478: Con CNat - - -theNode4479->theNode4478 - - -R - - -theNode4523 - -theNode4523: Con Sig - - -theNode4526->theNode4523 - - -L - - -theNode4525 - -theNode4525: Con CNat - - -theNode4526->theNode4525 - - -R - - -theNode4533 - -theNode4533: Con Sig - - -theNode4535 - -theNode4535: Con CNat - - -theNode4536 - -theNode4536: App theNode4536 Prod Nat (?α_19_26__9) - - -theNode4536->theNode4533 - - -L - - -theNode4536->theNode4535 - - -R - - -theNode4531 - -theNode4531: Con CNat - - -theNode4538 - -theNode4538: App theNode4538 Prod Nat (?α_19_26__9) - - -theNode4531->theNode4538 - - - -theNode4538->α_19_26__9 - - -R - - -theNode4538->theNode4536 - - -L - - -theNode4567 - -theNode4567: Con CSucc - - -theNode4569 - -theNode4569: Con CSucc - - -theNode4571 - -theNode4571: Con CZero - - -theNode4572 - -theNode4572: App theNode4572 Succ Zero - - -theNode4572->theNode4569 - - -L - - -theNode4572->theNode4571 - - -R - - -theNode4573 - -theNode4573: App theNode4573 Succ ((Succ Zero)) - - -theNode4573->theNode4567 - - -L - - -theNode4573->theNode4572 - - -R - - -theNode4574 - -theNode4574: App theNode4574 ?α_19_12__18 Succ ((Succ Zero)) - - -theNode4574->theNode - - -L - - -theNode4574->theNode4573 - - -R - - -theNode4577 - -theNode4577: Con Pi - - -theNode4579 - -theNode4579: Con Sig - - -theNode4581 - -theNode4581: Con CNat - - -theNode4582 - -theNode4582: App theNode4582 Prod Nat (?α_19_26__9) - - -theNode4582->theNode4579 - - -L - - -theNode4582->theNode4581 - - -R - - -theNode4584 - -theNode4584: App theNode4584 Prod Nat (?α_19_26__9) - - -theNode4584->α_19_26__9 - - -R - - -theNode4584->theNode4582 - - -L - - -theNode4585 - -theNode4585: App theNode4585 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4585->theNode4577 - - -L - - -theNode4585->theNode4584 - - -R - - -theNode4588 - -theNode4588: Con Pi - - -theNode4590 - -theNode4590: Con CNat - - -theNode4591 - -theNode4591: App theNode4591 Nat -> Prod Nat (?α_19_26__9) - - -theNode4591->theNode4588 - - -L - - -theNode4591->theNode4590 - - -R - - -theNode4594 - -theNode4594: Con Sig - - -theNode4596 - -theNode4596: Con CNat - - -theNode4597 - -theNode4597: App theNode4597 Prod Nat (?α_19_26__9) - - -theNode4597->theNode4594 - - -L - - -theNode4597->theNode4596 - - -R - - -theNode4599 - -theNode4599: App theNode4599 Prod Nat (?α_19_26__9) - - -theNode4599->α_19_26__9 - - -R - - -theNode4599->theNode4597 - - -L - - -theNode4601 - -theNode4601: BoundVar arg4592 - - -theNode4602 - -theNode4602: Lam theNode4602  arg . Prod Nat (?α_19_26__9) - - -theNode4602->theNode4599 - - -R - - -theNode4602->theNode4601 - - -L - - -theNode4603 - -theNode4603: App theNode4603 Nat -> Prod Nat (?α_19_26__9) - - -theNode4603->theNode4591 - - -L - - -theNode4603->theNode4602 - - -R - - -theNode4605 - -theNode4605: BoundVar arg4586 - - -theNode4606 - -theNode4606: Lam theNode4606  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode4606->theNode4603 - - -R - - -theNode4606->theNode4605 - - -L - - -theNode4575 - -theNode4575: Elim theNode4575 ?α_19_12__18 Succ ((Succ Zero)) - - -theNode4575->α_19_12__18 - - -L - - -theNode4575->theNode4574 - - -R - - -theNode4607 - -theNode4607: App theNode4607 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4575->theNode4607 - - - -theNode4607->theNode4585 - - -L - - -theNode4607->theNode4606 - - -R - - -theNode4623 - -theNode4623: Con Pi - - -theNode4625 - -theNode4625: Con CNat - - -theNode4626 - -theNode4626: App theNode4626 Nat -> Prod Nat (?α_19_26__9) - - -theNode4626->theNode4623 - - -L - - -theNode4626->theNode4625 - - -R - - -theNode4629 - -theNode4629: Con Sig - - -theNode4631 - -theNode4631: Con CNat - - -theNode4632 - -theNode4632: App theNode4632 Prod Nat (?α_19_26__9) - - -theNode4632->theNode4629 - - -L - - -theNode4632->theNode4631 - - -R - - -theNode4634 - -theNode4634: App theNode4634 Prod Nat (?α_19_26__9) - - -theNode4634->α_19_26__9 - - -R - - -theNode4634->theNode4632 - - -L - - -theNode4636 - -theNode4636: BoundVar arg4627 - - -theNode4637 - -theNode4637: Lam theNode4637  arg . Prod Nat (?α_19_26__9) - - -theNode4637->theNode4634 - - -R - - -theNode4637->theNode4636 - - -L - - -theNode4638 - -theNode4638: App theNode4638 Nat -> Prod Nat (?α_19_26__9) - - -theNode4638->theNode4626 - - -L - - -theNode4638->theNode4637 - - -R - - -theNode4640 - -theNode4640: BoundVar arg4621 - - -theNode4642 - -theNode4642: App theNode4642 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4648 - -theNode4648: App theNode4648 ?α_19_31__24 -> (?α_19_12__25) - - -theNode4642->theNode4648 - - - -theNode4620 - -theNode4620: App theNode4620 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode4642->theNode4620 - - -L - - -theNode4641 - -theNode4641: Lam theNode4641  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode4642->theNode4641 - - -R - - -theNode4646 - -theNode4646: App theNode4646 ?α_19_31__24 -> (?α_19_12__25) - - -theNode4648->theNode4646 - - -L - - -α_19_12__25 - -α_19_12__25: Meta α_19_12__25 - - -theNode4648->α_19_12__25 - - -R - - -theNode4612 - -theNode4612: Con Pi - - -theNode4620->theNode4612 - - -L - - -theNode4619 - -theNode4619: App theNode4619 Prod Nat (?α_19_26__9) - - -theNode4620->theNode4619 - - -R - - -theNode4644 - -theNode4644: Con Pi - - -theNode4646->theNode4644 - - -L - - -α_19_31__24 - -α_19_31__24: Meta α_19_31__24 - - -theNode4646->α_19_31__24 - - -R - - -theNode4724 - -theNode4724: App theNode4724 Prod Nat (?α_19_26__9) - - -α_19_31__24->theNode4724 - - - -theNode6182 - -theNode6182: App theNode6182 Prod Nat (?α_19_26__9) - - -α_19_31__24->theNode6182 - - - -theNode5433 - -theNode5433: Lam theNode5433  arg . ?x4882 (fst) arg (snd) arg - - -α_19_12__25->theNode5433 - - - -theNode5455 - -theNode5455: Lam theNode5455  arg . ?x4882 (fst) arg (snd) arg - - -α_19_12__25->theNode5455 - - - -theNode5422 - -theNode5422: BoundVar arg5419 - - -theNode5423 - -theNode5423: Elim theNode5423 (fst) arg5419 - - -theNode5423->theNode - - -R - - -theNode5423->theNode5422 - - -L - - -theNode5424 - -theNode5424: App theNode5424 ?x4882 (fst) arg5419 (snd) arg5419 - - -theNode5424->theNode - - -L - - -theNode5424->theNode5423 - - -R - - -theNode5425 - -theNode5425: Elim theNode5425 ?x4882 (fst) arg5419 (snd) arg5419 - - -theNode5425->theNode5424 - - -R - - -x4882 - -x4882: Meta x4882 - - -theNode5425->x4882 - - -L - - -theNode5427 - -theNode5427: BoundVar arg5419 - - -theNode5428 - -theNode5428: Elim theNode5428 (snd) arg5419 - - -theNode5428->theNode - - -R - - -theNode5428->theNode5427 - - -L - - -theNode5429 - -theNode5429: App theNode5429 ?x4882 (fst) arg5419 (snd) arg5419 - - -theNode5429->theNode - - -L - - -theNode5429->theNode5428 - - -R - - -theNode5430 - -theNode5430: Elim theNode5430 ?x4882 (fst) arg5419 (snd) arg5419 - - -theNode5430->theNode5425 - - -L - - -theNode5430->theNode5429 - - -R - - -theNode5432 - -theNode5432: BoundVar arg5419 - - -theNode5896 - -theNode5896: Lam theNode5896  arg arg1 . Nat -> Prod Nat (?α_19_26__9) - - -x4882->theNode5896 - - - -theNode5444 - -theNode5444: BoundVar arg5441 - - -theNode5445 - -theNode5445: Elim theNode5445 (fst) arg5441 - - -theNode5445->theNode - - -R - - -theNode5445->theNode5444 - - -L - - -theNode5446 - -theNode5446: App theNode5446 ?x4882 (fst) arg5441 (snd) arg5441 - - -theNode5446->theNode - - -L - - -theNode5446->theNode5445 - - -R - - -theNode5447 - -theNode5447: Elim theNode5447 ?x4882 (fst) arg5441 (snd) arg5441 - - -theNode5447->x4882 - - -L - - -theNode5447->theNode5446 - - -R - - -theNode5449 - -theNode5449: BoundVar arg5441 - - -theNode5450 - -theNode5450: Elim theNode5450 (snd) arg5441 - - -theNode5450->theNode - - -R - - -theNode5450->theNode5449 - - -L - - -theNode5451 - -theNode5451: App theNode5451 ?x4882 (fst) arg5441 (snd) arg5441 - - -theNode5451->theNode - - -L - - -theNode5451->theNode5450 - - -R - - -theNode5452 - -theNode5452: Elim theNode5452 ?x4882 (fst) arg5441 (snd) arg5441 - - -theNode5452->theNode5447 - - -L - - -theNode5452->theNode5451 - - -R - - -theNode5454 - -theNode5454: BoundVar arg5441 - - -theNode5464 - -theNode5464: Con Pi - - -theNode5466 - -theNode5466: Con CNat - - -theNode5467 - -theNode5467: App theNode5467 Nat -> Prod Nat (?α_19_26__9) - - -theNode5467->theNode5464 - - -L - - -theNode5467->theNode5466 - - -R - - -theNode5470 - -theNode5470: Con Sig - - -theNode5472 - -theNode5472: Con CNat - - -theNode5473 - -theNode5473: App theNode5473 Prod Nat (?α_19_26__9) - - -theNode5473->theNode5470 - - -L - - -theNode5473->theNode5472 - - -R - - -theNode5475 - -theNode5475: App theNode5475 Prod Nat (?α_19_26__9) - - -theNode5475->α_19_26__9 - - -R - - -theNode5475->theNode5473 - - -L - - -theNode5477 - -theNode5477: BoundVar arg5468 - - -theNode5478 - -theNode5478: Lam theNode5478  arg . Prod Nat (?α_19_26__9) - - -theNode5478->theNode5475 - - -R - - -theNode5478->theNode5477 - - -L - - -theNode5479 - -theNode5479: App theNode5479 Nat -> Prod Nat (?α_19_26__9) - - -theNode5479->theNode5467 - - -L - - -theNode5479->theNode5478 - - -R - - -theNode5481 - -theNode5481: BoundVar arg5462 - - -theNode5486 - -theNode5486: BoundVar arg5483 - - -theNode5487 - -theNode5487: Elim theNode5487 (fst) arg5483 - - -theNode5487->theNode - - -R - - -theNode5487->theNode5486 - - -L - - -theNode5488 - -theNode5488: App theNode5488 ?x4882 (fst) arg5483 (snd) arg5483 - - -theNode5488->theNode - - -L - - -theNode5488->theNode5487 - - -R - - -theNode5489 - -theNode5489: Elim theNode5489 ?x4882 (fst) arg5483 (snd) arg5483 - - -theNode5489->x4882 - - -L - - -theNode5489->theNode5488 - - -R - - -theNode5491 - -theNode5491: BoundVar arg5483 - - -theNode5492 - -theNode5492: Elim theNode5492 (snd) arg5483 - - -theNode5492->theNode - - -R - - -theNode5492->theNode5491 - - -L - - -theNode5493 - -theNode5493: App theNode5493 ?x4882 (fst) arg5483 (snd) arg5483 - - -theNode5493->theNode - - -L - - -theNode5493->theNode5492 - - -R - - -theNode5494 - -theNode5494: Elim theNode5494 ?x4882 (fst) arg5483 (snd) arg5483 - - -theNode5494->theNode5489 - - -L - - -theNode5494->theNode5493 - - -R - - -theNode5496 - -theNode5496: BoundVar arg5483 - - -theNode5482 - -theNode5482: Lam theNode5482  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode5482->theNode5479 - - -R - - -theNode5482->theNode5481 - - -L - - -theNode5497 - -theNode5497: Lam theNode5497  arg . ?x4882 (fst) arg (snd) arg - - -theNode5482->theNode5497 - - - -theNode5497->theNode5494 - - -R - - -theNode5497->theNode5496 - - -L - - -theNode5673 - -theNode5673: Con Pi - - -theNode5675 - -theNode5675: Con CNat - - -theNode5676 - -theNode5676: App theNode5676 Nat -> Prod Nat (?α_19_26__9) - - -theNode5676->theNode5673 - - -L - - -theNode5676->theNode5675 - - -R - - -theNode5679 - -theNode5679: Con Sig - - -theNode5681 - -theNode5681: Con CNat - - -theNode5682 - -theNode5682: App theNode5682 Prod Nat (?α_19_26__9) - - -theNode5682->theNode5679 - - -L - - -theNode5682->theNode5681 - - -R - - -theNode5684 - -theNode5684: App theNode5684 Prod Nat (?α_19_26__9) - - -theNode5684->α_19_26__9 - - -R - - -theNode5684->theNode5682 - - -L - - -theNode5686 - -theNode5686: BoundVar arg5677 - - -theNode5687 - -theNode5687: Lam theNode5687  arg . Prod Nat (?α_19_26__9) - - -theNode5687->theNode5684 - - -R - - -theNode5687->theNode5686 - - -L - - -theNode5691 - -theNode5691: BoundVar x5669 - - -theNode5692 - -theNode5692: App theNode5692 ?x4882 x5669 x5670 - - -theNode5692->theNode - - -L - - -theNode5692->theNode5691 - - -R - - -theNode5693 - -theNode5693: Elim theNode5693 ?x4882 x5669 x5670 - - -theNode5693->x4882 - - -L - - -theNode5693->theNode5692 - - -R - - -theNode5695 - -theNode5695: BoundVar x5670 - - -theNode5696 - -theNode5696: App theNode5696 ?x4882 x5669 x5670 - - -theNode5696->theNode - - -L - - -theNode5696->theNode5695 - - -R - - -theNode5688 - -theNode5688: App theNode5688 Nat -> Prod Nat (?α_19_26__9) - - -theNode5688->theNode5676 - - -L - - -theNode5688->theNode5687 - - -R - - -theNode5697 - -theNode5697: Elim theNode5697 ?x4882 x5669 x5670 - - -theNode5688->theNode5697 - - - -theNode5697->theNode5693 - - -L - - -theNode5697->theNode5696 - - -R - - -theNode5875 - -theNode5875: Con Pi - - -theNode5877 - -theNode5877: Con CNat - - -theNode5878 - -theNode5878: App theNode5878 Nat -> Prod Nat (?α_19_26__9) - - -theNode5878->theNode5875 - - -L - - -theNode5878->theNode5877 - - -R - - -theNode5881 - -theNode5881: Con Sig - - -theNode5883 - -theNode5883: Con CNat - - -theNode5884 - -theNode5884: App theNode5884 Prod Nat (?α_19_26__9) - - -theNode5884->theNode5881 - - -L - - -theNode5884->theNode5883 - - -R - - -theNode5886 - -theNode5886: App theNode5886 Prod Nat (?α_19_26__9) - - -theNode5886->α_19_26__9 - - -R - - -theNode5886->theNode5884 - - -L - - -theNode5888 - -theNode5888: BoundVar arg5879 - - -theNode5889 - -theNode5889: Lam theNode5889  arg . Prod Nat (?α_19_26__9) - - -theNode5889->theNode5886 - - -R - - -theNode5889->theNode5888 - - -L - - -theNode5890 - -theNode5890: App theNode5890 Nat -> Prod Nat (?α_19_26__9) - - -theNode5890->theNode5878 - - -L - - -theNode5890->theNode5889 - - -R - - -theNode5892 - -theNode5892: BoundVar arg5873 - - -theNode5893 - -theNode5893: Lam theNode5893  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode5893->theNode5890 - - -R - - -theNode5893->theNode5892 - - -L - - -theNode5895 - -theNode5895: BoundVar arg5872 - - -theNode5896->theNode5893 - - -R - - -theNode5896->theNode5895 - - -L - - -theNode6065 - -theNode6065: BoundVar arg6062 - - -theNode6066 - -theNode6066: Elim theNode6066 (fst) arg6062 - - -theNode6066->theNode - - -R - - -theNode6066->theNode6065 - - -L - - -theNode6067 - -theNode6067: App theNode6067 ?x4882 (fst) arg6062 (snd) arg6062 - - -theNode6067->theNode - - -L - - -theNode6067->theNode6066 - - -R - - -theNode6068 - -theNode6068: Elim theNode6068 ?x4882 (fst) arg6062 (snd) arg6062 - - -theNode6068->x4882 - - -L - - -theNode6068->theNode6067 - - -R - - -theNode6070 - -theNode6070: BoundVar arg6062 - - -theNode6071 - -theNode6071: Elim theNode6071 (snd) arg6062 - - -theNode6071->theNode - - -R - - -theNode6071->theNode6070 - - -L - - -theNode6072 - -theNode6072: App theNode6072 ?x4882 (fst) arg6062 (snd) arg6062 - - -theNode6072->theNode - - -L - - -theNode6072->theNode6071 - - -R - - -theNode6073 - -theNode6073: Elim theNode6073 ?x4882 (fst) arg6062 (snd) arg6062 - - -theNode6073->theNode6068 - - -L - - -theNode6073->theNode6072 - - -R - - -theNode6075 - -theNode6075: BoundVar arg6062 - - -theNode6079 - -theNode6079: Con Pi - - -theNode6081 - -theNode6081: Con CNat - - -theNode6082 - -theNode6082: App theNode6082 Nat -> Prod Nat (?α_19_26__9) - - -theNode6082->theNode6079 - - -L - - -theNode6082->theNode6081 - - -R - - -theNode6085 - -theNode6085: Con Sig - - -theNode6087 - -theNode6087: Con CNat - - -theNode6088 - -theNode6088: App theNode6088 Prod Nat (?α_19_26__9) - - -theNode6088->theNode6085 - - -L - - -theNode6088->theNode6087 - - -R - - -theNode6090 - -theNode6090: App theNode6090 Prod Nat (?α_19_26__9) - - -theNode6090->α_19_26__9 - - -R - - -theNode6090->theNode6088 - - -L - - -theNode6092 - -theNode6092: BoundVar arg6083 - - -theNode6093 - -theNode6093: Lam theNode6093  arg . Prod Nat (?α_19_26__9) - - -theNode6093->theNode6090 - - -R - - -theNode6093->theNode6092 - - -L - - -theNode6094 - -theNode6094: App theNode6094 Nat -> Prod Nat (?α_19_26__9) - - -theNode6094->theNode6082 - - -L - - -theNode6094->theNode6093 - - -R - - -theNode6096 - -theNode6096: BoundVar arg6077 - - -theNode6076 - -theNode6076: Lam theNode6076  arg . ?x4882 (fst) arg (snd) arg - - -theNode6076->theNode6073 - - -R - - -theNode6076->theNode6075 - - -L - - -theNode6097 - -theNode6097: Lam theNode6097  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode6076->theNode6097 - - - -theNode6097->theNode6094 - - -R - - -theNode6097->theNode6096 - - -L - - -theNode6102 - -theNode6102: BoundVar arg6099 - - -theNode6103 - -theNode6103: Elim theNode6103 (fst) arg6099 - - -theNode6103->theNode - - -R - - -theNode6103->theNode6102 - - -L - - -theNode6104 - -theNode6104: App theNode6104 ?x4882 (fst) arg6099 (snd) arg6099 - - -theNode6104->theNode - - -L - - -theNode6104->theNode6103 - - -R - - -theNode6105 - -theNode6105: Elim theNode6105 ?x4882 (fst) arg6099 (snd) arg6099 - - -theNode6105->x4882 - - -L - - -theNode6105->theNode6104 - - -R - - -theNode6107 - -theNode6107: BoundVar arg6099 - - -theNode6108 - -theNode6108: Elim theNode6108 (snd) arg6099 - - -theNode6108->theNode - - -R - - -theNode6108->theNode6107 - - -L - - -theNode6109 - -theNode6109: App theNode6109 ?x4882 (fst) arg6099 (snd) arg6099 - - -theNode6109->theNode - - -L - - -theNode6109->theNode6108 - - -R - - -theNode6110 - -theNode6110: Elim theNode6110 ?x4882 (fst) arg6099 (snd) arg6099 - - -theNode6110->theNode6105 - - -L - - -theNode6110->theNode6109 - - -R - - -theNode6112 - -theNode6112: BoundVar arg6099 - - -theNode6116 - -theNode6116: Con Pi - - -theNode6118 - -theNode6118: Con CNat - - -theNode6119 - -theNode6119: App theNode6119 Nat -> Prod Nat (?α_19_26__9) - - -theNode6119->theNode6116 - - -L - - -theNode6119->theNode6118 - - -R - - -theNode6122 - -theNode6122: Con Sig - - -theNode6124 - -theNode6124: Con CNat - - -theNode6125 - -theNode6125: App theNode6125 Prod Nat (?α_19_26__9) - - -theNode6125->theNode6122 - - -L - - -theNode6125->theNode6124 - - -R - - -theNode6127 - -theNode6127: App theNode6127 Prod Nat (?α_19_26__9) - - -theNode6127->α_19_26__9 - - -R - - -theNode6127->theNode6125 - - -L - - -theNode6129 - -theNode6129: BoundVar arg6120 - - -theNode6130 - -theNode6130: Lam theNode6130  arg . Prod Nat (?α_19_26__9) - - -theNode6130->theNode6127 - - -R - - -theNode6130->theNode6129 - - -L - - -theNode6131 - -theNode6131: App theNode6131 Nat -> Prod Nat (?α_19_26__9) - - -theNode6131->theNode6119 - - -L - - -theNode6131->theNode6130 - - -R - - -theNode6133 - -theNode6133: BoundVar arg6114 - - -theNode6113 - -theNode6113: Lam theNode6113  arg . ?x4882 (fst) arg (snd) arg - - -theNode6113->theNode6110 - - -R - - -theNode6113->theNode6112 - - -L - - -theNode6134 - -theNode6134: Lam theNode6134  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode6113->theNode6134 - - - -theNode6134->theNode6131 - - -R - - -theNode6134->theNode6133 - - -L - - -theNode6154 - -theNode6154: Con Pi - - -theNode6156 - -theNode6156: Con CNat - - -theNode6157 - -theNode6157: App theNode6157 Nat -> Prod Nat (?α_19_26__9) - - -theNode6157->theNode6154 - - -L - - -theNode6157->theNode6156 - - -R - - -theNode6160 - -theNode6160: Con Sig - - -theNode6162 - -theNode6162: Con CNat - - -theNode6163 - -theNode6163: App theNode6163 Prod Nat (?α_19_26__9) - - -theNode6163->theNode6160 - - -L - - -theNode6163->theNode6162 - - -R - - -theNode6165 - -theNode6165: App theNode6165 Prod Nat (?α_19_26__9) - - -theNode6165->α_19_26__9 - - -R - - -theNode6165->theNode6163 - - -L - - -theNode6167 - -theNode6167: BoundVar arg6158 - - -theNode6168 - -theNode6168: Lam theNode6168  arg . Prod Nat (?α_19_26__9) - - -theNode6168->theNode6165 - - -R - - -theNode6168->theNode6167 - - -L - - -theNode6169 - -theNode6169: App theNode6169 Nat -> Prod Nat (?α_19_26__9) - - -theNode6169->theNode6157 - - -L - - -theNode6169->theNode6168 - - -R - - -theNode6171 - -theNode6171: BoundVar arg6152 - - -theNode6141 - -theNode6141: App theNode6141 ?α_19_31__24 -> (?α_19_12__25) - - -theNode6141->α_19_12__25 - - -R - - -theNode6173 - -theNode6173: App theNode6173 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode6141->theNode6173 - - - -theNode6139 - -theNode6139: App theNode6139 ?α_19_31__24 -> (?α_19_12__25) - - -theNode6141->theNode6139 - - -L - - -theNode6151 - -theNode6151: App theNode6151 (Prod Nat (?α_19_26__9)) -> Nat -> Prod Nat (?α_19_26__9) - - -theNode6173->theNode6151 - - -L - - -theNode6172 - -theNode6172: Lam theNode6172  arg . Nat -> Prod Nat (?α_19_26__9) - - -theNode6173->theNode6172 - - -R - - -theNode6139->α_19_31__24 - - -R - - -theNode6137 - -theNode6137: Con Pi - - -theNode6139->theNode6137 - - -L - - -theNode6143 - -theNode6143: Con Pi - - -theNode6151->theNode6143 - - -L - - -theNode6150 - -theNode6150: App theNode6150 Prod Nat (?α_19_26__9) - - -theNode6151->theNode6150 - - -R - - -theNode6172->theNode6169 - - -R - - -theNode6172->theNode6171 - - -L - - -theNode4641->theNode4638 - - -R - - -theNode4641->theNode4640 - - -L - - -theNode5433->theNode5430 - - -R - - -theNode5433->theNode5432 - - -L - - -theNode5455->theNode5452 - - -R - - -theNode5455->theNode5454 - - -L - - -theNode6150->α_19_26__9 - - -R - - -theNode6148 - -theNode6148: App theNode6148 Prod Nat (?α_19_26__9) - - -theNode6150->theNode6148 - - -L - - -theNode4666 - -theNode4666: App theNode4666 Prod Nat (?α_19_26__9) - - -theNode4666->α_19_26__9 - - -R - - -theNode4666->α_19_31__24 - - - -theNode4664 - -theNode4664: App theNode4664 Prod Nat (?α_19_26__9) - - -theNode4666->theNode4664 - - -L - - -theNode4619->α_19_26__9 - - -R - - -theNode4617 - -theNode4617: App theNode4617 Prod Nat (?α_19_26__9) - - -theNode4619->theNode4617 - - -L - - -theNode4724->α_19_26__9 - - -R - - -theNode4722 - -theNode4722: App theNode4722 Prod Nat (?α_19_26__9) - - -theNode4724->theNode4722 - - -L - - -theNode6182->α_19_26__9 - - -R - - -theNode6180 - -theNode6180: App theNode6180 Prod Nat (?α_19_26__9) - - -theNode6182->theNode6180 - - -L - - -theNode4614 - -theNode4614: Con Sig - - -theNode4617->theNode4614 - - -L - - -theNode4616 - -theNode4616: Con CNat - - -theNode4617->theNode4616 - - -R - - -theNode4661 - -theNode4661: Con Sig - - -theNode4664->theNode4661 - - -L - - -theNode4663 - -theNode4663: Con CNat - - -theNode4664->theNode4663 - - -R - - -theNode4719 - -theNode4719: Con Sig - - -theNode4722->theNode4719 - - -L - - -theNode4721 - -theNode4721: Con CNat - - -theNode4722->theNode4721 - - -R - - -theNode6145 - -theNode6145: Con Sig - - -theNode6148->theNode6145 - - -L - - -theNode6147 - -theNode6147: Con CNat - - -theNode6148->theNode6147 - - -R - - -theNode6177 - -theNode6177: Con Sig - - -theNode6180->theNode6177 - - -L - - -theNode6179 - -theNode6179: Con CNat - - -theNode6180->theNode6179 - - -R - - -theNode6187 - -theNode6187: Con Sig - - -theNode6189 - -theNode6189: Con CNat - - -theNode6190 - -theNode6190: App theNode6190 Prod Nat (?α_19_26__9) - - -theNode6190->theNode6187 - - -L - - -theNode6190->theNode6189 - - -R - - -theNode6185 - -theNode6185: Con CNat - - -theNode6192 - -theNode6192: App theNode6192 Prod Nat (?α_19_26__9) - - -theNode6185->theNode6192 - - - -theNode6192->α_19_26__9 - - -R - - -theNode6192->theNode6190 - - -L - - -theNode6221 - -theNode6221: Con CSucc - - -theNode6223 - -theNode6223: Con CSucc - - -theNode6225 - -theNode6225: Con CSucc - - -theNode6227 - -theNode6227: Con CZero - - -theNode6228 - -theNode6228: App theNode6228 Succ Zero - - -theNode6228->theNode6225 - - -L - - -theNode6228->theNode6227 - - -R - - -theNode6229 - -theNode6229: App theNode6229 Succ ((Succ Zero)) - - -theNode6229->theNode6223 - - -L - - -theNode6229->theNode6228 - - -R - - -theNode6230 - -theNode6230: App theNode6230 Succ ((Succ ((Succ Zero)))) - - -theNode6230->theNode6221 - - -L - - -theNode6230->theNode6229 - - -R - - -theNode6231 - -theNode6231: App theNode6231 ?α_19_12__25 Succ ((Succ ((Succ Zero)))) - - -theNode6231->theNode - - -L - - -theNode6231->theNode6230 - - -R - - -theNode6234 - -theNode6234: Con Pi - - -theNode6236 - -theNode6236: Con CNat - - -theNode6237 - -theNode6237: App theNode6237 Nat -> Prod Nat (?α_19_26__9) - - -theNode6237->theNode6234 - - -L - - -theNode6237->theNode6236 - - -R - - -theNode6240 - -theNode6240: Con Sig - - -theNode6242 - -theNode6242: Con CNat - - -theNode6243 - -theNode6243: App theNode6243 Prod Nat (?α_19_26__9) - - -theNode6243->theNode6240 - - -L - - -theNode6243->theNode6242 - - -R - - -theNode6245 - -theNode6245: App theNode6245 Prod Nat (?α_19_26__9) - - -theNode6245->α_19_26__9 - - -R - - -theNode6245->theNode6243 - - -L - - -theNode6247 - -theNode6247: BoundVar arg6238 - - -theNode6248 - -theNode6248: Lam theNode6248  arg . Prod Nat (?α_19_26__9) - - -theNode6248->theNode6245 - - -R - - -theNode6248->theNode6247 - - -L - - -theNode6232 - -theNode6232: Elim theNode6232 ?α_19_12__25 Succ ((Succ ((Succ Zero)))) - - -theNode6232->α_19_12__25 - - -L - - -theNode6232->theNode6231 - - -R - - -theNode6249 - -theNode6249: App theNode6249 Nat -> Prod Nat (?α_19_26__9) - - -theNode6232->theNode6249 - - - -theNode6249->theNode6237 - - -L - - -theNode6249->theNode6248 - - -R - - -theNode6259 - -theNode6259: Con Sig - - -theNode6261 - -theNode6261: Con CNat - - -theNode6262 - -theNode6262: App theNode6262 Prod Nat (?α_19_26__9) - - -theNode6262->theNode6259 - - -L - - -theNode6262->theNode6261 - - -R - - -theNode6264 - -theNode6264: App theNode6264 Prod Nat (?α_19_26__9) - - -theNode6264->α_19_26__9 - - -R - - -theNode6264->theNode6262 - - -L - - -theNode6266 - -theNode6266: BoundVar arg6257 - - -theNode6268 - -theNode6268: App theNode6268 Nat -> Prod Nat (?α_19_26__9) - - -theNode6274 - -theNode6274: App theNode6274 ?α_19_33__32 -> (?α_19_12__33) - - -theNode6268->theNode6274 - - - -theNode6256 - -theNode6256: App theNode6256 Nat -> Prod Nat (?α_19_26__9) - - -theNode6268->theNode6256 - - -L - - -theNode6267 - -theNode6267: Lam theNode6267  arg . Prod Nat (?α_19_26__9) - - -theNode6268->theNode6267 - - -R - - -theNode6272 - -theNode6272: App theNode6272 ?α_19_33__32 -> (?α_19_12__33) - - -theNode6274->theNode6272 - - -L - - -α_19_12__33 - -α_19_12__33: Meta α_19_12__33 - - -theNode6274->α_19_12__33 - - -R - - -theNode6253 - -theNode6253: Con Pi - - -theNode6256->theNode6253 - - -L - - -theNode6255 - -theNode6255: Con CNat - - -theNode6256->theNode6255 - - -R - - -theNode6270 - -theNode6270: Con Pi - - -theNode6272->theNode6270 - - -L - - -α_19_33__32 - -α_19_33__32: Meta α_19_33__32 - - -theNode6272->α_19_33__32 - - -R - - -theNode6293 - -theNode6293: Con CNat - - -α_19_33__32->theNode6293 - - - -theNode6578 - -theNode6578: Con CNat - - -α_19_33__32->theNode6578 - - - -theNode6302 - -theNode6302: Con Sig - - -theNode6304 - -theNode6304: Con CNat - - -theNode6305 - -theNode6305: App theNode6305 Prod Nat (?α_19_26__9) - - -theNode6305->theNode6302 - - -L - - -theNode6305->theNode6304 - - -R - - -theNode6307 - -theNode6307: App theNode6307 Prod Nat (?α_19_26__9) - - -theNode6307->α_19_26__9 - - -R - - -theNode6307->theNode6305 - - -L - - -theNode6309 - -theNode6309: BoundVar arg6300 - - -theNode6437 - -theNode6437: Lam theNode6437  arg . Prod Nat (?α_19_26__9) - - -α_19_12__33->theNode6437 - - - -theNode6550 - -theNode6550: Lam theNode6550  arg . Prod Nat (?α_19_26__9) - - -α_19_12__33->theNode6550 - - - -theNode6339 - -theNode6339: Con Sig - - -theNode6341 - -theNode6341: Con CNat - - -theNode6342 - -theNode6342: App theNode6342 Prod Nat (?α_19_26__9) - - -theNode6342->theNode6339 - - -L - - -theNode6342->theNode6341 - - -R - - -theNode6347 - -theNode6347: BoundVar x6337 - - -theNode6348 - -theNode6348: App theNode6348 ?α_19_12__33 x6337 - - -theNode6348->theNode - - -L - - -theNode6348->theNode6347 - - -R - - -theNode6344 - -theNode6344: App theNode6344 Prod Nat (?α_19_26__9) - - -theNode6344->α_19_26__9 - - -R - - -theNode6344->theNode6342 - - -L - - -theNode6349 - -theNode6349: Elim theNode6349 ?α_19_12__33 x6337 - - -theNode6344->theNode6349 - - - -theNode6349->α_19_12__33 - - -L - - -theNode6349->theNode6348 - - -R - - -theNode6429 - -theNode6429: Con Sig - - -theNode6431 - -theNode6431: Con CNat - - -theNode6432 - -theNode6432: App theNode6432 Prod Nat (?α_19_26__9) - - -theNode6432->theNode6429 - - -L - - -theNode6432->theNode6431 - - -R - - -theNode6434 - -theNode6434: App theNode6434 Prod Nat (?α_19_26__9) - - -theNode6434->α_19_26__9 - - -R - - -theNode6434->theNode6432 - - -L - - -theNode6436 - -theNode6436: BoundVar arg6427 - - -theNode6542 - -theNode6542: Con Sig - - -theNode6544 - -theNode6544: Con CNat - - -theNode6545 - -theNode6545: App theNode6545 Prod Nat (?α_19_26__9) - - -theNode6545->theNode6542 - - -L - - -theNode6545->theNode6544 - - -R - - -theNode6547 - -theNode6547: App theNode6547 Prod Nat (?α_19_26__9) - - -theNode6547->α_19_26__9 - - -R - - -theNode6547->theNode6545 - - -L - - -theNode6549 - -theNode6549: BoundVar arg6540 - - -theNode6565 - -theNode6565: Con Sig - - -theNode6567 - -theNode6567: Con CNat - - -theNode6568 - -theNode6568: App theNode6568 Prod Nat (?α_19_26__9) - - -theNode6568->theNode6565 - - -L - - -theNode6568->theNode6567 - - -R - - -theNode6570 - -theNode6570: App theNode6570 Prod Nat (?α_19_26__9) - - -theNode6570->α_19_26__9 - - -R - - -theNode6570->theNode6568 - - -L - - -theNode6572 - -theNode6572: BoundVar arg6563 - - -theNode6557 - -theNode6557: App theNode6557 ?α_19_33__32 -> (?α_19_12__33) - - -theNode6557->α_19_12__33 - - -R - - -theNode6574 - -theNode6574: App theNode6574 Nat -> Prod Nat (?α_19_26__9) - - -theNode6557->theNode6574 - - - -theNode6555 - -theNode6555: App theNode6555 ?α_19_33__32 -> (?α_19_12__33) - - -theNode6557->theNode6555 - - -L - - -theNode6562 - -theNode6562: App theNode6562 Nat -> Prod Nat (?α_19_26__9) - - -theNode6574->theNode6562 - - -L - - -theNode6573 - -theNode6573: Lam theNode6573  arg . Prod Nat (?α_19_26__9) - - -theNode6574->theNode6573 - - -R - - -theNode6555->α_19_33__32 - - -R - - -theNode6553 - -theNode6553: Con Pi - - -theNode6555->theNode6553 - - -L - - -theNode6559 - -theNode6559: Con Pi - - -theNode6562->theNode6559 - - -L - - -theNode6561 - -theNode6561: Con CNat - - -theNode6562->theNode6561 - - -R - - -theNode6573->theNode6570 - - -R - - -theNode6573->theNode6572 - - -L - - -theNode6310 - -theNode6310: Lam theNode6310  arg . Prod Nat (?α_19_26__9) - - -theNode6310->theNode6307 - - -R - - -theNode6310->theNode6309 - - -L - - -theNode6310->α_19_12__33 - - - -theNode6267->theNode6264 - - -R - - -theNode6267->theNode6266 - - -L - - -theNode6437->theNode6434 - - -R - - -theNode6437->theNode6436 - - -L - - -theNode6550->theNode6547 - - -R - - -theNode6550->theNode6549 - - -L - - -theNode6286 - -theNode6286: Con CNat - - -theNode6286->α_19_33__32 - - - -theNode6582 - -theNode6582: Con CZero - - -theNode6583 - -theNode6583: App theNode6583 ?α_19_12__33 Zero - - -theNode6583->theNode - - -L - - -theNode6583->theNode6582 - - -R - - -theNode6586 - -theNode6586: Con Sig - - -theNode6588 - -theNode6588: Con CNat - - -theNode6589 - -theNode6589: App theNode6589 Prod Nat (?α_19_26__9) - - -theNode6589->theNode6586 - - -L - - -theNode6589->theNode6588 - - -R - - -theNode6584 - -theNode6584: Elim theNode6584 ?α_19_12__33 Zero - - -theNode6584->α_19_12__33 - - -L - - -theNode6584->theNode6583 - - -R - - -theNode6591 - -theNode6591: App theNode6591 Prod Nat (?α_19_26__9) - - -theNode6584->theNode6591 - - - -theNode6591->α_19_26__9 - - -R - - -theNode6591->theNode6589 - - -L - - -topLevel37 - -topLevel37: Meta topLevel37 - - -theNode6657 - -theNode6657: App theNode6657 Prod Nat (?α_19_26__9) - - -topLevel37->theNode6657 - - - -theNode6599 - -theNode6599: App theNode6599 Prod Nat (?α_19_26__9) - - -theNode6599->α_19_26__9 - - -R - - -theNode6599->topLevel37 - - - -theNode6597 - -theNode6597: App theNode6597 Prod Nat (?α_19_26__9) - - -theNode6599->theNode6597 - - -L - - -theNode6657->α_19_26__9 - - -R - - -theNode6655 - -theNode6655: App theNode6655 Prod Nat (?α_19_26__9) - - -theNode6657->theNode6655 - - -L - - -theNode6594 - -theNode6594: Con Sig - - -theNode6597->theNode6594 - - -L - - -theNode6596 - -theNode6596: Con CNat - - -theNode6597->theNode6596 - - -R - - -theNode6652 - -theNode6652: Con Sig - - -theNode6655->theNode6652 - - -L - - -theNode6654 - -theNode6654: Con CNat - - -theNode6655->theNode6654 - - -R - - - diff --git a/prelude.lp b/prelude.lp deleted file mode 100644 index f0966e7..0000000 --- a/prelude.lp +++ /dev/null @@ -1,376 +0,0 @@ - --- identity and const -let id = (\ a x -> x) :: forall (a :: *) . a -> a -let const = (\ a b x y -> x) :: forall (a :: *) (b :: *) . a -> b -> a - --- addition of natural numbers -let plus = - natElim - ( \ _ -> Nat -> Nat ) -- motive - ( \ n -> n ) -- case for Zero - ( \ p rec n -> Succ (rec n) ) -- case for Succ - --- predecessor, mapping 0 to 0 -let pred = - natElim - ( \ _ -> Nat ) - Zero - ( \ n' _rec -> n' ) - --- a simpler elimination scheme for natural numbers -let natFold = - ( \ m mz ms -> natElim - ( \ _ -> m ) - mz - ( \ n' rec -> ms rec ) ) - :: forall (m :: *) . m -> (m -> m) -> Nat -> m - --- an eliminator for natural numbers that has special --- cases for 0 and 1 -let nat1Elim = - ( \ m m0 m1 ms -> natElim m m0 - (\ p rec -> natElim (\ n -> m (Succ n)) m1 ms p) ) - :: forall (m :: Nat -> *) . m 0 -> m 1 -> - (forall n :: Nat . m (Succ n) -> m (Succ (Succ n))) -> - forall (n :: Nat) . m n - - --- an eliminator for natural numbers that has special --- cases for 0, 1 and 2 -let nat2Elim = - ( \ m m0 m1 m2 ms -> nat1Elim m m0 m1 - (\ p rec -> natElim (\ n -> m (Succ (Succ n))) m2 ms p) ) - :: forall (m :: Nat -> *) . m 0 -> m 1 -> m 2 -> - (forall n :: Nat . m (Succ (Succ n)) -> m (Succ (Succ (Succ n)))) -> - forall (n :: Nat) . m n - - --- increment by one -let inc = natFold Nat (Succ Zero) Succ - - - -let myFinElim = finElim - --- embed Fin into Nat -let finNat = finElim (\ _ _ -> Nat) - (\ _ -> Zero) - (\ _ _ rec -> Succ rec) - --- unit type -let Unit = Fin 1 --- constructor -let U = FZero 0 - --- eliminator -let unitElim = - ( \ m mu -> finElim ( nat1Elim (\ n -> Fin n -> *) - (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) ) - ( natElim (\ n -> natElim (\ n -> Fin (Succ n) -> *) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FZero n)) - mu - (\ _ _ -> U) ) - ( \ n f _ -> finElim (\ n f -> natElim (\ n -> Fin (Succ n) -> *) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc n f)) - (\ _ -> U) - (\ _ _ _ -> U) - n f ) - 1 ) - :: forall (m :: Unit -> *) . m U -> forall (u :: Unit) . m u - --- empty type -let Void = Fin 0 - --- eliminator -let voidElim = - ( \ m -> finElim (natElim (\ n -> Fin n -> *) - (\ x -> m x) - (\ _ _ _ -> Unit)) - (\ _ -> U) - (\ _ _ _ -> U) - 0 ) - :: forall (m :: Void -> *) (v :: Void) . m v - --- type of booleans -let Bool = Fin 2 - --- constructors -let False = FZero 1 -let True = FSucc 1 (FZero 0) - --- eliminator -let boolElim = - ( \ m mf mt -> finElim ( nat2Elim (\ n -> Fin n -> *) - (\ _ -> Unit) (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) ) - ( nat1Elim ( \ n -> nat1Elim (\ n -> Fin (Succ n) -> *) - (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FZero n)) - U mf (\ _ _ -> U) ) - ( \ n f _ -> finElim ( \ n f -> nat1Elim (\ n -> Fin (Succ n) -> *) - (\ _ -> Unit) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc n f) ) - ( natElim - ( \ n -> natElim - (\ n -> Fin (Succ (Succ n)) -> *) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc (Succ n) (FZero n)) ) - mt (\ _ _ -> U) ) - ( \ n f _ -> finElim - (\ n f -> natElim - (\ n -> Fin (Succ (Succ n)) -> *) - (\ x -> m x) - (\ _ _ _ -> Unit) - n (FSucc (Succ n) (FSucc n f))) - (\ _ -> U) - (\ _ _ _ -> U) - n f ) - n f ) - 2 ) - :: forall (m :: Bool -> *) . m False -> m True -> forall (b :: Bool) . m b - --- boolean not, and, or, equivalence, xor -let not = boolElim (\ _ -> Bool) True False -let and = boolElim (\ _ -> Bool -> Bool) (\ _ -> False) (id Bool) -let or = boolElim (\ _ -> Bool -> Bool) (id Bool) (\ _ -> True) -let iff = boolElim (\ _ -> Bool -> Bool) not (id Bool) -let xor = boolElim (\ _ -> Bool -> Bool) (id Bool) not - --- even, odd, isZero, isSucc -let even = natFold Bool True not -let odd = natFold Bool False not -let isZero = natFold Bool True (\ _ -> False) -let isSucc = natFold Bool False (\ _ -> True) - - - --- equality on natural numbers -let natEq = - natElim - ( \ _ -> Nat -> Bool ) - ( natElim - ( \ _ -> Bool ) - True - ( \ n' _ -> False ) ) - ( \ m' rec_m' -> natElim - ( \ _ -> Bool ) - False - ( \ n' _ -> rec_m' n' )) - --- "oh so true" -let Prop = boolElim (\ _ -> *) Void Unit - --- reflexivity of equality on natural numbers -let pNatEqRefl = - natElim - (\ n -> Prop (natEq n n)) - U - (\ n' rec -> rec) - :: forall (n :: Nat) . Prop (natEq n n) - --- alias for type-level negation -let Not = (\ a -> a -> Void) :: * -> * - --- Leibniz prinicple (look at the type signature) -let leibniz = - ( \ a b f -> eqElim a - (\ x y eq_x_y -> Eq b (f x) (f y)) - (\ x -> Refl b (f x)) ) - :: forall (a :: *) (b :: *) (f :: a -> b) (x :: a) (y :: a) . - Eq a x y -> Eq b (f x) (f y) - --- symmetry of (general) equality -let symm = - ( \ a -> eqElim a - (\ x y eq_x_y -> Eq a y x) - (\ x -> Refl a x) ) - :: forall (a :: *) (x :: a) (y :: a) . - Eq a x y -> Eq a y x - --- transitivity of (general) equality -let tran = - ( \ a x y z eq_x_y -> eqElim a - (\ x y eq_x_y -> forall (z :: a) . Eq a y z -> Eq a x z) - (\ x z eq_x_z -> eq_x_z) - x y eq_x_y z ) - :: forall (a :: *) (x :: a) (y :: a) (z :: a) . - Eq a x y -> Eq a y z -> Eq a x z - --- apply an equality proof on two types -let apply = - eqElim * (\ a b _ -> a -> b) (\ _ x -> x) - :: forall (a :: *) (b :: *) (p :: Eq * a b) . a -> b - --- proof that 1 is not 0 -let p1IsNot0 = - (\ p -> apply Unit Void - (leibniz Nat * - (natElim (\ _ -> *) Void (\ _ _ -> Unit)) - 1 0 p) - U) - :: Not (Eq Nat 1 0) - --- proof that 0 is not 1 -let p0IsNot1 = - (\ p -> p1IsNot0 (symm Nat 0 1 p)) - :: Not (Eq Nat 0 1) - --- proof that zero is not a successor -let p0IsNoSucc = - natElim - ( \ n -> Not (Eq Nat 0 (Succ n)) ) - p0IsNot1 - ( \ n' rec_n' eq_0_SSn' -> - rec_n' (leibniz Nat Nat pred Zero (Succ (Succ n')) eq_0_SSn') ) - --- generate a vector of given length from a specified element (replicate) -let replicate = - ( natElim - ( \ n -> forall (a :: *) . a -> Vec a n ) - ( \ a _ -> Nil a ) - ( \ n' rec_n' a x -> Cons a n' x (rec_n' a x) ) ) - :: forall (n :: Nat) . forall (a :: *) . a -> Vec a n - --- alternative definition of replicate -let replicate' = - (\ a n x -> natElim (Vec a) - (Nil a) - (\ n' rec_n' -> Cons a n' x rec_n') n) - :: forall (a :: *) (n :: Nat) . a -> Vec a n - --- generate a vector of given length n, containing the natural numbers smaller than n -let fromto = - natElim - ( \ n -> Vec Nat n ) - ( Nil Nat ) - ( \ n' rec_n' -> Cons Nat n' n' rec_n' ) - --- append two vectors -let append = - ( \ a -> vecElim a - (\ m _ -> forall (n :: Nat) . Vec a n -> Vec a (plus m n)) - (\ _ v -> v) - (\ m v vs rec n w -> Cons a (plus m n) v (rec n w))) - :: forall (a :: *) (m :: Nat) (v :: Vec a m) (n :: Nat) (w :: Vec a n). - Vec a (plus m n) - --- helper function for tail, see below -let tail' = - (\ a -> vecElim a ( \ m v -> forall (n :: Nat) . Eq Nat m (Succ n) -> Vec a n ) - ( \ n eq_0_SuccN -> voidElim ( \ _ -> Vec a n ) - ( p0IsNoSucc n eq_0_SuccN ) ) - ( \ m' v vs rec_m' n eq_SuccM'_SuccN -> - eqElim Nat - (\ m' n e -> Vec a m' -> Vec a n) - (\ _ v -> v) - m' n - (leibniz Nat Nat pred (Succ m') (Succ n) eq_SuccM'_SuccN) vs)) - :: forall (a :: *) (m :: Nat) . Vec a m -> forall (n :: Nat) . Eq Nat m (Succ n) -> Vec a n - --- compute the tail of a vector -let tail = - (\ a n v -> tail' a (Succ n) v n (Refl Nat (Succ n))) - :: forall (a :: *) (n :: Nat) . Vec a (Succ n) -> Vec a n - --- projection out of a vector -let at = - (\ a -> vecElim a ( \ n v -> Fin n -> a ) - ( \ f -> voidElim (\ _ -> a) f ) - ( \ n' v vs rec_n' f_SuccN' -> - finElim ( \ n _ -> Eq Nat n (Succ n') -> a ) - ( \ n e -> v ) - ( \ n f_N _ eq_SuccN_SuccN' -> - rec_n' (eqElim Nat - (\ x y e -> Fin x -> Fin y) - (\ _ f -> f) - n n' - (leibniz Nat Nat pred - (Succ n) (Succ n') eq_SuccN_SuccN') - f_N)) - (Succ n') - f_SuccN' - (Refl Nat (Succ n')))) - :: forall (a :: *) (n :: Nat) . Vec a n -> Fin n -> a - --- head of a vector -let head = - (\ a n v -> at a (Succ n) v (FZero n)) - :: forall (a :: *) (n :: Nat) . Vec a (Succ n) -> a - --- vector map -let map = - (\ a b f -> vecElim a ( \ n _ -> Vec b n ) - ( Nil b ) - ( \ n x _ rec -> Cons b n (f x) rec )) - :: forall (a :: *) (b :: *) (f :: a -> b) (n :: Nat) . Vec a n -> Vec b n - --- proofs that 0 is the neutral element of addition --- one direction is trivial by definition of plus: -let p0PlusNisN = - Refl Nat - :: forall n :: Nat . Eq Nat (plus 0 n) n - --- the other direction requires induction on N: -let pNPlus0isN = - natElim ( \ n -> Eq Nat (plus n 0) n ) - ( Refl Nat 0 ) - ( \ n' rec -> leibniz Nat Nat Succ (plus n' 0) n' rec ) - :: forall n :: Nat . Eq Nat (plus n 0) n - - --------------------------------------------------- --- Product / Sigma types proofs and utilities --------------------------------------------------- - - -let Prod = - (\s t -> exists (x :: s) . t ) - :: * -> * -> * - ---fst and snd as functions -let getFst = - (\ _ _ x -> fst x) - :: forall (s :: *) (t :: s -> *) . (exists (x :: s) . (t x)) -> s - - -let zeroes = ( 0 , 0 ) :: Prod Nat Nat - -let v1 = (fst zeroes) :: Nat - -let v2 = (snd zeroes) :: Nat - -let geq = (\ x y -> exists (z :: Nat) . Eq Nat x (plus y z) ) :: Nat -> Nat -> * - -let gt = - (\ x y -> geq x (Succ y)) - :: Nat -> Nat -> * - -let leq = (\ x y -> geq y x) :: Nat -> Nat -> * - -let lt = (\ x y -> gt y x) :: Nat -> Nat -> * - - -let geq0 = - (\n -> (n , p0PlusNisN n) ) - :: forall (n :: Nat ) . geq n 0 - -let natsAreInf = - (\n -> (Succ n, (0, symm Nat (plus (Succ n) 0) (Succ n) (pNPlus0isN (Succ n))) ) ) - :: forall (n :: Nat) . exists (m :: Nat) . gt m n - ------- We can build binary sums out of Bools and Products -let sum = - (\ s t -> exists (b :: Bool) . boolElim (\_ -> *) s t b ) - :: * -> * -> * diff --git a/preludeTypes.txt b/preludeTypes.txt deleted file mode 100644 index 2ca4573..0000000 --- a/preludeTypes.txt +++ /dev/null @@ -1,177 +0,0 @@ - --- identity and const -id :: forall (a :: *) . a -> a -const :: forall (a :: *) (b :: *) . a -> b -> a - --- addition of natural numbers -plus :: Nat -> Nat -> Nat - --- predecessor, mapping 0 to 0 -pred :: Nat -> Nat -> Nat - --- a simpler elimination scheme for natural numbers -natFold :: forall (m :: *) . m -> (m -> m) -> Nat -> m - --- an eliminator for natural numbers that has special --- cases for 0 and 1 -nat1Elim :: forall (m :: Nat -> *) . m 0 -> m 1 -> - (forall n :: Nat . m (Succ n) -> m (Succ (Succ n))) -> - forall (n :: Nat) . m n - - --- an eliminator for natural numbers that has special --- cases for 0, 1 and 2 -nat2Elim :: forall (m :: Nat -> *) . m 0 -> m 1 -> m 2 -> - (forall n :: Nat . m (Succ (Succ n)) -> m (Succ (Succ (Succ n)))) -> - forall (n :: Nat) . m n - - --- increment by one -inc :: Nat -> Nat - - --- embed Fin into Nat -finNat :: forall (n :: Nat) . Fin n -> Nat - --- unit type -Unit :: * --- constructor -U :: Unit - --- eliminator -unitElim :: forall (m :: Unit -> *) . m U -> forall (u :: Unit) . m u - --- empty type -Void :: * - --- eliminator -voidElim :: forall (m :: Void -> *) (v :: Void) . m v - --- type of booleans -Bool :: * - --- constructors -False :: Bool -True :: Bool - --- eliminator -boolElim :: forall (m :: Bool -> *) . m False -> m True -> forall (b :: Bool) . m b - --- boolean not, and, or, equivalence, xor -not :: Bool -> Bool -and :: Bool -> Bool -> Bool -or :: Bool -> Bool -> Bool -iff :: Bool -> Bool -> Bool -xor :: Bool -> Bool -> Bool - --- even, odd, isZero, isSucc -even :: Nat -> Bool -odd :: Nat -> Bool -isZero :: Nat -> Bool -isSucc :: Nat -> Bool - - - --- equality on natural numbers -natEq :: Nat -> Nat - --- "oh so true" -Prop :: Bool -> * - --- reflexivity of equality on natural numbers -pNatEqRefl :: forall (n :: Nat) . Prop (natEq n n) - --- alias for type-level negation -Not :: * -> * - --- Leibniz prinicple (look at the type signature) -leibniz :: forall (a :: *) (b :: *) (f :: a -> b) (x :: a) (y :: a) . - Eq a x y -> Eq b (f x) (f y) - --- symmetry of (general) equality -symm :: forall (a :: *) (x :: a) (y :: a) . - Eq a x y -> Eq a y x - --- transitivity of (general) equality -tran :: forall (a :: *) (x :: a) (y :: a) (z :: a) . - Eq a x y -> Eq a y z -> Eq a x z - --- apply an equality proof on two types -apply :: forall (a :: *) (b :: *) (p :: Eq * a b) . a -> b - --- proof that 1 is not 0 -p1IsNot0 :: Not (Eq Nat 1 0) - --- proof that 0 is not 1 -p0IsNot1 :: Not (Eq Nat 0 1) - --- proof that zero is not a successor -p0IsNoSucc :: forall (n :: Nat) . Not (Eq Nat 0 (Succ n)) - - --- generate a vector of given length from a specified element (replicate) -replicate :: forall (n :: Nat) . forall (a :: *) . a -> Vec a n - --- alternative definition of replicate -replicate' :: forall (a :: *) (n :: Nat) . a -> Vec a n - --- generate a vector of given length n, containing the natural numbers smaller than n -fromto :: forall (n :: Nat) . Vec Nat n - - --- append two vectors -append :: forall (a :: *) (m :: Nat) (v :: Vec a m) (n :: Nat) (w :: Vec a n). - Vec a (plus m n) - --- helper function for tail, see below -tail' :: forall (a :: *) (m :: Nat) . Vec a m -> forall (n :: Nat) . Eq Nat m (Succ n) -> Vec a n - --- compute the tail of a vector -tail :: forall (a :: *) (n :: Nat) . Vec a (Succ n) -> Vec a n - --- projection out of a vector -at :: forall (a :: *) (n :: Nat) . Vec a n -> Fin n -> a - --- head of a vector -head :: forall (a :: *) (n :: Nat) . Vec a (Succ n) -> a - --- vector map -map :: forall (a :: *) (b :: *) (f :: a -> b) (n :: Nat) . Vec a n -> Vec b n - --- proofs that 0 is the neutral element of addition --- one direction is trivial by definition of plus: -p0PlusNisN :: forall n :: Nat . Eq Nat (plus 0 n) n - --- the other direction requires induction on N: -pNPlus0isN :: forall n :: Nat . Eq Nat (plus n 0) n - - --------------------------------------------------- --- Product / Sigma types proofs and utilities --------------------------------------------------- - - -Prod :: * -> * -> * - ---fst and snd as functions -getFst :: forall (s :: *) (t :: s -> *) . (exists (x :: s) . (t x)) -> s - - -zeroes :: Prod Nat Nat - -v1 :: Nat - -v2 :: Nat - -geq :: Nat -> Nat -> * - -gt :: Nat -> Nat -> * - -leq :: Nat -> Nat -> * - -lt :: Nat -> Nat -> * - - -geq0 :: forall (n :: Nat ) . geq n 0 - -natsAreInf :: forall (n :: Nat) . exists (m :: Nat) . gt m n diff --git a/q b/q deleted file mode 100644 index 5d53ba5..0000000 --- a/q +++ /dev/null @@ -1,1165 +0,0 @@ -commit f15b876059224d1cc87def3acd4fdf875c446c7c -Author: Joey Eremondi -Date: Fri May 6 21:45:09 2016 -0700 - - Add fns and inst for rigid - -commit e987ba50ea9813c97a810c14b74f8527ad516545 -Author: Joey Eremondi -Date: Fri May 6 18:48:30 2016 -0700 - - Fix compile errors with new FailPending lists - -commit 3c75a67e1524a743066a7e9a2c0e2297addb04cf -Author: Joey Eremondi -Date: Fri May 6 17:54:21 2016 -0700 - - Only put CF entries in context on fail - -commit a946a22f6a164d8dd948482ea0d4d815aac44b6b -Author: Joey Eremondi -Date: Fri May 6 17:47:01 2016 -0700 - - Solver pushes entry on failure - -commit 132c17812d09cf39e2380ed2f45147e5533edb30 -Author: Joey Eremondi -Date: Fri May 6 17:22:27 2016 -0700 - - NatIf compiling very slowly - -commit f9be85934c4bb7ea5e3c6726163743efa7b40186 -Author: Joey Eremondi -Date: Fri May 6 15:17:46 2016 -0700 - - Always flatten before equalize - -commit 4b26399646f608aa15f3b4a1f73909af9ccaea15 -Author: Joey Eremondi -Date: Fri May 6 13:58:12 2016 -0700 - - dot case for Bottom - -commit 8ac1c67325d5f152fb30a3ee3fedb7b18a576bbf -Author: Joey Eremondi -Date: Fri May 6 13:49:07 2016 -0700 - - Monad error throw in typeCheck - -commit 680141524933f77ccc5a5c05c6da53c14e87c07a -Author: Joey Eremondi -Date: Fri May 6 13:44:14 2016 -0700 - - Missing occurs and frees case - -commit f41822ac55c41d9e7fe3f0c48aeee16deaad2513 -Author: Joey Eremondi -Date: Fri May 6 13:39:24 2016 -0700 - - Missing case from Elim for Bottom - -commit 9a8debbf6c812aa451e8516f42ccf4d06ef5f3db -Author: Joey Eremondi -Date: Thu May 5 21:13:06 2016 -0700 - - Missing cases, clean some print stmts - -commit 32abed113fc6c05faad54ed36acd25b5454bd576 -Author: Joey Eremondi -Date: Thu May 5 18:19:05 2016 -0700 - - Unify does choice, not RigidRigid - -commit ff6c31114801240dea123117fd51035eebf7156d -Author: Joey Eremondi -Date: Wed May 4 15:55:24 2016 -0700 - - Debugging progress - -commit 0b24e8fea19527000775fc75b0f43dee1701b741 -Author: Joey Eremondi -Date: Wed May 4 15:09:10 2016 -0700 - - Pretty cases for new states - -commit 1eb152b046e0228e4cce8abba2b89309d024a8b2 -Author: Joey Eremondi -Date: Wed May 4 15:06:36 2016 -0700 - - Left return tuple for SplitChoice - -commit 041da7e4b5bebfecb8d7c842dadfe6d06a64e486 -Author: Joey Eremondi -Date: Wed May 4 14:57:44 2016 -0700 - - Include FailPending in update - -commit 1da8acad02c03fa9a9f87348c3645ae48a27f052 -Author: Joey Eremondi -Date: Wed May 4 14:52:32 2016 -0700 - - Add failed problems to fail list - -commit 3eaf12b92517146d24c573c3e33d8ded2e0ae61e -Author: Joey Eremondi -Date: Wed May 4 14:49:52 2016 -0700 - - Start setting framework for FailPending - -commit c91f858b282fd67ec73ef6dac4580dea9bafca88 -Author: Joey Eremondi -Date: Tue May 3 16:03:10 2016 -0700 - - Store creating var for choices - -commit c0eb1afa60e3434a1182adf1a009adef7000a364 -Author: Joey Eremondi -Date: Mon May 2 22:51:30 2016 -0700 - - Remove debug versions of push - -commit 693603596b59f34744a0d00cb4466452be5e657d -Author: Joey Eremondi -Date: Mon May 2 22:49:46 2016 -0700 - - Only split problems, not Entries - -commit d10728f802ed1fce2a61737831e4bd36573a8076 -Author: Joey Eremondi -Date: Mon May 2 20:29:55 2016 -0700 - - Fix goLeft order, debug stmts - -commit d9ed6f980a8f78603f477c929f210a29fdfda228 -Author: Joey Eremondi -Date: Mon May 2 20:11:07 2016 -0700 - - Bottom case for Prune - -commit 07f335f734419350a0caab11398181745b8ca9c2 -Author: Joey Eremondi -Date: Mon May 2 19:51:55 2016 -0700 - - Properly label problems as CF - -commit f5c28bec2d1fb200844f4ce5700a175efc256aa9 -Author: Joey Eremondi -Date: Mon May 2 19:39:11 2016 -0700 - - No choice for instantiate, lower - -commit c18aaca33468e9dfd9453b3321ec01a4d48ff2bc -Author: Joey Eremondi -Date: Mon May 2 18:47:32 2016 -0700 - - Don't use choice in immediate - -commit 64fdeef6cbf733bb348ae465c4d1e84d4fcf2f9b -Author: Joey Eremondi -Date: Mon May 2 18:37:51 2016 -0700 - - applySSS works on Right context, not left - -commit 8f0b726d084a0cdaf8d7a9bfef28193d676c89b7 -Author: Joey Eremondi -Date: Mon May 2 18:33:30 2016 -0700 - - Add immediate substs to avoid inf loops - -commit 2c3e978b483330ef04746d32a3e22c3085792bb3 -Author: Joey Eremondi -Date: Mon May 2 16:40:53 2016 -0700 - - SSS implemented, about to plug in - -commit cdf72c10c115b31e960ef6183295b38b5bb57680 -Author: Joey Eremondi -Date: Mon May 2 16:25:34 2016 -0700 - - Special type for SSS in right context - -commit edb2985d290d8875c5ebfd23b647c12719b80236 -Author: Joey Eremondi -Date: Mon May 2 15:55:19 2016 -0700 - - Implement splitChoice, not used yet - -commit 7af7bec6ecda301d9fd6ab76f61ff72a6a763c5a -Author: Joey Eremondi -Date: Mon May 2 15:21:13 2016 -0700 - - Flatten choices in final result - -commit 50755105103ba6f60d366cab93c5c4f3db6a84a6 -Author: Joey Eremondi -Date: Mon May 2 15:08:33 2016 -0700 - - Got solving, ignoring 2nd half of choice - -commit 9ecaead8a9f33a4d0ad78ee9f8fb6f660dc9ac2b -Author: Joey Eremondi -Date: Fri Apr 29 20:30:06 2016 -0700 - - Debugging attemtps - -commit fbdd17c65b890f3e9f91c168bfef34ce7389ccb4 -Author: Joey Eremondi -Date: Fri Apr 29 20:24:55 2016 -0700 - - Proper error on not found meta - -commit 0f70ac982867026d3516c07cd26aac885a885720 -Author: Joey Eremondi -Date: Fri Apr 29 16:54:22 2016 -0700 - - Remove test from Run - -commit 1b6ad9f7f1dcb7079be1dcd7a50e53bde09402fd -Author: Joey Eremondi -Date: Fri Apr 29 16:46:18 2016 -0700 - - Prelude compiling with CF holes (not choices) - -commit bae660353415715fbdca8fe230c483df21e9684b -Author: Joey Eremondi -Date: Fri Apr 29 16:42:32 2016 -0700 - - Prelude compiling with richer eqn info - -commit 4c54a3d0dd099f1aff3e61020e09ddbcd6fe8d2e -Author: Joey Eremondi -Date: Fri Apr 29 16:30:46 2016 -0700 - - Fix bug filtering non-source metas - -commit e4ae3eb952591ee8d1b53e1b5a34bfbcc2e3859e -Author: Joey Eremondi -Date: Fri Apr 29 16:23:17 2016 -0700 - - Got prelude compiling with fixed region system - -commit e7b641fe219cd57071418c85c40d458a38faca8d -Author: Joey Eremondi -Date: Fri Apr 29 15:57:45 2016 -0700 - - Prelude compiling with Region in StringErr - -commit 00df01f3c4d2bbabd077270e9a4bc291aa4acb0f -Author: Joey Eremondi -Date: Fri Apr 29 15:38:10 2016 -0700 - - Disable hole before diagnosing error - -commit cc32b0dee0147964eb9a964d6fe68779bb8d0b82 -Author: Joey Eremondi -Date: Fri Apr 29 15:27:59 2016 -0700 - - Remove old typecheck check - -commit 3b8641afaa9cf854ba7ea93281f409a08cc0de41 -Author: Joey Eremondi -Date: Fri Apr 29 15:13:12 2016 -0700 - - Flatten choices of infer in check - -commit 58a257bcbfe2cf7b030485d8382c4af59ba5c992 -Author: Joey Eremondi -Date: Fri Apr 29 15:10:22 2016 -0700 - - Add flattenChoice fn - -commit 26bc3b2cba36232244bd7ab0ca05815a1f35ed37 -Author: Joey Eremondi -Date: Fri Apr 29 15:05:36 2016 -0700 - - Choice in containsBottom - -commit f61834522312d293abcb93a756d1915544ae865f -Author: Joey Eremondi -Date: Fri Apr 29 15:05:04 2016 -0700 - - Choice expressions in check - -commit a729f6ee5705d6365186b432cd16652bc7e68afe -Author: Joey Eremondi -Date: Fri Apr 29 14:59:19 2016 -0700 - - Eval choice, type graph choice - -commit eaad4799731ff11300ccaec0a2912759bf357b43 -Author: Joey Eremondi -Date: Fri Apr 29 14:25:18 2016 -0700 - - Remove quote, replace with equalize - -commit c43afbc4e7ab921820623929d4d41eb958d40108 -Author: Joey Eremondi -Date: Wed Apr 20 18:53:31 2016 -0700 - - Re-add avoiding needless SET=SET - -commit 446f199a2fe835498a2b5f6c9e18966abb12ce3f -Author: Joey Eremondi -Date: Wed Apr 20 18:25:58 2016 -0700 - - Check if term can use first order unif - -commit c5d5a7ef47e4bfe3d1d8cc13946be1fe9c26576a -Author: Joey Eremondi -Date: Wed Apr 20 18:18:55 2016 -0700 - - Fix joinErrors bug - -commit 98c30909a316612414a5285cc2a598a6ff96d1d6 -Author: Joey Eremondi -Date: Wed Apr 20 18:12:10 2016 -0700 - - RigidRigid no longer throws error - -commit d7c2a99cadff447e5f2b5af9986d962482735a7a -Author: Joey Eremondi -Date: Wed Apr 20 17:57:06 2016 -0700 - - Clean up case stmts - -commit f6229162ea57939b19edbc6376996a056224e9ba -Author: Joey Eremondi -Date: Wed Apr 20 17:53:39 2016 -0700 - - Reintroduce VBot, EBot - -commit fe6ad8edaa3223f9a2c9351384f69aabd9ddffa6 -Author: Joey Eremondi -Date: Wed Apr 20 16:35:29 2016 -0700 - - Fixed some broken parts of equalize - -commit 96ddd1fd679a2b24fcf9f89d2947ad45c7cb5505 -Author: Joey Eremondi -Date: Wed Apr 20 15:35:44 2016 -0700 - - Proper parallel unbinding for lambdas - -commit 3e27d05e0ff8d06d58c3a1ac083258cc457f322b -Author: Joey Eremondi -Date: Tue Apr 19 20:57:04 2016 -0700 - - Print initial context - -commit af8f00bdf521c21f8547bb97db8bc8997cabaab4 -Author: Joey Eremondi -Date: Tue Apr 19 18:15:20 2016 -0700 - - Add debug Prune statements - -commit 5e7d73bd279dbaa04f519bfab1d1748784e4dc10 -Author: Joey Eremondi -Date: Wed Apr 6 18:56:56 2016 -0700 - - Nicer printing of Sigma, Pi, errors - -commit 27ff3f333d6a904d6a8db7ceddb478fabfaf33f8 -Author: Joey Eremondi -Date: Wed Apr 6 18:46:05 2016 -0700 - - Remove too many traces - -commit 631b78ffa9a69410099a4037306e245086626183 -Author: Joey Eremondi -Date: Wed Apr 6 15:51:31 2016 -0700 - - Include source region in initial entries - -commit be85095ec4f4a7fd9c666c04358197bfe38ba53c -Author: Joey Eremondi -Date: Wed Apr 6 15:20:19 2016 -0700 - - Add function to get info from entry - -commit 800a88c85332c077aed83fc49cbc9068a5644550 -Author: Joey Eremondi -Date: Wed Apr 6 12:51:58 2016 -0700 - - Adapt Constraint to new format - -commit 9b4b20e543dc79b09532e97f752a02bc4a7489a7 -Author: Joey Eremondi -Date: Wed Apr 6 12:46:51 2016 -0700 - - CreatedBy Pid is no longer optional - -commit 94be5704f64eae6c1ceeabcb895e02b295b1b421 -Author: Joey Eremondi -Date: Wed Apr 6 12:31:19 2016 -0700 - - Remove "define Nothing" cases - -commit a8c14837c3d89e6732f5c54f58b56ec0930fae7d -Author: Joey Eremondi -Date: Tue Apr 5 22:33:59 2016 -0700 - - Return GraphInfo when it exists - -commit 6fa804e96b0d8a27375753192a9aa2ed076a1426 -Author: Joey Eremondi -Date: Tue Apr 5 22:03:17 2016 -0700 - - Record creating probId for rigidRigid - -commit 212288ab6a43376ff79b353e8cc86d8b22522a6d -Author: Joey Eremondi -Date: Tue Apr 5 21:24:44 2016 -0700 - - Commit before storing creator in entry - -commit 794490a8b3a4cda404df886506cf4a5bc50867d8 -Author: Joey Eremondi -Date: Fri Apr 1 20:34:13 2016 -0700 - - Treat quantified variables as constants - -commit 52ea693fe987b2d4bbfab1903b547b3419402da4 -Author: Joey Eremondi -Date: Fri Apr 1 14:59:36 2016 -0700 - - Fix dot generation node ids - -commit a4652269650d4233701ff3c4b06c92a38d7792cc -Author: Joey Eremondi -Date: Fri Apr 1 14:48:39 2016 -0700 - - Add missing calls to Fresh - -commit 09522b3ae936995270a4e59bdd8e70ea54bada86 -Author: Joey Eremondi -Date: Thu Mar 31 19:31:45 2016 -0700 - - Get graphs printing to DOT - -commit ccdc17645efc6012be4666fc020baac9d61760c3 -Author: Joey Eremondi -Date: Wed Mar 30 21:20:53 2016 -0700 - - Typegraph diagnosis compiling, no errors, but wrong - -commit effe2ad05c68ed903d74cc36a5d7371498daf301 -Author: Joey Eremondi -Date: Wed Mar 30 20:04:10 2016 -0700 - - Fix leftover type error - -commit 5a3dd0032aae7afca19d55d4878bd8cb614c4550 -Author: Joey Eremondi -Date: Wed Mar 30 20:02:45 2016 -0700 - - Bugfixes, factor out constant type - -commit 9e1e8e2325970876b8c2ae722809028c39432caf -Author: Joey Eremondi -Date: Wed Mar 30 17:21:52 2016 -0700 - - Add missing edge case for Lambda - -commit d6821a3ef7b6c0a8b3974e0cca46dfb250feb90e -Author: Joey Eremondi -Date: Wed Mar 30 16:56:20 2016 -0700 - - Fix typos in prettyElim - -commit 87390854e1fa5c6ee16b3378154e2a615c15dfa4 -Author: Joey Eremondi -Date: Wed Mar 30 16:46:41 2016 -0700 - - Fix type error after extending state - -commit 28601e106d3e97000e84764e57c8b1f21c8a32ed -Author: Joey Eremondi -Date: Wed Mar 30 16:42:51 2016 -0700 - - First try at getting heuristic errors - -commit 318917cbcab5fc83a38999fc0cf038bc18da56f7 -Author: Joey Eremondi -Date: Tue Mar 29 20:17:38 2016 -0700 - - Functions to record substituted problems - -commit 113ad9605d47eaaa447bac8a61af30029b06cd2b -Author: Joey Eremondi -Date: Tue Mar 29 19:12:15 2016 -0700 - - Functions for recording entries - -commit 731f1b6b3bf4345e720b1a0cb8f63ab328e4c91c -Author: Joey Eremondi -Date: Mon Mar 28 19:19:28 2016 -0700 - - Empty graphs properly initialized - -commit 6832d54d1ca72b56e8d6572becf2de2b82925ccc -Author: Joey Eremondi -Date: Mon Mar 28 17:59:23 2016 -0700 - - Record solved values in type graph - -commit 652ccd75f2fec83b22ed44c18d347741df152d14 -Author: Joey Eremondi -Date: Mon Mar 28 17:43:05 2016 -0700 - - Move recordEqn to Unify fn - -commit 5683e4b5a3fe9a168680eb43b9f14c2dcd2e6ac7 -Author: Joey Eremondi -Date: Mon Mar 28 17:36:51 2016 -0700 - - Factor out recordEqn function - -commit de354b3596f0a47bd429130ea3bee23aca0407b2 -Author: Joey Eremondi -Date: Mon Mar 28 17:35:06 2016 -0700 - - Record rigid-rigid edges added - -commit 895a286dd7119efb4fb535f259582fac0c06458b -Author: Joey Eremondi -Date: Mon Mar 28 16:45:23 2016 -0700 - - Add TypeGraph to Contextual state - -commit 13ee9963cf06cf301a81ab55635cbd2acc97c93d -Author: Joey Eremondi -Date: Mon Mar 28 16:06:08 2016 -0700 - - Got ApplyHeuristics compiling with removals - -commit 5c3740544e6eb309a9c51f09a49df6686713be8a -Author: Joey Eremondi -Date: Mon Mar 28 16:01:36 2016 -0700 - - Got compiling after removals - -commit c9b01ba3887cb4405f60f9ae01173199884e1cca -Author: Joey Eremondi -Date: Mon Mar 28 15:49:57 2016 -0700 - - Got compiling with removals - -commit f48d1a0aad504faae890b06446e270a424f96596 -Author: Joey Eremondi -Date: Mon Mar 28 14:33:46 2016 -0700 - - Get Solver compiling with removals - -commit 301c329bec7d6de2b225b04c368a105a0c68a9a7 -Author: Joey Eremondi -Date: Thu Mar 24 20:59:43 2016 -0700 - - Use Nom, not Int - -commit c10946f6e26730b6a21827d252f9ceeacc0cdf86 -Author: Joey Eremondi -Date: Wed Mar 23 21:16:56 2016 -0700 - - Only keep typeclasses from types - -commit 946ae2fdd7d638a3ab8c3ff57e36dc6410141c00 -Author: Joey Eremondi -Date: Wed Mar 23 19:09:23 2016 -0700 - - Don't pipe uniques through addTerm - -commit 38dfe7f769a29f4c067a8e6a4cacc3b5577d39cf -Author: Joey Eremondi -Date: Wed Mar 23 19:03:17 2016 -0700 - - Move addTermGraph into FreshM - -commit 4d4c726f6b8e4f1d310dcb908b87682ad3b2152b -Author: Joey Eremondi -Date: Wed Mar 23 18:16:46 2016 -0700 - - Properly add Metavariables - -commit ad0e3ef53317d48133fe918b41708eeb3ec0cf75 -Author: Joey Eremondi -Date: Wed Mar 23 18:03:33 2016 -0700 - - Properly handle vars and Elims in termGraph - -commit 2a84fa769ef538fe50c373031e33c8be839c4cd6 -Merge: 1b0410b 78eba7e -Author: Joey Eremondi -Date: Wed Mar 23 17:33:36 2016 -0700 - - Merge CanElim factor from master - -commit 78eba7ebb7b2ed94f7cb06f0d1aca4d07eb3626f -Author: Joey Eremondi -Date: Wed Mar 23 17:31:00 2016 -0700 - - Factor out Elims into Canonical form - -commit 1b0410b2b93d96504a58df4356afc5d06612bd59 -Author: Joey Eremondi -Date: Tue Mar 22 22:50:49 2016 -0700 - - Remove doubled over section from merge - -commit 4ff987737b45f7d3e0c9cbe04f7da0db93773a44 -Merge: 2bb7e69 10ab337 -Author: Joey Eremondi -Date: Tue Mar 22 22:46:20 2016 -0700 - - Merge with master - -commit 10ab33771300d472bb14342760fb83177ff68c8b -Author: Joey Eremondi -Date: Tue Mar 22 11:26:29 2016 -0700 - - Clean up pretty print - -commit c53b4c88779a6af288e594d43586a1e06ad151e3 -Author: Joey Eremondi -Date: Tue Mar 22 10:37:06 2016 -0700 - - Merge changes: DataTypes to Can - -commit 2bb7e69291f08773c4a6e912081e9b389d059bc6 -Author: Joey Eremondi -Date: Tue Mar 22 10:35:26 2016 -0700 - - Commit before merge Tm into Master - -commit acf0ad0559490e9e58ce517935466a2004c97c61 -Author: Joey Eremondi -Date: Mon Mar 21 21:13:01 2016 -0700 - - Add back substitable - -commit c173f3dd83a3fd3083e55fe730bb94f50d5a3e99 -Author: Joey Eremondi -Date: Mon Mar 21 20:53:43 2016 -0700 - - Try removing Type dependency - -commit d3750d30536cdb709f6d4535016be6592d50bff7 -Author: Joey Eremondi -Date: Mon Mar 21 20:35:11 2016 -0700 - - Fill in Substitute hole - -commit 8826e8785264c95a65adeee475ce2d80179db39d -Author: Joey Eremondi -Date: Mon Mar 21 20:13:06 2016 -0700 - - Get Standard compiling with a couple holes - -commit c2980fe708900d13bb5f2d67e5551cebb24c54f4 -Author: Joey Eremondi -Date: Mon Mar 21 19:58:40 2016 -0700 - - Proper fold for Ctor add term graph - -commit f44e3125366d3cace5c83536e58100dec814dde6 -Author: Joey Eremondi -Date: Mon Mar 21 17:02:40 2016 -0700 - - Remove redundancies with Can - -commit 59fb8ab0c55e25633969dd393d01f386c0ca3455 -Author: Joey Eremondi -Date: Mon Mar 21 16:58:22 2016 -0700 - - Got prelude compiling with Can - -commit c0d7b9e18b52cc03b9259dc9e9115a612489eba6 -Author: Joey Eremondi -Date: Mon Mar 21 16:50:48 2016 -0700 - - Move custom types to Can - -commit 2733c5b576186e00a36ecc8cb4a03b3923e5c7bd -Author: Joey Eremondi -Date: Mon Mar 21 16:50:36 2016 -0700 - - Move custom types to Can - -commit 8951be32d7e8f83605bec416d99cd83e1184b151 -Author: Joey Eremondi -Date: Mon Mar 21 15:41:04 2016 -0700 - - Adapt Class to Tm structure - -commit c3edc2b52ad90dde965a27f40cfde84b81dc6a88 -Author: Joey Eremondi -Date: Mon Mar 21 15:31:51 2016 -0700 - - Copy Top src into project - -commit 0c02d4a89fd2b308b4d446be5889bad9b90b756e -Author: Joey Eremondi -Date: Mon Mar 21 14:11:32 2016 -0700 - - Pretty printing closer to source lang - -commit a9762a163d785e7876308651e0b0170ec5c70fb4 -Author: Joey Eremondi -Date: Sun Mar 20 15:16:36 2016 -0700 - - Nicer spacing of messages - -commit f4d1a601c745dd71731df21dc3dfbe6ea00212db -Author: Joey Eremondi -Date: Sun Mar 20 14:24:58 2016 -0700 - - Avoid internal type errors on meta failure - -commit bcd1dc6252e4b1262daeec06a2164f07632db5f5 -Author: Joey Eremondi -Date: Sun Mar 20 13:23:44 2016 -0700 - - Only show source metas in message - -commit c6d17c8305ef9befba8727a9100652dda6cd0a05 -Author: Joey Eremondi -Date: Sat Mar 19 21:58:06 2016 -0700 - - Fix unsafe Map.!, record all metas - -commit db7af4a4a82cac8d0a448ff5ef55d5c51e14e4cb -Author: Joey Eremondi -Date: Sat Mar 19 19:41:45 2016 -0700 - - Try fixing meta scope issues - -commit 1467d562b25939f1f1bc604b1bf4a7a01909ed19 -Author: Joey Eremondi -Date: Sat Mar 19 16:55:19 2016 -0700 - - Trace error IDs back to an initial location - -commit f0396cf4f40b8adb2428c56267a46f6fa9e8857e -Author: Joey Eremondi -Date: Sat Mar 19 16:20:38 2016 -0700 - - Record what problem we're in during Unify - -commit 2057e1b49f44dfee37aa19a533727ee7dfc78f16 -Author: Joey Eremondi -Date: Sat Mar 19 16:06:44 2016 -0700 - - Incorporate last seen problem into Context - -commit 5ab586d4dc6453a177ef53ebdaefafa645a8458a -Author: Joey Eremondi -Date: Sat Mar 19 13:55:15 2016 -0700 - - Clean error messages from unif - -commit ea926b16a759d4c6abb41d0e6d71881c3c137486 -Author: Joey Eremondi -Date: Fri Mar 18 15:42:32 2016 -0700 - - Nice inclusion of printed output in results - -commit 97a21b9f5302b8c969c9fd4fcf4ce4c0cb0150a8 -Author: Joey Eremondi -Date: Fri Mar 18 12:33:00 2016 -0700 - - Remove bad SumElim - -commit 29e71e33a2f4c0330c54b4596451998425108970 -Author: Joey Eremondi -Date: Fri Mar 18 12:20:39 2016 -0700 - - Include compiled Prelude in library - -commit e85ce2a2dbb7e533b8162fdf83c98433eb3ece4a -Author: Joey Eremondi -Date: Fri Mar 18 10:51:52 2016 -0700 - - Initial draft of compile lib fun - -commit 1d600375ce61bcdd37be262856412526137d7f76 -Author: Joey Eremondi -Date: Fri Mar 18 00:14:58 2016 -0700 - - Make error printing nicer - -commit c1dbacfb0e0c52ad2b3709b8eb1ae7668afcd797 -Author: Joey Eremondi -Date: Thu Mar 17 23:49:46 2016 -0700 - - Got solved metas printing nicely - -commit e54ba12fa63c5d8e77a2b94937991de847141e40 -Author: Joey Eremondi -Date: Thu Mar 17 23:21:01 2016 -0700 - - Use throwError wherever we can - -commit c3d2e77271bcda7b41ec0aa65215fa158a9df21d -Author: Joey Eremondi -Date: Thu Mar 17 23:05:55 2016 -0700 - - Fixed metavariable naming error - -commit 89914265b1bad94c9521a55c7a523840088e5c98 -Author: Joey Eremondi -Date: Thu Mar 17 22:05:38 2016 -0700 - - Incorporate solved values into compile results - -commit fc7d24edf99729626b1274463baab51e15729b56 -Author: Joey Eremondi -Date: Thu Mar 17 21:35:16 2016 -0700 - - Include unsolved metas in error - -commit 4beb49281e5badeb315f0291a2978ca99a25432d -Author: Joey Eremondi -Date: Thu Mar 17 21:14:30 2016 -0700 - - Add function to get solved and unsolved metas - -commit 08618fa6579f188b0129e5d7ea83745f64b460ab -Author: Joey Eremondi -Date: Thu Mar 17 21:01:07 2016 -0700 - - Add solved metas to constraint solution - -commit 86e7f0565d2cf859e13ef5ff28f16f0577c406d4 -Author: Joey Eremondi -Date: Thu Mar 17 20:46:47 2016 -0700 - - Better names for which env is which - -commit 95e7bea4153feba771928a3a1d556b0bc4495eb4 -Author: Joey Eremondi -Date: Thu Mar 17 20:43:04 2016 -0700 - - Create exposed Library file for interface - -commit 7e9e9abe371f9eb18ebf0497cd8a3ee75e5719c2 -Author: Joey Eremondi -Date: Thu Mar 17 17:49:23 2016 -0700 - - Remove test output - -commit c1c0cee0c27bd4325ac26435e41f625fc2fc033a -Author: Joey Eremondi -Date: Thu Mar 17 17:46:48 2016 -0700 - - Update cabal file, change name - -commit ae261bce21f28ca6b683a81f5846b3d30017dd1b -Author: Joey Eremondi -Date: Thu Mar 17 17:39:58 2016 -0700 - - Add basic README - -commit 92dbc8286c974d91f92a1ed7ec0c5c6f33df2e06 -Author: Joey Eremondi -Date: Thu Mar 17 17:37:19 2016 -0700 - - Add BSD3 license - -commit d7bdaa34358d160110a11faa8bfc29a8ed6cd749 -Author: Joey Eremondi -Date: Thu Mar 17 17:21:35 2016 -0700 - - Beautify source - -commit 3fdabdf2e03e6673678358cdcc8d9c0b027210f8 -Author: Joey Eremondi -Date: Thu Mar 17 17:12:53 2016 -0700 - - Add back test file - -commit ddae19779ca448e0b4fcdc9619b4416a3b08fb3b -Author: Joey Eremondi -Date: Thu Mar 17 16:58:32 2016 -0700 - - Un-check scratch files - -commit 775f6e8012493f3aa4cde42b0ca8c09f3467b48a -Author: Joey Eremondi -Date: Thu Mar 17 16:56:07 2016 -0700 - - Un-check scratch files - -commit 1ab3b7f0aca9e95a9d32502ab412101c48c442de -Author: Joey Eremondi -Date: Thu Mar 17 16:53:02 2016 -0700 - - Remove unused Solver file - -commit 513de1a5e60c8f2d03ea7460afd0f31bcfcc721d -Author: Joey Eremondi -Date: Thu Mar 17 16:48:08 2016 -0700 - - More code clean, remove unused files - -commit 3046ba3063304ee13e796783345656e70f5172bc -Author: Joey Eremondi -Date: Thu Mar 17 16:45:38 2016 -0700 - - Cleanup unused comments - -commit fd84b40219e0657da8dae3b4a452729717ec4c64 -Author: Joey Eremondi -Date: Thu Mar 17 16:37:40 2016 -0700 - - Rename and clean Test.hs to Run.hs - -commit df9d81df0e1d6a2e7eaa85e99a66d68085da5d57 -Author: Joey Eremondi -Date: Thu Mar 17 15:46:23 2016 -0700 - - Remove more warnings - -commit 30cdad3999ced5768cfdd83f1f8f5c8e79bc6a95 -Author: Joey Eremondi -Date: Thu Mar 17 15:08:55 2016 -0700 - - More imports cleanup - -commit 40120b9234e7bfdfb4259050deeb65428dd30357 -Author: Joey Eremondi -Date: Thu Mar 17 15:01:02 2016 -0700 - - Remove unused AnnExp, unused catchalls - -commit f333f63237c7e605d0abd9fe0da143c1e2f18fbe -Author: Joey Eremondi -Date: Thu Mar 17 14:50:21 2016 -0700 - - Remove unneeded imports, add sigs - -commit f489b9562e95f486760e046a712757ee0f4a2494 -Author: Joey Eremondi -Date: Thu Mar 17 14:45:44 2016 -0700 - - Remove some warnings - -commit a66df7a3a529de90d2694872fdb1942d215faf54 -Author: Joey Eremondi -Date: Wed Mar 16 23:57:29 2016 -0700 - - Start moving more into implicit - -commit 00727118c72ee391d17a26bde09baad27e3567aa -Author: Joey Eremondi -Date: Wed Mar 16 23:55:58 2016 -0700 - - Start moving more into implicit - -commit cab42039737903026d69181cd984e40c430e4d83 -Author: Joey Eremondi -Date: Wed Mar 16 23:52:11 2016 -0700 - - Make sure all subs are applied before validate - -commit aed5cb4cc59d7be90df34324d1f47545b101a308 -Author: Joey Eremondi -Date: Wed Mar 16 21:52:38 2016 -0700 - - Commit before debugging rollback - -commit 9e31f988d102c89c16dac953707b35b4d3728b34 -Author: Joey Eremondi -Date: Wed Mar 16 16:02:22 2016 -0700 - - Proper dependency graph for Pending and Fails - -commit 41cf0ae842235aeb44cda4a0a55b63d8399f4398 -Author: Joey Eremondi -Date: Wed Mar 16 15:10:39 2016 -0700 - - Try removing evalInEnv from CB - -commit 72b475f8d238956f1158dcbc83bdb67b0a0f0117 -Author: Joey Eremondi -Date: Wed Mar 16 14:50:16 2016 -0700 - - Nicer printing of Pi, Sigma - -commit 8d938078bee1630def5462260a42e61f9a7b995b -Author: Joey Eremondi -Date: Wed Mar 16 14:45:43 2016 -0700 - - Add Pair cases to Print - -commit a9910f379409baaef09b9de9e2413d4a5342ac26 -Author: Joey Eremondi -Date: Wed Mar 16 12:49:15 2016 -0700 - - Remove Pair as keyword - -commit 7638c5349d37993316e453344e70df80a4482c64 -Author: Joey Eremondi -Date: Wed Mar 16 11:52:25 2016 -0700 - - Got Pair parsing working - -commit a85a5ef0f215eecec6d532a453a698918bcdf7b1 -Author: Joey Eremondi -Date: Tue Mar 15 20:35:15 2016 -0700 - - Subst cases for pairs - -commit 082c50aabee2044b5c73453e2843946dc3f4f4fd -Author: Joey Eremondi -Date: Tue Mar 15 20:31:12 2016 -0700 - - Typecheck cases for hd, tl - -commit 09cd3a7c21130076b774c4ffbf436a5d478845b8 -Author: Joey Eremondi -Date: Tue Mar 15 20:12:01 2016 -0700 - - Add type cases for fst, snd - -commit c759f3b1cf508c034d7023ce23997a1b3e9d5097 -Author: Joey Eremondi -Date: Tue Mar 15 20:04:09 2016 -0700 - - Typechecking cases for Sigma, Pair - -commit 52d29e89954697db2b4e6a30bab5d27a3bfbee52 -Author: Joey Eremondi -Date: Tue Mar 15 19:46:49 2016 -0700 - - toUnifForm functions for pairs - -commit 30924179be7640f1fdc51ec4bb24de523703f254 -Author: Joey Eremondi -Date: Tue Mar 15 19:41:57 2016 -0700 - - Parser for fst, snd - -commit efb3f8feb29e4e6d3f0a3e3145c0a91f12ede355 -Author: Joey Eremondi -Date: Tue Mar 15 19:30:28 2016 -0700 - - Add Parser for Pairs, Sigma types - -commit 33108998da794d677e6ad0cc5e7f9286a24224f2 -Author: Joey Eremondi -Date: Tue Mar 15 15:42:21 2016 -0700 - - No extra line after prompt - -commit 74a1c753775941008014b5f1a9d96e95023622ee -Author: Joey Eremondi -Date: Tue Mar 15 15:39:57 2016 -0700 - - Remove stray ReadLine import - -commit 73478d8f5a8a726567810d5a0870ceb7159152b5 -Author: Joey Eremondi -Date: Tue Mar 15 15:39:14 2016 -0700 - - Remove ReadLine dependence - -commit 8ac43f1ce43d47f412700a99de8dc4145dc42abe -Author: Joey Eremondi -Date: Tue Mar 15 15:28:21 2016 -0700 - - Remove random. union-find - -commit 792ed845b83623f38b684b911cf4d4ed6f4c78c3 -Author: Joey Eremondi -Date: Tue Mar 15 14:08:10 2016 -0700 - - Use name for builtin fresh args - -commit 28c4f3403885ffb88eaf9f7842f854442ebbba07 -Author: Joey Eremondi -Date: Tue Mar 15 13:35:01 2016 -0700 - - Make Bwd a pattern synonym for List - -commit 4a9efae4f19a02db9553aa7f48c6fd72c1cbd97f -Author: Joey Eremondi -Date: Tue Mar 15 13:24:21 2016 -0700 - - Don't use Control.Monad.Error - -commit 72a36245a3110ffef67cdbab71844a59c508a28b -Author: Joey Eremondi -Date: Tue Mar 15 13:22:50 2016 -0700 - - Switch to Except - -commit de7babd7c84ccf2503e8131c9bce173c2a49fc06 -Author: Joey Eremondi -Date: Tue Mar 15 13:03:29 2016 -0700 - - Got Compiling with Map for env - -commit d90893aad3c00115d071c9207dbd0e64234d76ed -Author: Joey Eremondi -Date: Tue Mar 15 12:54:06 2016 -0700 - - Start using Map for env - -commit e131063a524a6952614770c9200948ccb32f2045 -Author: Joey Eremondi -Date: Mon Mar 14 22:45:45 2016 -0700 - - Got GHC Mod working with Profiling - -commit 43e61e838b75fac5aa4007e4d29c7afec1460eaa -Author: Joey Eremondi -Date: Mon Mar 14 22:25:42 2016 -0700 - - Got Compiling with Generics - -commit 472e7d7cbfa9e1bc7319961f8d5a2766c28638dc -Author: Joey Eremondi -Date: Mon Mar 14 21:10:50 2016 -0700 - - Add option to just read file - -commit 6df176dd5c59a65d69f667ff059d2823e2c8d21d -Author: Joey Eremondi -Date: Mon Mar 14 20:25:21 2016 -0700 - - Got append compiling - -commit 0814b628f8cc170ce259da679e0c07ff059eee52 -Author: Joey Eremondi -Date: Mon Mar 14 19:23:39 2016 -0700 - - Fix backwards typeCheck - -commit 0c1e0b759366184ff0e18a983ac05a542bc56f25 -Author: Joey Eremondi -Date: Mon Mar 14 18:32:54 2016 -0700 - - Add Elim for Vec, Eq - -commit 69446aacaa8e4fbb09e021a3ce170f34d1eb51cc -Author: Joey Eremondi -Date: Mon Mar 14 18:20:47 2016 -0700 - - Fix bad Result type for VecElim - -commit 80a7fe41b9cdf2ba054dc4e6d5274b5838cd4293 -Author: Joey Eremondi -Date: Mon Mar 14 18:20:35 2016 -0700 - - Add quoteSpine Vec and Eq - -commit 055cd9721b1ccd42073eaa6277074470b89fe79a -Author: Joey Eremondi -Date: Mon Mar 14 17:58:50 2016 -0700 - - Fix bad VecElim -> EqElim - -commit 0b8f8cb817623f4e00fdfcff5fe83af253b669f8 -Author: Joey Eremondi -Date: Mon Mar 14 17:47:04 2016 -0700 - - checkSpine for Vec and Eq diff --git a/test.lp b/test.lp deleted file mode 100644 index 4043285..0000000 --- a/test.lp +++ /dev/null @@ -1,25 +0,0 @@ ---let x = 3 :: Nat - ---let id = (\_ x -> x) :: forall (a :: *) . a -> a - -let nat1Elim = - ( \ m m0 m1 ms -> natElim m m0 - (\ p rec -> natElim (\ n -> m (Succ n)) m1 ms p) ) - :: forall (m :: Nat -> *) . m 0 -> m 1 -> - (forall n :: Nat . m (Succ n) -> m (Succ (Succ n))) -> - forall (n :: Nat) . m n - -let natIf3 = - (\_ x y z n -> nat1Elim _ x y (\ _ _ -> z) n ) :: forall (a :: *) . a -> a -> a -> Nat -> a - ---let myFun = (\x -> x) :: Nat -> Nat - ---let myPair = (3,3) :: exists (x :: Nat) . Nat - ---let test = natIf3 _ 1 ((\x -> x) :: Nat -> Nat) 3 0 - ---let test1 = natIf3 _ 1 (Nil Nat) 3 0 - ---let natNil = Nil Nat - -let test2 = (natIf3 _) (Nil *) 2 3 0