(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/sn3/nf2.ma".
+include "Basic-1/sn3/nf2.ma".
-include "LambdaDelta-1/sn3/fwd.ma".
+include "Basic-1/sn3/fwd.ma".
-include "LambdaDelta-1/nf2/iso.ma".
+include "Basic-1/nf2/iso.ma".
-include "LambdaDelta-1/pr3/iso.ma".
+include "Basic-1/pr3/iso.ma".
theorem sn3_pr3_trans:
\forall (c: C).(\forall (t1: T).((sn3 c t1) \to (\forall (t2: T).((pr3 c t1
H3 t2 H6) in (let H9 \def (eq_ind_r T t3 (\lambda (t: T).(pr3 c t2 t)) H2 t2
H6) in (H0 t0 H8 H7))))) (\lambda (H6: (((eq T t2 t3) \to (\forall (P:
Prop).P)))).(H1 t3 H6 H2 t0 H4)) H5)))))))))))) t1 H))).
+(* COMMENTS
+Initial nodes: 289
+END *)
theorem sn3_pr2_intro:
\forall (c: C).(\forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to
T).(pr2 c t t3)) H4 t3 H10) in (H6 H12 H11))))) (\lambda (H10: (((eq T t4 t3)
\to (\forall (P: Prop).P)))).(sn3_pr3_trans c t3 (H7 t3 H10 H4) t5 H5))
H9))))))))))) t1 t2 H1 H3)) H2)))))))).
+(* COMMENTS
+Initial nodes: 467
+END *)
theorem sn3_cast:
\forall (c: C).(\forall (u: T).((sn3 c u) \to (\forall (t: T).((sn3 c t) \to
H11))) H15))))) H13))) t2 H9))))))) H8)) (\lambda (H8: (pr2 c t0
t2)).(sn3_pr3_trans c t0 (sn3_sing c t0 H3) t2 (pr3_pr2 c t0 t2 H8)))
H7))))))))) t H2)))))) u H))).
+(* COMMENTS
+Initial nodes: 1239
+END *)
theorem sn3_cflat:
\forall (c: C).(\forall (t: T).((sn3 c t) \to (\forall (f: F).(\forall (u:
(\lambda (t2: T).(\lambda (H2: (((eq T t1 t2) \to (\forall (P:
Prop).P)))).(\lambda (H3: (pr2 (CHead c (Flat f) u) t1 t2)).(H1 t2 H2
(pr3_pr2 c t1 t2 (pr2_gen_cflat f c u t1 t2 H3)))))))))) t H))))).
+(* COMMENTS
+Initial nodes: 175
+END *)
theorem sn3_shift:
\forall (b: B).(\forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c
H0 \def H_x in (land_ind (sn3 c v) (sn3 (CHead c (Bind b) v) t) (sn3 (CHead c
(Bind b) v) t) (\lambda (_: (sn3 c v)).(\lambda (H2: (sn3 (CHead c (Bind b)
v) t)).H2)) H0))))))).
+(* COMMENTS
+Initial nodes: 95
+END *)
theorem sn3_change:
\forall (b: B).((not (eq B b Abbr)) \to (\forall (c: C).(\forall (v1:
Prop).P)))).(\lambda (H4: (pr2 (CHead c (Bind b) v2) t1 t2)).(H2 t2 H3
(pr3_pr2 (CHead c (Bind b) v1) t1 t2 (pr2_change b H c v2 t1 t2 H4
v1)))))))))) t H0))))))).
+(* COMMENTS
+Initial nodes: 239
+END *)
theorem sn3_gen_def:
\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
(pr3_pr2 c (TLRef i) (lift (S i) O v) (pr2_delta c d v i H (TLRef i) (TLRef
i) (pr0_refl (TLRef i)) (lift (S i) O v) (subst0_lref v i)))) d (getl_drop
Abbr c d v i H))))))).
+(* COMMENTS
+Initial nodes: 139
+END *)
theorem sn3_cdelta:
\forall (v: T).(\forall (t: T).(\forall (i: nat).(((\forall (w: T).(ex T
(Bind Abbr) v0))).(\lambda (H7: (sn3 c (THead k u1 t1))).(let H_y \def
(sn3_gen_head k c u1 t1 H7) in (H3 c d H6 H_y))))))))))))))))) i v t x H1)))
H0)))))).
+(* COMMENTS
+Initial nodes: 949
+END *)
theorem sn3_cpr3_trans:
\forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall
t2)))))).(sn3_sing (CHead c k u2) t1 (\lambda (t2: T).(\lambda (H3: (((eq T
t1 t2) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr3 (CHead c k u2) t1
t2)).(H2 t2 H3 (pr3_pr3_pr3_t c u1 u2 H t1 t2 k H4))))))))) t H0))))))).
+(* COMMENTS
+Initial nodes: 203
+END *)
theorem sn3_bind:
\forall (b: B).(\forall (c: C).(\forall (u: T).((sn3 c u) \to (\forall (t:
(Bind b) t1) t2 (sn3_sing (CHead c (Bind b) t1) t2 H3) (lift (S O) O t3) H10)
c (drop_drop (Bind b) O c c (drop_refl c) t1))) H9)))) H7)))))))))) t
H2)))))) u H)))).
+(* COMMENTS
+Initial nodes: 2401
+END *)
theorem sn3_beta:
\forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c (THead (Bind Abbr) v
False).(sn3 c (THead (Bind Abst) x6 (THead (Flat Appl) (lift (S O) O x5)
x4)))) with []) in H29) x1 H24)))))))) H21)) H20)) t3 H15)))))))))))))) H12))
H11))))))))) w H4))))))))))) y H0))))) H)))).
+(* COMMENTS
+Initial nodes: 5699
+END *)
theorem sn3_appl_lref:
\forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (v:
False])) I (THead (Bind x0) x1 x2) H8) in (False_ind (sn3 c (THead (Bind x0)
x5 (THead (Flat Appl) (lift (S O) O x4) x3))) H14)) t2 H9)))))))))))))) H6))
H5))))))))) v H0))))).
+(* COMMENTS
+Initial nodes: 2125
+END *)
theorem sn3_appl_abbr:
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(THead (Bind x0) x1 x2) H12) in (False_ind (sn3 c (THead (Bind x0) x5 (THead
(Flat Appl) (lift (S O) O x4) x3))) H18)) t2 H13)))))))))))))) H10))
H9))))))))))))) y H1)))) H0))))))).
+(* COMMENTS
+Initial nodes: 3727
+END *)
theorem sn3_appl_cast:
\forall (c: C).(\forall (v: T).(\forall (u: T).((sn3 c (THead (Flat Appl) v
H18) in (False_ind (sn3 c (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O)
O x6) x5))) H24)) t2 H19)))))))))))))) H16)) H15))))))))))))))) y0 H5))))
H4))))))))) y H0))))) H)))).
+(* COMMENTS
+Initial nodes: 5149
+END *)
theorem sn3_appl_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u:
x5) x4)) (pr2_head_1 c t1 x6 H27 (Bind b) (THead (Flat Appl) (lift (S O) O
x5) x4)))) x1 H25))))))) H22)) H21)) t3 H16)))))))))))))) H13))
H12)))))))))))))) y H4))))) H3))))))) u H0))))).
+(* COMMENTS
+Initial nodes: 9191
+END *)
theorem sn3_appl_appl:
\forall (v1: T).(\forall (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
H17) in (False_ind (sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O)
O x5) x4))) H23)) t3 H18)))))))))))))) H15)) H14)))))) t2 H3))))))))) v2
H4))))))))) y H0))))) H))))).
+(* COMMENTS
+Initial nodes: 9317
+END *)
theorem sn3_appl_beta:
\forall (c: C).(\forall (u: T).(\forall (v: T).(\forall (t: T).((sn3 c
Appl) u (THead (Bind Abbr) v t)) H (THead (Flat Appl) u u2) (pr3_thin_dx c
(THead (Bind Abbr) v t) u2 (pr3_iso_beta v w t c u2 H4 H5) u Appl))))))))
H1))))))))).
+(* COMMENTS
+Initial nodes: 289
+END *)
theorem sn3_appl_appls:
\forall (v1: T).(\forall (t1: T).(\forall (vs: TList).(let u1 \def (THeads
(Flat Appl) vs t1)) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
Appl) v2 u2))))))).(sn3_appl_appl v1 (THeads (Flat Appl) vs t1) c H v2 H0
H1))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
theorem sn3_appls_lref:
\forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (us:
(TCons t1 t2) (TLRef i)) u2) \to (\forall (P: Prop).P)))).(H9
(nf2_iso_appls_lref c i H (TCons t1 t2) u2 H8) (sn3 c (THead (Flat Appl) t
u2))))))))) H5))) H3))))))) t0))) us)))).
+(* COMMENTS
+Initial nodes: 577
+END *)
theorem sn3_appls_cast:
\forall (c: C).(\forall (vs: TList).(\forall (u: T).((sn3 c (THeads (Flat
t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat Appl)
(TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11 H12) t
Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
+(* COMMENTS
+Initial nodes: 1025
+END *)
theorem sn3_appls_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u:
t1) v H3) (THead (Flat Appl) v u2) (pr3_flat c v v (pr3_refl c v) (THead
(Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)) u2 H9
Appl)))))))))) H4))))))))) vs0))) vs)))))).
+(* COMMENTS
+Initial nodes: 1143
+END *)
theorem sn3_appls_beta:
\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (us: TList).((sn3 c
(THead (Flat Appl) u (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v
t))) H1 (THead (Flat Appl) u u2) (pr3_thin_dx c (THeads (Flat Appl) (TCons t0
t1) (THead (Bind Abbr) v t)) u2 H8 u Appl))))))))) H3)))))))))) us0))) us)))).
+(* COMMENTS
+Initial nodes: 987
+END *)
theorem sn3_lift:
\forall (d: C).(\forall (t: T).((sn3 d t) \to (\forall (c: C).(\forall (h:
H11 \def (eq_ind_r T x (\lambda (t0: T).(pr2 d t1 t0)) H7 t1 H9) in (H10
(refl_equal T (lift h i t1)) P))))) (pr3_pr2 d t1 x H7) c h i H2) t2 H6)))))
H5))))))))))))) t H))).
+(* COMMENTS
+Initial nodes: 439
+END *)
theorem sn3_abbr:
\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
(eq_ind_r C x0 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) v))) H12 d
H11) in (sn3_lift d v H0 c (S i) O (getl_drop Abbr c d v i H13))) x1 H10))))
H9))) t2 H6)))))) H4)) H3))))))))))).
+(* COMMENTS
+Initial nodes: 743
+END *)
theorem sn3_appls_abbr:
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(pr3_thin_dx c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
(pr3_iso_appls_abbr c d w i H (TCons t t0) u2 H6 H7) v Appl))))))))
H3)))))))) vs0))) vs)))))).
+(* COMMENTS
+Initial nodes: 797
+END *)
theorem sns3_lifts:
\forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h
(lifts h i t0))) (\lambda (H3: (sn3 d t)).(\lambda (H4: (sns3 d t0)).(conj
(sn3 c (lift h i t)) (sns3 c (lifts h i t0)) (sn3_lift d t H3 c h i H) (H0
H4)))) H2)))))) ts)))))).
+(* COMMENTS
+Initial nodes: 185
+END *)