File: lmem.th

package info (click to toggle)
hol88 2.02.19940316-35.1
  • links: PTS
  • area: main
  • in suites: bullseye
  • size: 66,004 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (4 lines) | stat: -rw-r--r-- 1,447 bytes parent folder | download | duplicates (9) 
1
2
3
4
 

(SETQ %THEORYDATA (QUOTE ((PARENTS HOL) (TYPES) (NAMETYPES) (OPERATORS (LMEM |fun| (%VARTYPE . *) (|fun| (|list| (%VARTYPE . *)) (|bool|)))) (PAIRED-INFIXES) (CURRIED-INFIXES) (PREDICATES) (VERSION . "2.01 (SUN4/AKCL)") (STAMP . 2940939269)))) 

(SETQ %THEOREMS (QUOTE ((SHARETYPES 2 (NIL%1 |list| (%VARTYPE . *)) (|x%0| %VARTYPE . *)) (AXIOM (LMEM_DEF PRED HOL_ASSERT COMB ((CONST HOL_DEFINITION) COMB ((COMB ((CONST |/\\|) COMB ((CONST !) ABS ((VAR |x| %T . |x%0|) COMB ((COMB ((CONST =) COMB ((COMB ((CONST LMEM) VAR |x| %T . |x%0|)) CONST NIL %T . NIL%1) |bool|)) CONST F) |bool|)))) COMB ((CONST !) ABS ((VAR |x| %T . |x%0|) COMB ((CONST !) ABS ((VAR |h| %T . |x%0|) COMB ((CONST !) ABS ((VAR |t| %T . NIL%1) COMB ((COMB ((CONST =) COMB ((COMB ((CONST LMEM) VAR |x| %T . |x%0|)) COMB ((COMB ((CONST CONS) VAR |h| %T . |x%0|)) VAR |t| %T . NIL%1) %T . NIL%1) |bool|)) COMB ((COMB ((CONST |\\/|) COMB ((COMB ((CONST =) VAR |x| %T . |x%0|)) VAR |h| %T . |x%0|))) COMB ((COMB ((CONST LMEM) VAR |x| %T . |x%0|)) VAR |t| %T . NIL%1))) |bool|)) |bool|)) |bool|)))))) (FACT (LIST_OF_BINDERS PRED HOL_ASSERT COMB ((CONST BINDERS) VAR |arb| %T . |x%0|) |bool|) (NULL_NOT_LMEM PRED HOL_ASSERT COMB ((CONST !) ABS ((VAR |x| %T . |x%0|) COMB ((CONST !) ABS ((VAR |l| %T . NIL%1) COMB ((COMB ((CONST ==>) COMB ((CONST NULL) VAR |l| %T . NIL%1))) COMB ((CONST ~) COMB ((COMB ((CONST LMEM) VAR |x| %T . |x%0|)) VAR |l| %T . NIL%1))))) |bool|)) |bool|)))))