DEFINITION aplus_asucc_false()
TYPE =
∀g:G.∀a:A.∀h:nat.(eq A (aplus g (asucc g a) h) a)→∀P:Prop.P
BODY =
assume g: G
assume a: A
we proceed by induction on a to prove ∀h:nat.(eq A (aplus g (asucc g a) h) a)→∀P:Prop.P
case ASort : n:nat n0:nat ⇒
the thesis becomes
∀h:nat
.(eq A (aplus g (asucc g (ASort n n0)) h) (ASort n n0))→∀P:Prop.P
assume h: nat
we must prove (eq A (aplus g (asucc g (ASort n n0)) h) (ASort n n0))→∀P:Prop.P
or equivalently
(eq
A
aplus g <λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort n n0)
→∀P:Prop.P
suppose H:
eq
A
aplus g <λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort n n0
assume P: Prop
we must prove
(eq
A
aplus g <λn2:nat.A> CASE O OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort O n0)
→P
or equivalently (eq A (aplus g (ASort O (next g n0)) h) (ASort O n0))→P
suppose H0: eq A (aplus g (ASort O (next g n0)) h) (ASort O n0)
(H1)
by (aplus_asort_simpl . . . .)
we proved
eq
A
aplus g (ASort O (next g n0)) h
ASort (minus O h) (next_plus g (next g n0) (minus h O))
we proceed by induction on the previous result to prove
eq
A
ASort (minus O h) (next_plus g (next g n0) (minus h O))
ASort O n0
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq
A
ASort (minus O h) (next_plus g (next g n0) (minus h O))
ASort O n0
end of H1
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:A.nat>
CASE ASort (minus O h) (next_plus g (next g n0) (minus h O)) OF
ASort n1⇒n1
| AHead ⇒
FIXnext_plus{
next_plus:G→nat→nat→nat
:=λg0:G.λn1:nat.λi:nat.<λn2:nat.nat> CASE i OF O⇒n1 | S i0⇒next g0 (next_plus g0 n1 i0)
}
g
next g n0
minus h O
<λ:A.nat>
CASE ASort O n0 OF
ASort n1⇒n1
| AHead ⇒
FIXnext_plus{
next_plus:G→nat→nat→nat
:=λg0:G.λn1:nat.λi:nat.<λn2:nat.nat> CASE i OF O⇒n1 | S i0⇒next g0 (next_plus g0 n1 i0)
}
g
next g n0
minus h O
eq
nat
λe:A
.<λ:A.nat>
CASE e OF
ASort n1⇒n1
| AHead ⇒
FIXnext_plus{
next_plus:G→nat→nat→nat
:=λg0:G.λn1:nat.λi:nat.<λn2:nat.nat> CASE i OF O⇒n1 | S i0⇒next g0 (next_plus g0 n1 i0)
}
g
next g n0
minus h O
ASort (minus O h) (next_plus g (next g n0) (minus h O))
λe:A
.<λ:A.nat>
CASE e OF
ASort n1⇒n1
| AHead ⇒
FIXnext_plus{
next_plus:G→nat→nat→nat
:=λg0:G.λn1:nat.λi:nat.<λn2:nat.nat> CASE i OF O⇒n1 | S i0⇒next g0 (next_plus g0 n1 i0)
}
g
next g n0
minus h O
ASort O n0
end of H2
(H3)
(h1)
consider H2
we proved
eq
nat
<λ:A.nat>
CASE ASort (minus O h) (next_plus g (next g n0) (minus h O)) OF
ASort n1⇒n1
| AHead ⇒
FIXnext_plus{
next_plus:G→nat→nat→nat
:=λg0:G.λn1:nat.λi:nat.<λn2:nat.nat> CASE i OF O⇒n1 | S i0⇒next g0 (next_plus g0 n1 i0)
}
g
next g n0
minus h O
<λ:A.nat>
CASE ASort O n0 OF
ASort n1⇒n1
| AHead ⇒
FIXnext_plus{
next_plus:G→nat→nat→nat
:=λg0:G.λn1:nat.λi:nat.<λn2:nat.nat> CASE i OF O⇒n1 | S i0⇒next g0 (next_plus g0 n1 i0)
}
g
next g n0
minus h O
eq nat (next_plus g (next g n0) (minus h O)) n0
end of h1
(h2)
by (minus_n_O .)
eq nat h (minus h O)
end of h2
by (eq_ind_r . . . h1 . h2)
eq nat (next_plus g (next g n0) h) n0
end of H3
(h1)
we proceed by induction on H3 to prove le (next_plus g (next g n0) h) n0
case refl_equal : ⇒
the thesis becomes le (next_plus g (next g n0) h) (next_plus g (next g n0) h)
by (le_n .)
le (next_plus g (next g n0) h) (next_plus g (next g n0) h)
le (next_plus g (next g n0) h) n0
end of h1
(h2)
by (next_plus_lt . . .)
lt n0 (next_plus g (next g n0) h)
end of h2
by (le_lt_false . . h1 h2 .)
we proved P
we proved (eq A (aplus g (ASort O (next g n0)) h) (ASort O n0))→P
(eq
A
aplus g <λn2:nat.A> CASE O OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort O n0)
→P
assume n1: nat
suppose :
(eq
A
aplus g <λn2:nat.A> CASE n1 OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort n1 n0)
→P
we must prove
(eq
A
aplus g <λn2:nat.A> CASE S n1 OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort (S n1) n0)
→P
or equivalently (eq A (aplus g (ASort n1 n0) h) (ASort (S n1) n0))→P
suppose H0: eq A (aplus g (ASort n1 n0) h) (ASort (S n1) n0)
(H1)
by (aplus_asort_simpl . . . .)
we proved
eq
A
aplus g (ASort n1 n0) h
ASort (minus n1 h) (next_plus g n0 (minus h n1))
we proceed by induction on the previous result to prove
eq
A
ASort (minus n1 h) (next_plus g n0 (minus h n1))
ASort (S n1) n0
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq
A
ASort (minus n1 h) (next_plus g n0 (minus h n1))
ASort (S n1) n0
end of H1
(H2)
by (f_equal . . . . . H1)
we proved
eq
nat
<λ:A.nat>
CASE ASort (minus n1 h) (next_plus g n0 (minus h n1)) OF
ASort n2 ⇒n2
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn2:nat
.λm:nat
.<λn3:nat.nat> CASE n2 OF O⇒O | S k⇒<λn3:nat.nat> CASE m OF O⇒S k | S l⇒minus k l
}
n1
h
<λ:A.nat>
CASE ASort (S n1) n0 OF
ASort n2 ⇒n2
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn2:nat
.λm:nat
.<λn3:nat.nat> CASE n2 OF O⇒O | S k⇒<λn3:nat.nat> CASE m OF O⇒S k | S l⇒minus k l
}
n1
h
eq
nat
λe:A
.<λ:A.nat>
CASE e OF
ASort n2 ⇒n2
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn2:nat
.λm:nat
.<λn3:nat.nat> CASE n2 OF O⇒O | S k⇒<λn3:nat.nat> CASE m OF O⇒S k | S l⇒minus k l
}
n1
h
ASort (minus n1 h) (next_plus g n0 (minus h n1))
λe:A
.<λ:A.nat>
CASE e OF
ASort n2 ⇒n2
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn2:nat
.λm:nat
.<λn3:nat.nat> CASE n2 OF O⇒O | S k⇒<λn3:nat.nat> CASE m OF O⇒S k | S l⇒minus k l
}
n1
h
ASort (S n1) n0
end of H2
(H4)
consider H2
we proved
eq
nat
<λ:A.nat>
CASE ASort (minus n1 h) (next_plus g n0 (minus h n1)) OF
ASort n2 ⇒n2
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn2:nat
.λm:nat
.<λn3:nat.nat> CASE n2 OF O⇒O | S k⇒<λn3:nat.nat> CASE m OF O⇒S k | S l⇒minus k l
}
n1
h
<λ:A.nat>
CASE ASort (S n1) n0 OF
ASort n2 ⇒n2
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn2:nat
.λm:nat
.<λn3:nat.nat> CASE n2 OF O⇒O | S k⇒<λn3:nat.nat> CASE m OF O⇒S k | S l⇒minus k l
}
n1
h
eq nat (minus n1 h) (S n1)
end of H4
we proceed by induction on H4 to prove le (S n1) n1
case refl_equal : ⇒
the thesis becomes le (minus n1 h) n1
by (minus_le . .)
le (minus n1 h) n1
we proved le (S n1) n1
by (le_Sx_x . previous .)
we proved P
we proved (eq A (aplus g (ASort n1 n0) h) (ASort (S n1) n0))→P
(eq
A
aplus g <λn2:nat.A> CASE S n1 OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort (S n1) n0)
→P
by (previous . H)
we proved P
we proved
(eq
A
aplus g <λn1:nat.A> CASE n OF O⇒ASort O (next g n0) | S h0⇒ASort h0 n0 h
ASort n n0)
→∀P:Prop.P
that is equivalent to (eq A (aplus g (asucc g (ASort n n0)) h) (ASort n n0))→∀P:Prop.P
∀h:nat
.(eq A (aplus g (asucc g (ASort n n0)) h) (ASort n n0))→∀P:Prop.P
case AHead : a0:A a1:A ⇒
the thesis becomes
∀h:nat
.(eq A (aplus g (asucc g (AHead a0 a1)) h) (AHead a0 a1))→∀P:Prop.P
() by induction hypothesis we know ∀h:nat.(eq A (aplus g (asucc g a0) h) a0)→∀P:Prop.P
(H0) by induction hypothesis we know ∀h:nat.(eq A (aplus g (asucc g a1) h) a1)→∀P:Prop.P
assume h: nat
we must prove (eq A (aplus g (asucc g (AHead a0 a1)) h) (AHead a0 a1))→∀P:Prop.P
or equivalently (eq A (aplus g (AHead a0 (asucc g a1)) h) (AHead a0 a1))→∀P:Prop.P
suppose H1: eq A (aplus g (AHead a0 (asucc g a1)) h) (AHead a0 a1)
assume P: Prop
(H2)
by (aplus_ahead_simpl . . . .)
we proved
eq
A
aplus g (AHead a0 (asucc g a1)) h
AHead a0 (aplus g (asucc g a1) h)
we proceed by induction on the previous result to prove eq A (AHead a0 (aplus g (asucc g a1) h)) (AHead a0 a1)
case refl_equal : ⇒
the thesis becomes the hypothesis H1
eq A (AHead a0 (aplus g (asucc g a1) h)) (AHead a0 a1)
end of H2
(H3)
by (f_equal . . . . . H2)
we proved
eq
A
<λ:A.A>
CASE AHead a0 (aplus g (asucc g a1) h) OF
ASort ⇒
FIXaplus{
aplus:G→A→nat→A
:=λg0:G.λa2:A.λn:nat.<λn1:nat.A> CASE n OF O⇒a2 | S n0⇒asucc g0 (aplus g0 a2 n0)
}
g
asucc g a1
h
| AHead a2⇒a2
<λ:A.A>
CASE AHead a0 a1 OF
ASort ⇒
FIXaplus{
aplus:G→A→nat→A
:=λg0:G.λa2:A.λn:nat.<λn1:nat.A> CASE n OF O⇒a2 | S n0⇒asucc g0 (aplus g0 a2 n0)
}
g
asucc g a1
h
| AHead a2⇒a2
eq
A
λe:A
.<λ:A.A>
CASE e OF
ASort ⇒
FIXaplus{
aplus:G→A→nat→A
:=λg0:G.λa2:A.λn:nat.<λn1:nat.A> CASE n OF O⇒a2 | S n0⇒asucc g0 (aplus g0 a2 n0)
}
g
asucc g a1
h
| AHead a2⇒a2
AHead a0 (aplus g (asucc g a1) h)
λe:A
.<λ:A.A>
CASE e OF
ASort ⇒
FIXaplus{
aplus:G→A→nat→A
:=λg0:G.λa2:A.λn:nat.<λn1:nat.A> CASE n OF O⇒a2 | S n0⇒asucc g0 (aplus g0 a2 n0)
}
g
asucc g a1
h
| AHead a2⇒a2
AHead a0 a1
end of H3
consider H3
we proved
eq
A
<λ:A.A>
CASE AHead a0 (aplus g (asucc g a1) h) OF
ASort ⇒
FIXaplus{
aplus:G→A→nat→A
:=λg0:G.λa2:A.λn:nat.<λn1:nat.A> CASE n OF O⇒a2 | S n0⇒asucc g0 (aplus g0 a2 n0)
}
g
asucc g a1
h
| AHead a2⇒a2
<λ:A.A>
CASE AHead a0 a1 OF
ASort ⇒
FIXaplus{
aplus:G→A→nat→A
:=λg0:G.λa2:A.λn:nat.<λn1:nat.A> CASE n OF O⇒a2 | S n0⇒asucc g0 (aplus g0 a2 n0)
}
g
asucc g a1
h
| AHead a2⇒a2
that is equivalent to eq A (aplus g (asucc g a1) h) a1
by (H0 . previous .)
we proved P
we proved (eq A (aplus g (AHead a0 (asucc g a1)) h) (AHead a0 a1))→∀P:Prop.P
that is equivalent to (eq A (aplus g (asucc g (AHead a0 a1)) h) (AHead a0 a1))→∀P:Prop.P
∀h:nat
.(eq A (aplus g (asucc g (AHead a0 a1)) h) (AHead a0 a1))→∀P:Prop.P
we proved ∀h:nat.(eq A (aplus g (asucc g a) h) a)→∀P:Prop.P
we proved ∀g:G.∀a:A.∀h:nat.(eq A (aplus g (asucc g a) h) a)→∀P:Prop.P