DEFINITION aplus_inj()
TYPE =
∀g:G.∀h1:nat.∀h2:nat.∀a:A.(eq A (aplus g a h1) (aplus g a h2))→(eq nat h1 h2)
BODY =
assume g: G
assume h1: nat
we proceed by induction on h1 to prove ∀h2:nat.∀a:A.(eq A (aplus g a h1) (aplus g a h2))→(eq nat h1 h2)
case O : ⇒
the thesis becomes ∀h2:nat.∀a:A.(eq A (aplus g a O) (aplus g a h2))→(eq nat O h2)
assume h2: nat
we proceed by induction on h2 to prove ∀a:A.(eq A (aplus g a O) (aplus g a h2))→(eq nat O h2)
case O : ⇒
the thesis becomes ∀a:A.(eq A (aplus g a O) (aplus g a O))→(eq nat O O)
assume a: A
we must prove (eq A (aplus g a O) (aplus g a O))→(eq nat O O)
or equivalently (eq A a a)→(eq nat O O)
suppose : eq A a a
by (refl_equal . .)
we proved eq nat O O
we proved (eq A a a)→(eq nat O O)
that is equivalent to (eq A (aplus g a O) (aplus g a O))→(eq nat O O)
∀a:A.(eq A (aplus g a O) (aplus g a O))→(eq nat O O)
case S : n:nat ⇒
the thesis becomes ∀a:A.(eq A (aplus g a O) (aplus g a (S n)))→(eq nat O (S n))
() by induction hypothesis we know ∀a:A.(eq A a (aplus g a n))→(eq nat O n)
assume a: A
we must prove (eq A (aplus g a O) (aplus g a (S n)))→(eq nat O (S n))
or equivalently (eq A a (asucc g (aplus g a n)))→(eq nat O (S n))
suppose H0: eq A a (asucc g (aplus g a n))
(H1)
by (aplus_asucc . . .)
we proved eq A (aplus g (asucc g a) n) (asucc g (aplus g a n))
by (eq_ind_r . . . H0 . previous)
eq A a (aplus g (asucc g a) n)
end of H1
by (sym_eq . . . H1)
we proved eq A (aplus g (asucc g a) n) a
by (aplus_asucc_false . . . previous .)
we proved eq nat O (S n)
we proved (eq A a (asucc g (aplus g a n)))→(eq nat O (S n))
that is equivalent to (eq A (aplus g a O) (aplus g a (S n)))→(eq nat O (S n))
∀a:A.(eq A (aplus g a O) (aplus g a (S n)))→(eq nat O (S n))
we proved ∀a:A.(eq A (aplus g a O) (aplus g a h2))→(eq nat O h2)
∀h2:nat.∀a:A.(eq A (aplus g a O) (aplus g a h2))→(eq nat O h2)
case S : n:nat ⇒
the thesis becomes ∀h2:nat.∀a:A.(eq A (aplus g a (S n)) (aplus g a h2))→(eq nat (S n) h2)
(H) by induction hypothesis we know ∀h2:nat.∀a:A.(eq A (aplus g a n) (aplus g a h2))→(eq nat n h2)
assume h2: nat
we proceed by induction on h2 to prove ∀a:A.(eq A (aplus g a (S n)) (aplus g a h2))→(eq nat (S n) h2)
case O : ⇒
the thesis becomes ∀a:A.(eq A (aplus g a (S n)) (aplus g a O))→(eq nat (S n) O)
assume a: A
we must prove (eq A (aplus g a (S n)) (aplus g a O))→(eq nat (S n) O)
or equivalently (eq A (asucc g (aplus g a n)) a)→(eq nat (S n) O)
suppose H0: eq A (asucc g (aplus g a n)) a
(H1)
by (aplus_asucc . . .)
we proved eq A (aplus g (asucc g a) n) (asucc g (aplus g a n))
by (eq_ind_r . . . H0 . previous)
eq A (aplus g (asucc g a) n) a
end of H1
by (aplus_asucc_false . . . H1 .)
we proved eq nat (S n) O
we proved (eq A (asucc g (aplus g a n)) a)→(eq nat (S n) O)
that is equivalent to (eq A (aplus g a (S n)) (aplus g a O))→(eq nat (S n) O)
∀a:A.(eq A (aplus g a (S n)) (aplus g a O))→(eq nat (S n) O)
case S : n0:nat ⇒
the thesis becomes
∀a:A
.eq A (aplus g a (S n)) (aplus g a (S n0))
→eq nat (S n) (S n0)
() by induction hypothesis we know
∀a:A
.(eq A (asucc g (aplus g a n)) (aplus g a n0))→(eq nat (S n) n0)
assume a: A
we must prove
eq A (aplus g a (S n)) (aplus g a (S n0))
→eq nat (S n) (S n0)
or equivalently
eq A (asucc g (aplus g a n)) (asucc g (aplus g a n0))
→eq nat (S n) (S n0)
suppose H1: eq A (asucc g (aplus g a n)) (asucc g (aplus g a n0))
(H2)
by (aplus_asucc . . .)
we proved eq A (aplus g (asucc g a) n) (asucc g (aplus g a n))
by (eq_ind_r . . . H1 . previous)
eq A (aplus g (asucc g a) n) (asucc g (aplus g a n0))
end of H2
(H3)
by (aplus_asucc . . .)
we proved eq A (aplus g (asucc g a) n0) (asucc g (aplus g a n0))
by (eq_ind_r . . . H2 . previous)
eq A (aplus g (asucc g a) n) (aplus g (asucc g a) n0)
end of H3
by (H . . H3)
we proved eq nat n n0
by (f_equal . . . . . previous)
we proved eq nat (S n) (S n0)
we proved
eq A (asucc g (aplus g a n)) (asucc g (aplus g a n0))
→eq nat (S n) (S n0)
that is equivalent to
eq A (aplus g a (S n)) (aplus g a (S n0))
→eq nat (S n) (S n0)
∀a:A
.eq A (aplus g a (S n)) (aplus g a (S n0))
→eq nat (S n) (S n0)
we proved ∀a:A.(eq A (aplus g a (S n)) (aplus g a h2))→(eq nat (S n) h2)
∀h2:nat.∀a:A.(eq A (aplus g a (S n)) (aplus g a h2))→(eq nat (S n) h2)
we proved ∀h2:nat.∀a:A.(eq A (aplus g a h1) (aplus g a h2))→(eq nat h1 h2)
we proved ∀g:G.∀h1:nat.∀h2:nat.∀a:A.(eq A (aplus g a h1) (aplus g a h2))→(eq nat h1 h2)