DEFINITION minus_x_Sy()
TYPE =
∀x:nat
.∀y:nat.(lt y x)→(eq nat (minus x y) (S (minus x (S y))))
BODY =
assume x: nat
we proceed by induction on x to prove ∀y:nat.(lt y x)→(eq nat (minus x y) (S (minus x (S y))))
case O : ⇒
the thesis becomes ∀y:nat.(lt y O)→(eq nat (minus O y) (S (minus O (S y))))
assume y: nat
suppose H: lt y O
(H0)
by cases on H we prove (eq nat O O)→(eq nat (minus O y) (S (minus O (S y))))
case le_n ⇒
the thesis becomes
(eq nat (S y) O)→(eq nat (minus O y) (S (minus O (S y))))
suppose H0: eq nat (S y) O
(H1)
we proceed by induction on H0 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S y OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S y OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H1
consider H1
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove eq nat (minus O y) (S (minus O (S y)))
we proved eq nat (minus O y) (S (minus O (S y)))
(eq nat (S y) O)→(eq nat (minus O y) (S (minus O (S y))))
case le_S m:nat H0:le (S y) m ⇒
the thesis becomes ∀H1:(eq nat (S m) O).(eq nat (minus O y) (S (minus O (S y))))
suppose H1: eq nat (S m) O
(H2)
we proceed by induction on H1 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S m OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S m OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H2
consider H2
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove (le (S y) m)→(eq nat (minus O y) (S (minus O (S y))))
we proved (le (S y) m)→(eq nat (minus O y) (S (minus O (S y))))
by (previous H0)
we proved eq nat (minus O y) (S (minus O (S y)))
∀H1:(eq nat (S m) O).(eq nat (minus O y) (S (minus O (S y))))
(eq nat O O)→(eq nat (minus O y) (S (minus O (S y))))
end of H0
by (refl_equal . .)
we proved eq nat O O
by (H0 previous)
we proved eq nat (minus O y) (S (minus O (S y)))
∀y:nat.(lt y O)→(eq nat (minus O y) (S (minus O (S y))))
case S : n:nat ⇒
the thesis becomes
∀y:nat
.lt y (S n)
→eq nat (minus (S n) y) (S (minus (S n) (S y)))
(H) by induction hypothesis we know ∀y:nat.(lt y n)→(eq nat (minus n y) (S (minus n (S y))))
assume y: nat
we proceed by induction on y to prove
lt y (S n)
→eq nat (minus (S n) y) (S (minus (S n) (S y)))
case O : ⇒
the thesis becomes
lt O (S n)
→eq nat (minus (S n) O) (S (minus (S n) (S O)))
suppose : lt O (S n)
by (minus_n_O .)
we proved eq nat n (minus n O)
we proceed by induction on the previous result to prove eq nat (S n) (S (minus n O))
case refl_equal : ⇒
the thesis becomes eq nat (S n) (S n)
by (refl_equal . .)
eq nat (S n) (S n)
we proved eq nat (S n) (S (minus n O))
that is equivalent to eq nat (minus (S n) O) (S (minus (S n) (S O)))
lt O (S n)
→eq nat (minus (S n) O) (S (minus (S n) (S O)))
case S : n0:nat ⇒
the thesis becomes ∀H1:(lt (S n0) (S n)).(eq nat (minus n n0) (S (minus n (S n0))))
() by induction hypothesis we know
lt n0 (S n)
→eq nat (minus (S n) n0) (S (minus (S n) (S n0)))
suppose H1: lt (S n0) (S n)
(H2)
consider H1
we proved lt (S n0) (S n)
that is equivalent to le (S (S n0)) (S n)
by (le_S_n . . previous)
le (S n0) n
end of H2
consider H2
we proved le (S n0) n
that is equivalent to lt n0 n
by (H . previous)
we proved eq nat (minus n n0) (S (minus n (S n0)))
that is equivalent to eq nat (minus (S n) (S n0)) (S (minus (S n) (S (S n0))))
∀H1:(lt (S n0) (S n)).(eq nat (minus n n0) (S (minus n (S n0))))
we proved
lt y (S n)
→eq nat (minus (S n) y) (S (minus (S n) (S y)))
∀y:nat
.lt y (S n)
→eq nat (minus (S n) y) (S (minus (S n) (S y)))
we proved ∀y:nat.(lt y x)→(eq nat (minus x y) (S (minus x (S y))))
we proved
∀x:nat
.∀y:nat.(lt y x)→(eq nat (minus x y) (S (minus x (S y))))