Lines Matching defs:b0
18 else if (node = "b0") then X
21 And (Xnor (s "a0")(s "b0"))
29 (s_b' node = (s_b "a0" = s_b "b0") /\ (s_b "a1" = s_b "b1"))`;
48 THEN Cases_on `s_b "b0"`
76 THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"b0"``)
80 THEN Cases_on `s "b0"` THEN Cases_on `s' "b0"`
97 val b0 = (T, "b0", ``b0:bool``, 0, 1);
99 val out = (T, "out", ``(a0:bool=b0)/\(a1=b1)``, 1, 2);
100 val A = TF [a0,a1,b0,b1] ;
117 val b0 = (T, "b0", ``T:bool``, 0, 1);
120 val A = TF [a0, a1, b0, b1] ;
137 val b0 = (T, "b0", ``b0:bool``, 0, 1);
139 val out = (T, "out", ``(a0:bool=b0)/\(a1=b1)``, 1, 2);
140 val A = TF [a0,a1,b0,b1] ;
157 val b0 = (T, "b0", ``v0:bool``, 0, 1);
160 val A = TF [a0,a1,b0,b1] ;
177 val b0 = (T, "b0", ``T:bool``, 0, 1);
180 val A = TF [a0, a1, b0, b1] ;
197 val b0 = (T, "b0", ``T:bool``, 0, 1);
200 val A = TF [a0,a1,b0,b1] ;
217 val b0 = (T, "b0", ``T:bool``, 0, 1);
220 val A = TF [a0,a1,b0,b1] ;
237 val b0 = (T, "b0", ``T:bool``, 0, 1);
240 val A = TF [a0,a1,b0,b1] ;