DEFINITION minus_minus()
TYPE =
∀z:nat
.∀x:nat
.∀y:nat
.le z x
→(le z y)→(eq nat (minus x z) (minus y z))→(eq nat x y)
BODY =
assume z: nat
we proceed by induction on z to prove
∀x:nat
.∀y:nat
.le z x
→(le z y)→(eq nat (minus x z) (minus y z))→(eq nat x y)
case O : ⇒
the thesis becomes
∀x:nat
.∀y:nat
.le O x
→(le O y)→(eq nat (minus x O) (minus y O))→(eq nat x y)
assume x: nat
assume y: nat
suppose : le O x
suppose : le O y
suppose H1: eq nat (minus x O) (minus y O)
(H2)
by (minus_n_O .)
we proved eq nat x (minus x O)
by (eq_ind_r . . . H1 . previous)
eq nat x (minus y O)
end of H2
(H3)
by (minus_n_O .)
we proved eq nat y (minus y O)
by (eq_ind_r . . . H2 . previous)
eq nat x y
end of H3
consider H3
we proved eq nat x y
∀x:nat
.∀y:nat
.le O x
→(le O y)→(eq nat (minus x O) (minus y O))→(eq nat x y)
case S : z0:nat ⇒
the thesis becomes
∀x:nat
.∀y:nat
.le (S z0) x
→(le (S z0) y
→(eq nat (minus x (S z0)) (minus y (S z0)))→(eq nat x y))
(IH) by induction hypothesis we know
∀x:nat
.∀y:nat
.le z0 x
→(le z0 y)→(eq nat (minus x z0) (minus y z0))→(eq nat x y)
assume x: nat
we proceed by induction on x to prove
∀y:nat
.le (S z0) x
→(le (S z0) y
→(eq nat (minus x (S z0)) (minus y (S z0)))→(eq nat x y))
case O : ⇒
the thesis becomes
∀y:nat
.le (S z0) O
→(le (S z0) y
→(eq nat (minus O (S z0)) (minus y (S z0)))→(eq nat O y))
assume y: nat
suppose H: le (S z0) O
suppose : le (S z0) y
suppose : eq nat (minus O (S z0)) (minus y (S z0))
by (le_gen_S . . H)
we proved ex2 nat λn:nat.eq nat O (S n) λn:nat.le z0 n
we proceed by induction on the previous result to prove eq nat O y
case ex_intro2 : x0:nat H2:eq nat O (S x0) :le z0 x0 ⇒
the thesis becomes eq nat O y
(H4)
we proceed by induction on H2 to prove <λ:nat.Prop> CASE S x0 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 x0 OF O⇒True | S ⇒False
end of H4
consider H4
we proved <λ:nat.Prop> CASE S x0 OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq nat O y
eq nat O y
we proved eq nat O y
∀y:nat
.le (S z0) O
→(le (S z0) y
→(eq nat (minus O (S z0)) (minus y (S z0)))→(eq nat O y))
case S : x0:nat ⇒
the thesis becomes
∀y:nat
.le (S z0) (S x0)
→(le (S z0) y
→(eq nat (minus (S x0) (S z0)) (minus y (S z0)))→(eq nat (S x0) y))
() by induction hypothesis we know
∀y:nat
.le (S z0) x0
→(le (S z0) y
→(eq nat (minus x0 (S z0)) (minus y (S z0)))→(eq nat x0 y))
assume y: nat
we proceed by induction on y to prove
le (S z0) (S x0)
→(le (S z0) y
→(eq nat (minus (S x0) (S z0)) (minus y (S z0)))→(eq nat (S x0) y))
case O : ⇒
the thesis becomes
le (S z0) (S x0)
→(le (S z0) O
→(eq nat (minus (S x0) (S z0)) (minus O (S z0)))→(eq nat (S x0) O))
suppose H: le (S z0) (S x0)
suppose H0: le (S z0) O
suppose : eq nat (minus (S x0) (S z0)) (minus O (S z0))
by (le_gen_S . . H0)
we proved ex2 nat λn:nat.eq nat O (S n) λn:nat.le z0 n
we proceed by induction on the previous result to prove eq nat (S x0) O
case ex_intro2 : x1:nat H2:eq nat O (S x1) :le z0 x1 ⇒
the thesis becomes eq nat (S x0) O
(H4)
we proceed by induction on H2 to prove <λ:nat.Prop> CASE S x1 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 x1 OF O⇒True | S ⇒False
end of H4
consider H4
we proved <λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove eq nat (S x0) O
eq nat (S x0) O
we proved eq nat (S x0) O
le (S z0) (S x0)
→(le (S z0) O
→(eq nat (minus (S x0) (S z0)) (minus O (S z0)))→(eq nat (S x0) O))
case S : y0:nat ⇒
the thesis becomes
∀H:le (S z0) (S x0)
.∀H0:le (S z0) (S y0)
.∀H1:eq nat (minus (S x0) (S z0)) (minus (S y0) (S z0))
.eq nat (S x0) (S y0)
() by induction hypothesis we know
le (S z0) (S x0)
→(le (S z0) y0
→(eq nat (minus (S x0) (S z0)) (minus y0 (S z0)))→(eq nat (S x0) y0))
suppose H: le (S z0) (S x0)
suppose H0: le (S z0) (S y0)
suppose H1: eq nat (minus (S x0) (S z0)) (minus (S y0) (S z0))
(h1) by (le_S_n . . H) we proved le z0 x0
(h2) by (le_S_n . . H0) we proved le z0 y0
(h3)
consider H1
we proved eq nat (minus (S x0) (S z0)) (minus (S y0) (S z0))
eq nat (minus x0 z0) (minus y0 z0)
end of h3
by (IH . . h1 h2 h3)
we proved eq nat x0 y0
by (f_equal . . . . . previous)
we proved eq nat (S x0) (S y0)
∀H:le (S z0) (S x0)
.∀H0:le (S z0) (S y0)
.∀H1:eq nat (minus (S x0) (S z0)) (minus (S y0) (S z0))
.eq nat (S x0) (S y0)
we proved
le (S z0) (S x0)
→(le (S z0) y
→(eq nat (minus (S x0) (S z0)) (minus y (S z0)))→(eq nat (S x0) y))
∀y:nat
.le (S z0) (S x0)
→(le (S z0) y
→(eq nat (minus (S x0) (S z0)) (minus y (S z0)))→(eq nat (S x0) y))
we proved
∀y:nat
.le (S z0) x
→(le (S z0) y
→(eq nat (minus x (S z0)) (minus y (S z0)))→(eq nat x y))
∀x:nat
.∀y:nat
.le (S z0) x
→(le (S z0) y
→(eq nat (minus x (S z0)) (minus y (S z0)))→(eq nat x y))
we proved
∀x:nat
.∀y:nat
.le z x
→(le z y)→(eq nat (minus x z) (minus y z))→(eq nat x y)
we proved
∀z:nat
.∀x:nat
.∀y:nat
.le z x
→(le z y)→(eq nat (minus x z) (minus y z))→(eq nat x y)