include "basics/relations.ma".
(********** bool **********)
-inductive bool: Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="bool"\ 6inductive bool: Type[0] ≝
| true : bool
| false : bool.
-(* destruct does not work *)
-theorem not_eq_true_false : \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="not_eq_true_false"\ 6theorem not_eq_true_false : \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
@\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq change with match \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 with [true ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6|false ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6]
>Heq // qed.
-definition notb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+\ 5img class="anchor" src="icons/tick.png" id="notb"\ 6definition notb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
λ b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. match b with [true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6|false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 ].
interpretation "boolean not" 'not x = (notb x).
-theorem notb_elim: ∀ b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
+\ 5img class="anchor" src="icons/tick.png" id="notb_elim"\ 6theorem notb_elim: ∀ b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
match b with
[ true ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
| false ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6] → P (\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b).
#b #P elim b normalize // qed.
-theorem notb_notb: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
+\ 5img class="anchor" src="icons/tick.png" id="notb_notb"\ 6theorem notb_notb: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
#b elim b // qed.
-theorem injective_notb: \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="injective_notb"\ 6theorem injective_notb: \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6.
#b1 #b2 #H // qed.
-theorem noteq_to_eqnot: ∀b1,b2. b1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b2 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2.
+\ 5img class="anchor" src="icons/tick.png" id="noteq_to_eqnot"\ 6theorem noteq_to_eqnot: ∀b1,b2. b1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b2 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2.
* * // #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 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/
qed.
-theorem eqnot_to_noteq: ∀b1,b2. b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2 → b1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b2.
+\ 5img class="anchor" src="icons/tick.png" id="eqnot_to_noteq"\ 6theorem eqnot_to_noteq: ∀b1,b2. b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2 → b1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b2.
* * normalize // #H @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … \ 5a href="cic:/matita/basics/bool/not_eq_true_false.def(3)"\ 6not_eq_true_false\ 5/a\ 6) //
qed.
-definition andb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+\ 5img class="anchor" src="icons/tick.png" id="andb"\ 6definition andb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
λb1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. match b1 with [ true ⇒ b2 | false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ].
interpretation "boolean and" 'and x y = (andb x y).
-theorem andb_elim: ∀ b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. ∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
+\ 5img class="anchor" src="icons/tick.png" id="andb_elim"\ 6theorem andb_elim: ∀ b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. ∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
match b1 with [ true ⇒ P b2 | false ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6] → P (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2).
#b1 #b2 #P (elim b1) normalize // qed.
-theorem andb_true_l: ∀ b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="true_to_andb_true"\ 6theorem true_to_andb_true: ∀b1,b2. b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#b1 cases b1 normalize //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="andb_true_l"\ 6theorem andb_true_l: ∀ b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#b1 (cases b1) normalize // qed.
-theorem andb_true_r: ∀b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="andb_true_r"\ 6theorem andb_true_r: ∀b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#b1 #b2 (cases b1) normalize // (cases b2) // qed.
-theorem andb_true: ∀b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="andb_true"\ 6theorem andb_true: ∀b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6, \ 5a href="cic:/matita/basics/bool/andb_true_l.def(4)"\ 6andb_true_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-definition orb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+\ 5img class="anchor" src="icons/tick.png" id="orb"\ 6definition orb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
λb1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.match b1 with [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | false ⇒ b2].
interpretation "boolean or" 'or x y = (orb x y).
-theorem orb_elim: ∀ b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. ∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
+\ 5img class="anchor" src="icons/tick.png" id="orb_elim"\ 6theorem orb_elim: ∀ b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. ∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
match b1 with [ true ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | false ⇒ P b2] → P (\ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 b1 b2).
#b1 #b2 #P (elim b1) normalize // qed.
-lemma orb_true_r1: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="orb_true_r1"\ 6lemma orb_true_r1: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (b1 \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#b1 #b2 #H >H // qed.
-lemma orb_true_r2: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="orb_true_r2"\ 6lemma orb_true_r2: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (b1 \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#b1 #b2 #H >H cases b1 // qed.
-lemma orb_true_l: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="orb_true_l"\ 6lemma orb_true_l: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
(b1 \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 (b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6).
* normalize /\ 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, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-definition xorb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+\ 5img class="anchor" src="icons/tick.png" id="xorb"\ 6definition xorb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
λb1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
match b1 with
[ true ⇒ match b2 with [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 | false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 ]
| false ⇒ match b2 with [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ]].
notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
-(* notation > "£ term 46 e & term 46 t & term 46 f" non associative with precedence 46 *)
- for @{ 'ite $e $t $f }.
+ for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }.
notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
- for @{ match $e with [ true ⇒ $t | false ⇒ $f] }.
-
-definition ite ≝ λA:Type[0].λe.λt,f:A.match e with [ true ⇒ t | false ⇒ f ].
-
-interpretation "if then else" 'ite e t f = (ite ? e t f).
-
-(* axiom foo : ∀b.\ 5a title="if then else" href="cic:/fakeuri.def(1)"\ 6£\ 5/a\ 6 b & \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 & \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6. *)
-axiom foo : ∀b. if b then True else False.
+ for @{ match $e with [ true ⇒ $t | false ⇒ $f] }.
-(*theorem bool_to_decidable_eq:
+\ 5img class="anchor" src="icons/tick.png" id="bool_to_decidable_eq"\ 6theorem bool_to_decidable_eq:
∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (b1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b2).
#b1 #b2 (cases b1) (cases b2) /\ 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, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ %2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem true_or_false:
+\ 5img class="anchor" src="icons/tick.png" id="true_or_false"\ 6theorem true_or_false:
∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
-#b (cases b) /\ 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, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.*)
\ No newline at end of file
+#b (cases b) /\ 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, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
\ No newline at end of file
projects / helm.git / blobdiff