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