[STATEMENT]
lemma a_meet_d: "a \<sqinter> (d_aux a b c) = (a \<sqinter> b) \<squnion> (c \<sqinter> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "a \<sqinter> (d_aux a b c) = a \<sqinter> ((a \<sqinter> b) \<squnion> (b \<sqinter> c) \<squnion> (c \<sqinter> a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a)
[PROOF STEP]
by (simp add: d_aux_def)
[PROOF STATE]
proof (state)
this:
a \<sqinter> d_aux a b c = a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<sqinter> d_aux a b c = a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "... = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a) = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)
[PROOF STEP]
by (simp add: sup_assoc, simp add: sup_commute)
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a) = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> b \<sqinter> c \<squnion> c \<sqinter> a) = a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "... = (a \<sqinter> b \<squnion> c \<sqinter> a) \<squnion> (a \<sqinter> (b \<sqinter> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c)
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a \<sqinter> (a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c)

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
have "... = (a \<sqinter> b) \<squnion> (c \<sqinter> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
by (rule order.antisym, simp_all, rule_tac y = "a \<sqinter> b" in order_trans, simp_all)
[PROOF STATE]
proof (state)
this:
a \<sqinter> b \<squnion> c \<sqinter> a \<squnion> a \<sqinter> (b \<sqinter> c) = a \<sqinter> b \<squnion> c \<sqinter> a

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a

goal (1 subgoal):
 1. a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<sqinter> d_aux a b c = a \<sqinter> b \<squnion> c \<sqinter> a

goal:
No subgoals!
[PROOF STEP]
qed