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

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

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

About:
listnatural_numberlambdafunctionuniverseequalandallexists

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