DEFINITION pc3_abst_dec()
TYPE =
∀g:G
.∀c:C
.∀u1:T
.∀t1:T
.ty3 g c u1 t1
→∀u2:T
.∀t2:T
.ty3 g c u2 t2
→(or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False)
BODY =
assume g: G
assume c: C
assume u1: T
assume t1: T
suppose H: ty3 g c u1 t1
assume u2: T
assume t2: T
suppose H0: ty3 g c u2 t2
(H1) by (ty3_sn3 . . . . H) we proved sn3 c u1
(H2) by (ty3_sn3 . . . . H0) we proved sn3 c u2
(H_x)
by (nf2_sn3 . . H1)
ex2 T λu:T.pr3 c u1 u λu:T.nf2 c u
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
case ex_intro2 : x:T H4:pr3 c u1 x H5:nf2 c x ⇒
the thesis becomes
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
(H_x0)
by (nf2_sn3 . . H2)
ex2 T λu:T.pr3 c u2 u λu:T.nf2 c u
end of H_x0
(H6) consider H_x0
we proceed by induction on H6 to prove
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
case ex_intro2 : x0:T H7:pr3 c u2 x0 H8:nf2 c x0 ⇒
the thesis becomes
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
(H_x1)
by (abst_dec . .)
or
ex T λt:T.eq T x (THead (Bind Abst) x0 t)
∀t:T.(eq T x (THead (Bind Abst) x0 t))→∀P:Prop.P
end of H_x1
(H9) consider H_x1
we proceed by induction on H9 to prove
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
case or_introl : H10:ex T λt:T.eq T x (THead (Bind Abst) x0 t) ⇒
the thesis becomes
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
we proceed by induction on H10 to prove
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
case ex_intro : x1:T H11:eq T x (THead (Bind Abst) x0 x1) ⇒
the thesis becomes
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
(H13)
we proceed by induction on H11 to prove pr3 c u1 (THead (Bind Abst) x0 x1)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
pr3 c u1 (THead (Bind Abst) x0 x1)
end of H13
(H_y)
by (ty3_sred_pr3 . . . H13 . . H)
ty3 g c (THead (Bind Abst) x0 x1) t1
end of H_y
by (pr3_refl . .)
we proved pr3 (CHead c (Bind Abst) x0) x1 x1
by (pr3_head_12 . . . H7 . . . previous)
we proved pr3 c (THead (Bind Abst) u2 x1) (THead (Bind Abst) x0 x1)
by (pc3_pr3_t . . . H13 . previous)
we proved pc3 c u1 (THead (Bind Abst) u2 x1)
by (ex4_2_intro . . . . . . . . previous H_y H7 H8)
we proved
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
by (or_introl . . previous)
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
case or_intror : H10:∀t:T.(eq T x (THead (Bind Abst) x0 t))→∀P:Prop.P ⇒
the thesis becomes
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
assume u: T
suppose H11: pc3 c u1 (THead (Bind Abst) u2 u)
(H12) consider H11
consider H12
we proved pc3 c u1 (THead (Bind Abst) u2 u)
that is equivalent to ex2 T λt:T.pr3 c u1 t λt:T.pr3 c (THead (Bind Abst) u2 u) t
we proceed by induction on the previous result to prove False
case ex_intro2 : x1:T H13:pr3 c u1 x1 H14:pr3 c (THead (Bind Abst) u2 u) x1 ⇒
the thesis becomes False
by (pr3_confluence . . . H13 . H4)
we proved ex2 T λt:T.pr3 c x1 t λt:T.pr3 c x t
we proceed by induction on the previous result to prove False
case ex_intro2 : x2:T H15:pr3 c x1 x2 H16:pr3 c x x2 ⇒
the thesis becomes False
(H_y)
by (nf2_pr3_unfold . . . H16 H5)
eq T x x2
end of H_y
(H17)
by (eq_ind_r . . . H15 . H_y)
pr3 c x1 x
end of H17
(H18)
by (pr3_gen_abst . . . . H14)
ex3_2
T
T
λu2:T.λt2:T.eq T x1 (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c u2 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) u t2)
end of H18
we proceed by induction on H18 to prove False
case ex3_2_intro : x3:T x4:T H19:eq T x1 (THead (Bind Abst) x3 x4) H20:pr3 c u2 x3 :∀b:B.∀u0:T.(pr3 (CHead c (Bind b) u0) u x4) ⇒
the thesis becomes False
(H22)
we proceed by induction on H19 to prove pr3 c (THead (Bind Abst) x3 x4) x
case refl_equal : ⇒
the thesis becomes the hypothesis H17
pr3 c (THead (Bind Abst) x3 x4) x
end of H22
(H23)
by (pr3_gen_abst . . . . H22)
ex3_2
T
T
λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
λu2:T.λ:T.pr3 c x3 u2
λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) x4 t2)
end of H23
we proceed by induction on H23 to prove False
case ex3_2_intro : x5:T x6:T H24:eq T x (THead (Bind Abst) x5 x6) H25:pr3 c x3 x5 :∀b:B.∀u0:T.(pr3 (CHead c (Bind b) u0) x4 x6) ⇒
the thesis becomes False
(H27)
we proceed by induction on H24 to prove
∀t0:T
.(eq T (THead (Bind Abst) x5 x6) (THead (Bind Abst) x0 t0))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes the hypothesis H10
∀t0:T
.(eq T (THead (Bind Abst) x5 x6) (THead (Bind Abst) x0 t0))→∀P:Prop.P
end of H27
(H28)
we proceed by induction on H24 to prove nf2 c (THead (Bind Abst) x5 x6)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
nf2 c (THead (Bind Abst) x5 x6)
end of H28
(H29)
by (nf2_gen_abst . . . H28)
land (nf2 c x5) (nf2 (CHead c (Bind Abst) x5) x6)
end of H29
we proceed by induction on H29 to prove False
case conj : H30:nf2 c x5 :nf2 (CHead c (Bind Abst) x5) x6 ⇒
the thesis becomes False
(H32)
by (nf2_pr3_confluence . . H8 . H30 . H7)
(pr3 c u2 x5)→(eq T x0 x5)
end of H32
(h1)
by (refl_equal . .)
eq K (Bind Abst) (Bind Abst)
end of h1
(h2)
by (pr3_t . . . H20 . H25)
we proved pr3 c u2 x5
by (H32 previous)
eq T x0 x5
end of h2
(h3)
by (refl_equal . .)
eq T x6 x6
end of h3
by (f_equal3 . . . . . . . . . . . h1 h2 h3)
we proved eq T (THead (Bind Abst) x0 x6) (THead (Bind Abst) x5 x6)
by (sym_eq . . . previous)
we proved eq T (THead (Bind Abst) x5 x6) (THead (Bind Abst) x0 x6)
by (H27 . previous .)
False
False
False
False
False
we proved False
we proved ∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
by (or_intror . . previous)
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
we proved
or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False
we proved
∀g:G
.∀c:C
.∀u1:T
.∀t1:T
.ty3 g c u1 t1
→∀u2:T
.∀t2:T
.ty3 g c u2 t2
→(or
ex4_2
T
T
λu:T.λ:T.pc3 c u1 (THead (Bind Abst) u2 u)
λu:T.λv2:T.ty3 g c (THead (Bind Abst) v2 u) t1
λ:T.λv2:T.pr3 c u2 v2
λ:T.λv2:T.nf2 c v2
∀u:T.(pc3 c u1 (THead (Bind Abst) u2 u))→False)