DEFINITION leq_asucc_false()
TYPE =
∀g:G.∀a:A.(leq g (asucc g a) a)→∀P:Prop.P
BODY =
assume g: G
assume a: A
we proceed by induction on a to prove (leq g (asucc g a) a)→∀P:Prop.P
case ASort : n:nat n0:nat ⇒
the thesis becomes (leq g (asucc g (ASort n n0)) (ASort n n0))→∀P:Prop.P
we must prove (leq g (asucc g (ASort n n0)) (ASort n n0))→∀P:Prop.P
or equivalently
(leq
g
<λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort n n0)
→∀P:Prop.P
suppose H:
leq
g
<λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort n n0
assume P: Prop
we must prove
(leq
g
<λn2:nat.A> CASE O OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort O n0)
→P
or equivalently (leq g (ASort O (next g n0)) (ASort O n0))→P
suppose H0: leq g (ASort O (next g n0)) (ASort O n0)
(H_x)
by (leq_gen_sort1 . . . . H0)
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 n0) (ASort h2 n2)
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove P
case ex2_3_intro : x0:nat x1:nat x2:nat H2:eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort x1 x0) x2) H3:eq A (ASort O n0) (ASort x1 x0) ⇒
the thesis becomes P
(H4)
by (f_equal . . . . . H3)
we proved
eq
nat
<λ:A.nat> CASE ASort O n0 OF ASort n1 ⇒n1 | AHead ⇒O
<λ:A.nat> CASE ASort x1 x0 OF ASort n1 ⇒n1 | AHead ⇒O
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n1 ⇒n1 | AHead ⇒O (ASort O n0)
λe:A.<λ:A.nat> CASE e OF ASort n1 ⇒n1 | AHead ⇒O (ASort x1 x0)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
nat
<λ:A.nat> CASE ASort O n0 OF ASort n1⇒n1 | AHead ⇒n0
<λ:A.nat> CASE ASort x1 x0 OF ASort n1⇒n1 | AHead ⇒n0
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n1⇒n1 | AHead ⇒n0 (ASort O n0)
λe:A.<λ:A.nat> CASE e OF ASort n1⇒n1 | AHead ⇒n0 (ASort x1 x0)
end of H5
suppose H6: eq nat O x1
(H7)
by (eq_ind_r . . . H2 . H6)
eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort O x0) x2)
end of H7
(H8)
consider H5
we proved
eq
nat
<λ:A.nat> CASE ASort O n0 OF ASort n1⇒n1 | AHead ⇒n0
<λ:A.nat> CASE ASort x1 x0 OF ASort n1⇒n1 | AHead ⇒n0
that is equivalent to eq nat n0 x0
by (eq_ind_r . . . H7 . previous)
eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort O n0) x2)
end of H8
(H9)
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 . . . H8 . previous)
eq A (aplus g (ASort O n0) (S x2)) (aplus g (ASort O n0) x2)
end of H9
(H_y)
by (aplus_inj . . . . H9)
eq nat (S x2) x2
end of H_y
by (le_n .)
we proved le x2 x2
by (eq_ind_r . . . previous . H_y)
we proved le (S x2) x2
by (le_Sx_x . previous .)
we proved P
(eq nat O x1)→P
end of h1
(h2)
consider H4
we proved
eq
nat
<λ:A.nat> CASE ASort O n0 OF ASort n1 ⇒n1 | AHead ⇒O
<λ:A.nat> CASE ASort x1 x0 OF ASort n1 ⇒n1 | AHead ⇒O
eq nat O x1
end of h2
by (h1 h2)
P
we proved P
we proved (leq g (ASort O (next g n0)) (ASort O n0))→P
(leq
g
<λn2:nat.A> CASE O OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort O n0)
→P
assume n1: nat
suppose :
(leq
g
<λn2:nat.A> CASE n1 OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort n1 n0)
→P
we must prove
(leq
g
<λn2:nat.A> CASE S n1 OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort (S n1) n0)
→P
or equivalently (leq g (ASort n1 n0) (ASort (S n1) n0))→P
suppose H0: leq g (ASort n1 n0) (ASort (S n1) n0)
(H_x)
by (leq_gen_sort1 . . . . H0)
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 (ASort (S n1) n0) (ASort h2 n2)
end of H_x
(H1) consider H_x
we proceed by induction on H1 to prove P
case ex2_3_intro : x0:nat x1:nat x2:nat H2:eq A (aplus g (ASort n1 n0) x2) (aplus g (ASort x1 x0) x2) H3:eq A (ASort (S n1) n0) (ASort x1 x0) ⇒
the thesis becomes P
(H4)
by (f_equal . . . . . H3)
we proved
eq
nat
<λ:A.nat> CASE ASort (S n1) n0 OF ASort n2 ⇒n2 | AHead ⇒S n1
<λ:A.nat> CASE ASort x1 x0 OF ASort n2 ⇒n2 | AHead ⇒S n1
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n2 ⇒n2 | AHead ⇒S n1 (ASort (S n1) n0)
λe:A.<λ:A.nat> CASE e OF ASort n2 ⇒n2 | AHead ⇒S n1 (ASort x1 x0)
end of H4
(h1)
(H5)
by (f_equal . . . . . H3)
we proved
eq
nat
<λ:A.nat> CASE ASort (S n1) n0 OF ASort n2⇒n2 | AHead ⇒n0
<λ:A.nat> CASE ASort x1 x0 OF ASort n2⇒n2 | AHead ⇒n0
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n2⇒n2 | AHead ⇒n0 (ASort (S n1) n0)
λe:A.<λ:A.nat> CASE e OF ASort n2⇒n2 | AHead ⇒n0 (ASort x1 x0)
end of H5
suppose H6: eq nat (S n1) x1
(H7)
by (eq_ind_r . . . H2 . H6)
eq A (aplus g (ASort n1 n0) x2) (aplus g (ASort (S n1) x0) x2)
end of H7
(H8)
consider H5
we proved
eq
nat
<λ:A.nat> CASE ASort (S n1) n0 OF ASort n2⇒n2 | AHead ⇒n0
<λ:A.nat> CASE ASort x1 x0 OF ASort n2⇒n2 | AHead ⇒n0
that is equivalent to eq nat n0 x0
by (eq_ind_r . . . H7 . previous)
eq A (aplus g (ASort n1 n0) x2) (aplus g (ASort (S n1) n0) x2)
end of H8
(H9)
by (aplus_sort_S_S_simpl . . . .)
we proved eq A (aplus g (ASort (S n1) n0) (S x2)) (aplus g (ASort n1 n0) x2)
by (eq_ind_r . . . H8 . previous)
eq A (aplus g (ASort (S n1) n0) (S x2)) (aplus g (ASort (S n1) n0) x2)
end of H9
(H_y)
by (aplus_inj . . . . H9)
eq nat (S x2) x2
end of H_y
by (le_n .)
we proved le x2 x2
by (eq_ind_r . . . previous . H_y)
we proved le (S x2) x2
by (le_Sx_x . previous .)
we proved P
(eq nat (S n1) x1)→P
end of h1
(h2)
consider H4
we proved
eq
nat
<λ:A.nat> CASE ASort (S n1) n0 OF ASort n2 ⇒n2 | AHead ⇒S n1
<λ:A.nat> CASE ASort x1 x0 OF ASort n2 ⇒n2 | AHead ⇒S n1
eq nat (S n1) x1
end of h2
by (h1 h2)
P
we proved P
we proved (leq g (ASort n1 n0) (ASort (S n1) n0))→P
(leq
g
<λn2:nat.A> CASE S n1 OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort (S n1) n0)
→P
by (previous . H)
we proved P
we proved
(leq
g
<λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h⇒ASort h n0
ASort n n0)
→∀P:Prop.P
(leq g (asucc g (ASort n n0)) (ASort n n0))→∀P:Prop.P
case AHead : a0:A a1:A ⇒
the thesis becomes (leq g (asucc g (AHead a0 a1)) (AHead a0 a1))→∀P:Prop.P
() by induction hypothesis we know (leq g (asucc g a0) a0)→∀P:Prop.P
(H0) by induction hypothesis we know (leq g (asucc g a1) a1)→∀P:Prop.P
we must prove (leq g (asucc g (AHead a0 a1)) (AHead a0 a1))→∀P:Prop.P
or equivalently (leq g (AHead a0 (asucc g a1)) (AHead a0 a1))→∀P:Prop.P
suppose H1: leq g (AHead a0 (asucc g a1)) (AHead a0 a1)
assume P: Prop
(H_x)
by (leq_gen_head1 . . . . H1)
ex3_2
A
A
λa3:A.λ:A.leq g a0 a3
λ:A.λa4:A.leq g (asucc g a1) a4
λa3:A.λa4:A.eq A (AHead a0 a1) (AHead a3 a4)
end of H_x
(H2) consider H_x
we proceed by induction on H2 to prove P
case ex3_2_intro : x0:A x1:A H3:leq g a0 x0 H4:leq g (asucc g a1) x1 H5:eq A (AHead a0 a1) (AHead x0 x1) ⇒
the thesis becomes P
(H6)
by (f_equal . . . . . H5)
we proved
eq
A
<λ:A.A> CASE AHead a0 a1 OF ASort ⇒a0 | AHead a2 ⇒a2
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a0 | AHead a2 ⇒a2
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a0 | AHead a2 ⇒a2 (AHead a0 a1)
λe:A.<λ:A.A> CASE e OF ASort ⇒a0 | AHead a2 ⇒a2 (AHead x0 x1)
end of H6
(h1)
(H7)
by (f_equal . . . . . H5)
we proved
eq
A
<λ:A.A> CASE AHead a0 a1 OF ASort ⇒a1 | AHead a2⇒a2
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a1 | AHead a2⇒a2
eq
A
λe:A.<λ:A.A> CASE e OF ASort ⇒a1 | AHead a2⇒a2 (AHead a0 a1)
λe:A.<λ:A.A> CASE e OF ASort ⇒a1 | AHead a2⇒a2 (AHead x0 x1)
end of H7
suppose H8: eq A a0 x0
(H9)
consider H7
we proved
eq
A
<λ:A.A> CASE AHead a0 a1 OF ASort ⇒a1 | AHead a2⇒a2
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a1 | AHead a2⇒a2
that is equivalent to eq A a1 x1
by (eq_ind_r . . . H4 . previous)
leq g (asucc g a1) a1
end of H9
by (H0 H9 .)
we proved P
(eq A a0 x0)→P
end of h1
(h2)
consider H6
we proved
eq
A
<λ:A.A> CASE AHead a0 a1 OF ASort ⇒a0 | AHead a2 ⇒a2
<λ:A.A> CASE AHead x0 x1 OF ASort ⇒a0 | AHead a2 ⇒a2
eq A a0 x0
end of h2
by (h1 h2)
P
we proved P
we proved (leq g (AHead a0 (asucc g a1)) (AHead a0 a1))→∀P:Prop.P
(leq g (asucc g (AHead a0 a1)) (AHead a0 a1))→∀P:Prop.P
we proved (leq g (asucc g a) a)→∀P:Prop.P
we proved ∀g:G.∀a:A.(leq g (asucc g a) a)→∀P:Prop.P