DEFINITION aplus_gz_le()
TYPE =
∀k:nat
.∀h:nat
.∀n:nat
.le h k
→eq A (aplus gz (ASort h n) k) (ASort O (plus (minus k h) n))
BODY =
assume k: nat
we proceed by induction on k to prove
∀h:nat
.∀n0:nat
.le h k
→eq A (aplus gz (ASort h n0) k) (ASort O (plus (minus k h) n0))
case O : ⇒
the thesis becomes
∀h:nat
.∀n:nat
.le h O
→eq A (aplus gz (ASort h n) O) (ASort O (plus (minus O h) n))
assume h: nat
assume n: nat
suppose H: le h O
(H_y)
by (le_n_O_eq . H)
eq nat O h
end of H_y
we proceed by induction on H_y to prove eq A (ASort h n) (ASort O n)
case refl_equal : ⇒
the thesis becomes eq A (ASort O n) (ASort O n)
by (refl_equal . .)
eq A (ASort O n) (ASort O n)
we proved eq A (ASort h n) (ASort O n)
that is equivalent to eq A (aplus gz (ASort h n) O) (ASort O (plus (minus O h) n))
∀h:nat
.∀n:nat
.le h O
→eq A (aplus gz (ASort h n) O) (ASort O (plus (minus O h) n))
case S : k0:nat ⇒
the thesis becomes
∀h:nat
.∀n0:nat
.le h (S k0)
→(eq
A
asucc gz (aplus gz (ASort h n0) k0)
ASort O (plus <λn1:nat.nat> CASE h OF O⇒S k0 | S l⇒minus k0 l n0))
(IH) by induction hypothesis we know
∀h:nat
.∀n:nat
.le h k0
→eq A (aplus gz (ASort h n) k0) (ASort O (plus (minus k0 h) n))
assume h: nat
we proceed by induction on h to prove
∀n0:nat
.le h (S k0)
→(eq
A
asucc gz (aplus gz (ASort h n0) k0)
ASort O (plus <λn1:nat.nat> CASE h OF O⇒S k0 | S l⇒minus k0 l n0))
case O : ⇒
the thesis becomes
∀n:nat
.le O (S k0)
→(eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort O (plus <λn1:nat.nat> CASE O OF O⇒S k0 | S l⇒minus k0 l n))
assume n: nat
suppose : le O (S k0)
by (aplus_asucc . . .)
we proved
eq
A
aplus gz (asucc gz (ASort O n)) k0
asucc gz (aplus gz (ASort O n) k0)
we proceed by induction on the previous result to prove
eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort O (S (plus k0 n))
case refl_equal : ⇒
the thesis becomes
eq
A
aplus gz (asucc gz (ASort O n)) k0
ASort O (S (plus k0 n))
(h1)
by (minus_n_O .)
we proved eq nat k0 (minus k0 O)
we proceed by induction on the previous result to prove
eq
A
ASort O (plus (minus k0 O) (S n))
ASort O (S (plus k0 n))
case refl_equal : ⇒
the thesis becomes eq A (ASort O (plus k0 (S n))) (ASort O (S (plus k0 n)))
by (plus_n_Sm . .)
we proved eq nat (S (plus k0 n)) (plus k0 (S n))
we proceed by induction on the previous result to prove eq A (ASort O (plus k0 (S n))) (ASort O (S (plus k0 n)))
case refl_equal : ⇒
the thesis becomes eq A (ASort O (S (plus k0 n))) (ASort O (S (plus k0 n)))
by (refl_equal . .)
eq A (ASort O (S (plus k0 n))) (ASort O (S (plus k0 n)))
eq A (ASort O (plus k0 (S n))) (ASort O (S (plus k0 n)))
eq
A
ASort O (plus (minus k0 O) (S n))
ASort O (S (plus k0 n))
end of h1
(h2)
by (le_O_n .)
we proved le O k0
by (IH . . previous)
eq
A
aplus gz (ASort O (S n)) k0
ASort O (plus (minus k0 O) (S n))
end of h2
by (eq_ind_r . . . h1 . h2)
we proved eq A (aplus gz (ASort O (S n)) k0) (ASort O (S (plus k0 n)))
eq
A
aplus gz (asucc gz (ASort O n)) k0
ASort O (S (plus k0 n))
we proved
eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort O (S (plus k0 n))
that is equivalent to
eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort O (plus <λn1:nat.nat> CASE O OF O⇒S k0 | S l⇒minus k0 l n)
∀n:nat
.le O (S k0)
→(eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort O (plus <λn1:nat.nat> CASE O OF O⇒S k0 | S l⇒minus k0 l n))
case S : n:nat ⇒
the thesis becomes
∀n0:nat
.∀H0:le (S n) (S k0)
.eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
ASort O (plus (minus k0 n) n0)
() by induction hypothesis we know
∀n0:nat
.le n (S k0)
→(eq
A
asucc gz (aplus gz (ASort n n0) k0)
ASort O (plus <λn1:nat.nat> CASE n OF O⇒S k0 | S l⇒minus k0 l n0))
assume n0: nat
suppose H0: le (S n) (S k0)
(H_y) by (le_S_n . . H0) we proved le n k0
by (IH . . H_y)
we proved eq A (aplus gz (ASort n n0) k0) (ASort O (plus (minus k0 n) n0))
we proceed by induction on the previous result to prove
eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
ASort O (plus (minus k0 n) n0)
case refl_equal : ⇒
the thesis becomes
eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
aplus gz (ASort n n0) k0
by (aplus_asucc . . .)
we proved
eq
A
aplus gz (asucc gz (ASort (S n) n0)) k0
asucc gz (aplus gz (ASort (S n) n0) k0)
we proceed by induction on the previous result to prove
eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
aplus gz (ASort n n0) k0
case refl_equal : ⇒
the thesis becomes
eq
A
aplus gz (asucc gz (ASort (S n) n0)) k0
aplus gz (ASort n n0) k0
by (refl_equal . .)
we proved eq A (aplus gz (ASort n n0) k0) (aplus gz (ASort n n0) k0)
eq
A
aplus gz (asucc gz (ASort (S n) n0)) k0
aplus gz (ASort n n0) k0
eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
aplus gz (ASort n n0) k0
we proved
eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
ASort O (plus (minus k0 n) n0)
that is equivalent to
eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
ASort O (plus <λn1:nat.nat> CASE S n OF O⇒S k0 | S l⇒minus k0 l n0)
∀n0:nat
.∀H0:le (S n) (S k0)
.eq
A
asucc gz (aplus gz (ASort (S n) n0) k0)
ASort O (plus (minus k0 n) n0)
we proved
∀n0:nat
.le h (S k0)
→(eq
A
asucc gz (aplus gz (ASort h n0) k0)
ASort O (plus <λn1:nat.nat> CASE h OF O⇒S k0 | S l⇒minus k0 l n0))
that is equivalent to
∀n0:nat
.le h (S k0)
→(eq
A
aplus gz (ASort h n0) (S k0)
ASort O (plus (minus (S k0) h) n0))
∀h:nat
.∀n0:nat
.le h (S k0)
→(eq
A
asucc gz (aplus gz (ASort h n0) k0)
ASort O (plus <λn1:nat.nat> CASE h OF O⇒S k0 | S l⇒minus k0 l n0))
we proved
∀h:nat
.∀n0:nat
.le h k
→eq A (aplus gz (ASort h n0) k) (ASort O (plus (minus k h) n0))
we proved
∀k:nat
.∀h:nat
.∀n0:nat
.le h k
→eq A (aplus gz (ASort h n0) k) (ASort O (plus (minus k h) n0))