Lines Matching refs:a1
17 else if (node = "a1") then X
22 (Xnor (s "a1")(s "b1"))
29 (s_b' node = (s_b "a0" = s_b "b0") /\ (s_b "a1" = s_b "b1"))`;
49 THEN Cases_on `s_b "a1"`
75 THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``)
81 THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"`
96 val a1 = (T, "a1", ``a1:bool``, 0, 1);
99 val out = (T, "out", ``(a0:bool=b0)/\(a1=b1)``, 1, 2);
100 val A = TF [a0,a1,b0,b1] ;
116 val a1 = (T, "a1", ``T:bool``, 0, 1);
120 val A = TF [a0, a1, b0, b1] ;
136 val a1 = (T, "a1", ``a1:bool``, 0, 1);
139 val out = (T, "out", ``(a0:bool=b0)/\(a1=b1)``, 1, 2);
140 val A = TF [a0,a1,b0,b1] ;
156 val a1 = (T, "a1", ``v1:bool``, 0, 1);
160 val A = TF [a0,a1,b0,b1] ;
176 val a1 = (T, "a1", ``T:bool``, 0, 1);
180 val A = TF [a0, a1, b0, b1] ;
196 val a1 = (T, "a1", ``F:bool``, 0, 1);
200 val A = TF [a0,a1,b0,b1] ;
216 val a1 = (T, "a1", ``F:bool``, 0, 1);
220 val A = TF [a0,a1,b0,b1] ;
236 val a1 = (T, "a1", ``F:bool``, 0, 1);
240 val A = TF [a0,a1,b0,b1] ;