1 include "arithmetics/nat.ma".
3 \ 5img class="anchor" src="icons/tick.png" id="decidable_not"
\ 6lemma decidable_not: ∀P.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 P →
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6P).
4 #P * #H [%2 % * /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/ | /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/]
7 \ 5img class="anchor" src="icons/tick.png" id="decidable_or"
\ 6lemma decidable_or: ∀P,Q.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 P →
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 Q →
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (P
\ 5a title="logical or" href="cic:/fakeuri.def(1)"
\ 6∨
\ 5/a
\ 6Q).
8 #P #Q * #HP [#_ %1 %1 // |* #HQ [ %1 %2 // | %2 % * /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/]
11 \ 5img class="anchor" src="icons/tick.png" id="decidable_forall"
\ 6lemma decidable_forall: ∀P. (∀i.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (P i))→
12 ∀n.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (∀i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → P i).
14 [%1 #i #lti0 @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … lti0) @
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6 //
17 [%1 #i #lei0 cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … lei0) #H1
18 [@H @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 @H1 |>(
\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"
\ 6injective_S
\ 5/a
\ 6 … H1) @HPm]
19 |%2 @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … HPm) #H1 @H1 //
21 |%2 @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 #i #leim @H1 @
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6 //
26 \ 5img class="anchor" src="icons/tick.png" id="not_exists_to_forall"
\ 6lemma not_exists_to_forall: ∀P,n.
27 \ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6(
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 P i) → ∀i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6 P i.
29 [#_ #i #lti0 @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … lti0) @
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6 //
30 |#m #Hind #H1 #i #leiS cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … leiS) #H2
31 [@(Hind … (
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 … H2)) @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H1) *
32 #a * #leam #Pa %{a} % // @
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6 //
33 |@(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H1) #Pi %{i} % //
38 \ 5img class="anchor" src="icons/tick.png" id="not_forall_to_exists"
\ 6lemma not_forall_to_exists: ∀P,n. (∀i.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (P i)) →
39 \ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6(∀i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → P i) → (
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6 (P i)).
41 [* #H @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @H #i #lti0 @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 … lti0) @
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6 //
42 |#m #Hind #H1 cases (decP m) #H2
44 [#i * #leim #nPi %{i} % // @
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6 //
45 |@(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H1) #H3 #i #leiS cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … leiS)
46 [#ltiS @H3 @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 // |#eqi //]