| | Some definitions of interest. |
|
| accumulate | Def process u j where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } == if P(j;u) F(j;u) else G(j;list_accum(s',i'.process s' i' where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } ;H(j;u);N(j;u))) fi (recursive) |
| | | Thm*  A,B:Type, P:(B  A ), F,G,H:(BAA), N:(BA(B List)), M:(A ). (i:B, s:A. P(i,s)   M(F(i,s)) M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A.  P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; }  {s:A| M(s)M(u) }) |
|
| assert | Def  b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| nat | Def == {i: | 0i } |
| | | Thm* Type |
|
| sublist | Def L1  L2 ==  f:(||L1||||L2||). increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))] T) |
| | | Thm* T:Type, L1,L2:T List. L1 L2 Prop |
|
| le | Def AB == B < A |
| | | Thm* i,j:. (ij) Prop |
|
| list_accum | Def list_accum(x,a.f(x;a);y;l) == Case of l; nil y ; b.l' list_accum(x,a.f(x;a);f(y;b);l') (recursive) |
| | | Thm* T,T':Type, l:T List, y:T', f:(T'TT'). list_accum(x,a.f(x,a);y;l) T' |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
