Thm* as:T*. (as[0..||as||
]) = as whole_segment
Thm* as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j
]) @ (as[j..k
])) = (as[i..k
])
append_segment
Thm* x:
, as:T*. x < ||as||
firstn(x+1;as) = (firstn(x;as) @ [as[x]])
firstn_lem1
Thm* as:T*. firstn(||as||;as) = as firstn_lem0
Thm* L,La:T*.
Fin(T)
(
La':T*.
(
t:T. mem_f(T;t;La)
mem_f(T;t;L)
mem_f(T;t;La'))
& (
t:T. mem_f(T;t;La')
mem_f(T;t;La))
& (||La'||
1
mem_f(T;hd(La');L)))
shorten_list
Thm* L:T*, t:T. mem_f(T;t;L)
(
i:
||L||. L[i] = t) mem_select
Thm* L:T*, i:
||L||. mem_f(T;L[i];L) select_mem
Thm* L:T*. ||L||
1
mem_f(T;hd(L);L) hd_mem
Thm* L:T*. 0 < ||L||
L = hd(L).tl(L) hd_tl
Thm* L:T*. ||L||
0
L = nil zero_nil
In prior sections: list 1 finite sets