Properties of the Tatami Protocol
We want to prove
ok?(database(init)) = true
.
Show
ok?(database(init)) = true
by reduction.
Properties of the Tatami Protocol
We want to prove
S:State
F:Elt
((ok?(database(S)) = true) and (ok?(parents(F),database(S)) = true) implies
(ok?(database(insert(F,S))) = true and
ok?(database(submit(F,S))) = true ))
.
Quantifier elimination introduces new
constants f :Elt and s :State
.
Implication elimination assumes
(ok?(database(s)) = true) and (ok?(parents(f),database(s)) = true)
.
Change hypothesis
(ok?(database(s)) = true) and (ok?(parents(f),database(s)) = true)
to rewritng rule.
Conjunction elimination introduces subgoals as follows:
ok?(database(insert(f,s))) = true
.
Show
ok?(database(insert(f,s))) = true
by reduction.
ok?(database(submit(f,s))) = true
.
Show
ok?(database(submit(f,s))) = true
by reduction.
Properties of the Tatami Protocol
We want to prove
S:State
(ok?(database(S)) = true implies
(F:Elt (ok?(database(receive(F,S))) = true) and
F:Elt (U:User (ok?(database(ack(U,F,S))) = true)) ))
.
Quantifier elimination introduces new
constant s :State
.
Implication elimination assumes
(ok?(database(s)) = true)
.
Change hypothesis
(ok?(database(s)) = true)
to rewritng rule.
Conjunction elimination introduces subgoals as follows:
forall F:Elt (ok?(database(receive(F,s))) = true)
.
Quantifier elimination introduces new
constant f :Elt
.
Show
ok?(database(receive(f,s))) = true
by reduction.
forall F:Elt (forall U:User (ok?(database(ack(U,F,s))) = true))
.
Quantifier elimination introduces new
constants f :Elt and u :User
.
Show
(ok?(database(ack(u,f,s))) = true)
by reduction.
This page was generated
by Kumo on
Fri Jun 12 12:38:48 PDT 1998
from code written by Grigore Rosu,