From 3b4ea42319085ec5dde6e7d402fa9b9cbb6a6271 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sun, 17 Nov 2024 19:06:52 +0100 Subject: [PATCH] allow more letters in identifiers (#333) - allow ' as first letter in an identifier (fix #328) - allow more letters in identifiers: + * ~ & ^ @ = $ % / < | \ - > The main modifs are in parsing/lexer.mll and parsing/menhir_parser.mly. Spaces are added in test files (e.g. writing A -> A instead of A->A). The error code for tests/KO/nsteps1.dk (`#EVAL[-1]`) is changed in tests/main.ml from lexing error to scoping error because '-' is now allowed in identifiers but the argument of `#EVAL` must be a non-negative integer. --- libraries/theories/fol.dk | 14 +- libraries/theories/ott.dk | 2 +- parsing/lexer.mll | 4 +- parsing/menhir_parser.mly | 4 +- tests/KO/SR_unsat_1.dk | 4 +- tests/KO/SR_unsat_2.dk | 4 +- tests/KO/SR_unsat_a1.dk | 4 +- tests/KO/SR_unsat_a2.dk | 4 +- tests/KO/SR_unsat_a2_2.dk | 4 +- tests/KO/SR_unsat_b1.dk | 4 +- tests/KO/SR_unsat_b2.dk | 4 +- tests/KO/SR_unsat_b3.dk | 4 +- tests/KO/SR_unsat_c1.dk | 4 +- tests/KO/SR_unsat_c2.dk | 4 +- tests/KO/SR_unsat_e1.dk | 4 +- tests/KO/SR_unsat_e2.dk | 4 +- tests/KO/SR_unsat_f1.dk | 4 +- tests/KO/def.dk | 2 +- tests/KO/typing_abstraction.dk | 2 +- tests/KO/unsound.dk | 4 +- tests/OK/SR_sat_bv1.dk | 790 ++++++++++++++++----------------- tests/OK/SR_sat_bv2.dk | 14 +- tests/OK/domainfree.dk | 4 +- tests/OK/dotpat.dk | 6 +- tests/OK/firstOrder.dk | 6 +- tests/OK/firstOrder_v2.dk | 12 +- tests/OK/fixpoints.dk | 12 +- tests/OK/higher_order_cstr3.dk | 50 +-- tests/main.ml | 2 +- 29 files changed, 491 insertions(+), 489 deletions(-) diff --git a/libraries/theories/fol.dk b/libraries/theories/fol.dk index 9f5a0e66..80bdf510 100644 --- a/libraries/theories/fol.dk +++ b/libraries/theories/fol.dk @@ -61,19 +61,19 @@ def and_elim_2 : A:Prop -> B:Prop -> prf (and A B) -> prf B := A:Prop => B:Prop => p:prf (and A B) => p B (a:prf A => b:prf B => b). (; Universal quantificator ;) -def forall_intro: P:(Term->Prop) -> (t:Term -> prf (P t)) -> prf (forall P) -:= P:(Term->Prop) => p:(t:Term -> prf (P t)) => p. +def forall_intro: P:(Term -> Prop) -> (t:Term -> prf (P t)) -> prf (forall P) +:= P:(Term -> Prop) => p:(t:Term -> prf (P t)) => p. -def forall_elim: P:(Term->Prop) -> t:Term -> p:prf (forall P) -> prf (P t) -:= P:(Term->Prop) => t:Term => p:prf (forall P) => p t. +def forall_elim: P:(Term -> Prop) -> t:Term -> p:prf (forall P) -> prf (P t) +:= P:(Term -> Prop) => t:Term => p:prf (forall P) => p t. (; Existential quantificator ;) -def exists_intro: P:(Term->Prop) -> t:Term -> prf (P t) -> prf (exists P) +def exists_intro: P:(Term -> Prop) -> t:Term -> prf (P t) -> prf (exists P) := P:(Term -> Prop) => t:Term => p:prf (P t) => A:Prop => f:(x:Term -> prf (P x) -> prf A) => f t p. -def exists_elim: P:(Term->Prop) -> Q:Prop -> prf (exists P) -> prf (forall (x : Term => imp (P x) Q)) -> prf Q -:= P:(Term->Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x : Term => imp (P x) Q)) +def exists_elim: P:(Term -> Prop) -> Q:Prop -> prf (exists P) -> prf (forall (x : Term => imp (P x) Q)) -> prf Q +:= P:(Term -> Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x : Term => imp (P x) Q)) => p1 Q p2. diff --git a/libraries/theories/ott.dk b/libraries/theories/ott.dk index 04d39075..d484de3b 100644 --- a/libraries/theories/ott.dk +++ b/libraries/theories/ott.dk @@ -177,7 +177,7 @@ coh : A : type -> B : type -> Q : Proof (EQ A B) -> a : term A -> b1 a1 (a0 a1 Qa) (Qb a1 (a0 a1 Qa) (H a1 Qa)) (x (a0 a1 Qa))) (fst (proof (EQ A1 A0)) (__ : Proof (EQ A1 A0) => - proof (all A1 (x1 : term A1=> all A0 (x0 : term A0 => + proof (all A1 (x1 : term A1 => all A0 (x0 : term A0 => imp (eq A1 x1 A0 x0) (EQ (B0 x0) (B1 x1)))))) Q) (a1 : term A1 => Q : Proof (EQ A1 A0) => coe A1 A0 Q a1) diff --git a/parsing/lexer.mll b/parsing/lexer.mll index a601766c..ad3a6b3e 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -21,9 +21,9 @@ } let space = [' ' '\t' '\r'] +let letter = ['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?' '\'' '+' '*' '~' '&' '^' '@' '=' '$' '%' '/' '<' '|' '-' '\\' '>'] let mident = ['a'-'z' 'A'-'Z' '0'-'9' '_']+ -let ident = ['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?']['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?' '\'' ]* -let capital = ['A'-'Z']+ +let ident = letter+ rule token = parse | space { token lexbuf } diff --git a/parsing/menhir_parser.mly b/parsing/menhir_parser.mly index 6d43200c..a9e908ed 100644 --- a/parsing/menhir_parser.mly +++ b/parsing/menhir_parser.mly @@ -27,7 +27,9 @@ let mk_config loc lid = | "CBN" when !strat = None -> strat := Some ByName | "CBV" when !strat = None -> strat := Some ByValue | "CBSV" when !strat = None -> strat := Some ByStrongValue - | i when !nb_steps = None -> nb_steps := Some (int_of_string i) + | i when !nb_steps = None -> + let n = int_of_string i in + if n < 0 then raise Exit else nb_steps := Some n | _ -> raise Exit in try List.iter proc lid; diff --git a/tests/KO/SR_unsat_1.dk b/tests/KO/SR_unsat_1.dk index 7a75fb34..f2762e03 100644 --- a/tests/KO/SR_unsat_1.dk +++ b/tests/KO/SR_unsat_1.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must* or *may* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a)) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t y ) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a)) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t y ) --> A. diff --git a/tests/KO/SR_unsat_2.dk b/tests/KO/SR_unsat_2.dk index a473dce9..a730c6af 100644 --- a/tests/KO/SR_unsat_2.dk +++ b/tests/KO/SR_unsat_2.dk @@ -15,5 +15,5 @@ def b : A -> A -> A. See SR_sat.dk for examples of satisfiable constraints. ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a)) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c a (c a y))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a)) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c a (c a y))) --> A. diff --git a/tests/KO/SR_unsat_a1.dk b/tests/KO/SR_unsat_a1.dk index 8fd951e0..89ade227 100644 --- a/tests/KO/SR_unsat_a1.dk +++ b/tests/KO/SR_unsat_a1.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must* or *may* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x y)) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (b x x)) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x y)) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (b x x)) --> A. diff --git a/tests/KO/SR_unsat_a2.dk b/tests/KO/SR_unsat_a2.dk index c97a901e..3b62a9c5 100644 --- a/tests/KO/SR_unsat_a2.dk +++ b/tests/KO/SR_unsat_a2.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must* or *may* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x y)) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y x))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x y)) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c x (Y x))) --> A. diff --git a/tests/KO/SR_unsat_a2_2.dk b/tests/KO/SR_unsat_a2_2.dk index 38a56edc..5174fc80 100644 --- a/tests/KO/SR_unsat_a2_2.dk +++ b/tests/KO/SR_unsat_a2_2.dk @@ -19,8 +19,8 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must* or *may* contain y ;) -def a2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c (c (c a x) a) (c a y))) -> Type. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y))) --> A. +def a2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c (c (c a x) a) (c a y))) -> Type. +[X,Y] a2 (x => y => X x y) (y => Y y) (x => y => t (c (Y x) (Y y))) --> A. (; From the following constraints: Y x = c (c a x) a Y y = c a y diff --git a/tests/KO/SR_unsat_b1.dk b/tests/KO/SR_unsat_b1.dk index b84d3a29..0fa62d6b 100644 --- a/tests/KO/SR_unsat_b1.dk +++ b/tests/KO/SR_unsat_b1.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must*, *may* or *may not* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (X (c y y) a))) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c y x)) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (X (c y y) a))) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c y x)) --> A. diff --git a/tests/KO/SR_unsat_b2.dk b/tests/KO/SR_unsat_b2.dk index 3f06402d..a48baac3 100644 --- a/tests/KO/SR_unsat_b2.dk +++ b/tests/KO/SR_unsat_b2.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must*, *may* or *may not* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (X (c y y) a))) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y y) y)) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (X (c y y) a))) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c (Y y) y)) --> A. diff --git a/tests/KO/SR_unsat_b3.dk b/tests/KO/SR_unsat_b3.dk index c7c3f797..1a729f0e 100644 --- a/tests/KO/SR_unsat_b3.dk +++ b/tests/KO/SR_unsat_b3.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must*, *may* or *may not* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (X (c y y) a))) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y y) (b y y))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (X (c y y) a))) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c (Y y) (b y y))) --> A. diff --git a/tests/KO/SR_unsat_c1.dk b/tests/KO/SR_unsat_c1.dk index 2322bc6e..3b71292e 100644 --- a/tests/KO/SR_unsat_c1.dk +++ b/tests/KO/SR_unsat_c1.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *may* or *may not* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (b x x))) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (c x y))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (b x x))) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c (Y x) (c x y))) --> A. diff --git a/tests/KO/SR_unsat_c2.dk b/tests/KO/SR_unsat_c2.dk index 6828b166..8c844297 100644 --- a/tests/KO/SR_unsat_c2.dk +++ b/tests/KO/SR_unsat_c2.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *may* or *may not* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (b x x))) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y y) (b x y))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (b x x))) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c (Y y) (b x y))) --> A. diff --git a/tests/KO/SR_unsat_e1.dk b/tests/KO/SR_unsat_e1.dk index 889b65fe..caed3cc6 100644 --- a/tests/KO/SR_unsat_e1.dk +++ b/tests/KO/SR_unsat_e1.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must*, *may* or *may not* contain x and *may* or *may not* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a )) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (c a y))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a )) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c (Y x) (c a y))) --> A. diff --git a/tests/KO/SR_unsat_e2.dk b/tests/KO/SR_unsat_e2.dk index 5401ba5c..548ba2af 100644 --- a/tests/KO/SR_unsat_e2.dk +++ b/tests/KO/SR_unsat_e2.dk @@ -19,5 +19,5 @@ def b : A -> A -> A. are convertible with terms that *must*, *may* or *may not* contain x and *may* or *may not* contain y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a )) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c y (c a y))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a )) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c y (c a y))) --> A. diff --git a/tests/KO/SR_unsat_f1.dk b/tests/KO/SR_unsat_f1.dk index abd705e7..29d8d9ef 100644 --- a/tests/KO/SR_unsat_f1.dk +++ b/tests/KO/SR_unsat_f1.dk @@ -18,5 +18,5 @@ def b : A -> A -> A. (; Terms that *may not* contain x or y are convertible with terms that *may* or *may not* contain x or y ;) -def d : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b a a)) -> Type. -[X,Y] d (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a y) (b a a))) --> A. +def d : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b a a)) -> Type. +[X,Y] d (x => y => X x y) (y => Y y) (x => y => t (c (c a y) (b a a))) --> A. diff --git a/tests/KO/def.dk b/tests/KO/def.dk index ecb64e35..2753c65e 100644 --- a/tests/KO/def.dk +++ b/tests/KO/def.dk @@ -1,3 +1,3 @@ A : Type. -P : A->Type. +P : A -> Type. def magic (a1:A) (a2:A) (H:P a1) : P a2 := H. diff --git a/tests/KO/typing_abstraction.dk b/tests/KO/typing_abstraction.dk index 6b54f22f..407870ca 100644 --- a/tests/KO/typing_abstraction.dk +++ b/tests/KO/typing_abstraction.dk @@ -1,6 +1,6 @@ A : Type. y : A. -P : A->Type. +P : A -> Type. p : P y. id : x:A -> P x -> P x. def T : P y. diff --git a/tests/KO/unsound.dk b/tests/KO/unsound.dk index 089b2995..5f8400b4 100644 --- a/tests/KO/unsound.dk +++ b/tests/KO/unsound.dk @@ -8,8 +8,8 @@ def A:Type. [] A --> Nat. -g:X->Nat. -f:Nat->X. +g:X -> Nat. +f:Nat -> X. def l1 := x:Nat => g (f x). def l2 := y:A => l1 y. diff --git a/tests/OK/SR_sat_bv1.dk b/tests/OK/SR_sat_bv1.dk index fe8749b7..293a7a61 100644 --- a/tests/OK/SR_sat_bv1.dk +++ b/tests/OK/SR_sat_bv1.dk @@ -19,45 +19,45 @@ def b : A -> A -> A. are convertible with terms that *must* or *may* contain x and *must* or *may* contain y ;) -def a1 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x y )) -> Type. -def a2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c (c (c a x) a) (c a y))) -> Type. +def a1 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x y )) -> Type. +def a2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c (c (c a x) a) (c a y))) -> Type. (; Terms that *must* contain x and *may* contain y are convertible with terms that *must* or *may* contain x and *must*, *may* or *may not* contain y ;) -def b1 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c x (X (c y y) a) )) -> Type. -def b2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c (c (b y y) a) (c a x))) -> Type. +def b1 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (X (c y y) a) )) -> Type. +def b2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c (c (b y y) a) (c a x))) -> Type. (; Terms that *must* contain x and *may not* contain y are convertible with terms that *must* or *may* contain x and *may* or *may not* contain y ;) -def c1 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T x ) -> Type. -def c2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c a (c a x) )) -> Type. -def c3 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c (c a x) (c a a))) -> Type. +def c1 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T x ) -> Type. +def c2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c a (c a x) )) -> Type. +def c3 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c (c a x) (c a a))) -> Type. (; Terms that *may* contain x and *may* contain y are convertible with terms that *must*, *may* or *may not* contain x and *must*, *may* or *may not* contain y ;) -def d1 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x y )) -> Type. -def d2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (X (c x x) y )) -> Type. -def d3 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c (Y y) (b x x))) -> Type. +def d1 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x y )) -> Type. +def d2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (X (c x x) y )) -> Type. +def d3 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c (Y y) (b x x))) -> Type. (; Terms that *may* contain x and *may not* contain y are convertible with terms that *must*, *may* or *may not* contain x and *may* or *may not* contain y ;) -def e1 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b x a )) -> Type. -def e2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (X a (c x x))) -> Type. +def e1 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b x a )) -> Type. +def e2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (X a (c x x))) -> Type. (; Terms that *may not* contain x or y are convertible with terms that *may* or *may not* contain x or y ;) -def f1 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T a ) -> Type. -def f2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (b a a)) -> Type. -def f3 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c a a)) -> Type. +def f1 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T a ) -> Type. +def f2 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (b a a)) -> Type. +def f3 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c a a)) -> Type. @@ -66,422 +66,422 @@ def f3 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c a a)) -> Type. (; ------------------------------------------------------------------------ ;) (; must / must ;) -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x y)) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x y)) --> A. (; must / may ;) -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y y) )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (X x y))) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b y y))) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b x y))) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b (c y a) y))) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b x (c y a)))) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b (X x y) a))) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b x (Y y)))) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y y) )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (X x y))) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b y y))) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b x y))) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b (c y a) y))) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b x (c y a)))) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b (X x y) a))) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b x (Y y)))) --> A. (; may / may ;) -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x y) (Y y) )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (X x y) )) --> A. -[X,Y] a1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (b (c y y) a) )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c (b x y) (Y y) )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c (b x x) (X x y) )) --> A. +[X,Y] a1 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (b (c y y) a) )) --> A. (; must / must ;) -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c (c a x) a) (c a y))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (c (c a x) a) (c a y))) --> A. (; must / may ;) -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (X x y))) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (b y y))) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (b y y))) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (b x y))) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (b (c y a) y))) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (b x (c y a)))) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (b (X x y) a))) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (b x (Y y)))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (X x y))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (b y y))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (b y y))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (b x y))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x x) (b (c y a) y))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x x) (b x (c y a)))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x x) (b (X x y) a))) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x x) (b x (Y y)))) --> A. (; may / may ;) -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (X x y) )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x y) (Y y) )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (X x y) )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (b (c y y) a) )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (X x y) )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x y) (Y y) )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x x) (X x y) )) --> A. +[X,Y] a2 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (b (c y y) a) )) --> A. (; must / must ;) -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x y)) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x y)) --> A. (; must / may ;) -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y y) )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b y y))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (X x y))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b x y))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b a (c a (c (b a y) x))))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b x (c a (c (b x (c y a)) a))))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b a (c a (c (X x y) a))))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b a (c a (c (Y y) a))))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y y) )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b y y))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (X x y))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b x y))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b a (c a (c (b a y) x))))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b x (c a (c (b x (c y a)) a))))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b a (c a (c (X x y) a))))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b a (c a (c (Y y) a))))) --> A. (; must / may not;) -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x a)) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b a a))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b a (c x x)))) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y x))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x a)) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b a a))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b a (c x x)))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y x))) --> A. (; may / may ;) -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (c (X x y) a) )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (Y y) )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a x) (X x y) )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (c a a) )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (c (X x y) a) )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c (b x x) (Y y) )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c (b a x) (X x y) )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] b1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] b1 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; must / may ;) -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y y) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y y) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x y) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a (c a (c (b a y) x))) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x (c a (c (b x (c y a)) a))) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a (c a (c (X x y) a))) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a (c a (c (Y y) a))) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y y) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b y y) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x y) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b a (c a (c (b a y) x))) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b x (c a (c (b x (c y a)) a))) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b a (c a (c (X x y) a))) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b a (c a (c (Y y) a))) (c a x))) --> A. (; must / may not;) -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b (c a a) a) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a a) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a (c x x)) (c a x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b (c a a) a) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b a a) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (b a (c x x)) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (c a x))) --> A. (; may / may ;) -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c (X x y) a) (Y x))) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) (Y x) )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y y) (b x x) )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) (b a x) )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (b y x) )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (c (X x y) a) (Y x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) (Y x) )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y y) (b x x) )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) (b a x) )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (b y x) )) --> A. (; may / may not ;) -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (Y x) )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (Y x) )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] b2 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; must / may not;) -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t x) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t x) --> A. (; may / may ;) -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a (c (X x y) a) )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y x) (Y y) )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b x y) (Y y) )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (X y x) (X x y) )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y x) (c a a) )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b a (c (X x y) a) )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y x) (Y y) )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (b x y) (Y y) )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (X y x) (X x y) )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y x) a )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] c1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y x) a )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] c1 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; must / may not;) -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a (c a x) )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (c a (c a x) )) --> A. (; may / may ;) -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a (c (X x y) a) )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y x) (Y y) )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b x y) (Y y) )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (X y x) (X x y) )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y x) (c a a) )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b a (c (X x y) a) )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y x) (Y y) )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (b x y) (Y y) )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (X y x) (X x y) )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y x) a )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] c2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y x) a )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] c2 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; must / may not;) -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a x) (c a a) )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (c (c a x) (c a a) )) --> A. (; may / may ;) -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a (c (X x y) a) )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y x) (Y y) )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b x y) (Y y) )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (X y x) (X x y) )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y x) (c a a) )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b a (c (X x y) a) )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (Y x) (Y y) )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (b x y) (Y y) )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (X y x) (X x y) )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y x) a )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] c3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (Y x) a )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] c3 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; must / must ;) -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x y)) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c y x)) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x (c y x))))) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a (c x a)) (c a (c a (c a y))))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c x y)) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c y x)) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x (c y x))))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a (c x a)) (c a (c a (c a y))))) --> A. (; must / may ;) -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y y) )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b y y))) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a y) x)) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) x)) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y y) )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b y y))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (b a y) x)) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) x)) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. (; must / may not;) -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a x)) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x x)) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t x) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y x))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c a x)) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c x x)) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t x) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y x))) --> A. (; may / may ;) -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a (c (X x y) a) )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y y) (Y y) )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (X x y) )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (c a a) )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c a (c (X x y) a) )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (b y y) (Y y) )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (X x y) )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t a ) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a a )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] d1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t a ) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (c a a )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] d1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. (; must / must ;) -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x y)) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c y x)) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x (c y x))))) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a (c x a)) (c a (c a (c a y))))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c x y)) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c y x)) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x (c y x))))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a (c x a)) (c a (c a (c a y))))) --> A. (; must / may ;) -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y y) )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b y y))) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a y) x)) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) x)) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y y) )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c x (b y y))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (b a y) x)) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) x)) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. (; must / may not;) -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a x)) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x x)) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t x) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y x))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c a x)) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c x x)) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t x) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y x))) --> A. (; may / may ;) -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a (c (X x y) a) )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y y) (Y y) )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (X x y) )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (c a a) )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c a (c (X x y) a) )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (b y y) (Y y) )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (X x y) )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t a ) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a a )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] d2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t a ) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (c a a )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] d2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. (; may / may ;) -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y y) (Y y) )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (X x y) )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (c a a) )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (c (b y y) (Y y) )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (X x y) )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] d3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] d3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. (; must / may ;) -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y y) )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b y y))) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a y) x)) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) x)) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y y) )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c x (b y y))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (b a y) x)) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) x)) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. (; must / may not;) -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a x)) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x x)) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t x) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y x))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c a x)) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c x x)) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t x) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y x))) --> A. (; may / may ;) -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a (c (X x y) a) )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y y) (Y y) )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (X x y) )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (c a a) )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c a (c (X x y) a) )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (b y y) (Y y) )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (X x y) )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t a ) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a a )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] e1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t a ) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (c a a )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] e1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. (; must / may ;) -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y y) )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b y y))) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a y) x)) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) x)) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y y) )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c x (b y y))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (b a y) x)) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) x)) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. (; must / may not;) -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a x)) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x x)) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t x) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y x))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c a x)) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c x x)) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t x) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c x (Y x))) --> A. (; may / may ;) -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a (c (X x y) a) )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y y) (Y y) )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (X x y) )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (c a a) )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c a (c (X x y) a) )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (b y y) (Y y) )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (X x y) )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t a ) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a a )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] e2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t a ) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (c a a )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] e2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. (; may / may ;) -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. (; may / may not ;) -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t a ) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] f1 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t a ) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] f1 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. (; may / may ;) -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. (; may / may not ;) -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t a ) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a a )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] f2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t a ) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (c a a )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] f2 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. (; may / may ;) -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. (; may / may not ;) -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (c a a )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] f3 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (c a a )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] f3 (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. @@ -528,52 +528,52 @@ def g7:(x:A -> T (b (b (c a x) a) a)) -> Type. (; (; must / must ;) -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c x y)) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c y x)) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x (c y x))))) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a (c x a)) (c a (c a (c a y))))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c x y)) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c y x)) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x (c y x))))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c a (c x a)) (c a (c a (c a y))))) --> A. (; must / may ;) -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y y) )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (b y y))) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b a y) x)) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) x)) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c x (Y y) )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c x (b y y))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (b a y) x)) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (X x y) x)) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c a (c (b a y) x))))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c x (c a (c (b x (c y a)) a))))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c x a) (c a (c a (c (X x y) a))))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c a x) (c a (c a (c (Y y) a))))) --> A. (; must / may not;) -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c a x)) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c x x)) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t x) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c x (Y x))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c a x)) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c x x)) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t x) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (c a (c x x)))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c x (Y x))) --> A. (; may / may ;) -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b x y )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (X x y )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c a (c (X x y) a) )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y y) (Y y) )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (X x y) )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (c a a) )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b x y )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (X x y )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c a (c (X x y) a) )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b (c a x) y )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b (b y y) x )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b (Y y) x )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (b y y) (Y y) )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (c a a) (X x y) )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (b y x) (c a a) )) --> A. (; may / may not ;) -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b x a )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b a x )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (Y x )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) a )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) x )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b a a) (c a x))) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b x a )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b a x )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (Y x )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c (Y x) a )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) x )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b (b a a) (c a x))) --> A. (; may not / may not ;) -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t a ) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (c a a )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b a a )) --> A. -[X,Y] xx (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a a) a)) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t a ) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (c a a )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b a a )) --> A. +[X,Y] xx (x => y => X x y) (y => Y y) ( x => y => t (b (c a a) a)) --> A. ;) diff --git a/tests/OK/SR_sat_bv2.dk b/tests/OK/SR_sat_bv2.dk index 3bbf339a..53138246 100644 --- a/tests/OK/SR_sat_bv2.dk +++ b/tests/OK/SR_sat_bv2.dk @@ -20,7 +20,7 @@ def b': A -> A -> A. are convertible with terms that *must* or *may* contain x and *must* or *may* contain y ;) -def a1 : X:(A->A->A) -> Y:(A->A) -> +def a1 : X:(A -> A -> A) -> Y:(A -> A) -> (x:A -> y:A -> T (c x (c y @@ -29,7 +29,7 @@ def a1 : X:(A->A->A) -> Y:(A->A) -> (c (b x y) (b a a))))))) -> Type. -[X,Y] a1 (x=>y=>X x y) (x=>Y x) (x=>y=>t +[X,Y] a1 (x => y => X x y) (x => Y x) (x => y => t (c x (c y (c (b x x) @@ -37,7 +37,7 @@ def a1 : X:(A->A->A) -> Y:(A->A) -> (c (b x y) (b a a))))))) --> A. -[X,Y] a1 (x=>y=>X x y) (x=>Y x) (x=>y=>t +[X,Y] a1 (x => y => X x y) (x => Y x) (x => y => t (c (b a (c x x)) (c (Y y) (c (b' (c x x) a) @@ -45,7 +45,7 @@ def a1 : X:(A->A->A) -> Y:(A->A) -> (c (b' (c x x) (b y y)) (b' x y))))))) --> A. -[X,Y] a1 (x=>y=>X x y) (x=>Y x) (x=>y=>t +[X,Y] a1 (x => y => X x y) (x => Y x) (x => y => t (c (X x y) (c (b (c y y) (c x x)) (c x @@ -57,7 +57,7 @@ def a1 : X:(A->A->A) -> Y:(A->A) -> are convertible with terms that *must* or *may* contain x and *must* or *may* contain y ;) -def a2 : X1:(A->A->A) -> X2:(A->A->A) -> X3:(A->A->A) -> X4:(A->A->A) -> +def a2 : X1:(A -> A -> A) -> X2:(A -> A -> A) -> X3:(A -> A -> A) -> X4:(A -> A -> A) -> (x:A -> y:A -> T (c x (c y @@ -67,8 +67,8 @@ def a2 : X1:(A->A->A) -> X2:(A->A->A) -> X3:(A->A->A) -> X4:(A->A->A) -> (X4 a a))))))) -> Type. -def b1 : X:(A->A->A) -> Y:(A->A) -> - (x:A -> y:A -> f : (A->A->A) -> +def b1 : X:(A -> A -> A) -> Y:(A -> A) -> + (x:A -> y:A -> f : (A -> A -> A) -> T (f (c x y) (f (c (b x x) (b a y)) diff --git a/tests/OK/domainfree.dk b/tests/OK/domainfree.dk index 82cd9f78..633f38e1 100644 --- a/tests/OK/domainfree.dk +++ b/tests/OK/domainfree.dk @@ -1,3 +1,3 @@ A:Type. -F:(A->A)->A. -def f := F (x=>x). +F:(A -> A) -> A. +def f := F (x => x). diff --git a/tests/OK/dotpat.dk b/tests/OK/dotpat.dk index 873b228d..f37cde2e 100644 --- a/tests/OK/dotpat.dk +++ b/tests/OK/dotpat.dk @@ -1,13 +1,13 @@ N: Type. Z: N. -S: N->N. +S: N -> N. -def plus: N->N->N. +def plus: N -> N -> N. [y] plus Z y --> y [x,y] plus (S x) y --> S (plus x y). -V: N->Type. +V: N -> Type. Nil: V Z. Con: n:N -> V n -> N -> V (S n). diff --git a/tests/OK/firstOrder.dk b/tests/OK/firstOrder.dk index 0340de81..6915bd03 100644 --- a/tests/OK/firstOrder.dk +++ b/tests/OK/firstOrder.dk @@ -43,6 +43,6 @@ DeMorgan2 : A:Prop -> B:Prop -> prf (imp (or A B) (not (and (not A) (not B)))). U:Type. -forall : (U->Prop) -> Prop. -forall_intro : P:(U->Prop) -> (x:U -> prf (P x)) -> prf (forall P). -forall_elim : P:(U->Prop) -> prf (forall P) -> x:U -> prf (P x). +forall : (U -> Prop) -> Prop. +forall_intro : P:(U -> Prop) -> (x:U -> prf (P x)) -> prf (forall P). +forall_elim : P:(U -> Prop) -> prf (forall P) -> x:U -> prf (P x). diff --git a/tests/OK/firstOrder_v2.dk b/tests/OK/firstOrder_v2.dk index 2440e977..cbd6b8d6 100644 --- a/tests/OK/firstOrder_v2.dk +++ b/tests/OK/firstOrder_v2.dk @@ -58,15 +58,15 @@ def and_elim_2 : A:Prop -> B:Prop -> prf (and A B) -> prf B lem B B (q:prf B => q) (q:prf (not B) => false_elim B (p (x:prf A => q))). (; Universal quantificator ;) -def forall_intro: P:(Term->Prop) -> (t:Term -> prf (P t)) -> prf (forall P) -:= P:(Term->Prop) => p:(t:Term -> prf (P t)) => p. +def forall_intro: P:(Term -> Prop) -> (t:Term -> prf (P t)) -> prf (forall P) +:= P:(Term -> Prop) => p:(t:Term -> prf (P t)) => p. -def forall_elim: P:(Term->Prop) -> t:Term -> p:prf (forall P) -> prf (P t) -:= P:(Term->Prop) => t:Term => p:prf (forall P) => p t. +def forall_elim: P:(Term -> Prop) -> t:Term -> p:prf (forall P) -> prf (P t) +:= P:(Term -> Prop) => t:Term => p:prf (forall P) => p t. (; Existential quantificator ;) -def exists_intro: P:(Term->Prop) -> t:Term -> prf (P t) -> prf (exists P) +def exists_intro: P:(Term -> Prop) -> t:Term -> prf (P t) -> prf (exists P) := P:(Term -> Prop) => t:Term => p:prf (P t) => q:prf (forall (u:Term => not (P u))) => q t p. e: (Term -> Prop) -> Term. (;Hilbert operator;) -exists_elim: P:(Term->Prop) -> prf (exists P) -> prf (P (e P)). +exists_elim: P:(Term -> Prop) -> prf (exists P) -> prf (P (e P)). diff --git a/tests/OK/fixpoints.dk b/tests/OK/fixpoints.dk index f76d0191..a4534d60 100644 --- a/tests/OK/fixpoints.dk +++ b/tests/OK/fixpoints.dk @@ -1055,10 +1055,10 @@ def plus : y : T set nat -> T set nat := fixproj set 1 - (c=>c + (c => c (SA 0 set (prod set set set I nat (x => prod set set set I nat (y => nat))))) - (c=>c + (c => c (plus => x => y => match____nat set (x0 : T set nat => nat) y (x' : T set nat => Succ (plus x' y)) x)) @@ -1076,10 +1076,10 @@ def times : y : T set nat -> T set nat := fixproj set 1 - (c=>c + (c => c (SA 0 set (prod set set set I nat (x => prod set set set I nat (y => nat))))) - (c=>c + (c => c (times => x => y => match____nat set (x0 : T set nat => nat) Z (x' : T set nat => plus y (times x' y)) x)) @@ -1187,11 +1187,11 @@ def vect__rect : T (type z) (P (Succ n) (cons n n0 v))) => fixproj (type z) 1 - (c=>c + (c => c (SA 0 (type z) (prod set (type z) (type z) I nat (n => prod set (type z) (type z) I (vect n) (v => P n v))))) - (c=>c + (c => c (vect__rect => n => v => match____vect (type z) (n0 : T set nat => v0 : T set (vect n0) => P n0 v0) diff --git a/tests/OK/higher_order_cstr3.dk b/tests/OK/higher_order_cstr3.dk index 8e891088..7e269086 100644 --- a/tests/OK/higher_order_cstr3.dk +++ b/tests/OK/higher_order_cstr3.dk @@ -9,69 +9,69 @@ def R : A -> A -> Type. [x] R a x --> T x. -def f1 : x:(A->A) -> (z:A -> T (x z)) -> (z:A -> T (x z)). +def f1 : x:(A -> A) -> (z:A -> T (x z)) -> (z:A -> T (x z)). [x] f1 x (z => t a) --> z => t a. -def f2 : x:(A->A) -> (z:A -> T (x z)) -> T (x b). +def f2 : x:(A -> A) -> (z:A -> T (x z)) -> T (x b). [x] f2 x (z => t a) --> t a. -def f3 : x:(A->A) -> (z:A -> T (x z)) -> (z:A -> T (x z)). +def f3 : x:(A -> A) -> (z:A -> T (x z)) -> (z:A -> T (x z)). [x] f3 x (z => t z) --> z => t z. -def f4 : x:(A->A) -> (z:A -> T (x z)) -> T (x b). +def f4 : x:(A -> A) -> (z:A -> T (x z)) -> T (x b). [x] f4 x (z => t z) --> t b. -def g1 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z:A -> T (y z). +def g1 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z:A -> T (y z). [x,y] g1 x y (z => t a) (z => t a) --> z => t a. -def g2 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). +def g2 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). [x,y] g2 x y (z => t a) (z => t a) --> t a. -def g3 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z:A -> T (y z). +def g3 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z:A -> T (y z). [x,y] g3 x y (z => t z) (z => t a) --> z => t z. -def g4 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). +def g4 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). [x,y] g4 x y (z => t z) (z => t a) --> t b. -def h1 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). +def h1 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). [x,y] h1 (z => x z) y (z => t a) (z => t (x z)) --> z => t a. -def h2 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). +def h2 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). [x,y] h2 (z => x z) y (z => t a) (z => t (x z)) --> t a. -def h3 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). +def h3 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). [x,y] h3 (z => x z) y (z => t z) (z => t (x z)) --> z => t z. -def h4 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). -[x,y] h4 (z=>x z) y (z => t z) (z => t (x z)) --> t b. +def h4 : x:(A -> A) -> y:(A -> A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). +[x,y] h4 (z => x z) y (z => t z) (z => t (x z)) --> t b. -def g'1 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +def g'1 : x:(A -> A) -> y:(A -> A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). [x,y] g'1 x y (z => t a) (z => t a) --> z => t a. -def g'2 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). +def g'2 : x:(A -> A) -> y:(A -> A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). [x,y] g'2 x y (z => t a) (z => t a) --> t a. -def g'3 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +def g'3 : x:(A -> A) -> y:(A -> A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). [x,y] g'3 x y (z => t a) (z => t z) --> z => t z. -def g'4 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). +def g'4 : x:(A -> A) -> y:(A -> A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). [x,y] g'4 x y (z => t a) (z => t z) --> t b. -def h'1 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). -[x,y] h'1 (z=>x z) y (z => t (x z)) (z => t a) --> z => t a. +def h'1 : x:(A -> A) -> y:(A -> A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +[x,y] h'1 (z => x z) y (z => t (x z)) (z => t a) --> z => t a. -def h'2 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). -[x,y] h'2 (z=>x z) y (z => t (x z)) (z => t a) --> t a. +def h'2 : x:(A -> A) -> y:(A -> A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). +[x,y] h'2 (z => x z) y (z => t (x z)) (z => t a) --> t a. -def h'3 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). -[x,y] h'3 (z=>x z) y (z => t (x z)) (z => t z) --> z => t z. +def h'3 : x:(A -> A) -> y:(A -> A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +[x,y] h'3 (z => x z) y (z => t (x z)) (z => t z) --> z => t z. -def h'4 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). -[x,y] h'4 (z=>x z) y (z => t (x z)) (z => t z) --> t b. +def h'4 : x:(A -> A) -> y:(A -> A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). +[x,y] h'4 (z => x z) y (z => t (x z)) (z => t z) --> t b. diff --git a/tests/main.ml b/tests/main.ml index f706f4a3..44319283 100644 --- a/tests/main.ml +++ b/tests/main.ml @@ -228,7 +228,7 @@ module Check = struct ko ~error:(`Code 701) ~basename:"nested_comments_2.dk" []; ko ~error:(`Code 101) ~basename:"noninjectivity.dk" []; ko ~error:(`Code 507) ~basename:"nonleftlinear.dk" [Left_linear]; - ko ~error:(`Code 701) ~basename:"nsteps1.dk" []; + ko ~error:(`Code 703) ~basename:"nsteps1.dk" []; ko ~error:(`Code 702) ~basename:"parsing_eof.dk" []; ko ~error:(`Code 104) ~basename:"product_expected_6.dk" []; ko ~error:(`Code 403) ~basename:"prv_fail_1.dk" [Import "tests/LIB"];