Properties of the Tatami Protocol

We want to prove

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