Nuprl - Proof: w-withlnk wf

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-withlnk wf

the_w:World, l:IdLnk, mss:Msg List.

withlnk(l;mss)

(t:Id

the_w.M(l,t)) List

By:

All_Wld

Generated subgoals:

1 1. T : IdIdType
2. TA : IdIdType
3. M : IdLnkIdType
4. i:Id(x:IdT(i,x))
5. i:Idaction(w-action-dec(TA;M;i))
6. i:Id({m:Msg(M)| source(mlnk(m)) = i } List)
7. Top
8. l : IdLnk
9. Msg(M) List
10. ms : {x:Msg(M)| (ms.mlnk(ms) = l)(x) }
2of(ms) t:IdM(l,t)
5 steps

2 1. T : IdIdType
2. TA : IdIdType
3. M : IdLnkIdType
4. i:Id(x:IdT(i,x))
5. i:Idaction(w-action-dec(TA;M;i))
6. i:Id({m:Msg(M)| source(mlnk(m)) = i } List)
7. Top
8. l : IdLnk
9. Msg(M) List
10. x : Msg(M)
(ms.mlnk(ms) = l)(x)
1 step

About:

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

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

1	1. T : IdIdType 2. TA : IdIdType 3. M : IdLnkIdType 4. i:Id(x:IdT(i,x)) 5. i:Idaction(w-action-dec(TA;M;i)) 6. i:Id({m:Msg(M)\| source(mlnk(m)) = i } List) 7. Top 8. l : IdLnk 9. Msg(M) List 10. ms : {x:Msg(M)\| (ms.mlnk(ms) = l)(x) } 2of(ms) t:IdM(l,t)	5 steps
2	1. T : IdIdType 2. TA : IdIdType 3. M : IdLnkIdType 4. i:Id(x:IdT(i,x)) 5. i:Idaction(w-action-dec(TA;M;i)) 6. i:Id({m:Msg(M)\| source(mlnk(m)) = i } List) 7. Top 8. l : IdLnk 9. Msg(M) List 10. x : Msg(M) (ms.mlnk(ms) = l)(x)	1 step