D:Dsys, w:World. PossibleWorld(D;w)  Prop{i'}

By:

let T0  Complete (Auto THEN DoSubsume THEN BackThruSomeHyp) , let T1 let  DoSubsume THEN Subst (locl(act(kind(a(i;t)))) ~ kind(a(i;t))) 0 let  THENL let  [MoveToConcl -1 THEN GenConclAtAddr [1;1;1] THEN KindCase -2 let  ;BackThruSomeHyp] , let T2 let  Try (Unfold `ma-v` 0 THEN Unfold `ma-valtype` 0 THEN Fold `ma-da` 0) let  THEN let  DoSubsume let  THEN let  BackThruSomeHyp , let T3  Unfold `ma-st` 0 THEN Unfold `ma-state` 0 THEN Fold `ma-ds` 0 THEN T0 , let T4  Unfold `w-Msg` 0 , let T  Complete (Auto THEN (T0 ORELSE T1 ORELSE T2 ORELSE T3 ORELSE T4)) in UnivCD THEN Unfold `possible-world` 0 THEN Repeat (Repeat (Analyze THENL [T;Id]) THEN Repeat (Analyze THENL [Id;T])) THEN Analyze THEN Try T

1

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   withlnk(l;m(i;t))    (tg:Idif source(l) = i M(i).da(rcv(l; tg)) else Top fi) List

5 steps

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