(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/ex1/defs.ma".
+include "Basic-1/ex1/defs.ma".
-include "LambdaDelta-1/ty3/fwd.ma".
+include "Basic-1/ty3/fwd.ma".
-include "LambdaDelta-1/pc3/fwd.ma".
+include "Basic-1/pc3/fwd.ma".
-include "LambdaDelta-1/nf2/pr3.ma".
+include "Basic-1/nf2/pr3.ma".
-include "LambdaDelta-1/nf2/props.ma".
+include "Basic-1/nf2/props.ma".
-include "LambdaDelta-1/arity/defs.ma".
+include "Basic-1/arity/defs.ma".
-include "LambdaDelta-1/leq/props.ma".
+include "Basic-1/leq/props.ma".
theorem ex1__leq_sort_SS:
\forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc
\def
\lambda (g: G).(\lambda (k: nat).(\lambda (n: nat).(leq_refl g (asucc g
(asucc g (ASort (S (S k)) n)))))).
+(* COMMENTS
+Initial nodes: 27
+END *)
theorem ex1_arity:
\forall (g: G).(arity g ex1_c ex1_t (ASort O O))
O))) (ex1__leq_sort_SS g O O))) (TSort O) (ASort O O) (arity_sort g (CHead
(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O))
(Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) O))).
+(* COMMENTS
+Initial nodes: 753
+END *)
theorem ex1_ty3:
\forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P:
(TLRef O)) x0 O H2))))))) (ty3_gen_appl g (CHead (CHead (CHead (CSort O)
(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef
O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) u H))))).
+(* COMMENTS
+Initial nodes: 9973
+END *)