DEFINITION plus_plus()
TYPE =
∀z:nat
.∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 z
→(le x2 z
→(eq nat (plus (minus z x1) y1) (plus (minus z x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
BODY =
assume z: nat
we proceed by induction on z to prove
∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 z
→(le x2 z
→(eq nat (plus (minus z x1) y1) (plus (minus z x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
case O : ⇒
the thesis becomes
∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 O
→(le x2 O
→(eq nat (plus (minus O x1) y1) (plus (minus O x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
assume x1: nat
assume x2: nat
assume y1: nat
assume y2: nat
suppose H: le x1 O
suppose H0: le x2 O
we must prove
eq nat (plus (minus O x1) y1) (plus (minus O x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)
or equivalently (eq nat y1 y2)→(eq nat (plus x1 y2) (plus x2 y1))
suppose H1: eq nat y1 y2
we proceed by induction on H1 to prove eq nat (plus x1 y2) (plus x2 y1)
case refl_equal : ⇒
the thesis becomes eq nat (plus x1 y1) (plus x2 y1)
(H_y)
by (le_n_O_eq . H0)
eq nat O x2
end of H_y
we proceed by induction on H_y to prove eq nat (plus x1 y1) (plus x2 y1)
case refl_equal : ⇒
the thesis becomes eq nat (plus x1 y1) (plus O y1)
(H_y0)
by (le_n_O_eq . H)
eq nat O x1
end of H_y0
we proceed by induction on H_y0 to prove eq nat (plus x1 y1) (plus O y1)
case refl_equal : ⇒
the thesis becomes eq nat (plus O y1) (plus O y1)
by (refl_equal . .)
eq nat (plus O y1) (plus O y1)
eq nat (plus x1 y1) (plus O y1)
eq nat (plus x1 y1) (plus x2 y1)
we proved eq nat (plus x1 y2) (plus x2 y1)
we proved (eq nat y1 y2)→(eq nat (plus x1 y2) (plus x2 y1))
that is equivalent to
eq nat (plus (minus O x1) y1) (plus (minus O x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)
∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 O
→(le x2 O
→(eq nat (plus (minus O x1) y1) (plus (minus O x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
case S : z0:nat ⇒
the thesis becomes
∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) x1) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
(IH) by induction hypothesis we know
∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 z0
→(le x2 z0
→(eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
assume x1: nat
we proceed by induction on x1 to prove
∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) x1) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
case O : ⇒
the thesis becomes
∀x2:nat
.∀y1:nat
.∀y2:nat
.le O (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus O y2) (plus x2 y1)))
assume x2: nat
we proceed by induction on x2 to prove
∀y1:nat
.∀y2:nat
.le O (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus O y2) (plus x2 y1)))
case O : ⇒
the thesis becomes
∀y1:nat
.∀y2:nat
.le O (S z0)
→(le O (S z0)
→(eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) O) y2)
→eq nat (plus O y2) (plus O y1)))
assume y1: nat
assume y2: nat
suppose : le O (S z0)
suppose : le O (S z0)
we must prove
eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) O) y2)
→eq nat (plus O y2) (plus O y1)
or equivalently
eq nat (S (plus z0 y1)) (S (plus z0 y2))
→eq nat (plus O y2) (plus O y1)
suppose H1: eq nat (S (plus z0 y1)) (S (plus z0 y2))
(H_y)
by (IH . .)
∀y1:nat
.∀y2:nat
.le O z0
→(le O z0
→(eq nat (plus (minus z0 O) y1) (plus (minus z0 O) y2)
→eq nat (plus O y2) (plus O y1)))
end of H_y
(H2)
(h1)
consider H_y
we proved
∀y1:nat
.∀y2:nat
.le O z0
→(le O z0
→(eq nat (plus (minus z0 O) y1) (plus (minus z0 O) y2)
→eq nat (plus O y2) (plus O y1)))
∀y3:nat
.∀y4:nat
.le O z0
→(le O z0
→(eq nat (plus (minus z0 O) y3) (plus (minus z0 O) y4))→(eq nat y4 y3))
end of h1
(h2)
by (minus_n_O .)
eq nat z0 (minus z0 O)
end of h2
by (eq_ind_r . . . h1 . h2)
∀y3:nat
.∀y4:nat
.le O z0
→(le O z0)→(eq nat (plus z0 y3) (plus z0 y4))→(eq nat y4 y3)
end of H2
(h1) by (le_O_n .) we proved le O z0
(h2) by (le_O_n .) we proved le O z0
(h3)
by (eq_add_S . . H1)
eq nat (plus z0 y1) (plus z0 y2)
end of h3
by (H2 . . h1 h2 h3)
we proved eq nat y2 y1
that is equivalent to eq nat (plus O y2) (plus O y1)
we proved
eq nat (S (plus z0 y1)) (S (plus z0 y2))
→eq nat (plus O y2) (plus O y1)
that is equivalent to
eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) O) y2)
→eq nat (plus O y2) (plus O y1)
∀y1:nat
.∀y2:nat
.le O (S z0)
→(le O (S z0)
→(eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) O) y2)
→eq nat (plus O y2) (plus O y1)))
case S : x3:nat ⇒
the thesis becomes
∀y1:nat
.∀y2:nat
.le O (S z0)
→∀H0:le (S x3) (S z0)
.eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) (S x3)) y2)
→eq nat (plus O y2) (plus (S x3) y1)
() by induction hypothesis we know
∀y1:nat
.∀y2:nat
.le O (S z0)
→(le x3 (S z0)
→((eq
nat
S (plus z0 y1)
plus <λn:nat.nat> CASE x3 OF O⇒S z0 | S l⇒minus z0 l y2)
→eq nat y2 (plus x3 y1)))
assume y1: nat
assume y2: nat
suppose : le O (S z0)
suppose H0: le (S x3) (S z0)
we must prove
eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) (S x3)) y2)
→eq nat (plus O y2) (plus (S x3) y1)
or equivalently
eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2)
→eq nat (plus O y2) (plus (S x3) y1)
suppose H1: eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2)
(H_y)
by (IH . . .)
∀y2:nat
.le O z0
→(le x3 z0
→(eq nat (plus (minus z0 O) (S y1)) (plus (minus z0 x3) y2)
→eq nat (plus O y2) (plus x3 (S y1))))
end of H_y
(H2)
(h1)
consider H_y
we proved
∀y2:nat
.le O z0
→(le x3 z0
→(eq nat (plus (minus z0 O) (S y1)) (plus (minus z0 x3) y2)
→eq nat (plus O y2) (plus x3 (S y1))))
∀y3:nat
.le O z0
→(le x3 z0
→(eq nat (plus (minus z0 O) (S y1)) (plus (minus z0 x3) y3)
→eq nat y3 (plus x3 (S y1))))
end of h1
(h2)
by (minus_n_O .)
eq nat z0 (minus z0 O)
end of h2
by (eq_ind_r . . . h1 . h2)
∀y3:nat
.le O z0
→(le x3 z0
→(eq nat (plus z0 (S y1)) (plus (minus z0 x3) y3)
→eq nat y3 (plus x3 (S y1))))
end of H2
(H3)
by (plus_n_Sm . .)
we proved eq nat (S (plus z0 y1)) (plus z0 (S y1))
by (eq_ind_r . . . H2 . previous)
∀y3:nat
.le O z0
→(le x3 z0
→(eq nat (S (plus z0 y1)) (plus (minus z0 x3) y3)
→eq nat y3 (plus x3 (S y1))))
end of H3
(H4)
by (plus_n_Sm . .)
we proved eq nat (S (plus x3 y1)) (plus x3 (S y1))
by (eq_ind_r . . . H3 . previous)
∀y3:nat
.le O z0
→(le x3 z0
→(eq nat (S (plus z0 y1)) (plus (minus z0 x3) y3)
→eq nat y3 (S (plus x3 y1))))
end of H4
(h1) by (le_O_n .) we proved le O z0
(h2) by (le_S_n . . H0) we proved le x3 z0
by (H4 . h1 h2 H1)
we proved eq nat y2 (S (plus x3 y1))
that is equivalent to eq nat (plus O y2) (plus (S x3) y1)
we proved
eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2)
→eq nat (plus O y2) (plus (S x3) y1)
that is equivalent to
eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) (S x3)) y2)
→eq nat (plus O y2) (plus (S x3) y1)
∀y1:nat
.∀y2:nat
.le O (S z0)
→∀H0:le (S x3) (S z0)
.eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) (S x3)) y2)
→eq nat (plus O y2) (plus (S x3) y1)
we proved
∀y1:nat
.∀y2:nat
.le O (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus O y2) (plus x2 y1)))
∀x2:nat
.∀y1:nat
.∀y2:nat
.le O (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) O) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus O y2) (plus x2 y1)))
case S : x2:nat ⇒
the thesis becomes
∀x3:nat
.∀y1:nat
.∀y2:nat
.le (S x2) (S z0)
→(le x3 (S z0)
→(eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) x3) y2)
→eq nat (plus (S x2) y2) (plus x3 y1)))
() by induction hypothesis we know
∀x3:nat
.∀y1:nat
.∀y2:nat
.le x2 (S z0)
→(le x3 (S z0)
→(eq nat (plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)
→eq nat (plus x2 y2) (plus x3 y1)))
assume x3: nat
we proceed by induction on x3 to prove
∀y1:nat
.∀y2:nat
.le (S x2) (S z0)
→(le x3 (S z0)
→(eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) x3) y2)
→eq nat (plus (S x2) y2) (plus x3 y1)))
case O : ⇒
the thesis becomes
∀y1:nat
.∀y2:nat
.le (S x2) (S z0)
→(le O (S z0)
→(eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) O) y2)
→eq nat (plus (S x2) y2) (plus O y1)))
assume y1: nat
assume y2: nat
suppose H: le (S x2) (S z0)
suppose : le O (S z0)
we must prove
eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) O) y2)
→eq nat (plus (S x2) y2) (plus O y1)
or equivalently
eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))
→eq nat (plus (S x2) y2) (plus O y1)
suppose H1: eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))
(H_y)
by (IH . . . .)
le x2 z0
→(le O z0
→(eq nat (plus (minus z0 x2) y1) (plus (minus z0 O) (S y2))
→eq nat (plus x2 (S y2)) (plus O y1)))
end of H_y
(H2)
(h1)
consider H_y
we proved
le x2 z0
→(le O z0
→(eq nat (plus (minus z0 x2) y1) (plus (minus z0 O) (S y2))
→eq nat (plus x2 (S y2)) (plus O y1)))
le x2 z0
→(le O z0
→(eq nat (plus (minus z0 x2) y1) (plus (minus z0 O) (S y2))
→eq nat (plus x2 (S y2)) y1))
end of h1
(h2)
by (minus_n_O .)
eq nat z0 (minus z0 O)
end of h2
by (eq_ind_r . . . h1 . h2)
le x2 z0
→(le O z0
→(eq nat (plus (minus z0 x2) y1) (plus z0 (S y2))
→eq nat (plus x2 (S y2)) y1))
end of H2
(H3)
by (plus_n_Sm . .)
we proved eq nat (S (plus z0 y2)) (plus z0 (S y2))
by (eq_ind_r . . . H2 . previous)
le x2 z0
→(le O z0
→(eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))
→eq nat (plus x2 (S y2)) y1))
end of H3
(H4)
by (plus_n_Sm . .)
we proved eq nat (S (plus x2 y2)) (plus x2 (S y2))
by (eq_ind_r . . . H3 . previous)
le x2 z0
→(le O z0
→(eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))
→eq nat (S (plus x2 y2)) y1))
end of H4
(h1) by (le_S_n . . H) we proved le x2 z0
(h2) by (le_O_n .) we proved le O z0
by (H4 h1 h2 H1)
we proved eq nat (S (plus x2 y2)) y1
that is equivalent to eq nat (plus (S x2) y2) (plus O y1)
we proved
eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))
→eq nat (plus (S x2) y2) (plus O y1)
that is equivalent to
eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) O) y2)
→eq nat (plus (S x2) y2) (plus O y1)
∀y1:nat
.∀y2:nat
.le (S x2) (S z0)
→(le O (S z0)
→(eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) O) y2)
→eq nat (plus (S x2) y2) (plus O y1)))
case S : x4:nat ⇒
the thesis becomes
∀y1:nat
.∀y2:nat
.∀H:le (S x2) (S z0)
.∀H0:le (S x4) (S z0)
.eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) (S x4)) y2)
→eq nat (plus (S x2) y2) (plus (S x4) y1)
() by induction hypothesis we know
∀y1:nat
.∀y2:nat
.le (S x2) (S z0)
→(le x4 (S z0)
→((eq
nat
plus (minus z0 x2) y1
plus <λn:nat.nat> CASE x4 OF O⇒S z0 | S l⇒minus z0 l y2)
→eq nat (S (plus x2 y2)) (plus x4 y1)))
assume y1: nat
assume y2: nat
suppose H: le (S x2) (S z0)
suppose H0: le (S x4) (S z0)
we must prove
eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) (S x4)) y2)
→eq nat (plus (S x2) y2) (plus (S x4) y1)
or equivalently
eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4) y2)
→eq nat (plus (S x2) y2) (plus (S x4) y1)
suppose H1: eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4) y2)
(h1) by (le_S_n . . H) we proved le x2 z0
(h2) by (le_S_n . . H0) we proved le x4 z0
by (IH . . . . h1 h2 H1)
we proved eq nat (plus x2 y2) (plus x4 y1)
by (f_equal . . . . . previous)
we proved eq nat (S (plus x2 y2)) (S (plus x4 y1))
that is equivalent to eq nat (plus (S x2) y2) (plus (S x4) y1)
we proved
eq nat (plus (minus z0 x2) y1) (plus (minus z0 x4) y2)
→eq nat (plus (S x2) y2) (plus (S x4) y1)
that is equivalent to
eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) (S x4)) y2)
→eq nat (plus (S x2) y2) (plus (S x4) y1)
∀y1:nat
.∀y2:nat
.∀H:le (S x2) (S z0)
.∀H0:le (S x4) (S z0)
.eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) (S x4)) y2)
→eq nat (plus (S x2) y2) (plus (S x4) y1)
we proved
∀y1:nat
.∀y2:nat
.le (S x2) (S z0)
→(le x3 (S z0)
→(eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) x3) y2)
→eq nat (plus (S x2) y2) (plus x3 y1)))
∀x3:nat
.∀y1:nat
.∀y2:nat
.le (S x2) (S z0)
→(le x3 (S z0)
→(eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) x3) y2)
→eq nat (plus (S x2) y2) (plus x3 y1)))
we proved
∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) x1) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 (S z0)
→(le x2 (S z0)
→(eq nat (plus (minus (S z0) x1) y1) (plus (minus (S z0) x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
we proved
∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 z
→(le x2 z
→(eq nat (plus (minus z x1) y1) (plus (minus z x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))
we proved
∀z:nat
.∀x1:nat
.∀x2:nat
.∀y1:nat
.∀y2:nat
.le x1 z
→(le x2 z
→(eq nat (plus (minus z x1) y1) (plus (minus z x2) y2)
→eq nat (plus x1 y2) (plus x2 y1)))