Properties of the Tatami Protocol
Commutativity of insert.

We want to prove

F1,F2:Elt S:State insert(F1,insert(F2,S)) = insert(F2, insert(F1,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 F1,F2:Elt S:State    (database(insert(F1,insert(F2,S))) = database(insert(F2, insert(F1,S)))     and
temp-mem(insert(F1,insert(F2,S))) = temp-mem(insert(F2, insert(F1,S)))     and
U:User (not-ack(U,insert(F1,insert(F2,S))) = not-ack(U,insert(F2, insert(F1,S)))) )
• Quantifier elimination introduces new constants f1 f2 :Elt and s :State .
• Conjunction elimination introduces subgoals as follows:
1. (database(insert(f1,insert(f2,s))) = database(insert(f2, insert(f1,s)))) .
• Show (database(insert(f1,insert(f2,s))) = database(insert(f2, insert(f1,s)))) by reduction.
2. (temp-mem(insert(f1,insert(f2,s))) = temp-mem(insert(f2, insert(f1,s)))) .
• Show (temp-mem(insert(f1,insert(f2,s))) = temp-mem(insert(f2, insert(f1,s)))) by reduction.
3. forall U:User (not-ack(U,insert(f1,insert(f2,s))) = not-ack(U,insert(f2, insert(f1,s)))) .
Properties of the Tatami Protocol

Commutativity of submit.

We want to prove

F1,F2:Elt S:State submit(F1,submit(F2,S)) = submit(F2, submit(F1,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 F1,F2:Elt S:State    (database(submit(F1,submit(F2,S))) = database(submit(F2, submit(F1,S)))     and
temp-mem(submit(F1,submit(F2,S))) = temp-mem(submit(F2, submit(F1,S)))     and
U:User (not-ack(U,submit(F1,submit(F2,S))) = not-ack(U,submit(F2, submit(F1,S)))) )
• Quantifier elimination introduces new constants f1 f2 :Elt and s :State .
• Conjunction elimination introduces subgoals as follows:
1. (database(submit(f1,submit(f2,s))) = database(submit(f2, submit(f1,s)))) .
• Show (database(submit(f1,submit(f2,s))) = database(submit(f2, submit(f1,s)))) by reduction.
2. (temp-mem(submit(f1,submit(f2,s))) = temp-mem(submit(f2, submit(f1,s)))) .
• Show (temp-mem(submit(f1,submit(f2,s))) = temp-mem(submit(f2, submit(f1,s)))) by reduction.
3. forall U:User (not-ack(U,submit(f1,submit(f2,s))) = not-ack(U,submit(f2, submit(f1,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 f1 f2 :Elt and s :State .
• Conjunction elimination introduces subgoals as follows:
Properties of the Tatami Protocol

Commutativity of ack.

We want to prove

F1,F2:Elt U1,U2:User S:State ack(U1,F1,ack(U2,F2,S)) = ack(U2,F2,ack(U1,F1,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 F1,F2:Elt U1,U2:User S:State    (database(ack(U1,F1,ack(U2,F2,S))) = database(ack(U2,F2,ack(U1,F1,S)))     and
temp-mem(ack(U1,F1,ack(U2,F2,S))) = temp-mem(ack(U2,F2,ack(U1,F1,S)))     and
U:User (not-ack(U,ack(U1,F1,ack(U2,F2,S))) = not-ack(U,ack(U2,F2,ack(U1,F1,S)))) )
• Quantifier elimination introduces new constants f1 f2 :Elt and u1 u2 :User and s :State .
• Introduce the lemma L:Set (del(f1,del(f2,L)) = del(f2,del(f1,L))) .
• Change hypothesis L:Set (del(f1,del(f2,L)) = del(f2,del(f1,L))) to rewritng rule.
• Case analysis uses the lemma U:User ((((((U =\= u1) and (U =\= u2)) and (u1 =\= u2)) or ((U =\= u1) and (u1 = u2))) or ((U = u1) and (U =\= u2))) or ((U = u2) and (U =\= u1))) or ((U = u1) and (u2 = u1)) on u to get the following subgoals
1. ((u =\= u1) and (u =\= u2)) and (u1 =\= u2)     implies
(database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
• Implication elimination assumes ((u =\= u1) and (u =\= u2)) and (u1 =\= u2) .
• Conjunction elimination introduces subgoals as follows:
1.    database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))
• Conjunction elimination introduces subgoals as follows:
1. (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s))))
• Show (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))) by reduction.
2. (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s))))
• Show (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))) by reduction.
2. U:User not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))
2. (u =\= u1) and (u1 = u2)     implies
(database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
3. (u = u1) and (u =\= u2)     implies
(database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
4. (u = u2) and (u =\= u1)     implies
(database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
5. (u = u1) and (u2 = u1)     implies
(database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))     and
temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))     and
U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) )
• Implication elimination assumes (u = u1) and (u2 = u1) .
• Change hypothesis (u = u1) and (u2 = u1) to rewritng rule.
• Conjunction elimination introduces subgoals as follows:
1. (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))) .
• Show (database(ack(u1,f1,ack(u2,f2,s))) = database(ack(u2,f2,ack(u1,f1,s)))) by reduction.
2. (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))) .
• Show (temp-mem(ack(u1,f1,ack(u2,f2,s))) = temp-mem(ack(u2,f2,ack(u1,f1,s)))) by reduction.
3. forall U:User (not-ack(U,ack(u1,f1,ack(u2,f2,s))) = not-ack(U,ack(u2,f2,ack(u1,f1,s)))) .