Nuprl - Proof: adjl-edge-accum-properties

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

A:AdjList, T:Type, s:T, x:Vertices(adjl-graph(A)), f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. (y:Vertices(adjl-graph(A)). x-adjl-graph(A)- > y (y L)) & adjl-edge-accum(A;s',x'.f(s',x');s;x) = list_accum(s',x'.f(s',x');s;L)

By: Unfolds [`adjl-graph`;`adjl-edge-accum`] 0 THEN Reduce 0 THEN InstConcl [A.out(x)] THEN All (Unfold `edge`) THEN All Reduce THEN ExRepD THEN Try ((Analyze -1) THEN (Reduce 0))

Generated subgoals:

1 1. A: AdjList
2. T: Type
3. s: T
4. x: A.size
5. f: TA.sizeT
6. y: A.size
7. e: x:A.size||A.out(x)||
8. < 1of(e),(A.out(1of(e)))[2of(e)] > = < x,y >
(y A.out(x)) 1 step

2 1. A: AdjList
2. T: Type
3. s: T
4. x: A.size
5. f: TA.sizeT
6. y: A.size
7. i:
8. i < ||A.out(x)|| & y = (A.out(x))[i]
e:(x:A.size||A.out(x)||). < 1of(e),(A.out(1of(e)))[2of(e)] > = < x,y > 2 steps

About:

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

1	1. `A:` `AdjList` 2. `T:` `Type` 3. `s:` `T` 4. `x:` `A.size` 5. `f:` `TA.sizeT` 6. `y:` `A.size` 7. `e:` `x:A.size\|\|A.out(x)\|\|` 8. `< 1of(e),(A.out(1of(e)))[2of(e)] > = < x,y >` `(y A.out(x))`	1 step

2	1. `A:` `AdjList` 2. `T:` `Type` 3. `s:` `T` 4. `x:` `A.size` 5. `f:` `TA.sizeT` 6. `y:` `A.size` 7. `i:` 8. `i < \|\|A.out(x)\|\| & y = (A.out(x))[i]` `e:(x:A.size\|\|A.out(x)\|\|). < 1of(e),(A.out(1of(e)))[2of(e)] > = < x,y >`	2 steps