DEFINITION asucc_inj()
TYPE =
∀g:G.∀a1:A.∀a2:A.(leq g (asucc g a1) (asucc g a2))→(leq g a1 a2)
BODY =
assume g: G
assume a1: A
we proceed by induction on a1 to prove ∀a2:A.(leq g (asucc g a1) (asucc g a2))→(leq g a1 a2)
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀a2:A
.(leq g (asucc g (ASort n n0)) (asucc g a2))→(leq g (ASort n n0) a2)
assume a2: A
we proceed by induction on a2 to prove
(leq g (asucc g (ASort n n0)) (asucc g a2))→(leq g (ASort n n0) a2)
case ASort : n1:nat n2:nat ⇒
the thesis becomes
∀H:leq g (asucc g (ASort n n0)) (asucc g (ASort n1 n2))
.leq g (ASort n n0) (ASort n1 n2)
suppose H: leq g (asucc g (ASort n n0)) (asucc g (ASort n1 n2))
suppose H0: leq g (asucc g (ASort O n0)) (asucc g (ASort n1 n2))
suppose H1: leq g (asucc g (ASort O n0)) (asucc g (ASort O n2))
(H_x)
consider H1
we proved leq g (asucc g (ASort O n0)) (asucc g (ASort O n2))
that is equivalent to leq g (ASort O (next g n0)) (ASort O (next g n2))
by (leq_gen_sort1 . . . . previous)
ex2_3
nat
nat
nat
λn2:nat
.λh2:nat
.λk:nat.eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A (ASort O (next g n2)) (ASort h2 n2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove leq g (ASort O n0) (ASort O n2)
case ex2_3_intro : x0:nat x1:nat x2:nat H3:eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort x1 x0) x2) H4:eq A (ASort O (next g n2)) (ASort x1 x0) ⇒
the thesis becomes leq g (ASort O n0) (ASort O n2)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat> CASE ASort O (next g n2) OF ASort n3 ⇒n3 | AHead ⇒O
<λ:A.nat> CASE ASort x1 x0 OF ASort n3 ⇒n3 | AHead ⇒O
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n3 ⇒n3 | AHead ⇒O (ASort O (next g n2))
λe:A.<λ:A.nat> CASE e OF ASort n3 ⇒n3 | AHead ⇒O (ASort x1 x0)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat>
CASE ASort O (next g n2) OF
ASort n3⇒n3
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
<λ:A.nat>
CASE ASort x1 x0 OF
ASort n3⇒n3
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
eq
nat
λe:A
.<λ:A.nat>
CASE e OF
ASort n3⇒n3
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
ASort O (next g n2)
λe:A
.<λ:A.nat>
CASE e OF
ASort n3⇒n3
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
ASort x1 x0
end of H6
suppose H7: eq nat O x1
(H8)
by (eq_ind_r . . . H3 . H7)
eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort O x0) x2)
end of H8
(H9)
consider H6
we proved
eq
nat
<λ:A.nat>
CASE ASort O (next g n2) OF
ASort n3⇒n3
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
<λ:A.nat>
CASE ASort x1 x0 OF
ASort n3⇒n3
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
that is equivalent to eq nat (next g n2) x0
by (eq_ind_r . . . H8 . previous)
eq
A
aplus g (ASort O (next g n0)) x2
aplus g (ASort O (next g n2)) x2
end of H9
(H10)
by (aplus_sort_O_S_simpl . . .)
we proved eq A (aplus g (ASort O n0) (S x2)) (aplus g (ASort O (next g n0)) x2)
by (eq_ind_r . . . H9 . previous)
eq A (aplus g (ASort O n0) (S x2)) (aplus g (ASort O (next g n2)) x2)
end of H10
(H11)
by (aplus_sort_O_S_simpl . . .)
we proved eq A (aplus g (ASort O n2) (S x2)) (aplus g (ASort O (next g n2)) x2)
by (eq_ind_r . . . H10 . previous)
eq A (aplus g (ASort O n0) (S x2)) (aplus g (ASort O n2) (S x2))
end of H11
by (leq_sort . . . . . . H11)
we proved leq g (ASort O n0) (ASort O n2)
(eq nat O x1)→(leq g (ASort O n0) (ASort O n2))
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:A.nat> CASE ASort O (next g n2) OF ASort n3 ⇒n3 | AHead ⇒O
<λ:A.nat> CASE ASort x1 x0 OF ASort n3 ⇒n3 | AHead ⇒O
eq nat O x1
end of h2
by (h1 h2)
leq g (ASort O n0) (ASort O n2)
we proved leq g (ASort O n0) (ASort O n2)
leq g (asucc g (ASort O n0)) (asucc g (ASort O n2))
→leq g (ASort O n0) (ASort O n2)
assume n3: nat
suppose :
leq g (asucc g (ASort O n0)) (asucc g (ASort n3 n2))
→leq g (ASort O n0) (ASort n3 n2)
suppose H1: leq g (asucc g (ASort O n0)) (asucc g (ASort (S n3) n2))
(H_x)
consider H1
we proved leq g (asucc g (ASort O n0)) (asucc g (ASort (S n3) n2))
that is equivalent to leq g (ASort O (next g n0)) (ASort n3 n2)
by (leq_gen_sort1 . . . . previous)
ex2_3
nat
nat
nat
λn2:nat
.λh2:nat
.λk:nat.eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A (ASort n3 n2) (ASort h2 n2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove leq g (ASort O n0) (ASort (S n3) n2)
case ex2_3_intro : x0:nat x1:nat x2:nat H3:eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort x1 x0) x2) H4:eq A (ASort n3 n2) (ASort x1 x0) ⇒
the thesis becomes leq g (ASort O n0) (ASort (S n3) n2)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat> CASE ASort n3 n2 OF ASort n4 ⇒n4 | AHead ⇒n3
<λ:A.nat> CASE ASort x1 x0 OF ASort n4 ⇒n4 | AHead ⇒n3
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n4 ⇒n4 | AHead ⇒n3 (ASort n3 n2)
λe:A.<λ:A.nat> CASE e OF ASort n4 ⇒n4 | AHead ⇒n3 (ASort x1 x0)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat> CASE ASort n3 n2 OF ASort n4⇒n4 | AHead ⇒n2
<λ:A.nat> CASE ASort x1 x0 OF ASort n4⇒n4 | AHead ⇒n2
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n4⇒n4 | AHead ⇒n2 (ASort n3 n2)
λe:A.<λ:A.nat> CASE e OF ASort n4⇒n4 | AHead ⇒n2 (ASort x1 x0)
end of H6
suppose H7: eq nat n3 x1
(H8)
by (eq_ind_r . . . H3 . H7)
eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort n3 x0) x2)
end of H8
(H9)
consider H6
we proved
eq
nat
<λ:A.nat> CASE ASort n3 n2 OF ASort n4⇒n4 | AHead ⇒n2
<λ:A.nat> CASE ASort x1 x0 OF ASort n4⇒n4 | AHead ⇒n2
that is equivalent to eq nat n2 x0
by (eq_ind_r . . . H8 . previous)
eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort n3 n2) x2)
end of H9
(H10)
by (aplus_sort_O_S_simpl . . .)
we proved eq A (aplus g (ASort O n0) (S x2)) (aplus g (ASort O (next g n0)) x2)
by (eq_ind_r . . . H9 . previous)
eq A (aplus g (ASort O n0) (S x2)) (aplus g (ASort n3 n2) x2)
end of H10
(H11)
by (aplus_sort_S_S_simpl . . . .)
we proved eq A (aplus g (ASort (S n3) n2) (S x2)) (aplus g (ASort n3 n2) x2)
by (eq_ind_r . . . H10 . previous)
eq A (aplus g (ASort O n0) (S x2)) (aplus g (ASort (S n3) n2) (S x2))
end of H11
by (leq_sort . . . . . . H11)
we proved leq g (ASort O n0) (ASort (S n3) n2)
(eq nat n3 x1)→(leq g (ASort O n0) (ASort (S n3) n2))
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:A.nat> CASE ASort n3 n2 OF ASort n4 ⇒n4 | AHead ⇒n3
<λ:A.nat> CASE ASort x1 x0 OF ASort n4 ⇒n4 | AHead ⇒n3
eq nat n3 x1
end of h2
by (h1 h2)
leq g (ASort O n0) (ASort (S n3) n2)
we proved leq g (ASort O n0) (ASort (S n3) n2)
∀H1:leq g (asucc g (ASort O n0)) (asucc g (ASort (S n3) n2))
.leq g (ASort O n0) (ASort (S n3) n2)
by (previous . H0)
we proved leq g (ASort O n0) (ASort n1 n2)
leq g (asucc g (ASort O n0)) (asucc g (ASort n1 n2))
→leq g (ASort O n0) (ASort n1 n2)
assume n3: nat
suppose IHn:
leq g (asucc g (ASort n3 n0)) (asucc g (ASort n1 n2))
→leq g (ASort n3 n0) (ASort n1 n2)
suppose H0: leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n1 n2))
suppose H1: leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort O n2))
suppose :
leq g (asucc g (ASort n3 n0)) (asucc g (ASort O n2))
→leq g (ASort n3 n0) (ASort O n2)
(H_x)
consider H1
we proved leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort O n2))
that is equivalent to leq g (ASort n3 n0) (ASort O (next g n2))
by (leq_gen_sort1 . . . . previous)
ex2_3
nat
nat
nat
λn2:nat.λh2:nat.λk:nat.eq A (aplus g (ASort n3 n0) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A (ASort O (next g n2)) (ASort h2 n2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove leq g (ASort (S n3) n0) (ASort O n2)
case ex2_3_intro : x0:nat x1:nat x2:nat H3:eq A (aplus g (ASort n3 n0) x2) (aplus g (ASort x1 x0) x2) H4:eq A (ASort O (next g n2)) (ASort x1 x0) ⇒
the thesis becomes leq g (ASort (S n3) n0) (ASort O n2)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat> CASE ASort O (next g n2) OF ASort n4 ⇒n4 | AHead ⇒O
<λ:A.nat> CASE ASort x1 x0 OF ASort n4 ⇒n4 | AHead ⇒O
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n4 ⇒n4 | AHead ⇒O (ASort O (next g n2))
λe:A.<λ:A.nat> CASE e OF ASort n4 ⇒n4 | AHead ⇒O (ASort x1 x0)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat>
CASE ASort O (next g n2) OF
ASort n4⇒n4
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
<λ:A.nat>
CASE ASort x1 x0 OF
ASort n4⇒n4
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
eq
nat
λe:A
.<λ:A.nat>
CASE e OF
ASort n4⇒n4
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
ASort O (next g n2)
λe:A
.<λ:A.nat>
CASE e OF
ASort n4⇒n4
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
ASort x1 x0
end of H6
suppose H7: eq nat O x1
(H8)
by (eq_ind_r . . . H3 . H7)
eq A (aplus g (ASort n3 n0) x2) (aplus g (ASort O x0) x2)
end of H8
(H9)
consider H6
we proved
eq
nat
<λ:A.nat>
CASE ASort O (next g n2) OF
ASort n4⇒n4
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
<λ:A.nat>
CASE ASort x1 x0 OF
ASort n4⇒n4
| AHead ⇒<λg1:G.nat→nat> CASE g OF mk_G next ⇒next n2
that is equivalent to eq nat (next g n2) x0
by (eq_ind_r . . . H8 . previous)
eq A (aplus g (ASort n3 n0) x2) (aplus g (ASort O (next g n2)) x2)
end of H9
(H10)
by (aplus_sort_S_S_simpl . . . .)
we proved eq A (aplus g (ASort (S n3) n0) (S x2)) (aplus g (ASort n3 n0) x2)
by (eq_ind_r . . . H9 . previous)
eq
A
aplus g (ASort (S n3) n0) (S x2)
aplus g (ASort O (next g n2)) x2
end of H10
(H11)
by (aplus_sort_O_S_simpl . . .)
we proved eq A (aplus g (ASort O n2) (S x2)) (aplus g (ASort O (next g n2)) x2)
by (eq_ind_r . . . H10 . previous)
eq A (aplus g (ASort (S n3) n0) (S x2)) (aplus g (ASort O n2) (S x2))
end of H11
by (leq_sort . . . . . . H11)
we proved leq g (ASort (S n3) n0) (ASort O n2)
(eq nat O x1)→(leq g (ASort (S n3) n0) (ASort O n2))
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:A.nat> CASE ASort O (next g n2) OF ASort n4 ⇒n4 | AHead ⇒O
<λ:A.nat> CASE ASort x1 x0 OF ASort n4 ⇒n4 | AHead ⇒O
eq nat O x1
end of h2
by (h1 h2)
leq g (ASort (S n3) n0) (ASort O n2)
we proved leq g (ASort (S n3) n0) (ASort O n2)
leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort O n2))
→(leq g (asucc g (ASort n3 n0)) (asucc g (ASort O n2))
→leq g (ASort n3 n0) (ASort O n2)
→leq g (ASort (S n3) n0) (ASort O n2))
assume n4: nat
suppose :
leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n4 n2))
→(leq g (asucc g (ASort n3 n0)) (asucc g (ASort n4 n2))
→leq g (ASort n3 n0) (ASort n4 n2)
→leq g (ASort (S n3) n0) (ASort n4 n2))
suppose H1: leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort (S n4) n2))
suppose :
leq g (asucc g (ASort n3 n0)) (asucc g (ASort (S n4) n2))
→leq g (ASort n3 n0) (ASort (S n4) n2)
(H_x)
consider H1
we proved leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort (S n4) n2))
that is equivalent to leq g (ASort n3 n0) (ASort n4 n2)
by (leq_gen_sort1 . . . . previous)
ex2_3
nat
nat
nat
λn2:nat.λh2:nat.λk:nat.eq A (aplus g (ASort n3 n0) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A (ASort n4 n2) (ASort h2 n2)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove leq g (ASort (S n3) n0) (ASort (S n4) n2)
case ex2_3_intro : x0:nat x1:nat x2:nat H3:eq A (aplus g (ASort n3 n0) x2) (aplus g (ASort x1 x0) x2) H4:eq A (ASort n4 n2) (ASort x1 x0) ⇒
the thesis becomes leq g (ASort (S n3) n0) (ASort (S n4) n2)
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat> CASE ASort n4 n2 OF ASort n5 ⇒n5 | AHead ⇒n4
<λ:A.nat> CASE ASort x1 x0 OF ASort n5 ⇒n5 | AHead ⇒n4
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n5 ⇒n5 | AHead ⇒n4 (ASort n4 n2)
λe:A.<λ:A.nat> CASE e OF ASort n5 ⇒n5 | AHead ⇒n4 (ASort x1 x0)
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat> CASE ASort n4 n2 OF ASort n5⇒n5 | AHead ⇒n2
<λ:A.nat> CASE ASort x1 x0 OF ASort n5⇒n5 | AHead ⇒n2
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n5⇒n5 | AHead ⇒n2 (ASort n4 n2)
λe:A.<λ:A.nat> CASE e OF ASort n5⇒n5 | AHead ⇒n2 (ASort x1 x0)
end of H6
suppose H7: eq nat n4 x1
(H8)
by (eq_ind_r . . . H3 . H7)
eq A (aplus g (ASort n3 n0) x2) (aplus g (ASort n4 x0) x2)
end of H8
(H9)
consider H6
we proved
eq
nat
<λ:A.nat> CASE ASort n4 n2 OF ASort n5⇒n5 | AHead ⇒n2
<λ:A.nat> CASE ASort x1 x0 OF ASort n5⇒n5 | AHead ⇒n2
that is equivalent to eq nat n2 x0
by (eq_ind_r . . . H8 . previous)
eq A (aplus g (ASort n3 n0) x2) (aplus g (ASort n4 n2) x2)
end of H9
(H10)
by (aplus_sort_S_S_simpl . . . .)
we proved eq A (aplus g (ASort (S n3) n0) (S x2)) (aplus g (ASort n3 n0) x2)
by (eq_ind_r . . . H9 . previous)
eq A (aplus g (ASort (S n3) n0) (S x2)) (aplus g (ASort n4 n2) x2)
end of H10
(H11)
by (aplus_sort_S_S_simpl . . . .)
we proved eq A (aplus g (ASort (S n4) n2) (S x2)) (aplus g (ASort n4 n2) x2)
by (eq_ind_r . . . H10 . previous)
eq
A
aplus g (ASort (S n3) n0) (S x2)
aplus g (ASort (S n4) n2) (S x2)
end of H11
by (leq_sort . . . . . . H11)
we proved leq g (ASort (S n3) n0) (ASort (S n4) n2)
(eq nat n4 x1)→(leq g (ASort (S n3) n0) (ASort (S n4) n2))
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:A.nat> CASE ASort n4 n2 OF ASort n5 ⇒n5 | AHead ⇒n4
<λ:A.nat> CASE ASort x1 x0 OF ASort n5 ⇒n5 | AHead ⇒n4
eq nat n4 x1
end of h2
by (h1 h2)
leq g (ASort (S n3) n0) (ASort (S n4) n2)
we proved leq g (ASort (S n3) n0) (ASort (S n4) n2)
∀H1:leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort (S n4) n2))
.leq g (asucc g (ASort n3 n0)) (asucc g (ASort (S n4) n2))
→leq g (ASort n3 n0) (ASort (S n4) n2)
→leq g (ASort (S n3) n0) (ASort (S n4) n2)
by (previous . H0 IHn)
we proved leq g (ASort (S n3) n0) (ASort n1 n2)
∀H0:leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n1 n2))
.leq g (ASort (S n3) n0) (ASort n1 n2)
by (previous . H)
we proved leq g (ASort n n0) (ASort n1 n2)
∀H:leq g (asucc g (ASort n n0)) (asucc g (ASort n1 n2))
.leq g (ASort n n0) (ASort n1 n2)
case AHead : a:A a0:A ⇒
the thesis becomes
∀H1:leq g (asucc g (ASort n n0)) (asucc g (AHead a a0))
.leq g (ASort n n0) (AHead a a0)
(H) by induction hypothesis we know
leq g (asucc g (ASort n n0)) (asucc g a)
→leq g (ASort n n0) a
(H0) by induction hypothesis we know
(leq g (asucc g (ASort n n0)) (asucc g a0))→(leq g (ASort n n0) a0)
suppose H1: leq g (asucc g (ASort n n0)) (asucc g (AHead a a0))
suppose :
leq g (asucc g (ASort O n0)) (asucc g a)
→leq g (ASort O n0) a
suppose :
(leq g (asucc g (ASort O n0)) (asucc g a0))→(leq g (ASort O n0) a0)
suppose H4: leq g (asucc g (ASort O n0)) (asucc g (AHead a a0))
(H_x)
consider H4
we proved leq g (asucc g (ASort O n0)) (asucc g (AHead a a0))
that is equivalent to leq g (ASort O (next g n0)) (AHead a (asucc g a0))
by (leq_gen_sort1 . . . . previous)
ex2_3
nat
nat
nat
λn2:nat
.λh2:nat
.λk:nat.eq A (aplus g (ASort O (next g n0)) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A (AHead a (asucc g a0)) (ASort h2 n2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove leq g (ASort O n0) (AHead a a0)
case ex2_3_intro : x0:nat x1:nat x2:nat :eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort x1 x0) x2) H7:eq A (AHead a (asucc g a0)) (ASort x1 x0) ⇒
the thesis becomes leq g (ASort O n0) (AHead a a0)
(H8)
we proceed by induction on H7 to prove <λ:A.Prop> CASE ASort x1 x0 OF ASort ⇒False | AHead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:A.Prop> CASE AHead a (asucc g a0) OF ASort ⇒False | AHead ⇒True
consider I
we proved True
<λ:A.Prop> CASE AHead a (asucc g a0) OF ASort ⇒False | AHead ⇒True
<λ:A.Prop> CASE ASort x1 x0 OF ASort ⇒False | AHead ⇒True
end of H8
consider H8
we proved <λ:A.Prop> CASE ASort x1 x0 OF ASort ⇒False | AHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove leq g (ASort O n0) (AHead a a0)
leq g (ASort O n0) (AHead a a0)
we proved leq g (ASort O n0) (AHead a a0)
leq g (asucc g (ASort O n0)) (asucc g a)
→leq g (ASort O n0) a
→((leq g (asucc g (ASort O n0)) (asucc g a0))→(leq g (ASort O n0) a0)
→(leq g (asucc g (ASort O n0)) (asucc g (AHead a a0))
→leq g (ASort O n0) (AHead a a0)))
assume n1: nat
suppose :
(leq g (asucc g (ASort n1 n0)) (asucc g a))→(leq g (ASort n1 n0) a)
→((leq g (asucc g (ASort n1 n0)) (asucc g a0))→(leq g (ASort n1 n0) a0)
→(leq g (asucc g (ASort n1 n0)) (asucc g (AHead a a0))
→leq g (ASort n1 n0) (AHead a a0)))
suppose :
leq g (asucc g (ASort (S n1) n0)) (asucc g a)
→leq g (ASort (S n1) n0) a
suppose :
leq g (asucc g (ASort (S n1) n0)) (asucc g a0)
→leq g (ASort (S n1) n0) a0
suppose H4: leq g (asucc g (ASort (S n1) n0)) (asucc g (AHead a a0))
(H_x)
consider H4
we proved leq g (asucc g (ASort (S n1) n0)) (asucc g (AHead a a0))
that is equivalent to leq g (ASort n1 n0) (AHead a (asucc g a0))
by (leq_gen_sort1 . . . . previous)
ex2_3
nat
nat
nat
λn2:nat.λh2:nat.λk:nat.eq A (aplus g (ASort n1 n0) k) (aplus g (ASort h2 n2) k)
λn2:nat.λh2:nat.λ:nat.eq A (AHead a (asucc g a0)) (ASort h2 n2)
end of H_x
(H5) consider H_x
we proceed by induction on H5 to prove leq g (ASort (S n1) n0) (AHead a a0)
case ex2_3_intro : x0:nat x1:nat x2:nat :eq A (aplus g (ASort n1 n0) x2) (aplus g (ASort x1 x0) x2) H7:eq A (AHead a (asucc g a0)) (ASort x1 x0) ⇒
the thesis becomes leq g (ASort (S n1) n0) (AHead a a0)
(H8)
we proceed by induction on H7 to prove <λ:A.Prop> CASE ASort x1 x0 OF ASort ⇒False | AHead ⇒True
case refl_equal : ⇒
the thesis becomes
<λ:A.Prop> CASE AHead a (asucc g a0) OF ASort ⇒False | AHead ⇒True
consider I
we proved True
<λ:A.Prop> CASE AHead a (asucc g a0) OF ASort ⇒False | AHead ⇒True
<λ:A.Prop> CASE ASort x1 x0 OF ASort ⇒False | AHead ⇒True
end of H8
consider H8
we proved <λ:A.Prop> CASE ASort x1 x0 OF ASort ⇒False | AHead ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove leq g (ASort (S n1) n0) (AHead a a0)
leq g (ASort (S n1) n0) (AHead a a0)
we proved leq g (ASort (S n1) n0) (AHead a a0)
leq g (asucc g (ASort (S n1) n0)) (asucc g a)
→leq g (ASort (S n1) n0) a
→(leq g (asucc g (ASort (S n1) n0)) (asucc g a0)
→leq g (ASort (S n1) n0) a0
→∀H4:leq g (asucc g (ASort (S n1) n0)) (asucc g (AHead a a0))
.leq g (ASort (S n1) n0) (AHead a a0))
by (previous . H H0 H1)
we proved leq g (ASort n n0) (AHead a a0)
∀H1:leq g (asucc g (ASort n n0)) (asucc g (AHead a a0))
.leq g (ASort n n0) (AHead a a0)
we proved
(leq g (asucc g (ASort n n0)) (asucc g a2))→(leq g (ASort n n0) a2)
∀a2:A
.(leq g (asucc g (ASort n n0)) (asucc g a2))→(leq g (ASort n n0) a2)
case AHead : a:A a0:A ⇒
the thesis becomes
∀a2:A
.(leq g (asucc g (AHead a a0)) (asucc g a2))→(leq g (AHead a a0) a2)
() by induction hypothesis we know ∀a2:A.(leq g (asucc g a) (asucc g a2))→(leq g a a2)
(H0) by induction hypothesis we know ∀a2:A.(leq g (asucc g a0) (asucc g a2))→(leq g a0 a2)
assume a2: A
we proceed by induction on a2 to prove
(leq g (asucc g (AHead a a0)) (asucc g a2))→(leq g (AHead a a0) a2)
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀H1:leq g (asucc g (AHead a a0)) (asucc g (ASort n n0))
.leq g (AHead a a0) (ASort n n0)
suppose H1: leq g (asucc g (AHead a a0)) (asucc g (ASort n n0))
suppose H2: leq g (asucc g (AHead a a0)) (asucc g (ASort O n0))
(H_x)
consider H2
we proved leq g (asucc g (AHead a a0)) (asucc g (ASort O n0))
that is equivalent to leq g (AHead a (asucc g a0)) (ASort O (next g n0))
by (leq_gen_head1 . . . . previous)
ex3_2
A
A
λa3:A.λ:A.leq g a a3
λ:A.λa4:A.leq g (asucc g a0) a4
λa3:A.λa4:A.eq A (ASort O (next g n0)) (AHead a3 a4)
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove leq g (AHead a a0) (ASort O n0)
case ex3_2_intro : x0:A x1:A :leq g a x0 :leq g (asucc g a0) x1 H6:eq A (ASort O (next g n0)) (AHead x0 x1) ⇒
the thesis becomes leq g (AHead a a0) (ASort O n0)
(H7)
we proceed by induction on H6 to prove <λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
case refl_equal : ⇒
the thesis becomes <λ:A.Prop> CASE ASort O (next g n0) OF ASort ⇒True | AHead ⇒False
consider I
we proved True
<λ:A.Prop> CASE ASort O (next g n0) OF ASort ⇒True | AHead ⇒False
<λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
end of H7
consider H7
we proved <λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove leq g (AHead a a0) (ASort O n0)
leq g (AHead a a0) (ASort O n0)
we proved leq g (AHead a a0) (ASort O n0)
leq g (asucc g (AHead a a0)) (asucc g (ASort O n0))
→leq g (AHead a a0) (ASort O n0)
assume n1: nat
suppose :
leq g (asucc g (AHead a a0)) (asucc g (ASort n1 n0))
→leq g (AHead a a0) (ASort n1 n0)
suppose H2: leq g (asucc g (AHead a a0)) (asucc g (ASort (S n1) n0))
(H_x)
consider H2
we proved leq g (asucc g (AHead a a0)) (asucc g (ASort (S n1) n0))
that is equivalent to leq g (AHead a (asucc g a0)) (ASort n1 n0)
by (leq_gen_head1 . . . . previous)
ex3_2
A
A
λa3:A.λ:A.leq g a a3
λ:A.λa4:A.leq g (asucc g a0) a4
λa3:A.λa4:A.eq A (ASort n1 n0) (AHead a3 a4)
end of H_x
(H3) consider H_x
we proceed by induction on H3 to prove leq g (AHead a a0) (ASort (S n1) n0)
case ex3_2_intro : x0:A x1:A :leq g a x0 :leq g (asucc g a0) x1 H6:eq A (ASort n1 n0) (AHead x0 x1) ⇒
the thesis becomes leq g (AHead a a0) (ASort (S n1) n0)
(H7)
we proceed by induction on H6 to prove <λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
case refl_equal : ⇒
the thesis becomes <λ:A.Prop> CASE ASort n1 n0 OF ASort ⇒True | AHead ⇒False
consider I
we proved True
<λ:A.Prop> CASE ASort n1 n0 OF ASort ⇒True | AHead ⇒False
<λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
end of H7
consider H7
we proved <λ:A.Prop> CASE AHead x0 x1 OF ASort ⇒True | AHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove leq g (AHead a a0) (ASort (S n1) n0)
leq g (AHead a a0) (ASort (S n1) n0)
we proved leq g (AHead a a0) (ASort (S n1) n0)
∀H2:leq g (asucc g (AHead a a0)) (asucc g (ASort (S n1) n0))
.leq g (AHead a a0) (ASort (S n1) n0)
by (previous . H1)
we proved leq g (AHead a a0) (ASort n n0)
∀H1:leq g (asucc g (AHead a a0)) (asucc g (ASort n n0))
.leq g (AHead a a0) (ASort n n0)
case AHead : a3:A a4:A ⇒
the thesis becomes
∀H3:leq g (asucc g (AHead a a0)) (asucc g (AHead a3 a4))
.leq g (AHead a a0) (AHead a3 a4)
() by induction hypothesis we know
(leq g (asucc g (AHead a a0)) (asucc g a3))→(leq g (AHead a a0) a3)
() by induction hypothesis we know
(leq g (asucc g (AHead a a0)) (asucc g a4))→(leq g (AHead a a0) a4)
suppose H3: leq g (asucc g (AHead a a0)) (asucc g (AHead a3 a4))
(H_x)
consider H3
we proved leq g (asucc g (AHead a a0)) (asucc g (AHead a3 a4))
that is equivalent to leq g (AHead a (asucc g a0)) (AHead a3 (asucc g a4))
by (leq_gen_head1 . . . . previous)
ex3_2
A
A
λa3:A.λ:A.leq g a a3
λ:A.λa4:A.leq g (asucc g a0) a4
λa3:A.λa4:A.eq A (AHead a3 (asucc g a4)) (AHead a3 a4)
end of H_x
(H4) consider H_x
we proceed by induction on H4 to prove leq g (AHead a a0) (AHead a3 a4)
case ex3_2_intro : x0:A x1:A H5:leq g a x0 H6:leq g (asucc g a0) x1 H7:eq A (AHead a3 (asucc g a4)) (AHead x0 x1) ⇒
the thesis becomes leq g (AHead a a0) (AHead a3 a4)
(H8)
by (f_equal . . . . . H7)
we proved
eq
A
<λ:A.A> CASE AHead a3 (asucc g a4) OF ASort ⇒a3 | AHead a5 ⇒a5
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a3 | AHead a5 ⇒a5
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a3 | AHead a5 ⇒a5 (AHead a3 (asucc g a4))
λe:A.<λ:A.A> CASE e OF ASort ⇒a3 | AHead a5 ⇒a5 (AHead x0 x1)
end of H8
(h1)
(H9)
by (f_equal . . . . . H7)
we proved
eq
A
<λ:A.A>
CASE AHead a3 (asucc g a4) OF
ASort ⇒
FIXasucc{
asucc:G→A→A
:=λg0:G
.λl:A
.<λa5:A.A>
CASE l OF
ASort n0 n⇒<λn1:nat.A> CASE n0 OF O⇒ASort O (next g0 n) | S h⇒ASort h n
| AHead a5 a6⇒AHead a5 (asucc g0 a6)
}
g
a4
| AHead a5⇒a5
<λ:A.A>
CASE AHead x0 x1 OF
ASort ⇒
FIXasucc{
asucc:G→A→A
:=λg0:G
.λl:A
.<λa5:A.A>
CASE l OF
ASort n0 n⇒<λn1:nat.A> CASE n0 OF O⇒ASort O (next g0 n) | S h⇒ASort h n
| AHead a5 a6⇒AHead a5 (asucc g0 a6)
}
g
a4
| AHead a5⇒a5
eq
A
λe:A
.<λ:A.A>
CASE e OF
ASort ⇒
FIXasucc{
asucc:G→A→A
:=λg0:G
.λl:A
.<λa5:A.A>
CASE l OF
ASort n0 n⇒<λn1:nat.A> CASE n0 OF O⇒ASort O (next g0 n) | S h⇒ASort h n
| AHead a5 a6⇒AHead a5 (asucc g0 a6)
}
g
a4
| AHead a5⇒a5
AHead a3 (asucc g a4)
λe:A
.<λ:A.A>
CASE e OF
ASort ⇒
FIXasucc{
asucc:G→A→A
:=λg0:G
.λl:A
.<λa5:A.A>
CASE l OF
ASort n0 n⇒<λn1:nat.A> CASE n0 OF O⇒ASort O (next g0 n) | S h⇒ASort h n
| AHead a5 a6⇒AHead a5 (asucc g0 a6)
}
g
a4
| AHead a5⇒a5
AHead x0 x1
end of H9
suppose H10: eq A a3 x0
(H11)
consider H9
we proved
eq
A
<λ:A.A>
CASE AHead a3 (asucc g a4) OF
ASort ⇒
FIXasucc{
asucc:G→A→A
:=λg0:G
.λl:A
.<λa5:A.A>
CASE l OF
ASort n0 n⇒<λn1:nat.A> CASE n0 OF O⇒ASort O (next g0 n) | S h⇒ASort h n
| AHead a5 a6⇒AHead a5 (asucc g0 a6)
}
g
a4
| AHead a5⇒a5
<λ:A.A>
CASE AHead x0 x1 OF
ASort ⇒
FIXasucc{
asucc:G→A→A
:=λg0:G
.λl:A
.<λa5:A.A>
CASE l OF
ASort n0 n⇒<λn1:nat.A> CASE n0 OF O⇒ASort O (next g0 n) | S h⇒ASort h n
| AHead a5 a6⇒AHead a5 (asucc g0 a6)
}
g
a4
| AHead a5⇒a5
that is equivalent to eq A (asucc g a4) x1
by (eq_ind_r . . . H6 . previous)
leq g (asucc g a0) (asucc g a4)
end of H11
(H12)
by (eq_ind_r . . . H5 . H10)
leq g a a3
end of H12
by (H0 . H11)
we proved leq g a0 a4
by (leq_head . . . H12 . . previous)
we proved leq g (AHead a a0) (AHead a3 a4)
(eq A a3 x0)→(leq g (AHead a a0) (AHead a3 a4))
end of h1
(h2)
consider H8
we proved
eq
A
<λ:A.A> CASE AHead a3 (asucc g a4) OF ASort ⇒a3 | AHead a5 ⇒a5
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a3 | AHead a5 ⇒a5
eq A a3 x0
end of h2
by (h1 h2)
leq g (AHead a a0) (AHead a3 a4)
we proved leq g (AHead a a0) (AHead a3 a4)
∀H3:leq g (asucc g (AHead a a0)) (asucc g (AHead a3 a4))
.leq g (AHead a a0) (AHead a3 a4)
we proved
(leq g (asucc g (AHead a a0)) (asucc g a2))→(leq g (AHead a a0) a2)
∀a2:A
.(leq g (asucc g (AHead a a0)) (asucc g a2))→(leq g (AHead a a0) a2)
we proved ∀a2:A.(leq g (asucc g a1) (asucc g a2))→(leq g a1 a2)
we proved ∀g:G.∀a1:A.∀a2:A.(leq g (asucc g a1) (asucc g a2))→(leq g a1 a2)