1(IN-PACKAGE "ACL2") 2 3(INCLUDE-BOOK "total-order") 4 5(DEFUN MEMBERP (A X) 6 (IF (CONSP X) 7 (IF (EQUAL A (CAR X)) 8 (EQUAL A (CAR X)) 9 (MEMBERP A (CDR X))) 10 'NIL)) 11 12(DEFUN DROP (A X) 13 (IF (ENDP X) 14 'NIL 15 (IF (EQUAL A (CAR X)) 16 (DROP A (CDR X)) 17 (CONS (CAR X) (DROP A (CDR X)))))) 18 19(DEFUN INSERT (A X) 20 (IF (ENDP X) 21 (CONS A 'NIL) 22 (IF (EQUAL A (CAR X)) 23 X 24 (IF (<< A (CAR X)) 25 (CONS A X) 26 (CONS (CAR X) (INSERT A (CDR X))))))) 27 28(DEFUN ORDEREDP (X) 29 (IF (ENDP (CDR X)) 30 (ENDP (CDR X)) 31 (IF (<< (CAR X) (CAR (CDR X))) 32 (ORDEREDP (CDR X)) 33 'NIL))) 34 35(DEFUN UNIQUEP (X) 36 (IF (ENDP X) 37 (ENDP X) 38 (IF (NOT (MEMBERP (CAR X) (CDR X))) 39 (UNIQUEP (CDR X)) 40 'NIL))) 41 42(DEFTHM MEMBERP-INSERT-SAME (EQUAL (MEMBERP A (INSERT A X)) 'T)) 43 44(DEFTHM MEMBERP-INSERT-DIFF 45 (IMPLIES (NOT (EQUAL A B)) 46 (EQUAL (MEMBERP A (INSERT B X)) 47 (MEMBERP A X)))) 48 49(DEFTHM MEMBERP-DROP-SAME (EQUAL (MEMBERP A (DROP A X)) 'NIL)) 50 51(DEFTHM MEMBERP-DROP-DIFF 52 (IMPLIES (NOT (EQUAL A B)) 53 (EQUAL (MEMBERP A (DROP B X)) 54 (MEMBERP A X)))) 55 56(DEFTHM ORDERED-IMPLIES-UNIQUE (IMPLIES (ORDEREDP X) (UNIQUEP X))) 57 58(DEFTHM MEMBERP-YES-REDUCE-INSERT 59 (IMPLIES (IF (ORDEREDP X) (MEMBERP A X) 'NIL) 60 (EQUAL (INSERT A X) X))) 61 62(DEFTHM MEMBERP-NO-REDUCE-DROP 63 (IMPLIES (IF (TRUE-LISTP X) 64 (NOT (MEMBERP A X)) 65 'NIL) 66 (EQUAL (DROP A X) X))) 67 68(DEFTHM DROP-PRESERVES-ORDEREDP 69 (IMPLIES (ORDEREDP X) 70 (ORDEREDP (DROP A X)))) 71 72(DEFTHM INSERT-PRESERVES-ORDEREDP 73 (IMPLIES (ORDEREDP X) 74 (ORDEREDP (INSERT A X)))) 75 76(DEFTHM DROP-OF-INSERT-IS-SAME 77 (IMPLIES (IF (TRUE-LISTP X) 78 (NOT (MEMBERP A X)) 79 'NIL) 80 (EQUAL (DROP A (INSERT A X)) X))) 81 82(DEFTHM INSERT-OF-DROP-IS-SAME 83 (IMPLIES (IF (ORDEREDP X) 84 (IF (TRUE-LISTP X) (MEMBERP A X) 'NIL) 85 'NIL) 86 (EQUAL (INSERT A (DROP A X)) X))) 87 88(DEFTHM INSERT-RETURNS-TRUE-LISTS 89 (IMPLIES (TRUE-LISTP X) 90 (TRUE-LISTP (INSERT A X)))) 91