DEFINITION arity_gen_sort()
TYPE =
∀g:G.∀c:C.∀n:nat.∀a:A.(arity g c (TSort n) a)→(leq g a (ASort O n))
BODY =
assume g: G
assume c: C
assume n: nat
assume a: A
suppose H: arity g c (TSort n) a
assume y: T
suppose H0: arity g c y a
we proceed by induction on H0 to prove (eq T y (TSort n))→(leq g a (ASort O n))
case arity_sort : :C n0:nat ⇒
the thesis becomes ∀H1:(eq T (TSort n0) (TSort n)).(leq g (ASort O n0) (ASort O n))
suppose H1: eq T (TSort n0) (TSort n)
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:T.nat> CASE TSort n0 OF TSort n1⇒n1 | TLRef ⇒n0 | THead ⇒n0
<λ:T.nat> CASE TSort n OF TSort n1⇒n1 | TLRef ⇒n0 | THead ⇒n0
eq
nat
λe:T.<λ:T.nat> CASE e OF TSort n1⇒n1 | TLRef ⇒n0 | THead ⇒n0 (TSort n0)
λe:T.<λ:T.nat> CASE e OF TSort n1⇒n1 | TLRef ⇒n0 | THead ⇒n0 (TSort n)
end of H2
(h1)
by (leq_refl . .)
leq g (ASort O n) (ASort O n)
end of h1
(h2)
consider H2
we proved
eq
nat
<λ:T.nat> CASE TSort n0 OF TSort n1⇒n1 | TLRef ⇒n0 | THead ⇒n0
<λ:T.nat> CASE TSort n OF TSort n1⇒n1 | TLRef ⇒n0 | THead ⇒n0
eq nat n0 n
end of h2
by (eq_ind_r . . . h1 . h2)
we proved leq g (ASort O n0) (ASort O n)
∀H1:(eq T (TSort n0) (TSort n)).(leq g (ASort O n0) (ASort O n))
case arity_abbr : c0:C d:C u:T i:nat :getl i c0 (CHead d (Bind Abbr) u) a0:A :arity g d u a0 ⇒
the thesis becomes ∀H4:(eq T (TLRef i) (TSort n)).(leq g a0 (ASort O n))
() by induction hypothesis we know (eq T u (TSort n))→(leq g a0 (ASort O n))
suppose H4: eq T (TLRef i) (TSort n)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE TSort n 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 TSort n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove leq g a0 (ASort O n)
we proved leq g a0 (ASort O n)
∀H4:(eq T (TLRef i) (TSort n)).(leq g a0 (ASort O n))
case arity_abst : c0:C d:C u:T i:nat :getl i c0 (CHead d (Bind Abst) u) a0:A :arity g d u (asucc g a0) ⇒
the thesis becomes ∀H4:(eq T (TLRef i) (TSort n)).(leq g a0 (ASort O n))
() by induction hypothesis we know (eq T u (TSort n))→(leq g (asucc g a0) (ASort O n))
suppose H4: eq T (TLRef i) (TSort n)
(H5)
we proceed by induction on H4 to prove
<λ:T.Prop>
CASE TSort n 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 TSort n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
end of H5
consider H5
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒True
| THead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove leq g a0 (ASort O n)
we proved leq g a0 (ASort O n)
∀H4:(eq T (TLRef i) (TSort n)).(leq g a0 (ASort O n))
case arity_bind : b:B :not (eq B b Abst) c0:C u:T a1:A :arity g c0 u a1 t:T a2:A :arity g (CHead c0 (Bind b) u) t a2 ⇒
the thesis becomes ∀H6:(eq T (THead (Bind b) u t) (TSort n)).(leq g a2 (ASort O n))
() by induction hypothesis we know (eq T u (TSort n))→(leq g a1 (ASort O n))
() by induction hypothesis we know (eq T t (TSort n))→(leq g a2 (ASort O n))
suppose H6: eq T (THead (Bind b) u t) (TSort n)
(H7)
we proceed by induction on H6 to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind b) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind b) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H7
consider H7
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove leq g a2 (ASort O n)
we proved leq g a2 (ASort O n)
∀H6:(eq T (THead (Bind b) u t) (TSort n)).(leq g a2 (ASort O n))
case arity_head : c0:C u:T a1:A :arity g c0 u (asucc g a1) t:T a2:A :arity g (CHead c0 (Bind Abst) u) t a2 ⇒
the thesis becomes
∀H5:eq T (THead (Bind Abst) u t) (TSort n)
.leq g (AHead a1 a2) (ASort O n)
() by induction hypothesis we know (eq T u (TSort n))→(leq g (asucc g a1) (ASort O n))
() by induction hypothesis we know (eq T t (TSort n))→(leq g a2 (ASort O n))
suppose H5: eq T (THead (Bind Abst) u t) (TSort n)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Bind Abst) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove leq g (AHead a1 a2) (ASort O n)
we proved leq g (AHead a1 a2) (ASort O n)
∀H5:eq T (THead (Bind Abst) u t) (TSort n)
.leq g (AHead a1 a2) (ASort O n)
case arity_appl : c0:C u:T a1:A :arity g c0 u a1 t:T a2:A :arity g c0 t (AHead a1 a2) ⇒
the thesis becomes ∀H5:(eq T (THead (Flat Appl) u t) (TSort n)).(leq g a2 (ASort O n))
() by induction hypothesis we know (eq T u (TSort n))→(leq g a1 (ASort O n))
() by induction hypothesis we know (eq T t (TSort n))→(leq g (AHead a1 a2) (ASort O n))
suppose H5: eq T (THead (Flat Appl) u t) (TSort n)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Appl) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Appl) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove leq g a2 (ASort O n)
we proved leq g a2 (ASort O n)
∀H5:(eq T (THead (Flat Appl) u t) (TSort n)).(leq g a2 (ASort O n))
case arity_cast : c0:C u:T a0:A :arity g c0 u (asucc g a0) t:T :arity g c0 t a0 ⇒
the thesis becomes ∀H5:(eq T (THead (Flat Cast) u t) (TSort n)).(leq g a0 (ASort O n))
() by induction hypothesis we know (eq T u (TSort n))→(leq g (asucc g a0) (ASort O n))
() by induction hypothesis we know (eq T t (TSort n))→(leq g a0 (ASort O n))
suppose H5: eq T (THead (Flat Cast) u t) (TSort n)
(H6)
we proceed by induction on H5 to prove
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
consider I
we proved True
<λ:T.Prop>
CASE THead (Flat Cast) u t OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
end of H6
consider H6
we proved
<λ:T.Prop>
CASE TSort n OF
TSort ⇒False
| TLRef ⇒False
| THead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove leq g a0 (ASort O n)
we proved leq g a0 (ASort O n)
∀H5:(eq T (THead (Flat Cast) u t) (TSort n)).(leq g a0 (ASort O n))
case arity_repl : c0:C t:T a1:A H1:arity g c0 t a1 a2:A H3:leq g a1 a2 ⇒
the thesis becomes ∀H4:(eq T t (TSort n)).(leq g a2 (ASort O n))
(H2) by induction hypothesis we know (eq T t (TSort n))→(leq g a1 (ASort O n))
suppose H4: eq T t (TSort n)
(H5)
by (f_equal . . . . . H4)
we proved eq T t (TSort n)
eq T (λe:T.e t) (λe:T.e (TSort n))
end of H5
(H6)
we proceed by induction on H5 to prove (eq T (TSort n) (TSort n))→(leq g a1 (ASort O n))
case refl_equal : ⇒
the thesis becomes the hypothesis H2
(eq T (TSort n) (TSort n))→(leq g a1 (ASort O n))
end of H6
(h1)
by (leq_sym . . . H3)
leq g a2 a1
end of h1
(h2)
by (refl_equal . .)
we proved eq T (TSort n) (TSort n)
by (H6 previous)
leq g a1 (ASort O n)
end of h2
by (leq_trans . . . h1 . h2)
we proved leq g a2 (ASort O n)
∀H4:(eq T t (TSort n)).(leq g a2 (ASort O n))
we proved (eq T y (TSort n))→(leq g a (ASort O n))
we proved
∀y:T
.arity g c y a
→(eq T y (TSort n))→(leq g a (ASort O n))
by (insert_eq . . . . previous H)
we proved leq g a (ASort O n)
we proved ∀g:G.∀c:C.∀n:nat.∀a:A.(arity g c (TSort n) a)→(leq g a (ASort O n))