Nuprl - Proof: src-edge 1

(3steps total) PrintForm Definitions mb event system 7 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: src-edge 1

1. T : Id

2. to : {i:Id| T(i) }

(IdLnk List)
3. from : {i:Id| T(i) }

(IdLnk List)
4. u : {l:IdLnk|

i:|T|. (l

from(i)) }
5.

i:|T|.
5. (

to(i).destination(l) = i
5. & T(source(l))
5. & (l

from(source(l)))
5. & (lnk-inv(l)

from(i)))
5. & (

from(i).source(l) = i
5. & & T(destination(l))
5. & & (l

to(destination(l)))
5. & & (lnk-inv(l)

to(i)))

T(source(u))

By:	Analyze -2 THEN Unhide THEN MaAuto THEN ExRepD THEN InstHyp [i] -1 THEN Unfold `l_all` -1 THEN InstHyp [u] -1

Generated subgoal:

1 4. u : IdLnk
5. i : |T|
6. (u  from(i))
7. i:|T|.
7. (lto(i).destination(l) = i
7. & T(source(l))
7. & (l  from(source(l)))
7. & (lnk-inv(l)  from(i)))
7. & (lfrom(i).source(l) = i
7. & & T(destination(l))
7. & & (l  to(destination(l)))
7. & & (lnk-inv(l)  to(i)))
8. (lto(i).destination(l) = i
8. & T(source(l))
8. & (l  from(source(l)))
8. & (lnk-inv(l)  from(i)))
9. l:IdLnk.
9. (l  from(i))
9.
9. source(l) = i
9. & T(destination(l))
9. & (l  to(destination(l)))
9. & (lnk-inv(l)  to(i))
10. source(u) = i
11. T(destination(u))
12. (u  to(destination(u)))
13. (lnk-inv(u)  to(i))
  T(source(u))
1 step

About:

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

(3steps total) PrintForm Definitions mb event system 7 Sections EventSystems Doc