TProp
@i (with ds: ds
@i action a:T
@i precondition a(v) is
@i P s v) realizes2 es.(
x:Id. vartype(i;x) 
r ds(x)?Top)
& (e:E. loc(e) = i 
Id 
kind(e) = locl(a) Knd (valtype(e) r T))
& (e:E.
& (loc(e) = i Id
& (
& ((kind(e) = locl(a) Knd P((
z.(z when e)),val(e)))
& (& (
e':E.
& (& ((e <loc e') 
e = e' E
& (& (& kind(e') = locl(a) Knd (v:T. 
P((z.(z after e')),v))))| By: |
let  [`ma-ds`
let ;`ma-da`
let ;`ma-din`
let ;`ma-dout`
let ;`ma-pre`
let ;`ma-npre`
let ;`ma-ef`
let ;`ma-init`
let ;`ma-decla`] in
RepeatFor 3 (Analyze 0 THENA Complete Auto) THEN AssertBY ((eqof(IdDeq)(i,i)) ~ true  )
(BackThru Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true)
THEN ES_Reduce THEN PW_Reduce -2 THEN AllHyps ( h.
(InstHyp [i] h THENA Complete Auto THEN Subst ((eqof(IdDeq)(i,i)) ~ true ) -1
(THENL ([Trivial;Thin h THEN Reduce -1 THEN Repeat (Unfolds maops -1 THEN Reduce -1)]) |
| 1 |
4. ds : x:Id fp-> Type{i} 5. P : State(ds) TProp{i}
6. w : World 7. p : FairFifo 8. FairFifo 9. l:IdLnk, tg:Id.
9. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i)
9. (w.M(l,tg)) r if <ds,<[locl(a)],x.T>,,<[a],x.P>,,,,, >
9. (w.M(l,tg)) r else fi.da(rcv(l; tg))
10. (eqof(IdDeq)(i,i)) ~ true
11. a@0:Id, t: .
11. t':.
11. t  t'
11. & isnull(a(i;t')) & kind(a(i;t')) = locl(a@0)
11. & locl(a@0) dom(<[locl(a)],x.T>)
11. & P@0 != <[a],x.P>(a@0) ==> v:<[locl(a)],x.T>(locl(a@0))?Top.
11. & P@0((x.s(i;t').x),v)
12. t:.
12. isnull(a(i;t))
12.
12. (islocal(kind(a(i;t))) 12. (
12. ((eqof(IdDeq)(a,act(kind(a(i;t)))) false)
12. (
12. (P(( x.s(i;t).x),val(a(i;t))))
12. & ( x:Id.
12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of()) 12. & (
12. & (s(i;t+1).x 12. & (= 12. & (2of()(<kind(a(i;t)),x>, x.s(i;t).x,val(a(i;t)))
12. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
12. & ( l:IdLnk.
12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;1of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;)) 12. & (
12. & (withlnk(l;m(i;t)) 12. & (= 12. & (if source(l) = i
12. & (if concat(map( tgf.map(x.<1of(tgf)
12. & (if concat(map( tgf.map(x.,x>;2of(tgf)
12. & (if concat(map( tgf.map(x.,x>;((x.s(i;t).x)
12. & (if concat(map( tgf.map(x.,x>;,val(a(i;t))));2of()(<kind(a(i;t)),l>)))
12. & (else nil fi 12. & ( (tg:Id
12. & ( ( if source(l) = i <[locl(a)],x.T>(rcv(l; tg))?Top else Top fi) List)
12. & ( x:Id.
12. & ( (deq-member(IdDeq;x;1of()) deq-member(KindDeq;kind(a(i;t));2of()(x)))
12. & (
12. & (s(i;t).x 12. & (= 12. & (s(i;t+1).x 12. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
12. & ( l:IdLnk, tg:Id.
12. & ( (deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l,tg>;1of())
12. & ( (
12. & ( (deq-member(KindDeq;kind(a(i;t));2of()(<l,tg>)))
12. & (
12. & (w-tagged(tg; onlnk(l;m(i;t))) = nil Msg List)
13. x:Id.
13. deq-member(IdDeq;x;1of()) 13.
13. s(i;0).x 13. = 13. 2of()(x) 13. if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Void fi
14. a@0:Action(i).
14. isnull(a@0) (valtype(i;a@0) r <[locl(a)],x.T>(kind(a@0))?Top)
15. x:Id.
15. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
(x:Id. vartype(i;x) r ds(x)?Top)
& (e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T))
& (e:E.
& (loc(e) = i Id
& (
& ((kind(e) = locl(a) P((z.(z when e)),val(e)))
& (& (e':E.
& (& ((e <loc e') e = e'
& (& (& kind(e') = locl(a) (v:T. P((z.(z after e')),v)))) | 161 steps |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |