Nuprl - Proof: adjl-edge-accum-properties 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 >

By: Analyze -1 THEN InstConcl [ < x,i > ] THEN Reduce 0

Generated subgoal:

1 8. i < ||A.out(x)||
9. y = (A.out(x))[i]
< x,(A.out(x))[i] > = < x,y > 1 step

About: