DEFINITION pr0_confluence__pr0_delta_delta()
TYPE =
∀u2:T
.∀t3:T
.∀w:T
.subst0 O u2 t3 w
→∀u3:T
.∀t5:T
.∀w0:T
.subst0 O u3 t5 w0
→∀x:T
.pr0 u2 x
→(pr0 u3 x
→∀x0:T
.pr0 t3 x0
→(pr0 t5 x0
→ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t))
BODY =
assume u2: T
assume t3: T
assume w: T
suppose H: subst0 O u2 t3 w
assume u3: T
assume t5: T
assume w0: T
suppose H0: subst0 O u3 t5 w0
assume x: T
suppose H1: pr0 u2 x
suppose H2: pr0 u3 x
assume x0: T
suppose H3: pr0 t3 x0
suppose H4: pr0 t5 x0
by (pr0_subst0 . . H4 . . . H0 . H2)
we proved or (pr0 w0 x0) (ex2 T λw2:T.pr0 w0 w2 λw2:T.subst0 O x x0 w2)
we proceed by induction on the previous result to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or_introl : H5:pr0 w0 x0 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
by (pr0_subst0 . . H3 . . . H . H1)
we proved or (pr0 w x0) (ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x x0 w2)
we proceed by induction on the previous result to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or_introl : H6:pr0 w x0 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
(h1)
by (pr0_comp . . H1 . . H6 .)
pr0 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) x x0)
end of h1
(h2)
by (pr0_comp . . H2 . . H5 .)
pr0 (THead (Bind Abbr) u3 w0) (THead (Bind Abbr) x x0)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or_intror : H6:ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x x0 w2 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
we proceed by induction on H6 to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case ex_intro2 : x1:T H7:pr0 w x1 H8:subst0 O x x0 x1 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
(h1)
by (pr0_comp . . H1 . . H7 .)
pr0 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) x x1)
end of h1
(h2)
by (pr0_delta . . H2 . . H5 . H8)
pr0 (THead (Bind Abbr) u3 w0) (THead (Bind Abbr) x x1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or_intror : H5:ex2 T λw2:T.pr0 w0 w2 λw2:T.subst0 O x x0 w2 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
we proceed by induction on H5 to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case ex_intro2 : x1:T H6:pr0 w0 x1 H7:subst0 O x x0 x1 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
by (pr0_subst0 . . H3 . . . H . H1)
we proved or (pr0 w x0) (ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x x0 w2)
we proceed by induction on the previous result to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or_introl : H8:pr0 w x0 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
(h1)
by (pr0_delta . . H1 . . H8 . H7)
pr0 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) x x1)
end of h1
(h2)
by (pr0_comp . . H2 . . H6 .)
pr0 (THead (Bind Abbr) u3 w0) (THead (Bind Abbr) x x1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or_intror : H8:ex2 T λw2:T.pr0 w w2 λw2:T.subst0 O x x0 w2 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
we proceed by induction on H8 to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case ex_intro2 : x2:T H9:pr0 w x2 H10:subst0 O x x0 x2 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
by (subst0_confluence_eq . . . . H10 . H7)
we proved or4 (eq T x2 x1) (ex2 T λt:T.subst0 O x x2 t λt:T.subst0 O x x1 t) (subst0 O x x2 x1) (subst0 O x x1 x2)
we proceed by induction on the previous result to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or4_intro0 : H11:eq T x2 x1 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
(H12)
we proceed by induction on H11 to prove pr0 w x1
case refl_equal : ⇒
the thesis becomes the hypothesis H9
pr0 w x1
end of H12
(h1)
by (pr0_comp . . H1 . . H12 .)
pr0 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) x x1)
end of h1
(h2)
by (pr0_comp . . H2 . . H6 .)
pr0 (THead (Bind Abbr) u3 w0) (THead (Bind Abbr) x x1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or4_intro1 : H11:ex2 T λt:T.subst0 O x x2 t λt:T.subst0 O x x1 t ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
we proceed by induction on H11 to prove
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case ex_intro2 : x3:T H12:subst0 O x x2 x3 H13:subst0 O x x1 x3 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
(h1)
by (pr0_delta . . H1 . . H9 . H12)
pr0 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) x x3)
end of h1
(h2)
by (pr0_delta . . H2 . . H6 . H13)
pr0 (THead (Bind Abbr) u3 w0) (THead (Bind Abbr) x x3)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or4_intro2 : H11:subst0 O x x2 x1 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
(h1)
by (pr0_delta . . H1 . . H9 . H11)
pr0 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) x x1)
end of h1
(h2)
by (pr0_comp . . H2 . . H6 .)
pr0 (THead (Bind Abbr) u3 w0) (THead (Bind Abbr) x x1)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
case or4_intro3 : H11:subst0 O x x1 x2 ⇒
the thesis becomes
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
(h1)
by (pr0_comp . . H1 . . H9 .)
pr0 (THead (Bind Abbr) u2 w) (THead (Bind Abbr) x x2)
end of h1
(h2)
by (pr0_delta . . H2 . . H6 . H11)
pr0 (THead (Bind Abbr) u3 w0) (THead (Bind Abbr) x x2)
end of h2
by (ex_intro2 . . . . h1 h2)
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
we proved
ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t
we proved
∀u2:T
.∀t3:T
.∀w:T
.subst0 O u2 t3 w
→∀u3:T
.∀t5:T
.∀w0:T
.subst0 O u3 t5 w0
→∀x:T
.pr0 u2 x
→(pr0 u3 x
→∀x0:T
.pr0 t3 x0
→(pr0 t5 x0
→ex2 T λt:T.pr0 (THead (Bind Abbr) u2 w) t λt:T.pr0 (THead (Bind Abbr) u3 w0) t))