int_seg	Def {i..j} == {k:| i k < j } Thm* m,n:. {m..n} Type
min_ar	Def MinAr(f;i;n) == if (f(n-i))=(f(n)) i else MinAr(f;i-1;n) fi (recursive) Thm* f:(), n:, i:(n+1). MinAr(f;i;n) (i+1)
nat	Def == {i:| 0i } Thm* Type
lelt	Def i j < k == ij & j < k
eq_bool	Def p=q == (pq) (pq) Thm* p,q:. p=q
le	Def AB == B < A Thm* i,j:. ij Prop
bnot	Def b == if b false else true fi Thm* b:. b
band	Def pq == if p q else false fi Thm* p,q:. (pq)
bor	Def p q == if p true else q fi Thm* p,q:. (p q)
not	Def A == A False Thm* A:Prop. (A) Prop

About: