DEFINITION nat_dec()
TYPE =
∀n1:nat.∀n2:nat.(or (eq nat n1 n2) (eq nat n1 n2)→∀P:Prop.P)
BODY =
assume n1: nat
we proceed by induction on n1 to prove ∀n2:nat.(or (eq nat n1 n2) (eq nat n1 n2)→∀P:Prop.P)
case O : ⇒
the thesis becomes ∀n2:nat.(or (eq nat O n2) (eq nat O n2)→∀P:Prop.P)
assume n2: nat
we proceed by induction on n2 to prove or (eq nat O n2) (eq nat O n2)→∀P:Prop.P
case O : ⇒
the thesis becomes or (eq nat O O) (eq nat O O)→∀P:Prop.P
by (refl_equal . .)
we proved eq nat O O
by (or_introl . . previous)
or (eq nat O O) (eq nat O O)→∀P:Prop.P
case S : n:nat ⇒
the thesis becomes or (eq nat O (S n)) (eq nat O (S n))→∀P:Prop.P
() by induction hypothesis we know or (eq nat O n) (eq nat O n)→∀P:Prop.P
suppose H0: eq nat O (S n)
assume P: Prop
(H1)
we proceed by induction on H0 to prove <λ:nat.Prop> CASE S n 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 n OF O⇒True | S ⇒False
end of H1
consider H1
we proved <λ:nat.Prop> CASE S n OF O⇒True | S ⇒False
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
we proved (eq nat O (S n))→∀P:Prop.P
by (or_intror . . previous)
or (eq nat O (S n)) (eq nat O (S n))→∀P:Prop.P
we proved or (eq nat O n2) (eq nat O n2)→∀P:Prop.P
∀n2:nat.(or (eq nat O n2) (eq nat O n2)→∀P:Prop.P)
case S : n:nat ⇒
the thesis becomes ∀n2:nat.(or (eq nat (S n) n2) (eq nat (S n) n2)→∀P:Prop.P)
(H) by induction hypothesis we know ∀n2:nat.(or (eq nat n n2) (eq nat n n2)→∀P:Prop.P)
assume n2: nat
we proceed by induction on n2 to prove or (eq nat (S n) n2) (eq nat (S n) n2)→∀P:Prop.P
case O : ⇒
the thesis becomes or (eq nat (S n) O) (eq nat (S n) O)→∀P:Prop.P
suppose H0: eq nat (S n) O
assume P: Prop
(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 n OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S n 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 P
we proved P
we proved (eq nat (S n) O)→∀P:Prop.P
by (or_intror . . previous)
or (eq nat (S n) O) (eq nat (S n) O)→∀P:Prop.P
case S : n0:nat ⇒
the thesis becomes or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
(H0) by induction hypothesis we know or (eq nat (S n) n0) (eq nat (S n) n0)→∀P:Prop.P
by (H .)
we proved or (eq nat n n0) (eq nat n n0)→∀P:Prop.P
we proceed by induction on the previous result to prove or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
case or_introl : H1:eq nat n n0 ⇒
the thesis becomes or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
we proceed by induction on H1 to prove or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
case refl_equal : ⇒
the thesis becomes or (eq nat (S n) (S n)) (eq nat (S n) (S n))→∀P:Prop.P
by (refl_equal . .)
we proved eq nat (S n) (S n)
by (or_introl . . previous)
or (eq nat (S n) (S n)) (eq nat (S n) (S n))→∀P:Prop.P
or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
case or_intror : H1:(eq nat n n0)→∀P:Prop.P ⇒
the thesis becomes or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
suppose H2: eq nat (S n) (S n0)
assume P: Prop
(H3)
by (f_equal . . . . . H2)
we proved
eq nat <λ:nat.nat> CASE S n OF O⇒n | S n3⇒n3 <λ:nat.nat> CASE S n0 OF O⇒n | S n3⇒n3
eq
nat
λe:nat.<λ:nat.nat> CASE e OF O⇒n | S n3⇒n3 (S n)
λe:nat.<λ:nat.nat> CASE e OF O⇒n | S n3⇒n3 (S n0)
end of H3
(H4)
consider H3
we proved
eq nat <λ:nat.nat> CASE S n OF O⇒n | S n3⇒n3 <λ:nat.nat> CASE S n0 OF O⇒n | S n3⇒n3
that is equivalent to eq nat n n0
by (eq_ind_r . . . H1 . previous)
(eq nat n n)→∀P0:Prop.P0
end of H4
by (refl_equal . .)
we proved eq nat n n
by (H4 previous .)
we proved P
we proved (eq nat (S n) (S n0))→∀P:Prop.P
by (or_intror . . previous)
or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
or (eq nat (S n) (S n0)) (eq nat (S n) (S n0))→∀P:Prop.P
we proved or (eq nat (S n) n2) (eq nat (S n) n2)→∀P:Prop.P
∀n2:nat.(or (eq nat (S n) n2) (eq nat (S n) n2)→∀P:Prop.P)
we proved ∀n2:nat.(or (eq nat n1 n2) (eq nat n1 n2)→∀P:Prop.P)
we proved ∀n1:nat.∀n2:nat.(or (eq nat n1 n2) (eq nat n1 n2)→∀P:Prop.P)