append |
Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive)
Thm* T:Type, as,bs:T*. (as @ bs) T*
|
biject |
Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)
Thm* A,B:Type, f:(A B). Bij(A; B; f) Prop
|
ge |
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
|
lelt |
Def i j < k == i j & j < k
|
le |
Def A B == B < A
Thm* i,j: . i j Prop
|
length |
Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
Thm* A:Type, l:A*. ||l||
Thm* ||nil|| 
|
nat_plus |
Def  == {i: | 0 < i }
Thm*  Type
|
segment |
Def as[m..n ] == firstn(n-m;nth_tl(m;as))
Thm* T:Type, as:T*, m,n: . (as[m..n ]) T*
|
surject |
Def Surj(A; B; f) == b:B. a:A. f(a) = b
Thm* A,B:Type, f:(A B). Surj(A; B; f) Prop
|
inject |
Def Inj(A; B; f) == a1,a2:A. f(a1) = f(a2) B  a1 = a2
Thm* A,B:Type, f:(A B). Inj(A; B; f) Prop
|
not |
Def A == A  False
Thm* A:Prop. ( A) Prop
|
nth_tl |
Def nth_tl(n;as) == if n 0 as else nth_tl(n-1;tl(as)) fi (recursive)
Thm* A:Type, as:A*, i: . nth_tl(i;as) A*
|
firstn |
Def firstn(n;as)
== Case of as; nil nil ; a.as' if 0 < n a.firstn(n-1;as') else nil fi
(recursive)
Thm* A:Type, as:A*, n: . firstn(n;as) A*
|
tl |
Def tl(l) == Case of l; nil nil ; h.t t
Thm* A:Type, l:A*. tl(l) A*
|
le_int |
Def i j ==  j < i
Thm* i,j: . i j 
|
lt_int |
Def i < j == if i < j true ; false fi
Thm* i,j: . i < j 
|
bnot |
Def  b == if b false else true fi
Thm* b: .  b 
|