| nd_computation |
Def NComp(Alph;St) == {C:(St Alph* List )|  i: (||C||-1). ||2of(C[i])|| > 0}
Thm* NComp(Alph;St)  Type
|
| select |
Def l[i] == hd(nth_tl(i;l))
Thm* l:A*, n: . 0 n   n < ||l|| l[n] A
|
| pi2 |
Def 2of(t) == t.2
Thm* B:(A  Type), p:a:AB(a). 2of(p) B(1of(p))
|
| list_p |
Def T List == {l:(T*)| ||l|| > 0}
Thm* (T List) Type
|
| length |
Def (rec) ||as|| == Case of as : null  0 ; a.as' ||as'||+1
Thm* l:A*. ||l||
Thm* ||nil||
|
| gt |
Def i > j == j < i
Thm* i,j:. i > j Prop
|
| int_seg |
Def {i..j } == {k:| i k < j}
Thm* m,n:. {m..n} Type
|
| nth_tl |
Def (rec) nth_tl(n;as) == if n z 0 as else nth_tl(n-1;tl(as)) fi
Thm* as:A*, i:. nth_tl(i;as) A*
|
| hd |
Def hd(l) == ListInd(l;"?";h,t,v.h)
Thm* l:A*. (||l||  1 ) hd(l) A
|
| lelt |
Def i j < k == ij & j < k
|
| tl |
Def tl(l) == ListInd(l;nil;h,t,v.t)
Thm* l:A*. tl(l) A*
|
| le_int |
Def i z j ==   j < z i
Thm* i,j:. i z j 
|
| le |
Def AB == B < A
Thm* i,j:. ij Prop
|
| lt_int |
Def i < z j == if i < j true ; false fi
Thm* i,j:. i < z j
|
| bnot |
Def b == if b false else true fi
Thm* b:. b
|
| not |
Def A == A False
Thm* (A) Prop
|