[STATEMENT]
lemma permute_flip_at:
  fixes a b c::"'a::at"
  shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)
[PROOF STEP]
unfolding flip_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom a \<rightleftharpoons> atom b) \<bullet> c = (if c = a then b else if c = b then a else c)
[PROOF STEP]
apply (rule atom_eq_iff [THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ((atom a \<rightleftharpoons> atom b) \<bullet> c) = atom (if c = a then b else if c = b then a else c)
[PROOF STEP]
apply (subst atom_eqvt [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atom a \<rightleftharpoons> atom b) \<bullet> atom c = atom (if c = a then b else if c = b then a else c)
[PROOF STEP]
apply (simp add: swap_atom)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done