(4steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: adjl-vertex-accum-properties
A:AdjList, T:Type, s:T, f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. no_repeats(Vertices(adjl-graph(A));L) & (y:Vertices(adjl-graph(A)). (y L)) & adjl-vertex-accum(A;s',x'.f(s',x');s) = list_accum(s',x'.f(s',x');s;L)
By:
Unfolds [`adjl-graph`;`adjl-vertex-accum`] 0
THEN
Reduce 0
THEN
InstConcl [upto(0;A.size)]
Generated subgoals:

11. A: AdjList
2. T: Type
3. s: T
4. f: TA.sizeT
no_repeats(A.size;upto(0;A.size))		1 step
 
21. A: AdjList
2. T: Type
3. s: T
4. f: TA.sizeT
5. y: A.size
(y upto(0;A.size))		1 step
 
31. A: AdjList
2. T: Type
3. s: T
4. f: TA.sizeT
primrec(A.size;s;x',s'. f(s',x')) = list_accum(s',x'.f(s',x');s;upto(0;A.size))		1 step

About:
listnatural_numberlambdafunctionuniverseequalandallexists

(4steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc