| | Who Cites list iso 2? |
|
| list_iso_2 | Def (~ eq)(L,M) == (( eq)(L,M)) ((eq)(M,L)) |
| | | Thm*  T:Type, eq:(T  T ). (~eq)  (T List)(T List) |
|
| sublist_2 | Def (eq)(L,M) == xL.x(eq) M |
| | | Thm* T:Type, eq:(TT). (eq) (T List)(T List) |
|
| list_all_2 | Def xL.P(x) == (letrec all L = (Case of L; nil  true ; h.t P(h)(all(t))) ) (L) |
| | | Thm* T:Type, P:(T), L:T List. xL.P(x) |
|
| band | Def pq == if p q else false fi |
| | | Thm* p,q:. (pq) |
|
| 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 |
|
| 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) |
