acl2/ml/hol_defaxiomsScript.sml

430      [oracles: DEFUN COMMON-LISP::ENDP] [axioms: ] [] |- endp x = atom x,
435   `endp x = atom x`;
445         itel [(endp lst,nil); (equal x (car lst),lst)]
452      itel [(endp lst,nil); (equal x (car lst),lst)]
460         itel [(endp x,y); (member_equal (car x) y,union_equal (cdr x) y)]
467         ite (endp x) t
489         itel [(endp lst,nil); (eq x (car lst),lst)] (member_eq x (cdr lst)),
495         ite (endp x) t (andl [member_eq (car x) y; subsetp_eq (cdr x) y]),
508         itel [(endp alist,nil); (eq x (caar alist),car alist)]
515         itel [(endp alist,nil); (equal x (caar alist),car alist)]
532           [(endp alist,nil);
540         itel [(endp l,t); (member_equal (car l) (cdr l),nil)]
546      |- strip_cars x = ite (endp x) nil (cons (caar x) (strip_cars (cdr x))),
604         itel [(endp l,nil); (zp n,car l)] (nth (add (int ~1) n) (cdr l)),
675         itel [(endp l,nil); (eql x (car l),l)] (member x (cdr l)),
681      itel [(endp l,nil); (eql x (car l),l)] (member x (cdr l))`,
688         itel [(endp l,t); (member (car l) (cdr l),nil)]
695         itel [(endp alist,nil); (eql x (caar alist),car alist)]
702       itel [(endp alist,nil); (eql x (caar alist),car alist)]
717         itel [(endp alist,nil); (eql x (cdar alist),car alist)]
724         itel [(endp alist,nil); (equal x (cdar alist),car alist)]
738         itel [(endp alist,nil); (eq x (cdar alist),car alist)]
1347           [(endp alist,nil); (string_equal acl2_str (caar alist),car alist)]
1546         ite (endp (cdr lst)) (car lst)
1570         itel [(endp l,nil); (equal acl2_str (symbol_name (car l)),l)]
1577      itel [(endp l,nil); (equal acl2_str (symbol_name (car l)),l)]
1585         ite (endp x) y (cons (car x) (binary_append (cdr x) y)),
1591      ite (endp x) y (cons (car x) (binary_append (cdr x) y))`,
1613         ite (endp x) (str "")
1620         itel [(endp l,nil); (eql x (car l),remove x (cdr l))]
1627         ite (endp x) nil
1635           [(endp l,nil);
1652           [(endp l,nil);
1663      |- revappend x y = ite (endp x) y (revappend (cdr x) (cons (car x) y)),
1678           [(endp l1,nil);
1685      |- strip_cdrs x = ite (endp x) nil (cons (cdar x) (strip_cdrs (cdr x))),
1702           [(endp alist,nil);
1722         ite (endp defuns) (reverse acc)
1787         ite (endp lst) ans
1807         itel [(endp x,nil); (member_eq (car x) y,t)]
1814         itel [(endp x,nil); (member_equal (car x) y,t)]
1821         ite (endp forms) nil
1830         itel [(endp lst,nil); (endp (cdr lst),car lst)]
1876           [(endp l,nil);
1887           [(endp l,nil);
1909         itel [(endp lst,nil); (equal item (car lst),acc)]
1916         itel [(endp lst,nil); (eql item (car lst),acc)]
1931         itel [(endp lst,nil); (eq item (car lst),acc)]
1962         ite (endp bindings)
1986         ite (ite (endp bindings) (endp bindings) (endp (cdr bindings)))
2229         ite (endp l1) (ite (endp l2) nil i)
2230           (ite (endp l2) nil
2239      ite (endp l1)
2240          (ite (endp l2) nil i)
2241          (ite (endp l2)
2314           [(endp seq,reverse acc);
2331         ite (endp x) t (andl [member (car x) y; subsetp (cdr x) y]),
2373           [(endp world_alist,default);
2384           [(endp world_alist,default);
2409         ite (endp l) (cons (cons key value) nil)
2418         itel [(endp l,nil); (eq key (caar l),cdr l)]
2433           [(endp alist,nil);
2444           [(endp world_alist,nil);
2458           [(endp alist,nil);
2473           [(endp world_alist,nil);
2518           [(endp l1,nil);
2548         itel [(endp l,nil); (eq key (car l),l)] (assoc_keyword key (cddr l)),
2763         itel [(endp l,nil); (zp n,car l)] (mv_nth (add (int ~1) n) (cdr l)),
2769      itel [(endp l,nil); (zp n,car l)] (mv_nth (add (int ~1) n) (cdr l))`,
2776         ite (endp args) nil
2969         ite (endp alist1) t
3024         ite (endp l) t
3358         itel [(endp l,nil); (eq x (caar l),cdr l)]
3400         ite (endp bindings) nil
3419         ite (endp bindings) nil
3433         ite (endp bindings) nil
3810           [(endp l,nil);
4008         ite (endp l) (nat 0) (add (car l) (mult b (power_eval (cdr l) b))),
4055           [(endp alist,List [cons name val]);
4064           [(endp alist,List [cons name val]);
4073           [(endp alist,List [cons name val]);
4162           [(endp lst1,lst2);
4195         ite (endp runes) acc
4348         itel [(endp alist,nil); (eq key (caar alist),cdr alist)]
4355         itel [(endp alist,nil); (equal key (caar alist),cdr alist)]
4490         ite (endp y) nil
4498           [(endp lst,nil);
4513           [(endp l1,nil);
4521      |- evens l = ite (endp l) nil (cons (car l) (evens (cddr l))),