DEFINITION leqz_leq()
TYPE =
∀a1:A.∀a2:A.(leq gz a1 a2)→(leqz a1 a2)
BODY =
assume a1: A
assume a2: A
suppose H: leq gz a1 a2
we proceed by induction on H to prove leqz a1 a2
case leq_sort : h1:nat h2:nat n1:nat n2:nat k:nat H0:eq A (aplus gz (ASort h1 n1) k) (aplus gz (ASort h2 n2) k) ⇒
the thesis becomes leqz (ASort h1 n1) (ASort h2 n2)
(h1)
suppose H1: lt k h1
(h1)
suppose H2: lt k h2
(H3)
consider H1
we proved lt k h1
that is equivalent to le (S k) h1
by (le_S . . previous)
we proved le (S k) (S h1)
by (le_S_n . . previous)
we proved le k h1
by (aplus_gz_ge . . . previous)
we proved eq A (aplus gz (ASort h1 n1) k) (ASort (minus h1 k) n1)
we proceed by induction on the previous result to prove eq A (ASort (minus h1 k) n1) (aplus gz (ASort h2 n2) k)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq A (ASort (minus h1 k) n1) (aplus gz (ASort h2 n2) k)
end of H3
(H4)
consider H2
we proved lt k h2
that is equivalent to le (S k) h2
by (le_S . . previous)
we proved le (S k) (S h2)
by (le_S_n . . previous)
we proved le k h2
by (aplus_gz_ge . . . previous)
we proved eq A (aplus gz (ASort h2 n2) k) (ASort (minus h2 k) n2)
we proceed by induction on the previous result to prove eq A (ASort (minus h1 k) n1) (ASort (minus h2 k) n2)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq A (ASort (minus h1 k) n1) (ASort (minus h2 k) n2)
end of H4
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat>
CASE ASort (minus h1 k) n1 OF
ASort n ⇒n
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn:nat
.λm:nat
.<λn3:nat.nat> CASE n OF O⇒O | S k0⇒<λn3:nat.nat> CASE m OF O⇒S k0 | S l⇒minus k0 l
}
h1
k
<λ:A.nat>
CASE ASort (minus h2 k) n2 OF
ASort n ⇒n
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn:nat
.λm:nat
.<λn3:nat.nat> CASE n OF O⇒O | S k0⇒<λn3:nat.nat> CASE m OF O⇒S k0 | S l⇒minus k0 l
}
h1
k
eq
nat
λe:A
.<λ:A.nat>
CASE e OF
ASort n ⇒n
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn:nat
.λm:nat
.<λn3:nat.nat> CASE n OF O⇒O | S k0⇒<λn3:nat.nat> CASE m OF O⇒S k0 | S l⇒minus k0 l
}
h1
k
ASort (minus h1 k) n1
λe:A
.<λ:A.nat>
CASE e OF
ASort n ⇒n
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn:nat
.λm:nat
.<λn3:nat.nat> CASE n OF O⇒O | S k0⇒<λn3:nat.nat> CASE m OF O⇒S k0 | S l⇒minus k0 l
}
h1
k
ASort (minus h2 k) n2
end of H5
(h1)
(H6)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat> CASE ASort (minus h1 k) n1 OF ASort n⇒n | AHead ⇒n1
<λ:A.nat> CASE ASort (minus h2 k) n2 OF ASort n⇒n | AHead ⇒n1
eq
nat
λe:A.<λ:A.nat> CASE e OF ASort n⇒n | AHead ⇒n1 (ASort (minus h1 k) n1)
λe:A.<λ:A.nat> CASE e OF ASort n⇒n | AHead ⇒n1 (ASort (minus h2 k) n2)
end of H6
suppose H7: eq nat (minus h1 k) (minus h2 k)
consider H6
we proved
eq
nat
<λ:A.nat> CASE ASort (minus h1 k) n1 OF ASort n⇒n | AHead ⇒n1
<λ:A.nat> CASE ASort (minus h2 k) n2 OF ASort n⇒n | AHead ⇒n1
that is equivalent to eq nat n1 n2
we proceed by induction on the previous result to prove leqz (ASort h1 n1) (ASort h2 n2)
case refl_equal : ⇒
the thesis becomes leqz (ASort h1 n1) (ASort h2 n1)
(h1)
consider H1
we proved lt k h1
that is equivalent to le (S k) h1
by (le_S . . previous)
we proved le (S k) (S h1)
by (le_S_n . . previous)
le k h1
end of h1
(h2)
consider H2
we proved lt k h2
that is equivalent to le (S k) h2
by (le_S . . previous)
we proved le (S k) (S h2)
by (le_S_n . . previous)
le k h2
end of h2
by (minus_minus . . . h1 h2 H7)
we proved eq nat h1 h2
we proceed by induction on the previous result to prove leqz (ASort h1 n1) (ASort h2 n1)
case refl_equal : ⇒
the thesis becomes leqz (ASort h1 n1) (ASort h1 n1)
by (refl_equal . .)
we proved eq nat (plus h1 n1) (plus h1 n1)
by (leqz_sort . . . . previous)
leqz (ASort h1 n1) (ASort h1 n1)
leqz (ASort h1 n1) (ASort h2 n1)
we proved leqz (ASort h1 n1) (ASort h2 n2)
(eq nat (minus h1 k) (minus h2 k))→(leqz (ASort h1 n1) (ASort h2 n2))
end of h1
(h2)
consider H5
we proved
eq
nat
<λ:A.nat>
CASE ASort (minus h1 k) n1 OF
ASort n ⇒n
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn:nat
.λm:nat
.<λn3:nat.nat> CASE n OF O⇒O | S k0⇒<λn3:nat.nat> CASE m OF O⇒S k0 | S l⇒minus k0 l
}
h1
k
<λ:A.nat>
CASE ASort (minus h2 k) n2 OF
ASort n ⇒n
| AHead ⇒
FIXminus{
minus:nat→nat→nat
:=λn:nat
.λm:nat
.<λn3:nat.nat> CASE n OF O⇒O | S k0⇒<λn3:nat.nat> CASE m OF O⇒S k0 | S l⇒minus k0 l
}
h1
k
eq nat (minus h1 k) (minus h2 k)
end of h2
by (h1 h2)
we proved leqz (ASort h1 n1) (ASort h2 n2)
(lt k h2)→(leqz (ASort h1 n1) (ASort h2 n2))
end of h1
(h2)
suppose H2: le h2 k
(H3)
consider H1
we proved lt k h1
that is equivalent to le (S k) h1
by (le_S . . previous)
we proved le (S k) (S h1)
by (le_S_n . . previous)
we proved le k h1
by (aplus_gz_ge . . . previous)
we proved eq A (aplus gz (ASort h1 n1) k) (ASort (minus h1 k) n1)
we proceed by induction on the previous result to prove eq A (ASort (minus h1 k) n1) (aplus gz (ASort h2 n2) k)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq A (ASort (minus h1 k) n1) (aplus gz (ASort h2 n2) k)
end of H3
(H4)
by (aplus_gz_le . . . H2)
we proved eq A (aplus gz (ASort h2 n2) k) (ASort O (plus (minus k h2) n2))
we proceed by induction on the previous result to prove eq A (ASort (minus h1 k) n1) (ASort O (plus (minus k h2) n2))
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq A (ASort (minus h1 k) n1) (ASort O (plus (minus k h2) n2))
end of H4
(H5)
by (minus_x_Sy . . H1)
we proved eq nat (minus h1 k) (S (minus h1 (S k)))
we proceed by induction on the previous result to prove
eq
A
ASort (S (minus h1 (S k))) n1
ASort O (plus (minus k h2) n2)
case refl_equal : ⇒
the thesis becomes the hypothesis H4
eq
A
ASort (S (minus h1 (S k))) n1
ASort O (plus (minus k h2) n2)
end of H5
(H6)
we proceed by induction on H5 to prove
<λ:A.Prop>
CASE ASort O (plus (minus k h2) n2) OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:A.Prop>
CASE ASort (S (minus h1 (S k))) n1 OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
consider I
we proved True
<λ:A.Prop>
CASE ASort (S (minus h1 (S k))) n1 OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
<λ:A.Prop>
CASE ASort O (plus (minus k h2) n2) OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
end of H6
consider H6
we proved
<λ:A.Prop>
CASE ASort O (plus (minus k h2) n2) OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove leqz (ASort h1 n1) (ASort h2 n2)
we proved leqz (ASort h1 n1) (ASort h2 n2)
(le h2 k)→(leqz (ASort h1 n1) (ASort h2 n2))
end of h2
by (lt_le_e . . . h1 h2)
we proved leqz (ASort h1 n1) (ASort h2 n2)
(lt k h1)→(leqz (ASort h1 n1) (ASort h2 n2))
end of h1
(h2)
suppose H1: le h1 k
(h1)
suppose H2: lt k h2
(H3)
by (aplus_gz_le . . . H1)
we proved eq A (aplus gz (ASort h1 n1) k) (ASort O (plus (minus k h1) n1))
we proceed by induction on the previous result to prove eq A (ASort O (plus (minus k h1) n1)) (aplus gz (ASort h2 n2) k)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq A (ASort O (plus (minus k h1) n1)) (aplus gz (ASort h2 n2) k)
end of H3
(H4)
consider H2
we proved lt k h2
that is equivalent to le (S k) h2
by (le_S . . previous)
we proved le (S k) (S h2)
by (le_S_n . . previous)
we proved le k h2
by (aplus_gz_ge . . . previous)
we proved eq A (aplus gz (ASort h2 n2) k) (ASort (minus h2 k) n2)
we proceed by induction on the previous result to prove eq A (ASort O (plus (minus k h1) n1)) (ASort (minus h2 k) n2)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq A (ASort O (plus (minus k h1) n1)) (ASort (minus h2 k) n2)
end of H4
(H5)
by (sym_eq . . . H4)
eq A (ASort (minus h2 k) n2) (ASort O (plus (minus k h1) n1))
end of H5
(H6)
by (minus_x_Sy . . H2)
we proved eq nat (minus h2 k) (S (minus h2 (S k)))
we proceed by induction on the previous result to prove
eq
A
ASort (S (minus h2 (S k))) n2
ASort O (plus (minus k h1) n1)
case refl_equal : ⇒
the thesis becomes the hypothesis H5
eq
A
ASort (S (minus h2 (S k))) n2
ASort O (plus (minus k h1) n1)
end of H6
(H7)
we proceed by induction on H6 to prove
<λ:A.Prop>
CASE ASort O (plus (minus k h1) n1) OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
case refl_equal : ⇒
the thesis becomes
<λ:A.Prop>
CASE ASort (S (minus h2 (S k))) n2 OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
consider I
we proved True
<λ:A.Prop>
CASE ASort (S (minus h2 (S k))) n2 OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
<λ:A.Prop>
CASE ASort O (plus (minus k h1) n1) OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
end of H7
consider H7
we proved
<λ:A.Prop>
CASE ASort O (plus (minus k h1) n1) OF
ASort n ⇒<λ:nat.Prop> CASE n OF O⇒False | S ⇒True
| AHead ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove leqz (ASort h1 n1) (ASort h2 n2)
we proved leqz (ASort h1 n1) (ASort h2 n2)
(lt k h2)→(leqz (ASort h1 n1) (ASort h2 n2))
end of h1
(h2)
suppose H2: le h2 k
(H3)
by (aplus_gz_le . . . H1)
we proved eq A (aplus gz (ASort h1 n1) k) (ASort O (plus (minus k h1) n1))
we proceed by induction on the previous result to prove eq A (ASort O (plus (minus k h1) n1)) (aplus gz (ASort h2 n2) k)
case refl_equal : ⇒
the thesis becomes the hypothesis H0
eq A (ASort O (plus (minus k h1) n1)) (aplus gz (ASort h2 n2) k)
end of H3
(H4)
by (aplus_gz_le . . . H2)
we proved eq A (aplus gz (ASort h2 n2) k) (ASort O (plus (minus k h2) n2))
we proceed by induction on the previous result to prove
eq
A
ASort O (plus (minus k h1) n1)
ASort O (plus (minus k h2) n2)
case refl_equal : ⇒
the thesis becomes the hypothesis H3
eq
A
ASort O (plus (minus k h1) n1)
ASort O (plus (minus k h2) n2)
end of H4
(H5)
by (f_equal . . . . . H4)
we proved
eq
nat
<λ:A.nat>
CASE ASort O (plus (minus k h1) n1) OF
ASort n⇒n
| AHead ⇒
FIXplus{
plus:nat→nat→nat
:=λn:nat.λm:nat.<λn3:nat.nat> CASE n OF O⇒m | S p⇒S (plus p m)
}
minus k h1
n1
<λ:A.nat>
CASE ASort O (plus (minus k h2) n2) OF
ASort n⇒n
| AHead ⇒
FIXplus{
plus:nat→nat→nat
:=λn:nat.λm:nat.<λn3:nat.nat> CASE n OF O⇒m | S p⇒S (plus p m)
}
minus k h1
n1
eq
nat
λe:A
.<λ:A.nat>
CASE e OF
ASort n⇒n
| AHead ⇒
FIXplus{
plus:nat→nat→nat
:=λn:nat.λm:nat.<λn3:nat.nat> CASE n OF O⇒m | S p⇒S (plus p m)
}
minus k h1
n1
ASort O (plus (minus k h1) n1)
λe:A
.<λ:A.nat>
CASE e OF
ASort n⇒n
| AHead ⇒
FIXplus{
plus:nat→nat→nat
:=λn:nat.λm:nat.<λn3:nat.nat> CASE n OF O⇒m | S p⇒S (plus p m)
}
minus k h1
n1
ASort O (plus (minus k h2) n2)
end of H5
(H_y)
consider H5
we proved
eq
nat
<λ:A.nat>
CASE ASort O (plus (minus k h1) n1) OF
ASort n⇒n
| AHead ⇒
FIXplus{
plus:nat→nat→nat
:=λn:nat.λm:nat.<λn3:nat.nat> CASE n OF O⇒m | S p⇒S (plus p m)
}
minus k h1
n1
<λ:A.nat>
CASE ASort O (plus (minus k h2) n2) OF
ASort n⇒n
| AHead ⇒
FIXplus{
plus:nat→nat→nat
:=λn:nat.λm:nat.<λn3:nat.nat> CASE n OF O⇒m | S p⇒S (plus p m)
}
minus k h1
n1
that is equivalent to eq nat (plus (minus k h1) n1) (plus (minus k h2) n2)
by (plus_plus . . . . . H1 H2 previous)
eq nat (plus h1 n2) (plus h2 n1)
end of H_y
by (leqz_sort . . . . H_y)
we proved leqz (ASort h1 n1) (ASort h2 n2)
(le h2 k)→(leqz (ASort h1 n1) (ASort h2 n2))
end of h2
by (lt_le_e . . . h1 h2)
we proved leqz (ASort h1 n1) (ASort h2 n2)
(le h1 k)→(leqz (ASort h1 n1) (ASort h2 n2))
end of h2
by (lt_le_e . . . h1 h2)
leqz (ASort h1 n1) (ASort h2 n2)
case leq_head : a0:A a3:A :leq gz a0 a3 a4:A a5:A :leq gz a4 a5 ⇒
the thesis becomes leqz (AHead a0 a4) (AHead a3 a5)
(H1) by induction hypothesis we know leqz a0 a3
(H3) by induction hypothesis we know leqz a4 a5
by (leqz_head . . H1 . . H3)
leqz (AHead a0 a4) (AHead a3 a5)
we proved leqz a1 a2
we proved ∀a1:A.∀a2:A.(leq gz a1 a2)→(leqz a1 a2)