Properties of the Tatami Protocol
Idemopotency of insert.

We want to prove

F:Elt (S:State (insert(F,insert(F,S)) = insert(F,S))) .
We use attribute coinduction to prove this is a behavorial property of the input specification.
• First, we prove the attribute coherence of the input specification.
• Introduce the lemma coherence(PROTOCOL) .
• This goal is true because coherence(PROTOCOL) is in the hypothesis.
• Then we prove F:Elt S:State    (database(insert(F,insert(F,S))) = database(insert(F,S))     and
temp-mem(insert(F,insert(F,S))) = temp-mem(insert(F,S))     and
U:User (not-ack(U,insert(F,insert(F,S))) = not-ack(U,insert(F,S))) )
• Quantifier elimination introduces new constants f :Elt and s :State .
• Conjunction elimination introduces subgoals as follows:
1. (database(insert(f,insert(f,s))) = database(insert(f,s))) .
• Show (database(insert(f,insert(f,s))) = database(insert(f,s))) by reduction.
2. (temp-mem(insert(f,insert(f,s))) = temp-mem(insert(f,s))) .
• Show (temp-mem(insert(f,insert(f,s))) = temp-mem(insert(f,s))) by reduction.
3. forall U:User (not-ack(U,insert(f,insert(f,s))) = not-ack(U,insert(f,s))) .
Properties of the Tatami Protocol

Idemopotency of submit.

We want to prove

F:Elt (S:State (submit(F,submit(F,S)) = submit(F,S))) .
We use attribute coinduction to prove this is a behavorial property of the input specification.
• First, we prove the attribute coherence of the input specification.
• Introduce the lemma coherence(PROTOCOL) .
• This goal is true because coherence(PROTOCOL) is in the hypothesis.
• Then we prove F:Elt S:State    (database(submit(F,submit(F,S))) = database(submit(F,S))     and
temp-mem(submit(F,submit(F,S))) = temp-mem(submit(F,S))     and
U:User (not-ack(U,submit(F,submit(F,S))) = not-ack(U,submit(F,S))) )
• Quantifier elimination introduces new constants f :Elt and s :State .
• Conjunction elimination introduces subgoals as follows:
1. (database(submit(f,submit(f,s))) = database(submit(f,s))) .
• Show (database(submit(f,submit(f,s))) = database(submit(f,s))) by reduction.
2. (temp-mem(submit(f,submit(f,s))) = temp-mem(submit(f,s))) .
• Show (temp-mem(submit(f,submit(f,s))) = temp-mem(submit(f,s))) by reduction.
3. forall U:User (not-ack(U,submit(f,submit(f,s))) = not-ack(U,submit(f,s))) .
Properties of the Tatami Protocol

We want to prove

We use attribute coinduction to prove this is a behavorial property of the input specification.
• First, we prove the attribute coherence of the input specification.
• Introduce the lemma coherence(PROTOCOL) .
• This goal is true because coherence(PROTOCOL) is in the hypothesis.
• Quantifier elimination introduces new constants f :Elt and s :State .
• Conjunction elimination introduces subgoals as follows:
Properties of the Tatami Protocol

Idemopotency of ack.

We want to prove

U':User F:Elt S:State ack(U',F,ack(U',F,S)) = ack(U',F,S) .
We use attribute coinduction to prove this is a behavorial property of the input specification.
• First, we prove the attribute coherence of the input specification.
• Introduce the lemma coherence(PROTOCOL) .
• This goal is true because coherence(PROTOCOL) is in the hypothesis.
• Then we prove U':User F:Elt S:State    (database(ack(U',F,ack(U',F,S))) = database(ack(U',F,S))     and
temp-mem(ack(U',F,ack(U',F,S))) = temp-mem(ack(U',F,S))     and
U:User (not-ack(U,ack(U',F,ack(U',F,S))) = not-ack(U,ack(U',F,S))) )
• Quantifier elimination introduces new constants f :Elt and u' :User and s :State .
• Conjunction elimination introduces subgoals as follows:
1.    database(ack(u',f,ack(u',f,s))) = database(ack(u',f,s))     and
temp-mem(ack(u',f,ack(u',f,s))) = temp-mem(ack(u',f,s))
• Conjunction elimination introduces subgoals as follows:
1. (database(ack(u',f,ack(u',f,s))) = database(ack(u',f,s)))
• Show (database(ack(u',f,ack(u',f,s))) = database(ack(u',f,s))) by reduction.
2. (temp-mem(ack(u',f,ack(u',f,s))) = temp-mem(ack(u',f,s)))
• Show (temp-mem(ack(u',f,ack(u',f,s))) = temp-mem(ack(u',f,s))) by reduction.
2. U:User (not-ack(U,ack(u',f,ack(u',f,s))) = not-ack(U,ack(u',f,s)))
• Quantifier elimination introduces a new constant u of sort User .
• Case analysis uses the lemma U:User ((U = u) or (U =\= u)) on u1 to get the following subgoals
1. (u1 = u) implies (not-ack(u,ack(u',f,ack(u',f,s))) = not-ack(u,ack(u',f,s)))
2. (u1 =\= u) implies (not-ack(u,ack(u',f,ack(u',f,s))) = not-ack(u,ack(u',f,s)))