DEFINITION tlt_head_dx()
TYPE =
∀k:K.∀u:T.∀t:T.(tlt t (THead k u t))
BODY =
assume k: K
we proceed by induction on k to prove
∀u:T.∀t:T.(lt (weight_map λ:nat.O t) (weight_map λ:nat.O (THead k u t)))
case Bind : b:B ⇒
the thesis becomes
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
weight_map λ:nat.O (THead (Bind b) u t)
we proceed by induction on b to prove
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
case Abbr : ⇒
the thesis becomes
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
assume u: T
assume t: T
(h1)
by (lt_n_Sn .)
lt (weight_map λ:nat.O t) (S (weight_map λ:nat.O t))
end of h1
(h2)
(h1)
by (weight_add_O .)
we proved eq nat (weight_map (wadd λ:nat.O O) t) (weight_map λ:nat.O t)
we proceed by induction on the previous result to prove
le
weight_map λ:nat.O t
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
case refl_equal : ⇒
the thesis becomes
le
weight_map (wadd λ:nat.O O) t
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
by (weight_add_S . .)
le
weight_map (wadd λ:nat.O O) t
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
le
weight_map λ:nat.O t
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
end of h1
(h2)
by (le_plus_r . .)
le
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
end of h2
by (le_trans . . . h1 h2)
we proved
le
weight_map λ:nat.O t
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
by (le_n_S . . previous)
le
S (weight_map λ:nat.O t)
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
end of h2
by (lt_le_trans . . . h1 h2)
we proved
lt
weight_map λ:nat.O t
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
that is equivalent to
lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Abbr OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
case Abst : ⇒
the thesis becomes
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
assume u: T
assume t: T
(h1)
by (le_plus_r . .)
we proved
le
weight_map λ:nat.O t
plus (weight_map λ:nat.O u) (weight_map λ:nat.O t)
by (le_n_S . . previous)
we proved
le
S (weight_map λ:nat.O t)
S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
lt
weight_map λ:nat.O t
S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
end of h1
(h2)
by (weight_add_O .)
eq nat (weight_map (wadd λ:nat.O O) t) (weight_map λ:nat.O t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
lt
weight_map λ:nat.O t
S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
that is equivalent to
lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Abst OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
case Void : ⇒
the thesis becomes
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
assume u: T
assume t: T
(h1)
by (le_plus_r . .)
we proved
le
weight_map λ:nat.O t
plus (weight_map λ:nat.O u) (weight_map λ:nat.O t)
by (le_n_S . . previous)
we proved
le
S (weight_map λ:nat.O t)
S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
lt
weight_map λ:nat.O t
S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
end of h1
(h2)
by (weight_add_O .)
eq nat (weight_map (wadd λ:nat.O O) t) (weight_map λ:nat.O t)
end of h2
by (eq_ind_r . . . h1 . h2)
we proved
lt
weight_map λ:nat.O t
S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
that is equivalent to
lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE Void OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
we proved
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
<λb1:B.nat>
CASE b OF
Abbr⇒
S
plus
weight_map λ:nat.O u
weight_map (wadd λ:nat.O (S (weight_map λ:nat.O u))) t
| Abst⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
| Void⇒S (plus (weight_map λ:nat.O u) (weight_map (wadd λ:nat.O O) t))
∀u:T
.∀t:T
.lt
weight_map λ:nat.O t
weight_map λ:nat.O (THead (Bind b) u t)
case Flat : :F ⇒
the thesis becomes
∀u:T
.∀t:T
.le
S (weight_map λ:nat.O t)
S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
assume u: T
assume t: T
by (le_plus_r . .)
we proved
le
weight_map λ:nat.O t
plus (weight_map λ:nat.O u) (weight_map λ:nat.O t)
by (le_n_S . . previous)
we proved
le
S (weight_map λ:nat.O t)
S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
that is equivalent to
lt
weight_map λ:nat.O t
weight_map λ:nat.O (THead (Flat __3) u t)
∀u:T
.∀t:T
.le
S (weight_map λ:nat.O t)
S (plus (weight_map λ:nat.O u) (weight_map λ:nat.O t))
we proved
∀u:T.∀t:T.(lt (weight_map λ:nat.O t) (weight_map λ:nat.O (THead k u t)))
that is equivalent to ∀u:T.∀t:T.(tlt t (THead k u t))
we proved ∀k:K.∀u:T.∀t:T.(tlt t (THead k u t))