nd_computation |
Def NComp(Alph;St) == {C:(St Thm* NComp(Alph;St) |
select |
Def l[i] == hd(nth_tl(i;l))
Thm* |
pi2 |
Def 2of(t) == t.2
Thm* |
list_p |
Def T List Thm* (T List |
length |
Def (rec) ||as|| == Case of as : null
Thm*
Thm* ||nil|| |
gt |
Def i > j == j < i
Thm* |
int_seg |
Def {i..j Thm* |
nth_tl |
Def (rec) nth_tl(n;as) == if n
Thm* |
hd |
Def hd(l) == ListInd(l;"?";h,t,v.h)
Thm* |
lelt |
Def i |
tl |
Def tl(l) == ListInd(l;nil;h,t,v.t)
Thm* |
le_int |
Def i Thm* |
le |
Def A Thm* |
lt_int |
Def i < z j == if i < j Thm* |
bnot |
Def Thm* |
not |
Def Thm* ( |