2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
13 (* ALphabet of the universal machine *)
15 include "basics/finset.ma".
18 include "turing/if_machine.ma".
19 include "turing/universal/tests.ma". *)
21 inductive unialpha : Type[0] ≝
22 | bit : bool → unialpha
28 definition unialpha_eq ≝
30 [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
31 | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ]
32 | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
33 | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
34 | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
36 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
37 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
38 | *: normalize % #Hfalse destruct ]
39 |*: * [1,6,11,16: #y ] normalize % #H1 destruct % ]
42 axiom unialpha_unique : uniqueb DeqUnialpha [bit true;bit false;comma;bar;grid] = true.
44 definition FSUnialpha ≝
45 mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] unialpha_unique.
47 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
49 definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].
51 definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
53 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
55 definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].
57 definition bit_or_null ≝ λc.is_bit c ∨ is_null c.