DEFINITION aplus_gz_ge()
TYPE =
∀n:nat
.∀k:nat
.∀h:nat
.le k h
→eq A (aplus gz (ASort h n) k) (ASort (minus h k) n)
BODY =
assume n: nat
assume k: nat
we proceed by induction on k to prove
∀h:nat
.le k h
→eq A (aplus gz (ASort h n) k) (ASort (minus h k) n)
case O : ⇒
the thesis becomes
∀h:nat
.le O h
→eq A (aplus gz (ASort h n) O) (ASort (minus h O) n)
assume h: nat
suppose : le O h
by (minus_n_O .)
we proved eq nat h (minus h O)
we proceed by induction on the previous result to prove eq A (ASort h n) (ASort (minus h O) n)
case refl_equal : ⇒
the thesis becomes eq A (ASort h n) (ASort h n)
by (refl_equal . .)
eq A (ASort h n) (ASort h n)
we proved eq A (ASort h n) (ASort (minus h O) n)
that is equivalent to eq A (aplus gz (ASort h n) O) (ASort (minus h O) n)
∀h:nat
.le O h
→eq A (aplus gz (ASort h n) O) (ASort (minus h O) n)
case S : k0:nat ⇒
the thesis becomes
∀h:nat
.le (S k0) h
→(eq
A
asucc gz (aplus gz (ASort h n) k0)
ASort (minus h (S k0)) n)
(IH) by induction hypothesis we know
∀h:nat
.(le k0 h)→(eq A (aplus gz (ASort h n) k0) (ASort (minus h k0) n))
assume h: nat
we proceed by induction on h to prove
le (S k0) h
→(eq
A
asucc gz (aplus gz (ASort h n) k0)
ASort (minus h (S k0)) n)
case O : ⇒
the thesis becomes
le (S k0) O
→(eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort (minus O (S k0)) n)
suppose H: le (S k0) O
by (le_gen_S . . H)
we proved ex2 nat λn:nat.eq nat O (S n) λn:nat.le k0 n
we proceed by induction on the previous result to prove eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O n)
case ex_intro2 : x:nat H0:eq nat O (S x) :le k0 x ⇒
the thesis becomes eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O n)
(H2)
we proceed by induction on H0 to prove <λ:nat.Prop> CASE S x OF O⇒True | S ⇒False
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
consider I
we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S x OF O⇒True | S ⇒False
end of H2
consider H2
we proved <λ:nat.Prop> CASE S x OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O n)
eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O n)
we proved eq A (asucc gz (aplus gz (ASort O n) k0)) (ASort O n)
that is equivalent to
eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort (minus O (S k0)) n
le (S k0) O
→(eq
A
asucc gz (aplus gz (ASort O n) k0)
ASort (minus O (S k0)) n)
case S : n0:nat ⇒
the thesis becomes
∀H0:le (S k0) (S n0)
.eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
ASort (minus n0 k0) n
() by induction hypothesis we know
le (S k0) n0
→(eq
A
asucc gz (aplus gz (ASort n0 n) k0)
ASort (minus n0 (S k0)) n)
suppose H0: le (S k0) (S n0)
(H_y) by (le_S_n . . H0) we proved le k0 n0
by (IH . H_y)
we proved eq A (aplus gz (ASort n0 n) k0) (ASort (minus n0 k0) n)
we proceed by induction on the previous result to prove
eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
ASort (minus n0 k0) n
case refl_equal : ⇒
the thesis becomes
eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
aplus gz (ASort n0 n) k0
by (aplus_asucc . . .)
we proved
eq
A
aplus gz (asucc gz (ASort (S n0) n)) k0
asucc gz (aplus gz (ASort (S n0) n) k0)
we proceed by induction on the previous result to prove
eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
aplus gz (ASort n0 n) k0
case refl_equal : ⇒
the thesis becomes
eq
A
aplus gz (asucc gz (ASort (S n0) n)) k0
aplus gz (ASort n0 n) k0
by (refl_equal . .)
we proved eq A (aplus gz (ASort n0 n) k0) (aplus gz (ASort n0 n) k0)
eq
A
aplus gz (asucc gz (ASort (S n0) n)) k0
aplus gz (ASort n0 n) k0
eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
aplus gz (ASort n0 n) k0
we proved
eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
ASort (minus n0 k0) n
that is equivalent to
eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
ASort (minus (S n0) (S k0)) n
∀H0:le (S k0) (S n0)
.eq
A
asucc gz (aplus gz (ASort (S n0) n) k0)
ASort (minus n0 k0) n
we proved
le (S k0) h
→(eq
A
asucc gz (aplus gz (ASort h n) k0)
ASort (minus h (S k0)) n)
that is equivalent to
le (S k0) h
→eq A (aplus gz (ASort h n) (S k0)) (ASort (minus h (S k0)) n)
∀h:nat
.le (S k0) h
→(eq
A
asucc gz (aplus gz (ASort h n) k0)
ASort (minus h (S k0)) n)
we proved
∀h:nat
.le k h
→eq A (aplus gz (ASort h n) k) (ASort (minus h k) n)
we proved
∀n:nat
.∀k:nat
.∀h:nat
.le k h
→eq A (aplus gz (ASort h n) k) (ASort (minus h k) n)