DEFINITION sn3_cast()
TYPE =
∀c:C.∀u:T.(sn3 c u)→∀t:T.(sn3 c t)→(sn3 c (THead (Flat Cast) u t))
BODY =
assume c: C
assume u: T
suppose H: sn3 c u
we proceed by induction on H to prove ∀t0:T.(sn3 c t0)→(sn3 c (THead (Flat Cast) u t0))
case sn3_sing : t1:T :∀t2:T.((eq T t1 t2)→∀P:Prop.P)→(pr3 c t1 t2)→(sn3 c t2) ⇒
the thesis becomes ∀t:T.∀H2:(sn3 c t).(sn3 c (THead (Flat Cast) t1 t))
(H1) by induction hypothesis we know
∀t2:T
.(eq T t1 t2)→∀P:Prop.P
→(pr3 c t1 t2)→∀t:T.(sn3 c t)→(sn3 c (THead (Flat Cast) t2 t))
assume t: T
suppose H2: sn3 c t
we proceed by induction on H2 to prove sn3 c (THead (Flat Cast) t1 t)
case sn3_sing : t0:T H3:∀t2:T.((eq T t0 t2)→∀P:Prop.P)→(pr3 c t0 t2)→(sn3 c t2) ⇒
the thesis becomes sn3 c (THead (Flat Cast) t1 t0)
(H4) by induction hypothesis we know
∀t2:T.((eq T t0 t2)→∀P:Prop.P)→(pr3 c t0 t2)→(sn3 c (THead (Flat Cast) t1 t2))
assume t2: T
suppose H5: (eq T (THead (Flat Cast) t1 t0) t2)→∀P:Prop.P
suppose H6: pr2 c (THead (Flat Cast) t1 t0) t2
(H7)
by (pr2_gen_cast . . . . H6)
or (ex3_2 T T λu2:T.λt2:T.eq T t2 (THead (Flat Cast) u2 t2) λu2:T.λ:T.pr2 c t1 u2 λ:T.λt2:T.pr2 c t0 t2) (pr2 c t0 t2)
end of H7
we proceed by induction on H7 to prove sn3 c t2
case or_introl : H8:ex3_2 T T λu2:T.λt3:T.eq T t2 (THead (Flat Cast) u2 t3) λu2:T.λ:T.pr2 c t1 u2 λ:T.λt3:T.pr2 c t0 t3 ⇒
the thesis becomes sn3 c t2
we proceed by induction on H8 to prove sn3 c t2
case ex3_2_intro : x0:T x1:T H9:eq T t2 (THead (Flat Cast) x0 x1) H10:pr2 c t1 x0 H11:pr2 c t0 x1 ⇒
the thesis becomes sn3 c t2
(H12)
we proceed by induction on H9 to prove
(eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) x0 x1))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H5
(eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) x0 x1))→∀P:Prop.P
end of H12
(H_x)
by (term_dec . .)
or (eq T x0 t1) (eq T x0 t1)→∀P:Prop.P
end of H_x
(H13) consider H_x
we proceed by induction on H13 to prove sn3 c (THead (Flat Cast) x0 x1)
case or_introl : H14:eq T x0 t1 ⇒
the thesis becomes sn3 c (THead (Flat Cast) x0 x1)
(H15)
we proceed by induction on H14 to prove
(eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) t1 x1))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H12
(eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) t1 x1))→∀P:Prop.P
end of H15
(H_x0)
by (term_dec . .)
or (eq T t0 x1) (eq T t0 x1)→∀P:Prop.P
end of H_x0
(H17) consider H_x0
we proceed by induction on H17 to prove sn3 c (THead (Flat Cast) t1 x1)
case or_introl : H18:eq T t0 x1 ⇒
the thesis becomes sn3 c (THead (Flat Cast) t1 x1)
(H19)
by (eq_ind_r . . . H15 . H18)
(eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) t1 t0))→∀P:Prop.P
end of H19
we proceed by induction on H18 to prove sn3 c (THead (Flat Cast) t1 x1)
case refl_equal : ⇒
the thesis becomes sn3 c (THead (Flat Cast) t1 t0)
by (refl_equal . .)
we proved eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) t1 t0)
by (H19 previous .)
sn3 c (THead (Flat Cast) t1 t0)
sn3 c (THead (Flat Cast) t1 x1)
case or_intror : H18:(eq T t0 x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Cast) t1 x1)
by (pr3_pr2 . . . H11)
we proved pr3 c t0 x1
by (H4 . H18 previous)
sn3 c (THead (Flat Cast) t1 x1)
we proved sn3 c (THead (Flat Cast) t1 x1)
by (eq_ind_r . . . previous . H14)
sn3 c (THead (Flat Cast) x0 x1)
case or_intror : H14:(eq T x0 t1)→∀P:Prop.P ⇒
the thesis becomes sn3 c (THead (Flat Cast) x0 x1)
(h1)
suppose H15: eq T t1 x0
assume P: Prop
(H16)
by (eq_ind_r . . . H14 . H15)
(eq T t1 t1)→∀P0:Prop.P0
end of H16
by (refl_equal . .)
we proved eq T t1 t1
by (H16 previous .)
we proved P
(eq T t1 x0)→∀P:Prop.P
end of h1
(h2) by (pr3_pr2 . . . H10) we proved pr3 c t1 x0
(h3)
(H_x0)
by (term_dec . .)
or (eq T t0 x1) (eq T t0 x1)→∀P:Prop.P
end of H_x0
(H15) consider H_x0
we proceed by induction on H15 to prove sn3 c x1
case or_introl : H16:eq T t0 x1 ⇒
the thesis becomes sn3 c x1
we proceed by induction on H16 to prove sn3 c x1
case refl_equal : ⇒
the thesis becomes sn3 c t0
by (sn3_sing . . H3)
sn3 c t0
sn3 c x1
case or_intror : H16:(eq T t0 x1)→∀P:Prop.P ⇒
the thesis becomes sn3 c x1
by (pr3_pr2 . . . H11)
we proved pr3 c t0 x1
by (H3 . H16 previous)
sn3 c x1
sn3 c x1
end of h3
by (H1 . h1 h2 . h3)
sn3 c (THead (Flat Cast) x0 x1)
we proved sn3 c (THead (Flat Cast) x0 x1)
by (eq_ind_r . . . previous . H9)
sn3 c t2
sn3 c t2
case or_intror : H8:pr2 c t0 t2 ⇒
the thesis becomes sn3 c t2
(h1) by (sn3_sing . . H3) we proved sn3 c t0
(h2) by (pr3_pr2 . . . H8) we proved pr3 c t0 t2
by (sn3_pr3_trans . . h1 . h2)
sn3 c t2
we proved sn3 c t2
we proved
∀t2:T
.(eq T (THead (Flat Cast) t1 t0) t2)→∀P:Prop.P
→(pr2 c (THead (Flat Cast) t1 t0) t2)→(sn3 c t2)
by (sn3_pr2_intro . . previous)
sn3 c (THead (Flat Cast) t1 t0)
we proved sn3 c (THead (Flat Cast) t1 t)
∀t:T.∀H2:(sn3 c t).(sn3 c (THead (Flat Cast) t1 t))
we proved ∀t0:T.(sn3 c t0)→(sn3 c (THead (Flat Cast) u t0))
we proved ∀c:C.∀u:T.(sn3 c u)→∀t0:T.(sn3 c t0)→(sn3 c (THead (Flat Cast) u t0))