DEFINITION pr2_confluence__pr2_delta_delta()
TYPE =
∀c:C
.∀d:C
.∀d0:C
.∀t0:T
.∀t1:T
.∀t2:T
.∀t3:T
.∀t4:T
.∀u:T
.∀u0:T
.∀i:nat
.∀i0:nat
.getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t3
→(subst0 i u t3 t1
→(getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t4)→(subst0 i0 u0 t4 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t))))
BODY =
assume c: C
assume d: C
assume d0: C
assume t0: T
assume t1: T
assume t2: T
assume t3: T
assume t4: T
assume u: T
assume u0: T
assume i: nat
assume i0: nat
suppose H: getl i c (CHead d (Bind Abbr) u)
suppose H0: pr0 t0 t3
suppose H1: subst0 i u t3 t1
suppose H2: getl i0 c (CHead d0 (Bind Abbr) u0)
suppose H3: pr0 t0 t4
suppose H4: subst0 i0 u0 t4 t2
by (pr0_confluence . . H3 . H0)
we proved ex2 T λt:T.pr0 t4 t λt:T.pr0 t3 t
we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case ex_intro2 : x:T H5:pr0 t4 x H6:pr0 t3 x ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
by (pr0_refl .)
we proved pr0 u u
by (pr0_subst0 . . H6 . . . H1 . previous)
we proved or (pr0 t1 x) (ex2 T λw2:T.pr0 t1 w2 λw2:T.subst0 i u x w2)
we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or_introl : H7:pr0 t1 x ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
by (pr0_refl .)
we proved pr0 u0 u0
by (pr0_subst0 . . H5 . . . H4 . previous)
we proved or (pr0 t2 x) (ex2 T λw2:T.pr0 t2 w2 λw2:T.subst0 i0 u0 x w2)
we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or_introl : H8:pr0 t2 x ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
by (pr2_free . . . H7)
pr2 c t1 x
end of h1
(h2)
by (pr2_free . . . H8)
pr2 c t2 x
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or_intror : H8:ex2 T λw2:T.pr0 t2 w2 λw2:T.subst0 i0 u0 x w2 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proceed by induction on H8 to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case ex_intro2 : x0:T H9:pr0 t2 x0 H10:subst0 i0 u0 x x0 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
by (pr2_delta . . . . H2 . . H7 . H10)
pr2 c t1 x0
end of h1
(h2)
by (pr2_free . . . H9)
pr2 c t2 x0
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or_intror : H7:ex2 T λw2:T.pr0 t1 w2 λw2:T.subst0 i u x w2 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proceed by induction on H7 to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case ex_intro2 : x0:T H8:pr0 t1 x0 H9:subst0 i u x x0 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
by (pr0_refl .)
we proved pr0 u0 u0
by (pr0_subst0 . . H5 . . . H4 . previous)
we proved or (pr0 t2 x) (ex2 T λw2:T.pr0 t2 w2 λw2:T.subst0 i0 u0 x w2)
we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or_introl : H10:pr0 t2 x ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
by (pr2_free . . . H8)
pr2 c t1 x0
end of h1
(h2)
by (pr2_delta . . . . H . . H10 . H9)
pr2 c t2 x0
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or_intror : H10:ex2 T λw2:T.pr0 t2 w2 λw2:T.subst0 i0 u0 x w2 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proceed by induction on H10 to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case ex_intro2 : x1:T H11:pr0 t2 x1 H12:subst0 i0 u0 x x1 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
suppose H13: not (eq nat i i0)
by (sym_not_eq . . . H13)
we proved not (eq nat i0 i)
by (subst0_confluence_neq . . . . H12 . . . H9 previous)
we proved ex2 T λt:T.subst0 i u x1 t λt:T.subst0 i0 u0 x0 t
we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case ex_intro2 : x2:T H14:subst0 i u x1 x2 H15:subst0 i0 u0 x0 x2 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
by (pr2_delta . . . . H2 . . H8 . H15)
pr2 c t1 x2
end of h1
(h2)
by (pr2_delta . . . . H . . H11 . H14)
pr2 c t2 x2
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(not (eq nat i i0))→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
end of h1
(h2)
suppose H13: eq nat i i0
(H14)
by (eq_ind_r . . . H12 . H13)
subst0 i u0 x x1
end of H14
(H15)
by (eq_ind_r . . . H2 . H13)
getl i c (CHead d0 (Bind Abbr) u0)
end of H15
(H16)
by (getl_mono . . . H . H15)
we proved eq C (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0)
we proceed by induction on the previous result to prove getl i c (CHead d0 (Bind Abbr) u0)
case refl_equal : ⇒
the thesis becomes the hypothesis H
getl i c (CHead d0 (Bind Abbr) u0)
end of H16
(H17)
by (getl_mono . . . H . H15)
we proved eq C (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq
C
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d (Bind Abbr) u)
λe:C.<λ:C.C> CASE e OF CSort ⇒d | CHead c0 ⇒c0 (CHead d0 (Bind Abbr) u0)
end of H17
(h1)
(H18)
by (getl_mono . . . H . H15)
we proved eq C (CHead d (Bind Abbr) u) (CHead d0 (Bind Abbr) u0)
by (f_equal . . . . . previous)
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
eq
T
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d (Bind Abbr) u)
λe:C.<λ:C.T> CASE e OF CSort ⇒u | CHead t⇒t (CHead d0 (Bind Abbr) u0)
end of H18
suppose H19: eq C d d0
(H20)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u u0
by (eq_ind_r . . . H14 . previous)
subst0 i u x x1
end of H20
(H21)
consider H18
we proved
eq
T
<λ:C.T> CASE CHead d (Bind Abbr) u OF CSort ⇒u | CHead t⇒t
<λ:C.T> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒u | CHead t⇒t
that is equivalent to eq T u u0
by (eq_ind_r . . . H16 . previous)
getl i c (CHead d0 (Bind Abbr) u)
end of H21
(H22)
by (eq_ind_r . . . H21 . H19)
getl i c (CHead d (Bind Abbr) u)
end of H22
by (subst0_confluence_eq . . . . H20 . H9)
we proved or4 (eq T x1 x0) (ex2 T λt:T.subst0 i u x1 t λt:T.subst0 i u x0 t) (subst0 i u x1 x0) (subst0 i u x0 x1)
we proceed by induction on the previous result to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or4_intro0 : H23:eq T x1 x0 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(H24)
we proceed by induction on H23 to prove pr0 t2 x0
case refl_equal : ⇒
the thesis becomes the hypothesis H11
pr0 t2 x0
end of H24
(h1)
by (pr2_free . . . H8)
pr2 c t1 x0
end of h1
(h2)
by (pr2_free . . . H24)
pr2 c t2 x0
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or4_intro1 : H23:ex2 T λt:T.subst0 i u x1 t λt:T.subst0 i u x0 t ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proceed by induction on H23 to prove ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case ex_intro2 : x2:T H24:subst0 i u x1 x2 H25:subst0 i u x0 x2 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
by (pr2_delta . . . . H22 . . H8 . H25)
pr2 c t1 x2
end of h1
(h2)
by (pr2_delta . . . . H22 . . H11 . H24)
pr2 c t2 x2
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or4_intro2 : H23:subst0 i u x1 x0 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
by (pr2_free . . . H8)
pr2 c t1 x0
end of h1
(h2)
by (pr2_delta . . . . H22 . . H11 . H23)
pr2 c t2 x0
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
case or4_intro3 : H23:subst0 i u x0 x1 ⇒
the thesis becomes ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(h1)
by (pr2_delta . . . . H22 . . H8 . H23)
pr2 c t1 x1
end of h1
(h2)
by (pr2_free . . . H11)
pr2 c t2 x1
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(eq C d d0)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
end of h1
(h2)
consider H17
we proved
eq
C
<λ:C.C> CASE CHead d (Bind Abbr) u OF CSort ⇒d | CHead c0 ⇒c0
<λ:C.C> CASE CHead d0 (Bind Abbr) u0 OF CSort ⇒d | CHead c0 ⇒c0
eq C d d0
end of h2
by (h1 h2)
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(eq nat i i0)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
end of h2
by (neq_eq_e . . . h1 h2)
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
we proved
∀c:C
.∀d:C
.∀d0:C
.∀t0:T
.∀t1:T
.∀t2:T
.∀t3:T
.∀t4:T
.∀u:T
.∀u0:T
.∀i:nat
.∀i0:nat
.getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t3
→(subst0 i u t3 t1
→(getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t4)→(subst0 i0 u0 t4 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t))))