Lines Matching defs:IF
6 (IF (NULL X)
8 (IF (CONSP X)
9 (IF (CONSP (CAR X))
10 (IF (RCDP (CDR X))
11 (IF (CDR (CAR X))
12 (IF (NULL (CDR X))
21 (IF (NOT (RCDP X))
23 (IF (CONSP X)
24 (IF (NULL (CDR X))
25 (IF (CONSP (CAR X))
26 (IF (NULL (CAR (CAR X)))
33 (DEFUN ACL2->RCD (X) (IF (IFRP X) (CONS (CONS 'NIL X) 'NIL) X))
35 (DEFUN RCD->ACL2 (X) (IF (IFRP X) (CDR (CAR X)) X))
38 (IF (IF (ENDP X)
42 (IF (EQUAL A (CAR (CAR X)))
49 (IF (IF (ENDP R)
52 (IF V (CONS (CONS A V) R) R)
53 (IF (EQUAL A (CAR (CAR R)))
54 (IF V (CONS (CONS A V) (CDR R)) (CDR R))
60 (IF (ENDP X)
73 (DEFTHM G-OF-S-REDUX (EQUAL (G A (S B V R)) (IF (EQUAL A B) V (G A R))))
88 (IF V (INSERT A (KEYS R))
97 (DEFTHM NON-NIL-IF-G-NON-NIL (IMPLIES (G A R) R))
104 (IF (ENDP UPDS)