DEFINITION arity_gen_cast()
TYPE =
∀g:G
.∀c:C
.∀u:T
.∀t:T
.∀a:A
.arity g c (THead (Flat Cast) u t) a
→land (arity g c u (asucc g a)) (arity g c t a)
BODY =
assume g: G
assume c: C
assume u: T
assume t: T
assume a: A
suppose H: arity g c (THead (Flat Cast) u t) a
assume y: T
suppose H0: arity g c y a
we proceed by induction on H0 to prove
eq T y (THead (Flat Cast) u t)
→land (arity g c u (asucc g a)) (arity g c t a)
case arity_sort : c0:C n:nat ⇒
the thesis becomes
∀H1:eq T (TSort n) (THead (Flat Cast) u t)
.land
arity g c0 u (asucc g (ASort O n))
arity g c0 t (ASort O n)
suppose H1: eq T (TSort n) (THead (Flat Cast) u t)
(H2)
we proceed by induction on H1 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
end of H2
consider H2
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒True
| TLRef ⇒False
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove
land
arity g c0 u (asucc g (ASort O n))
arity g c0 t (ASort O n)
we proved
land
arity g c0 u (asucc g (ASort O n))
arity g c0 t (ASort O n)
∀H1:eq T (TSort n) (THead (Flat Cast) u t)
.land
arity g c0 u (asucc g (ASort O n))
arity g c0 t (ASort O n)
case arity_abbr : c0:C d:C u0:T i:nat :getl i c0 (CHead d (Bind Abbr) u0) a0:A :arity g d u0 a0 ⇒
the thesis becomes
∀H4:eq T (TLRef i) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
() by induction hypothesis we know
eq T u0 (THead (Flat Cast) u t)
→land (arity g d u (asucc g a0)) (arity g d t a0)
suppose H4: eq T (TLRef i) (THead (Flat Cast) u t)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
we proved land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
∀H4:eq T (TLRef i) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
case arity_abst : c0:C d:C u0:T i:nat :getl i c0 (CHead d (Bind Abst) u0) a0:A :arity g d u0 (asucc g a0) ⇒
the thesis becomes
∀H4:eq T (TLRef i) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
() by induction hypothesis we know
eq T u0 (THead (Flat Cast) u t)
→(land
arity g d u (asucc g (asucc g a0))
arity g d t (asucc g a0))
suppose H4: eq T (TLRef i) (THead (Flat Cast) u t)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
consider I
we proved True
<λ:T.Prop>
CASE TLRef i OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
we proved land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
∀H4:eq T (TLRef i) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
case arity_bind : b:B :not (eq B b Abst) c0:C u0:T a1:A :arity g c0 u0 a1 t0:T a2:A :arity g (CHead c0 (Bind b) u0) t0 a2 ⇒
the thesis becomes
∀H6:eq T (THead (Bind b) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
() by induction hypothesis we know
eq T u0 (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g a1)) (arity g c0 t a1)
() by induction hypothesis we know
eq T t0 (THead (Flat Cast) u t)
→(land
arity g (CHead c0 (Bind b) u0) u (asucc g a2)
arity g (CHead c0 (Bind b) u0) t a2)
suppose H6: eq T (THead (Bind b) u0 t0) (THead (Flat Cast) u t)
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H7
consider H7
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
we proved land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
∀H6:eq T (THead (Bind b) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
case arity_head : c0:C u0:T a1:A :arity g c0 u0 (asucc g a1) t0:T a2:A :arity g (CHead c0 (Bind Abst) u0) t0 a2 ⇒
the thesis becomes
∀H5:eq T (THead (Bind Abst) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g (AHead a1 a2))) (arity g c0 t (AHead a1 a2))
() by induction hypothesis we know
eq T u0 (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g (asucc g a1))) (arity g c0 t (asucc g a1))
() by induction hypothesis we know
eq T t0 (THead (Flat Cast) u t)
→(land
arity g (CHead c0 (Bind Abst) u0) u (asucc g a2)
arity g (CHead c0 (Bind Abst) u0) t a2)
suppose H5: eq T (THead (Bind Abst) u0 t0) (THead (Flat Cast) u t)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abst) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abst) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
end of H6
consider H6
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove land (arity g c0 u (asucc g (AHead a1 a2))) (arity g c0 t (AHead a1 a2))
we proved land (arity g c0 u (asucc g (AHead a1 a2))) (arity g c0 t (AHead a1 a2))
∀H5:eq T (THead (Bind Abst) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g (AHead a1 a2))) (arity g c0 t (AHead a1 a2))
case arity_appl : c0:C u0:T a1:A :arity g c0 u0 a1 t0:T a2:A :arity g c0 t0 (AHead a1 a2) ⇒
the thesis becomes
∀H5:eq T (THead (Flat Appl) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
() by induction hypothesis we know
eq T u0 (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g a1)) (arity g c0 t a1)
() by induction hypothesis we know
eq T t0 (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g (AHead a1 a2))) (arity g c0 t (AHead a1 a2))
suppose H5: eq T (THead (Flat Appl) u0 t0) (THead (Flat Cast) u t)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) u0 t0 OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
end of H6
consider H6
we proved
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead k ⇒
<λ:K.Prop>
CASE k OF
Bind ⇒False
| Flat f⇒<λ:F.Prop> CASE f OF Appl⇒True | Cast⇒False
that is equivalent to False
we proceed by induction on the previous result to prove land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
we proved land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
∀H5:eq T (THead (Flat Appl) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
case arity_cast : c0:C u0:T a0:A H1:arity g c0 u0 (asucc g a0) t0:T H3:arity g c0 t0 a0 ⇒
the thesis becomes
∀H5:eq T (THead (Flat Cast) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
(H2) by induction hypothesis we know
eq T u0 (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g (asucc g a0))) (arity g c0 t (asucc g a0))
(H4) by induction hypothesis we know
eq T t0 (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
suppose H5: eq T (THead (Flat Cast) u0 t0) (THead (Flat Cast) u t)
(H6)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
THead (Flat Cast) u0 t0
λe:T.<λ:T.T> CASE e OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
THead (Flat Cast) u t
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
eq
T
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
THead (Flat Cast) u0 t0
λe:T.<λ:T.T> CASE e OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
THead (Flat Cast) u t
end of H7
suppose H8: eq T u0 u
(H10)
consider H7
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t0 OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒t0 | TLRef ⇒t0 | THead t1⇒t1
that is equivalent to eq T t0 t
we proceed by induction on the previous result to prove arity g c0 t a0
case refl_equal : ⇒
the thesis becomes the hypothesis H3
arity g c0 t a0
end of H10
(H12)
we proceed by induction on H8 to prove arity g c0 u (asucc g a0)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
arity g c0 u (asucc g a0)
end of H12
by (conj . . H12 H10)
we proved land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
(eq T u0 u)→(land (arity g c0 u (asucc g a0)) (arity g c0 t a0))
end of h1
(h2)
consider H6
we proved
eq
T
<λ:T.T> CASE THead (Flat Cast) u0 t0 OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
<λ:T.T> CASE THead (Flat Cast) u t OF TSort ⇒u0 | TLRef ⇒u0 | THead t1 ⇒t1
eq T u0 u
end of h2
by (h1 h2)
we proved land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
∀H5:eq T (THead (Flat Cast) u0 t0) (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a0)) (arity g c0 t a0)
case arity_repl : c0:C t0:T a1:A H1:arity g c0 t0 a1 a2:A H3:leq g a1 a2 ⇒
the thesis becomes
∀H4:eq T t0 (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
(H2) by induction hypothesis we know
eq T t0 (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g a1)) (arity g c0 t a1)
suppose H4: eq T t0 (THead (Flat Cast) u t)
(H5)
by (f_equal . . . . . H4)
we proved eq T t0 (THead (Flat Cast) u t)
eq T (λe:T.e t0) (λe:T.e (THead (Flat Cast) u t))
end of H5
(H6)
we proceed by induction on H5 to prove
eq T (THead (Flat Cast) u t) (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g a1)) (arity g c0 t a1)
case refl_equal : ⇒
the thesis becomes the hypothesis H2
eq T (THead (Flat Cast) u t) (THead (Flat Cast) u t)
→land (arity g c0 u (asucc g a1)) (arity g c0 t a1)
end of H6
(H8)
by (refl_equal . .)
we proved eq T (THead (Flat Cast) u t) (THead (Flat Cast) u t)
by (H6 previous)
land (arity g c0 u (asucc g a1)) (arity g c0 t a1)
end of H8
we proceed by induction on H8 to prove land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
case conj : H9:arity g c0 u (asucc g a1) H10:arity g c0 t a1 ⇒
the thesis becomes land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
(h1)
by (asucc_repl . . . H3)
we proved leq g (asucc g a1) (asucc g a2)
by (arity_repl . . . . H9 . previous)
arity g c0 u (asucc g a2)
end of h1
(h2)
by (arity_repl . . . . H10 . H3)
arity g c0 t a2
end of h2
by (conj . . h1 h2)
land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
we proved land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
∀H4:eq T t0 (THead (Flat Cast) u t)
.land (arity g c0 u (asucc g a2)) (arity g c0 t a2)
we proved
eq T y (THead (Flat Cast) u t)
→land (arity g c u (asucc g a)) (arity g c t a)
we proved
∀y:T
.arity g c y a
→(eq T y (THead (Flat Cast) u t)
→land (arity g c u (asucc g a)) (arity g c t a))
by (insert_eq . . . . previous H)
we proved land (arity g c u (asucc g a)) (arity g c t a)
we proved
∀g:G
.∀c:C
.∀u:T
.∀t:T
.∀a:A
.arity g c (THead (Flat Cast) u t) a
→land (arity g c u (asucc g a)) (arity g c t a)