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
27 definition unialpha_eq ≝
29 [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
30 | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
31 | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
32 | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
34 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
35 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
36 | *: normalize % #Hfalse destruct ]
37 |*: * [1,5,9,13: #y ] normalize % #H1 destruct % ]
40 axiom unialpha_unique : uniqueb DeqUnialpha [bit true;bit false;comma;bar;grid] = true.
42 definition FSUnialpha ≝
43 mk_FinSet DeqUnialpha [bit true;bit false;comma;bar;grid] unialpha_unique.
45 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
47 definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
49 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
51 definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].