Nuprl - Proof: possible-world wf 1 2

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: possible-world wf 1 2

1. D : Dsys
2. w : World
3.

i,x:Id. vartype(i;x)

r M(i).ds(x)
4.

i:Id, a:Action(i).

isnull(a)

(valtype(i;a)

r M(i).da(kind(a)))
5.

l:IdLnk, tg:Id. (w.M(l,tg))

r M(source(l)).da(rcv(l; tg))
6.

i,x:Id. M(i).init(x,s(i;0).x)
7. i : Id
8. t :

9.

isnull(a(i;t))
10. l : IdLnk
11. withlnk(l;m(i;t)) = withlnk(l;m(i;t))
12. (t:Id

w.M(l,t)) List
13. (t:Id

w.M(l,t)) List
14. t:Id

w.M(l,t)
15. t1 : Id

(w.M(l,t1))

if source(l) = i

M(i).da(rcv(l; t1)) else Top fi

By:	Analyze 0 THEN DoSubsume THEN SplitOnConclITE

Generated subgoals:

1 16. w.M(l,t1)
17. source(l) = i
(w.M(l,t1)) r M(i).da(rcv(l; t1))
1 step

2 16. w.M(l,t1)
17. source(l) = i
(w.M(l,t1)) r Top
1 step

About:

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

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