Nuprl - Proof: possible-world-monotonic 3

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: possible-world-monotonic 3

1. A : Dsys
2. B : Dsys
3. A

B
4. w : World
5.

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

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

i:Id, a:Action(i).

isnull(a)

(valtype(i;a)

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

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

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

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

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

By:	Auto THEN Using [`B',M(source(l)).da(rcv(l; tg))] (BackThru Thm* (A r B) (B r C) (A r C)) THEN Try BackThruSomeHyp THEN BackThru Thm* M1,M2:MsgA, k:Knd. M1 M2 (M2.da(k) r M1.da(k)) THEN AllHyps (h.Unfold `d-sub` h THEN BackThru h)

Generated subgoals:

None

About:

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