Origin
Sections
ClassicalProps(jlc)
Doc
formula_list
Nuprl Section: formula_list
Selected Objects
def
list_rank
(L) == reduce(
x,y.
(x)+y;0;L)
THM
list_rank_append_homomorphism
M,N:Formula List.
(M @ N) =
(M)+
(N)
(L) == reduce(
x,y. (x)+y;0;L)
M,N:Formula List. (M @ N) = (M)+(N) 
(L) == reduce(x,y. (x)+y;0;L)M,N:Formula List. (M @ N) = (M)+(N)