tests/inputs/circuits.lisp

42           (implies (and (uniquep vars)
214   (implies (not (memberp s states))
221   (implies (memberp s states)
314   (implies (memberp q (create-next-states-of-p p states vars equations))
320   (implies (subset states-prime (create-next-states-of-p p states vars
338   (implies (not (memberp s states))
346   (implies (memberp s states)
392   (implies (consp states)
406   (implies (consp y)
419   (implies (and (only-evaluations-p init vars)
455   (implies (not (equal v v-prime))
462   (implies (not (equal v v-prime))
476   (implies (not (memberp v vars))
486   (implies (memberp v vars)
497   (implies (subset vars vars-prime)
519   (implies (booleanp (<- st (evaluation-witness-variable vars st)))
525   (implies (and (boolean-list-p-states vars states)
531 (defthm boolean-p-states-implies-boolean-v
532   (implies (and (boolean-p-states v states)
539   (implies (and (boolean-list-p-states vars states)
546   (implies (and (boolean-list-p-states vars states)
553   (implies (boolean-list-p-states vars states)
564   (implies (circuitp C)
585   (implies (consp states)
594   (implies (and (< i (len x))
601   (implies (and (>= i (len x))
610   (implies (memberp q (assign-nil v states))
616   (implies (memberp q (assign-t v states))
622   (implies (and (consp states)
649   (implies (and (equal (len x) (len y))
656   (implies (and (consp states)
669   (implies (and (consp states)
679   (implies (and (consp states)
695   (implies (and (memberp v vars)
724   (implies (equal (<- p (falsifier-evaluation-eq p q vars))
731   (implies (not (memberp (falsifier-evaluation-eq p q vars) vars))
737   (implies (and (consp states)
753    (implies (equal (len x) 0)
759   (implies (and (consp states)
778   (implies (memberp e x)
785   (implies (subset x y)
792   (implies (memberp e x)
799   (implies (subset x y)
806   (implies (subset x y)
812   (implies (subset x y)
824   (implies (consp states)
831   (implies (and (evaluation-eq p q vars)
838   (implies (and (evaluation-eq p q vars)
856   (implies (and (evaluation-p st vars)
873   (implies (consp states)
882   (implies (evaluation-eq-member-p st states vars)
888   (implies (all-evaluations-p states vars)
910   (implies (and (strict-evaluation-list-p vars states)
917   (implies (and (strict-evaluation-list-p vars states)
924   (implies (and (strict-evaluation-list-p vars states)
933   (implies (and (strict-evaluation-list-p vars states)
951   (implies (and (strict-evaluation-list-p vars states)
969   (implies (and (integerp i)
979   (implies (and (integerp i)
996   (implies (memberp st states)
1003   (implies (memberp st states)
1010   (implies (and (consp states)
1025   (implies (and (consp states)
1044   (implies (and (consp states)
1052   (implies (and (consp states)
1067   (implies (strict-evaluation-p st vars)
1075   (implies (strict-evaluation-p st vars)
1083   (implies (strict-evaluation-list-p vars states)
1089   (implies (strict-evaluation-list-p vars states)
1102   (implies (null-list-p states)
1108   (implies (and (consp states)
1133   (implies (and (strict-evaluation-list-p vars init)
1142   (implies (circuitp C)
1151   (implies (circuitp C)