Nuprl - Proof: sends-rule 2 2

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sends-rule 2 2

1. i : Id
2. k : Knd
3. l : IdLnk
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : (tg:Id

State(ds)

ma-valtype(da; k)

(da(rcv(l; tg))?Void List)) List
7. source(l) = i
8. w : World
9. p : FairFifo
10. FairFifo
11.

i@0,x:Id.
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if eqof(IdDeq)(i@0,i)

11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if <ds
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,da
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,<[<k,l>],

x.f>
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(if ,

>
11. vartype(i@0;x)

r if deq-member(IdDeq;x;1of(1of(else fi)))

11. vartype(i@0;x)

r if 2of(1of(if eqof(IdDeq)(i@0,i)

11. vartype(i@0;x)

r if 2of(1of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
11. vartype(i@0;x)

r if 2of(1of(else fi))
11. vartype(i@0;x)

r if (x)
11. vartype(i@0;x)

r else Top fi
12.

i@0:Id, a:Action(i@0).
12.

isnull(a)
12.

12. (valtype(i@0;a)

r if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
12. (valtype(i@0;a)

r else fi.da(kind(a)))
13.

l@0:IdLnk, tg:Id.
13. (w.M(l@0,tg))

r if eqof(IdDeq)(source(l@0),i)

13. (w.M(l@0,tg))

r if <ds,da,,,,<[<k,l>],

x.f>,,,

>
13. (w.M(l@0,tg))

r else fi.da(rcv(l@0; tg))
14.

i@0,x:Id.
14. deq-member(IdDeq;x;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)

14. deq-member(IdDeq;x;1of(1of(2of(2of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
14. deq-member(IdDeq;x;1of(1of(2of(2of(else fi)))))
14.

14. s(i@0;0).x
14. =
14. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
14. 2of(1of(2of(2of(else fi))))
14. (x)
15.

i@0:Id, t:

.
15.

isnull(a(i@0;t))
15.

15. (islocal(kind(a(i@0;t)))
15. (

15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if eqof(IdDeq)
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if (i@0
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,i)

15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if <ds
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,da
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,<[<k,l>],

x.f>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,

>
15. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(else fi))))))
15. (

15. (2of(1of(2of(2of(2of(if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
15. (2of(1of(2of(2of(2of(else fi)))))
15. ((act(kind(a(i@0;t)))
15. (,

x.s(i@0;t).x
15. (,val(a(i@0;t))))
15. & (

x:Id.
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i@0;t))
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(2of(2of(2of(2of(
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if (i@0
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,i)

15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if <ds
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,da
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,<[<k,l>]
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,,

x.f>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(if ,

>
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x>;1of(1of(else fi)))))))
15. & (

15. & (s(i@0;t+1).x
15. & (=
15. & (2of(1of(2of(2of(2of(2of(if eqof(IdDeq)(i@0,i)

15. & (2of(1of(2of(2of(2of(2of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
15. & (2of(1of(2of(2of(2of(2of(else fi))))))
15. & ((<kind(a(i@0;t)),x>
15. & (,

x.s(i@0;t).x
15. & (,val(a(i@0;t))))
15. & (

l@0:IdLnk.
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;1of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;2of(
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if eqof(IdDeq)
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if (i@0
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,i)

15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if <ds
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,da
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[<k
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,<[,l>]
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,

x.
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,,f>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;if ,

>
15. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l@0>;else fi))))))))
15. & (

15. & (withlnk(l@0;m(i@0;t))
15. & (=
15. & (if source(l@0) = i@0

15. & (if concat(map(

tgf.map(

x.
15. & (if <1of(tgf),x>;2of(tgf)
15. & (if <1of(tgf),x>;((

x.s(i@0;t).x)
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(2of(2of(2of(2of(2of(
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if eqof(IdDeq)(i@0,i)

15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if <ds,da,,,,<[<k,l>],

x.f>,,,

>
15. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(else fi)))))))
15. & (if <1of(tgf),x>;,val(a(i@0;t))));(<kind(a(i@0;t)),l@0>)))
15. & (else nil fi)
15. & (

x:Id.
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if eqof(IdDeq)
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if (i@0
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,i)

15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if <ds
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,da
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,<[<k,l>],

x.f>
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(if ,

>
15. & (

(deq-member(IdDeq;x;1of(1of(2of(2of(2of(2of(2of(2of(else fi)))))))))
15. & (

(

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],

x.f>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,

>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(else fi))))))))
15. & (

(deq-member(KindDeq;kind(a(i@0;t));(x)))
15. & (

15. & (s(i@0;t).x = s(i@0;t+1).x)
15. & (

l@0:IdLnk, tg:Id.
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of(
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of(
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if eqof(IdDeq)
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if (i@0
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,i)

15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if <ds
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,da
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,<[<k,l>],

x.f>
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,

>
15. & (

(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;else fi))))))))))
15. & (

(

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(2of(
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i)

15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <ds
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,da
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[<k,l>],

x.f>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,

>
15. & (

(deq-member(KindDeq;kind(a(i@0;t));2of(1of(else fi)))))))))
15. & (

(deq-member(KindDeq;kind(a(i@0;t));(<l@0,tg>)))
15. & (

15. & (w-tagged(tg; onlnk(l@0;m(i@0;t))) = nil)
16.

i@0,a:Id, t:

.
16.

t':

.
16. t

t'
16. &

isnull(a(i@0;t')) & kind(a(i@0;t')) = locl(a)
16. &

a declared in if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
16. &

a declared in else fi
16. &

unsolvable if eqof(IdDeq)(i@0,i)

<ds,da,,,,<[<k,l>],

x.f>,,,

>
16. &

unsolvable else fi.pre(a,

x.s(i@0;t').x)
17. (

x:Id. vartype(i;x)

r ds(x)?Top)
17. & (

e:E. loc(e) = i

(valtype(e)

r ma-valtype(da; kind(e))))
17. & (

e:E. isrcv(e)

lnk(e) = l

(valtype(e)

r ma-valtype(da; kind(e))))
17. & ({m:Msg| source(mlnk(m)) = i }

r Msg((

l,tg. da(rcv(l; tg))?Top)))

e:E.

loc(e) = i

kind(e) = k

Knd

sends(l;e)

tagged-messages(l;

z.(z when e);val(e);f)

Msg((

l,tg. da(rcv(l; tg))?Top)) List

By:

let maops
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
AssertBY ((eqof(IdDeq)(i,i)) ~ true

)
(BackThru Thm*

d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true

)
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)])

Generated subgoal:

1 11. l@0:IdLnk, tg:Id.
11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
11. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
12. (eqof(IdDeq)(i,i)) ~ true
13. (x:Id. vartype(i;x) r ds(x)?Top)
13. & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
13. & (e:E. isrcv(e)  lnk(e) = l  (valtype(e) r ma-valtype(da; kind(e))))
13. & ({m:Msg| source(mlnk(m)) = i } r Msg((l,tg. da(rcv(l; tg))?Top)))
14. a:Id, t:.
14. t':.
14. tt'
14. & isnull(a(i;t')) & kind(a(i;t')) = locl(a)
14. &  locl(a)  dom(da)
14. &  P != (a) ==> v:da(locl(a))?Top. P((x.s(i;t').x),v)
15. t:.
15. isnull(a(i;t))
15.
15. (islocal(kind(a(i;t)))
15. (
15. (deq-member(IdDeq;act(kind(a(i;t)));1of())
15. (
15. (2of()(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
15. & (x:Id.
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
15. & (
15. & (s(i;t+1).x
15. & (=
15. & (2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t)))
15. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
15. & (l@0:IdLnk.
15. & ((eqof(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq))(<k,l>,<kind(a(i;t)),l@0>)
15. & (( false)
15. & (
15. & (withlnk(l@0;m(i;t))
15. & (=
15. & (if source(l@0) = i
15. & (if concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)
15. & (if concat(map(tgf.map(x.<1of(tgf),x>;((x.s(i;t).x)
15. & (if concat(map(tgf.map(x.<1of(tgf),x>;,val(a(i;t))));f))
15. & (else nil fi
15. & ( (tg:Idif source(l@0) = i da(rcv(l@0; tg))?Top else Top fi) List)
15. & (x:Id.
15. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x)))
15. & (
15. & (s(i;t).x
15. & (=
15. & (s(i;t+1).x
15. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi)
15. & (l@0:IdLnk, tg:Id.
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0,tg>;1of())
15. & ((
15. & ((deq-member(KindDeq;kind(a(i;t));2of()(<l@0,tg>)))
15. & (
15. & (w-tagged(tg; onlnk(l@0;m(i;t))) = nil  Msg List)
16. x:Id.
16. deq-member(IdDeq;x;1of())
16.
16. s(i;0).x
16. =
16. 2of()(x)
16.  if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Void fi
17. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
18. x:Id.
18. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
  e:E.
  loc(e) = i  Id

  kind(e) = k  Knd

  sends(l;e)
  =
  tagged-messages(l;z.(z when e);val(e);f)
   Msg((l,tg. da(rcv(l; tg))?Top)) List
109 steps

About:

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

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