By: |
|
1 |
5. da : a:Knd fp-> Type{i} 6. f : State(ds) ![]() ![]() ![]() ![]() 7. w : World 8. p : FairFifo 9. FairFifo 10. ![]() 10. vartype(i@0;x@0) ![]() ![]() ![]() 10. vartype(i@0;x@0) ![]() 11. ![]() 11. ![]() 11. ![]() ![]() 11. (valtype(i@0;a) ![]() ![]() ![]() 11. (valtype(i@0;a) ![]() 12. ![]() 12. (w.M(l,tg)) ![]() ![]() ![]() 12. (w.M(l,tg)) ![]() 13. ![]() 13. x0 != 1of(2of(2of(if eqof(IdDeq)(i@0,i) ![]() ![]() 13. x0 != 1of(2of(2of(else fi)))(x@0) ==> s(i@0;0).x@0 13. x0 != 1of(2of(2of(else fi)))(x@0) ==> = 13. x0 != 1of(2of(2of(else fi)))(x@0) ==> x0 13. x0 != 1of(2of(2of(else fi)))(x@0) ==> ![]() ![]() 13. x0 != 1of(2of(2of(else fi)))(x@0) ==> ![]() ![]() 13. x0 != 1of(2of(2of(else fi)))(x@0) ==> ![]() 14. ![]() ![]() 14. ![]() 14. ![]() ![]() 14. (islocal(kind(a(i@0;t))) 14. ( ![]() ![]() 14. (P != 1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) ![]() ![]() 14. (P != 1of(2of(2of(2of(else fi))))(act(kind(a(i@0;t)))) ==> P 14. (P != 1of(2of(2of(2of(else fi))))(act(kind(a(i@0;t)))) ==> (( ![]() 14. (P != 1of(2of(2of(2of(else fi))))(act(kind(a(i@0;t)))) ==> ,val(a(i@0;t)))) 14. & ( ![]() 14. & (E != 1of( 14. & (E != 2of(2of(2of(2of( 14. & (E != if eqof(IdDeq)(i@0,i) ![]() ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> s(i@0;t+1).x@0 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> = 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> E 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> (( ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ,val(a(i@0;t))) 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() ![]() 14. & (E != else fi)))))(<kind(a(i@0;t)),x@0>) ==> ![]() 14. & ( ![]() 14. & (if eqof(IdDeq)(i@0,i) ![]() ![]() 14. & (else fi.send(kind(a(i@0;t));l; ![]() 14. & (s(i@0;t).x;val(a(i@0;t));withlnk(l;m(i@0;t));i@0)) 14. & ( ![]() 14. & ( ![]() 14. & ( ![]() ![]() ![]() 14. & ( ![]() 14. & ( ![]() ![]() 14. & (s(i@0;t).x@0 14. & (= 14. & (s(i@0;t+1).x@0 14. & ( ![]() ![]() ![]() 14. & ( ![]() 14. & ( ![]() 14. & ( ![]() 14. & ( ![]() ![]() ![]() 14. & ( ![]() 14. & ( ![]() ![]() 14. & (w-tagged(tg; onlnk(l;m(i@0;t))) = nil ![]() 15. ![]() ![]() 15. ![]() ![]() 15. t ![]() 15. & ![]() 15. & ![]() ![]() ![]() ![]() 15. & ![]() ![]() ![]() 15. & ![]() ![]() 16. ![]() ![]() 17. ![]() ![]() ![]() ![]() ![]() 18. e : E 19. loc(e) = i ![]() 20. kind(e) = k ![]() ![]() ![]() ![]() ![]() | 22 steps |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() |