1new_theory`mux`;;
2
3new_definition
4 (`NAND_SPEC`, "!i1 i2 o. NAND_SPEC(i1,i2,o)  =  o  =  ~(i1  /\  i2)");;
5
6new_definition
7 (`INV_SPEC`, "!i o. INV_SPEC(i,o)  =  o  =  ~i");;
8
9new_definition
10 (`MUX_SPEC`, "!c i1 i2 o. MUX_SPEC(c,i1,i2,o)  =  o  =  (c => i1 | i2)");;
11
12 new_definition
13  (`MUX_IMP`,
14   "!c i1 i2 o.
15    MUX_IMP(c,i1,i2,o)  =
16    ?l1 l2 l3.
17     INV_SPEC(c,l1)  /\
18     NAND_SPEC(l1,i2,l2)  /\
19     NAND_SPEC(c,i1,l3)  /\
20     NAND_SPEC(l2,l3,o)");;
21
22close_theory();;
23
24load_theory`mux`;;
25
26let prims = maptok (axiom `mux`) `INV_SPEC NAND_SPEC`;;
27
28let MUX_IMP = axiom `mux` `MUX_IMP`;;
29
30let MUX_THM1 = save_thm(`MUX_THM1`, EXPAND prims MUX_IMP);;
31