Selected Objects

COM	list_3_history	Mem_f was copied from list_2. Whole_segment and Append_segment were taken from list_2 and reproved without groups_1 library.
COM	list_3_author	Alexey Nogin
THM	zero_nil	L:T*. ||L||0 L = nil
THM	hd_tl	L:T*. 0 < ||L|| L = hd(L).tl(L)
def	mem_f	(rec) mem_f(T;a;bs) == Case of bs; nil False ; b.bs' b = a T mem_f(T;a;bs')
THM	list_in_mem_f_list	as:T*. as {x:T| mem_f(T;x;as) }*
THM	mem_f_dec	s:S, l:S*. Fin(S) Dec(mem_f(S;s;l))
THM	hd_mem	L:T*. ||L||1 mem_f(T;hd(L);L)
THM	select_mem	L:T*, i:||L||. mem_f(T;L[i];L)
THM	mem_append	L1,L2:T*, t:T. mem_f(T;t;L1 @ L2) mem_f(T;t;L1) mem_f(T;t;L2)
THM	mem_select	L:T*, t:T. mem_f(T;t;L) (i:||L||. L[i] = t)
THM	shorten_list	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)))
def	add_action	(rec) (+f)(l) == Case of l; nil nil ; h.l' [h; f(h)/ (+f)(l')]
THM	add_action_mem	l:St*, f:(StSt), s:St. mem_f(St;s;(+f)(l)) mem_f(St;s;l) (s':St. mem_f(St;s';l) & f(s') = s)
def	lremove	(rec) l \ a == Case of l; nil nil ; h.l' if eq(a,h) l' \ a else h.(l' \ a) fi
THM	lremove_mem	l:St*, s:St, eq:(StSt), sx:St. mem_f(St;sx;l \ s) if eq(s,sx) False else mem_f(St;sx;l) fi
def	lshort	(rec) LShort(l) == Case of l; nil nil ; h.l' h.(LShort(l') \ h)
THM	lshort_mem	l:St*, eq:(StSt). (x,y:St. eq(x,y) x = y) (s:St. mem_f(St;s;l) mem_f(St;s;LShort(l)))
THM	firstn_lem0	as:T*. firstn(||as||;as) = as
THM	firstn_lem1	x:, as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]])
THM	nth_tl_lem0	y:, as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as)
THM	nth_tl_lem1	x,y:, as:T*. nth_tl(x;nth_tl(y;as)) = nth_tl(x+y;as)
THM	append_segment	as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}. ((as[i..j]) @ (as[j..k])) = (as[i..k])
THM	whole_segment	as:T*. (as[0..||as||]) = as