DEFINITION tcons_tapp_ex()
TYPE =
∀ts1:TList
.∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)
BODY =
assume ts1: TList
we proceed by induction on ts1 to prove
∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)
case TNil : ⇒
the thesis becomes
∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen TNil) (tslen ts2)
assume t1: T
(h1)
by (refl_equal . .)
we proved eq TList (TApp TNil t1) (TApp TNil t1)
eq TList (TCons t1 TNil) (TApp TNil t1)
end of h1
(h2)
by (refl_equal . .)
we proved eq nat (tslen TNil) (tslen TNil)
eq nat O (tslen TNil)
end of h2
by (ex2_2_intro . . . . . . h1 h2)
we proved
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
λts2:TList.λ:T.eq nat O (tslen ts2)
that is equivalent to
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen TNil) (tslen ts2)
∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 TNil) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen TNil) (tslen ts2)
case TCons : t:T t0:TList ⇒
the thesis becomes
∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
(H) by induction hypothesis we know
∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 t0) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen t0) (tslen ts2)
assume t1: T
(H_x)
by (H .)
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t t0) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen t0) (tslen ts2)
end of H_x
(H0) consider H_x
we proceed by induction on H0 to prove
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
case ex2_2_intro : x0:TList x1:T H1:eq TList (TCons t t0) (TApp x0 x1) H2:eq nat (tslen t0) (tslen x0) ⇒
the thesis becomes
ex2_2
TList
T
λts2:TList.λt3:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t3)
λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
(h1)
by (refl_equal . .)
we proved eq TList (TApp (TCons t1 x0) x1) (TApp (TCons t1 x0) x1)
eq TList (TCons t1 (TApp x0 x1)) (TApp (TCons t1 x0) x1)
end of h1
(h2)
by (refl_equal . .)
we proved eq nat (tslen (TCons t1 x0)) (tslen (TCons t1 x0))
eq nat (S (tslen x0)) (tslen (TCons t1 x0))
end of h2
by (ex2_2_intro . . . . . . h1 h2)
we proved
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 (TApp x0 x1)) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (S (tslen x0)) (tslen ts2)
by (eq_ind_r . . . previous . H2)
we proved
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 (TApp x0 x1)) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
by (eq_ind_r . . . previous . H1)
ex2_2
TList
T
λts2:TList.λt3:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t3)
λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
we proved
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
that is equivalent to
ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen (TCons t t0)) (tslen ts2)
∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 (TCons t t0)) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (S (tslen t0)) (tslen ts2)
we proved
∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)
we proved
∀ts1:TList
.∀t1:T
.ex2_2
TList
T
λts2:TList.λt2:T.eq TList (TCons t1 ts1) (TApp ts2 t2)
λts2:TList.λ:T.eq nat (tslen ts1) (tslen ts2)