| | Who Cites disjoint? |
|
| disjoint | Def disjoint(eq;L1;L2) ==  x L1.   x(eq) L2 |
| | | Thm* T:Type, eq:(T  T ), L1,L2:T List. disjoint(eq;L1;L2) Type |
|
| is_member | Def x(eq) L == (letrec is_member x eq L = (Case of L; nil  false ; h.t if eq(x,h) true else is_member(x,eq,t) fi) ) (x,eq,L) |
| | | Thm* T:Type, eq:(TT), u:T. u(eq) nil |
| | | Thm* T:Type, eq:(TT), x:T, L:T List. x(eq) L |
|
| bnot | Def b == if b false else true fi |
| | | Thm* b:. b |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| list_all | Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L) |
| | | Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type |
| | | Thm* T:Type, P:(TType). xnil.P(x) Type |
|
| letrec_body | Def = b == b |
|
| letrec_arg | Def x b(x) (x) == b(x) |
|
| letrec | Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive) |
