DEFINITION pr2_confluence()
TYPE =
∀c:C.∀t0:T.∀t1:T.(pr2 c t0 t1)→∀t2:T.(pr2 c t0 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
BODY =
assume c: C
assume t0: T
assume t1: T
suppose H: pr2 c t0 t1
assume t2: T
suppose H0: pr2 c t0 t2
(H1)
by cases on H we prove (eq C c c)→(eq T t0 t0)→(eq T t1 t1)→(ex2 T λt4:T.pr2 c t1 t4 λt4:T.pr2 c t2 t4)
case pr2_free c0:C t3:T t4:T H1:pr0 t3 t4 ⇒
the thesis becomes ∀H2:(eq C c0 c).∀H3:(eq T t3 t0).∀H4:(eq T t4 t1).(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
suppose H2: eq C c0 c
suppose H3: eq T t3 t0
suppose H4: eq T t4 t1
by (sym_eq . . . H2)
we proved eq C c c0
suppose H5: eq T t3 t0
by (sym_eq . . . H5)
we proved eq T t0 t3
we proceed by induction on the previous result to prove (eq T t4 t1)→(pr0 t3 t4)→(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
case refl_equal : ⇒
the thesis becomes (eq T t4 t1)→(pr0 t0 t4)→(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
suppose H6: eq T t4 t1
by (sym_eq . . . H6)
we proved eq T t1 t4
we proceed by induction on the previous result to prove (pr0 t0 t4)→(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
case refl_equal : ⇒
the thesis becomes (pr0 t0 t1)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6)
suppose H7: pr0 t0 t1
(H8)
by cases on H0 we prove (eq C c c)→(eq T t0 t0)→(eq T t2 t2)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6)
case pr2_free c1:C t5:T t6:T H8:pr0 t5 t6 ⇒
the thesis becomes ∀H9:(eq C c1 c).∀H10:(eq T t5 t0).∀H11:(eq T t6 t2).(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
suppose H9: eq C c1 c
suppose H10: eq T t5 t0
suppose H11: eq T t6 t2
by (sym_eq . . . H9)
we proved eq C c c1
suppose H12: eq T t5 t0
by (sym_eq . . . H12)
we proved eq T t0 t5
we proceed by induction on the previous result to prove (eq T t6 t2)→(pr0 t5 t6)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
case refl_equal : ⇒
the thesis becomes (eq T t6 t2)→(pr0 t0 t6)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
suppose H13: eq T t6 t2
by (sym_eq . . . H13)
we proved eq T t2 t6
we proceed by induction on the previous result to prove (pr0 t0 t6)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
case refl_equal : ⇒
the thesis becomes (pr0 t0 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
suppose H14: pr0 t0 t2
by (pr2_confluence__pr2_free_free . . . . H7 H14)
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
(pr0 t0 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
we proved (pr0 t0 t6)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
(eq T t6 t2)→(pr0 t0 t6)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
we proved (eq T t6 t2)→(pr0 t5 t6)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
(eq T t5 t0)→(eq T t6 t2)→(pr0 t5 t6)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
by (previous previous H10 H11 H8)
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
∀H9:(eq C c1 c).∀H10:(eq T t5 t0).∀H11:(eq T t6 t2).(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
case pr2_delta c1:C d:C u:T i:nat H8:getl i c1 (CHead d (Bind Abbr) u) t5:T t6:T H9:pr0 t5 t6 t:T H10:subst0 i u t6 t ⇒
the thesis becomes ∀H11:(eq C c1 c).∀H12:(eq T t5 t0).∀H13:(eq T t t2).(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
suppose H11: eq C c1 c
suppose H12: eq T t5 t0
suppose H13: eq T t t2
by (sym_eq . . . H11)
we proved eq C c c1
suppose H14: eq T t5 t0
by (sym_eq . . . H14)
we proved eq T t0 t5
we proceed by induction on the previous result to prove
eq T t t2
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t5 t6)→(subst0 i u t6 t)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8))
case refl_equal : ⇒
the thesis becomes
eq T t t2
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t6)→(subst0 i u t6 t)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8))
suppose H15: eq T t t2
by (sym_eq . . . H15)
we proved eq T t2 t
we proceed by induction on the previous result to prove
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t6)→(subst0 i u t6 t)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
case refl_equal : ⇒
the thesis becomes
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t6)→(subst0 i u t6 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
suppose H16: getl i c (CHead d (Bind Abbr) u)
suppose H17: pr0 t0 t6
suppose H18: subst0 i u t6 t2
by (pr2_confluence__pr2_free_delta . . . . . . . . H7 H16 H17 H18)
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t6)→(subst0 i u t6 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
we proved
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t6)→(subst0 i u t6 t)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
eq T t t2
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t6)→(subst0 i u t6 t)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8))
we proved
eq T t t2
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t5 t6)→(subst0 i u t6 t)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8))
eq T t5 t0
→(eq T t t2
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t5 t6)→(subst0 i u t6 t)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)))
by (previous previous H12 H13 H8 H9 H10)
we proved ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7
∀H11:(eq C c1 c).∀H12:(eq T t5 t0).∀H13:(eq T t t2).(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
(eq C c c)→(eq T t0 t0)→(eq T t2 t2)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6)
end of H8
(h1)
by (refl_equal . .)
eq C c c
end of h1
(h2)
by (refl_equal . .)
eq T t0 t0
end of h2
(h3)
by (refl_equal . .)
eq T t2 t2
end of h3
by (H8 h1 h2 h3)
we proved ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6
(pr0 t0 t1)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6)
we proved (pr0 t0 t4)→(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
(eq T t4 t1)→(pr0 t0 t4)→(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
we proved (eq T t4 t1)→(pr0 t3 t4)→(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
(eq T t3 t0)→(eq T t4 t1)→(pr0 t3 t4)→(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
by (previous previous H3 H4 H1)
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
∀H2:(eq C c0 c).∀H3:(eq T t3 t0).∀H4:(eq T t4 t1).(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
case pr2_delta c0:C d:C u:T i:nat H1:getl i c0 (CHead d (Bind Abbr) u) t3:T t4:T H2:pr0 t3 t4 t:T H3:subst0 i u t4 t ⇒
the thesis becomes ∀H4:(eq C c0 c).∀H5:(eq T t3 t0).∀H6:(eq T t t1).(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
suppose H4: eq C c0 c
suppose H5: eq T t3 t0
suppose H6: eq T t t1
by (sym_eq . . . H4)
we proved eq C c c0
suppose H7: eq T t3 t0
by (sym_eq . . . H7)
we proved eq T t0 t3
we proceed by induction on the previous result to prove
eq T t t1
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t3 t4)→(subst0 i u t4 t)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6))
case refl_equal : ⇒
the thesis becomes
eq T t t1
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t4)→(subst0 i u t4 t)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6))
suppose H8: eq T t t1
by (sym_eq . . . H8)
we proved eq T t1 t
we proceed by induction on the previous result to prove
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t4)→(subst0 i u t4 t)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6)
case refl_equal : ⇒
the thesis becomes
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t4)→(subst0 i u t4 t1)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
suppose H9: getl i c (CHead d (Bind Abbr) u)
suppose H10: pr0 t0 t4
suppose H11: subst0 i u t4 t1
(H12)
by cases on H0 we prove (eq C c c)→(eq T t0 t0)→(eq T t2 t2)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
case pr2_free c1:C t5:T t6:T H12:pr0 t5 t6 ⇒
the thesis becomes ∀H13:(eq C c1 c).∀H14:(eq T t5 t0).∀H15:(eq T t6 t2).(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
suppose H13: eq C c1 c
suppose H14: eq T t5 t0
suppose H15: eq T t6 t2
by (sym_eq . . . H13)
we proved eq C c c1
suppose H16: eq T t5 t0
by (sym_eq . . . H16)
we proved eq T t0 t5
we proceed by induction on the previous result to prove (eq T t6 t2)→(pr0 t5 t6)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
case refl_equal : ⇒
the thesis becomes (eq T t6 t2)→(pr0 t0 t6)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
suppose H17: eq T t6 t2
by (sym_eq . . . H17)
we proved eq T t2 t6
we proceed by induction on the previous result to prove (pr0 t0 t6)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
case refl_equal : ⇒
the thesis becomes (pr0 t0 t2)→(ex2 T λx:T.pr2 c t1 x λx:T.pr2 c t2 x)
suppose H18: pr0 t0 t2
by (pr2_confluence__pr2_free_delta . . . . . . . . H18 H9 H10 H11)
we proved ex2 T λt:T.pr2 c t2 t λt:T.pr2 c t1 t
by (ex2_sym . . . previous)
we proved ex2 T λx:T.pr2 c t1 x λx:T.pr2 c t2 x
(pr0 t0 t2)→(ex2 T λx:T.pr2 c t1 x λx:T.pr2 c t2 x)
we proved (pr0 t0 t6)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
(eq T t6 t2)→(pr0 t0 t6)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
we proved (eq T t6 t2)→(pr0 t5 t6)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
(eq T t5 t0)→(eq T t6 t2)→(pr0 t5 t6)→(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
by (previous previous H14 H15 H12)
we proved ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7
∀H13:(eq C c1 c).∀H14:(eq T t5 t0).∀H15:(eq T t6 t2).(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
case pr2_delta c1:C d0:C u0:T i0:nat H12:getl i0 c1 (CHead d0 (Bind Abbr) u0) t5:T t6:T H13:pr0 t5 t6 t7:T H14:subst0 i0 u0 t6 t7 ⇒
the thesis becomes ∀H15:(eq C c1 c).∀H16:(eq T t5 t0).∀H17:(eq T t7 t2).(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
suppose H15: eq C c1 c
suppose H16: eq T t5 t0
suppose H17: eq T t7 t2
by (sym_eq . . . H15)
we proved eq C c c1
suppose H18: eq T t5 t0
by (sym_eq . . . H18)
we proved eq T t0 t5
we proceed by induction on the previous result to prove
eq T t7 t2
→(getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t5 t6)→(subst0 i0 u0 t6 t7)→(ex2 T λt9:T.pr2 c t1 t9 λt9:T.pr2 c t2 t9))
case refl_equal : ⇒
the thesis becomes
eq T t7 t2
→(getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t6)→(subst0 i0 u0 t6 t7)→(ex2 T λt9:T.pr2 c t1 t9 λt9:T.pr2 c t2 t9))
suppose H19: eq T t7 t2
by (sym_eq . . . H19)
we proved eq T t2 t7
we proceed by induction on the previous result to prove
getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t6)→(subst0 i0 u0 t6 t7)→(ex2 T λt9:T.pr2 c t1 t9 λt9:T.pr2 c t2 t9)
case refl_equal : ⇒
the thesis becomes
getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t6)→(subst0 i0 u0 t6 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
suppose H20: getl i0 c (CHead d0 (Bind Abbr) u0)
suppose H21: pr0 t0 t6
suppose H22: subst0 i0 u0 t6 t2
by (pr2_confluence__pr2_delta_delta . . . . . . . . . . . . H9 H10 H11 H20 H21 H22)
we proved ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t
getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t6)→(subst0 i0 u0 t6 t2)→(ex2 T λt:T.pr2 c t1 t λt:T.pr2 c t2 t)
we proved
getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t6)→(subst0 i0 u0 t6 t7)→(ex2 T λt9:T.pr2 c t1 t9 λt9:T.pr2 c t2 t9)
eq T t7 t2
→(getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t0 t6)→(subst0 i0 u0 t6 t7)→(ex2 T λt9:T.pr2 c t1 t9 λt9:T.pr2 c t2 t9))
we proved
eq T t7 t2
→(getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t5 t6)→(subst0 i0 u0 t6 t7)→(ex2 T λt9:T.pr2 c t1 t9 λt9:T.pr2 c t2 t9))
eq T t5 t0
→(eq T t7 t2
→(getl i0 c (CHead d0 (Bind Abbr) u0)
→(pr0 t5 t6)→(subst0 i0 u0 t6 t7)→(ex2 T λt9:T.pr2 c t1 t9 λt9:T.pr2 c t2 t9)))
by (previous previous H16 H17 H12 H13 H14)
we proved ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8
∀H15:(eq C c1 c).∀H16:(eq T t5 t0).∀H17:(eq T t7 t2).(ex2 T λt8:T.pr2 c t1 t8 λt8:T.pr2 c t2 t8)
(eq C c c)→(eq T t0 t0)→(eq T t2 t2)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
end of H12
(h1)
by (refl_equal . .)
eq C c c
end of h1
(h2)
by (refl_equal . .)
eq T t0 t0
end of h2
(h3)
by (refl_equal . .)
eq T t2 t2
end of h3
by (H12 h1 h2 h3)
we proved ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t4)→(subst0 i u t4 t1)→(ex2 T λt7:T.pr2 c t1 t7 λt7:T.pr2 c t2 t7)
we proved
getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t4)→(subst0 i u t4 t)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6)
eq T t t1
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t0 t4)→(subst0 i u t4 t)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6))
we proved
eq T t t1
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t3 t4)→(subst0 i u t4 t)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6))
eq T t3 t0
→(eq T t t1
→(getl i c (CHead d (Bind Abbr) u)
→(pr0 t3 t4)→(subst0 i u t4 t)→(ex2 T λt6:T.pr2 c t1 t6 λt6:T.pr2 c t2 t6)))
by (previous previous H5 H6 H1 H2 H3)
we proved ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5
∀H4:(eq C c0 c).∀H5:(eq T t3 t0).∀H6:(eq T t t1).(ex2 T λt5:T.pr2 c t1 t5 λt5:T.pr2 c t2 t5)
(eq C c c)→(eq T t0 t0)→(eq T t1 t1)→(ex2 T λt4:T.pr2 c t1 t4 λt4:T.pr2 c t2 t4)
end of H1
(h1)
by (refl_equal . .)
eq C c c
end of h1
(h2)
by (refl_equal . .)
eq T t0 t0
end of h2
(h3)
by (refl_equal . .)
eq T t1 t1
end of h3
by (H1 h1 h2 h3)
we proved ex2 T λt4:T.pr2 c t1 t4 λt4:T.pr2 c t2 t4
we proved ∀c:C.∀t0:T.∀t1:T.(pr2 c t0 t1)→∀t2:T.(pr2 c t0 t2)→(ex2 T λt4:T.pr2 c t1 t4 λt4:T.pr2 c t2 t4)