Nuprl - Proof: concat map upto

(11steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: concat map upto

T:Type, f:(

(T List)), t,t':

t<t'

concat(map(f;upto(t))) @ (f(t))

concat(map(f;upto(t')))

By:	Auto THEN Subst ((concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;upto(t+1)))) 0

Generated subgoals:

1 1. T : Type
2. f : (T List)
3. t :
4. t' :
5. t<t'
(concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;upto(t+1)))
7 steps

2 1. T : Type
2. f : (T List)
3. t :
4. t' :
5. t<t'
concat(map(f;upto(t+1))) concat(map(f;upto(t')))
3 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(11steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

1	1. T : Type 2. f : (T List) 3. t : 4. t' : 5. t<t' (concat(map(f;upto(t))) @ (f(t))) ~ concat(map(f;upto(t+1)))	7 steps
2	1. T : Type 2. f : (T List) 3. t : 4. t' : 5. t<t' concat(map(f;upto(t+1))) concat(map(f;upto(t')))	3 steps