(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/nf2/defs.ma".
+include "Basic-1/nf2/defs.ma".
-include "LambdaDelta-1/pr2/fwd.ma".
+include "Basic-1/pr2/fwd.ma".
theorem nf2_sort:
\forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
\lambda (c: C).(\lambda (n: nat).(\lambda (t2: T).(\lambda (H: (pr2 c (TSort
n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal
T (TSort n)) t2 (pr2_gen_sort c t2 n H))))).
+(* COMMENTS
+Initial nodes: 55
+END *)
theorem nf2_csort_lref:
\forall (n: nat).(\forall (i: nat).(nf2 (CSort n) (TLRef i)))
(lift (S i) O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T
(TLRef i) t)) (getl_gen_sort n i (CHead x0 (Bind Abbr) x1) H2 (eq T (TLRef i)
(lift (S i) O x1))) t2 H3))))) H1)) H0))))).
+(* COMMENTS
+Initial nodes: 355
+END *)
theorem nf2_abst:
\forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v:
(Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) u x0 t
x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 b v))) t2 H3))))))
H2)))))))))).
+(* COMMENTS
+Initial nodes: 299
+END *)
theorem nf2_abst_shift:
\forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (t: T).((nf2 (CHead c
(THead (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst)
u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2
H3)))))) H2)))))))).
+(* COMMENTS
+Initial nodes: 295
+END *)
theorem nfs2_tapp:
\forall (c: C).(\forall (t: T).(\forall (ts: TList).((nfs2 c (TApp ts t))
t1)) (nf2 c t)) (\lambda (H5: (nfs2 c t1)).(\lambda (H6: (nf2 c t)).(conj
(land (nf2 c t0) (nfs2 c t1)) (nf2 c t) (conj (nf2 c t0) (nfs2 c t1) H2 H5)
H6))) H4))))) H1)))))) ts))).
+(* COMMENTS
+Initial nodes: 295
+END *)
theorem nf2_appls_lref:
\forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs:
Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead (Bind x0) x5
(THead (Flat Appl) (lift (S O) O x4) x3))) H16))))))) t0 H_y H9) t2
H10))))))))))))) H7)) H6))))))) H2)))))) vs)))).
+(* COMMENTS
+Initial nodes: 2915
+END *)
theorem nf2_appl_lref:
\forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (i: nat).((nf2 c
\lambda (c: C).(\lambda (u: T).(\lambda (H: (nf2 c u)).(\lambda (i:
nat).(\lambda (H0: (nf2 c (TLRef i))).(let H_y \def (nf2_appls_lref c i H0
(TCons u TNil)) in (H_y (conj (nf2 c u) True H I))))))).
+(* COMMENTS
+Initial nodes: 49
+END *)
theorem nf2_lref_abst:
\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c
Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H (CHead x0 (Bind Abbr) x1)
H3)) in (False_ind (eq T (TLRef i) (lift (S i) O x1)) H6))) t2 H4))))) H2))
H1)))))))).
+(* COMMENTS
+Initial nodes: 494
+END *)
theorem nf2_lift:
\forall (d: C).(\forall (t: T).((nf2 d t) \to (\forall (c: C).(\forall (h:
(\lambda (t0: T).(pr2 d t t0)) H4 t H_y) in (eq_ind T t (\lambda (t0: T).(eq
T (lift h i t) (lift h i t0))) (refl_equal T (lift h i t)) x H_y))) t2 H3))))
H2)))))))))).
+(* COMMENTS
+Initial nodes: 245
+END *)