Properties of the Tatami Protocol

We want to prove

coherence(PROTOCOL) .
Attribute coherence requires us to prove the following subgoals:
• S2,S1:State E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
(database(submit(E,S1)) = database(submit(E,S2))     and
temp-mem(submit(E,S1)) = temp-mem(submit(E,S2))     and
U:User (not-ack(U,submit(E,S1)) = not-ack(U,submit(E,S2))) ))
.
• Quantifier elimination introduces new constants e :Elt and s2 s1 :State .
• Implication elimination assumes    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
.
• Change hypothesis    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
to rewritng rule.
• Conjunction elimination introduces subgoals as follows:
1. database(submit(e,s1)) = database(submit(e,s2)) .
• Show database(submit(e,s1)) = database(submit(e,s2)) by reduction.
2. temp-mem(submit(e,s1)) = temp-mem(submit(e,s2)) .
• Show temp-mem(submit(e,s1)) = temp-mem(submit(e,s2)) by reduction.
3. forall U:User (not-ack(U,submit(e,s1)) = not-ack(U,submit(e,s2))) .
• S2,S1:State E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
(database(insert(E,S1)) = database(insert(E,S2))     and
temp-mem(insert(E,S1)) = temp-mem(insert(E,S2))     and
U:User (not-ack(U,insert(E,S1)) = not-ack(U,insert(E,S2))) ))
.
• Quantifier elimination introduces new constants e :Elt and s2 s1 :State .
• Implication elimination assumes    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
.
• Change hypothesis    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
to rewritng rule.
• Conjunction elimination introduces subgoals as follows:
1. database(insert(e,s1)) = database(insert(e,s2)) .
• Show database(insert(e,s1)) = database(insert(e,s2)) by reduction.
2. temp-mem(insert(e,s1)) = temp-mem(insert(e,s2)) .
• Show temp-mem(insert(e,s1)) = temp-mem(insert(e,s2)) by reduction.
3. forall U:User (not-ack(U,insert(e,s1)) = not-ack(U,insert(e,s2))) .
• S2,S1:State E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
.
• Quantifier elimination introduces new constants e :Elt and s2 s1 :State .
• Implication elimination assumes    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
.
• Change hypothesis    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
to rewritng rule.
• Conjunction elimination introduces subgoals as follows:
• S2,S1:State U':User E:Elt (((database(S1) = database(S2)) and (temp-mem(S1) = temp-mem(S2))) and (U:User (not-ack(U,S1) = not-ack(U,S2)))    implies
(database(ack(U',E,S1)) = database(ack(U',E,S2))     and
temp-mem(ack(U',E,S1)) = temp-mem(ack(U',E,S2))     and
U:User (not-ack(U,ack(U',E,S1)) = not-ack(U,ack(U',E,S2))) ))
.
• Quantifier elimination introduces new constants e :Elt and u' :User and s2 s1 :State .
• Implication elimination assumes    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
.
• Change hypothesis    database(s1) = database(s2)     and
temp-mem(s1) = temp-mem(s2)     and
U:User (not-ack(U,s1) = not-ack(U,s2))
to rewritng rule.
• Conjunction elimination introduces subgoals as follows:
1.    database(ack(u',e,s1)) = database(ack(u',e,s2))     and
temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2))
• Conjunction elimination introduces subgoals as follows:
1. database(ack(u',e,s1)) = database(ack(u',e,s2))
• Show database(ack(u',e,s1)) = database(ack(u',e,s2)) by reduction.
2. temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2))
• Show temp-mem(ack(u',e,s1)) = temp-mem(ack(u',e,s2)) by reduction.
2. U:User (not-ack(U,ack(u',e,s1)) = not-ack(U,ack(u',e,s2)))