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:
    1. ok?(database(insert(f,s))) = true .
      • Show ok?(database(insert(f,s))) = true by reduction.
    2. 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:
    1. forall F:Elt (ok?(database(receive(F,s))) = true) .
    2. forall F:Elt (forall U:User (ok?(database(ack(U,F,s))) = true)) .


    This page was generated
    by Kumo on Fri Jun 12 12:38:48 PDT 1998 from code written by Grigore Rosu,