[STATEMENT]
lemma lemma_4_5_v: "(a \<squnion>1 b) l\<rightarrow> c = (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>1 b l\<rightarrow> c = (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c)
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>1 b l\<rightarrow> c \<le> a l\<rightarrow> c \<and> a \<squnion>1 b l\<rightarrow> c \<le> b l\<rightarrow> c
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>1 b l\<rightarrow> c \<le> a l\<rightarrow> c
 2. a \<squnion>1 b l\<rightarrow> c \<le> b l\<rightarrow> c
 3. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule lemma_2_5_13_a)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<le> a \<squnion>1 b
 2. a \<squnion>1 b l\<rightarrow> c \<le> b l\<rightarrow> c
 3. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>1 b l\<rightarrow> c \<le> b l\<rightarrow> c
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule lemma_2_5_13_a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<le> a \<squnion>1 b
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst right_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c = (1::'a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (1::'a)
 2. (1::'a) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "(a l\<rightarrow> b) l\<rightarrow> ((a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1::'a) \<le> (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst left_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1::'a) * (a l\<rightarrow> b) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a l\<rightarrow> b \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst lemma_4_5_iii)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>1 b l\<rightarrow> b \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst right_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b l\<rightarrow> b) \<le> a \<squnion>1 b l\<rightarrow> c
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst left_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b l\<rightarrow> b) * (a \<squnion>1 b) \<le> c
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "b \<sqinter> c" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b l\<rightarrow> b) * (a \<squnion>1 b) \<le> b \<sqinter> c
 2. b \<sqinter> c \<le> c
 3. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst (2) inf_l_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b l\<rightarrow> b) * (a \<squnion>1 b) \<le> (b l\<rightarrow> c) * b
 2. b \<sqinter> c \<le> c
 3. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "((a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c)) * ((a \<squnion>1 b) \<sqinter> b)" in order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b l\<rightarrow> b) * (a \<squnion>1 b) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> b)
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> b) \<le> (b l\<rightarrow> c) * b
 3. b \<sqinter> c \<le> c
 4. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst (3) inf_l_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b l\<rightarrow> b) * (a \<squnion>1 b) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * ((a \<squnion>1 b l\<rightarrow> b) * (a \<squnion>1 b))
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> b) \<le> (b l\<rightarrow> c) * b
 3. b \<sqinter> c \<le> c
 4. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> b) \<le> (b l\<rightarrow> c) * b
 2. b \<sqinter> c \<le> c
 3. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subgoal_tac "(a \<squnion>1 b \<sqinter> b) = b")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<squnion>1 b \<sqinter> b = b \<Longrightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> b) \<le> (b l\<rightarrow> c) * b
 2. a \<squnion>1 b \<sqinter> b = b
 3. b \<sqinter> c \<le> c
 4. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>1 b \<sqinter> b = b
 2. b \<sqinter> c \<le> c
 3. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule order.antisym, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. b \<le> a \<squnion>1 b \<sqinter> b
 2. b \<sqinter> c \<le> c
 3. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c \<le> c
 2. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "((b l\<rightarrow> a) l\<rightarrow> ((a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c)) l\<rightarrow> ((a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> b) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
 2. ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (rule B1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subgoal_tac "(b l\<rightarrow> a) l\<rightarrow> ((a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c) = 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c = (1::'a) \<Longrightarrow> ((b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
 2. (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c = (1::'a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c \<le> (1::'a)
 2. (1::'a) \<le> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> (b l\<rightarrow> a) l\<rightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst left_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) * (b l\<rightarrow> a) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b l\<rightarrow> a \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst lemma_4_5_iii)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<squnion>1 a l\<rightarrow> a \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) r\<rightarrow> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst right_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (b \<squnion>1 a l\<rightarrow> a) \<le> a \<squnion>1 b l\<rightarrow> c
[PROOF STEP]
apply (subst left_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (b \<squnion>1 a l\<rightarrow> a) * (a \<squnion>1 b) \<le> c
[PROOF STEP]
apply (rule_tac y = "a \<sqinter> c" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (b \<squnion>1 a l\<rightarrow> a) * (a \<squnion>1 b) \<le> a \<sqinter> c
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subst (2) inf_l_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (b \<squnion>1 a l\<rightarrow> a) * (a \<squnion>1 b) \<le> (a l\<rightarrow> c) * a
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (rule_tac y = "((a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c)) * ((a \<squnion>1 b) \<sqinter> a)" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (b \<squnion>1 a l\<rightarrow> a) * (a \<squnion>1 b) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> a)
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> a) \<le> (a l\<rightarrow> c) * a
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subst (3) inf_l_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (b \<squnion>1 a l\<rightarrow> a) * (a \<squnion>1 b) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * ((a \<squnion>1 b l\<rightarrow> a) * (a \<squnion>1 b))
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> a) \<le> (a l\<rightarrow> c) * a
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subst sup1.sup_comute1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b l\<rightarrow> a) * (a \<squnion>1 b) \<le> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * ((a \<squnion>1 b l\<rightarrow> a) * (a \<squnion>1 b))
 2. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> a) \<le> (a l\<rightarrow> c) * a
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> a) \<le> (a l\<rightarrow> c) * a
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subgoal_tac "(a \<squnion>1 b \<sqinter> a) = a")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>1 b \<sqinter> a = a \<Longrightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) * (a \<squnion>1 b \<sqinter> a) \<le> (a l\<rightarrow> c) * a
 2. a \<squnion>1 b \<sqinter> a = a
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>1 b \<sqinter> a = a
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (rule order.antisym, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<le> a \<squnion>1 b \<sqinter> a
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> c \<le> c
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_5_vi: "(a \<squnion>2 b) r\<rightarrow> c = (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>2 b r\<rightarrow> c = (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)
 2. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b r\<rightarrow> c \<le> a r\<rightarrow> c \<and> a \<squnion>2 b r\<rightarrow> c \<le> b r\<rightarrow> c
 2. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b r\<rightarrow> c \<le> a r\<rightarrow> c
 2. a \<squnion>2 b r\<rightarrow> c \<le> b r\<rightarrow> c
 3. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule lemma_2_5_13_b)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<le> a \<squnion>2 b
 2. a \<squnion>2 b r\<rightarrow> c \<le> b r\<rightarrow> c
 3. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b r\<rightarrow> c \<le> b r\<rightarrow> c
 2. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule lemma_2_5_13_b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<le> a \<squnion>2 b
 2. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst left_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c = (1::'a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (1::'a)
 2. (1::'a) \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "(a r\<rightarrow> b) r\<rightarrow> ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1::'a) \<le> (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst right_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a r\<rightarrow> b) * (1::'a) \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a r\<rightarrow> b \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst lemma_4_5_iv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b r\<rightarrow> b \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst left_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a \<squnion>2 b r\<rightarrow> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> a \<squnion>2 b r\<rightarrow> c
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst right_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b * ((a \<squnion>2 b r\<rightarrow> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> c
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "b \<sqinter> c" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b * ((a \<squnion>2 b r\<rightarrow> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> b \<sqinter> c
 2. b \<sqinter> c \<le> c
 3. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst (2) inf_r_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b * ((a \<squnion>2 b r\<rightarrow> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> b * (b r\<rightarrow> c)
 2. b \<sqinter> c \<le> c
 3. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "((a \<squnion>2 b) \<sqinter> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))" in order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<squnion>2 b * ((a \<squnion>2 b r\<rightarrow> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> a \<squnion>2 b \<sqinter> b * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))
 2. a \<squnion>2 b \<sqinter> b * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> b * (b r\<rightarrow> c)
 3. b \<sqinter> c \<le> c
 4. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst (2) inf_r_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<squnion>2 b * ((a \<squnion>2 b r\<rightarrow> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> a \<squnion>2 b * (a \<squnion>2 b r\<rightarrow> b) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))
 2. a \<squnion>2 b \<sqinter> b * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> b * (b r\<rightarrow> c)
 3. b \<sqinter> c \<le> c
 4. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b \<sqinter> b * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> b * (b r\<rightarrow> c)
 2. b \<sqinter> c \<le> c
 3. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subgoal_tac "(a \<squnion>2 b \<sqinter> b) = b")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a \<squnion>2 b \<sqinter> b = b \<Longrightarrow> a \<squnion>2 b \<sqinter> b * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> b * (b r\<rightarrow> c)
 2. a \<squnion>2 b \<sqinter> b = b
 3. b \<sqinter> c \<le> c
 4. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b \<sqinter> b = b
 2. b \<sqinter> c \<le> c
 3. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule order.antisym, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. b \<le> a \<squnion>2 b \<sqinter> b
 2. b \<sqinter> c \<le> c
 3. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c \<le> c
 2. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule_tac y = "((b r\<rightarrow> a) r\<rightarrow> ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c)) r\<rightarrow> ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a r\<rightarrow> b) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
 2. ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (rule B2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subgoal_tac "(b r\<rightarrow> a) r\<rightarrow> ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c) = 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c = (1::'a) \<Longrightarrow> ((b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
 2. (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c = (1::'a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c = (1::'a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c \<le> (1::'a)
 2. (1::'a) \<le> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> (b r\<rightarrow> a) r\<rightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst right_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b r\<rightarrow> a) * (1::'a) \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b r\<rightarrow> a \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst lemma_4_5_iv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<squnion>2 a r\<rightarrow> a \<le> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) l\<rightarrow> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst left_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<squnion>2 a r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> a \<squnion>2 b r\<rightarrow> c
[PROOF STEP]
apply (subst right_residual [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>2 b * ((b \<squnion>2 a r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> c
[PROOF STEP]
apply (rule_tac y = "a \<sqinter> c" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b * ((b \<squnion>2 a r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> a \<sqinter> c
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subst (2) inf_r_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b * ((b \<squnion>2 a r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> a * (a r\<rightarrow> c)
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (rule_tac y = "((a \<squnion>2 b) \<sqinter> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b * ((b \<squnion>2 a r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> a \<squnion>2 b \<sqinter> a * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))
 2. a \<squnion>2 b \<sqinter> a * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> a * (a r\<rightarrow> c)
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subst (2) inf_r_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b * ((b \<squnion>2 a r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> a \<squnion>2 b * (a \<squnion>2 b r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))
 2. a \<squnion>2 b \<sqinter> a * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> a * (a r\<rightarrow> c)
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subst (2) sup2.sup_comute)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b * ((a \<squnion>2 b r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))) \<le> a \<squnion>2 b * (a \<squnion>2 b r\<rightarrow> a) * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c))
 2. a \<squnion>2 b \<sqinter> a * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> a * (a r\<rightarrow> c)
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b \<sqinter> a * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> a * (a r\<rightarrow> c)
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (subgoal_tac "(a \<squnion>2 b \<sqinter> a) = a")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<squnion>2 b \<sqinter> a = a \<Longrightarrow> a \<squnion>2 b \<sqinter> a * ((a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)) \<le> a * (a r\<rightarrow> c)
 2. a \<squnion>2 b \<sqinter> a = a
 3. a \<sqinter> c \<le> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>2 b \<sqinter> a = a
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply (rule order.antisym, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<le> a \<squnion>2 b \<sqinter> a
 2. a \<sqinter> c \<le> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> c \<le> c
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_5_a: "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> a \<squnion>1 b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<squnion>1 b \<le> c
[PROOF STEP]
apply (subst left_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<squnion>1 b l\<rightarrow> c = (1::'a)
[PROOF STEP]
apply (subst lemma_4_5_v)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c) = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_5_b: "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> a \<squnion>2 b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<squnion>2 b \<le> c
[PROOF STEP]
apply (subst right_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> a \<squnion>2 b r\<rightarrow> c = (1::'a)
[PROOF STEP]
apply (subst lemma_4_5_vi)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> c; b \<le> c\<rbrakk> \<Longrightarrow> (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c) = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_5: "a \<squnion>1 b = a \<squnion>2 b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion>1 b = a \<squnion>2 b
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion>1 b \<le> a \<squnion>2 b
 2. a \<squnion>2 b \<le> a \<squnion>1 b
[PROOF STEP]
by (simp_all add: lemma_4_5_a lemma_4_5_b)


[STATEMENT]
lemma (in pseudo_hoop_algebra) [simp]: "infimum {a, b} = {a \<sqinter> b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infimum {a, b} = {a \<sqinter> b}
[PROOF STEP]
apply (simp add: infimum_def lower_bound_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {aa. aa \<le> a \<and> aa \<le> b \<and> (\<forall>x. x \<le> a \<and> x \<le> b \<longrightarrow> x \<le> aa)} = {a \<sqinter> b}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x \<notin> {}; x \<le> a; x \<le> b; \<forall>xa. xa \<le> a \<and> xa \<le> b \<longrightarrow> xa \<le> x\<rbrakk> \<Longrightarrow> x = a \<sqinter> b
 2. \<And>x. a \<sqinter> b \<le> a
 3. \<And>x. a \<sqinter> b \<le> b
 4. \<And>x xa. \<lbrakk>xa \<le> a; xa \<le> b\<rbrakk> \<Longrightarrow> xa \<le> a \<sqinter> b
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x \<notin> {}; x \<le> a; x \<le> b; \<forall>xa. xa \<le> a \<and> xa \<le> b \<longrightarrow> xa \<le> x\<rbrakk> \<Longrightarrow> x \<le> a \<sqinter> b
 2. \<And>x. \<lbrakk>x \<notin> {}; x \<le> a; x \<le> b; \<forall>xa. xa \<le> a \<and> xa \<le> b \<longrightarrow> xa \<le> x\<rbrakk> \<Longrightarrow> a \<sqinter> b \<le> x
 3. \<And>x. a \<sqinter> b \<le> a
 4. \<And>x. a \<sqinter> b \<le> b
 5. \<And>x xa. \<lbrakk>xa \<le> a; xa \<le> b\<rbrakk> \<Longrightarrow> xa \<le> a \<sqinter> b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma (in pseudo_hoop_lattice) sup_impl_inf:
  "(a \<squnion> b) l\<rightarrow> c = (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<squnion> b) l\<rightarrow> c = (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c)
[PROOF STEP]
apply (cut_tac A = "{a, b}" and a = "a \<squnion> b" and b = c in lemma_2_8_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion> b \<in> supremum {a, b}
 2. (a \<squnion> b) l\<rightarrow> c \<in> infimum ((\<lambda>x. x l\<rightarrow> c) ` {a, b}) \<Longrightarrow> (a \<squnion> b) l\<rightarrow> c = (a l\<rightarrow> c) \<sqinter> (b l\<rightarrow> c)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma (in pseudo_hoop_lattice) sup_impr_inf:
  "(a \<squnion> b) r\<rightarrow> c = (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<squnion> b) r\<rightarrow> c = (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)
[PROOF STEP]
apply (cut_tac A = "{a, b}" and a = "a \<squnion> b" and b = c in lemma_2_8_i1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<squnion> b \<in> supremum {a, b}
 2. (a \<squnion> b) r\<rightarrow> c \<in> infimum ((\<lambda>x. x r\<rightarrow> c) ` {a, b}) \<Longrightarrow> (a \<squnion> b) r\<rightarrow> c = (a r\<rightarrow> c) \<sqinter> (b r\<rightarrow> c)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma (in pseudo_hoop_lattice) sup_times:
  "a * (b \<squnion> c) = (a * b) \<squnion> (a * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (b \<squnion> c) = a * b \<squnion> a * c
[PROOF STEP]
apply (cut_tac A = "{b, c}" and b = "b \<squnion> c" and a = a in lemma_2_9_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<squnion> c \<in> supremum {b, c}
 2. a * (b \<squnion> c) \<in> supremum ((*) a ` {b, c}) \<Longrightarrow> a * (b \<squnion> c) = a * b \<squnion> a * c
[PROOF STEP]
by simp_all


[STATEMENT]
lemma (in pseudo_hoop_lattice) sup_times_right:
  "(b \<squnion> c) * a = (b * a) \<squnion> (c * a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<squnion> c) * a = b * a \<squnion> c * a
[PROOF STEP]
apply (cut_tac A = "{b, c}" and b = "b \<squnion> c" and a = a in lemma_2_9_i1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<squnion> c \<in> supremum {b, c}
 2. (b \<squnion> c) * a \<in> supremum ((\<lambda>x. x * a) ` {b, c}) \<Longrightarrow> (b \<squnion> c) * a = b * a \<squnion> c * a
[PROOF STEP]
by simp_all


[STATEMENT]
lemma lemma_4_8_i: "a * (b \<sqinter> c) = (a * b) \<sqinter> (a * c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (b \<sqinter> c) = a * b \<sqinter> (a * c)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a * (b \<sqinter> c) \<le> a * b \<sqinter> (a * c)
 2. a * b \<sqinter> (a * c) \<le> a * (b \<sqinter> c)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b \<sqinter> (a * c) \<le> a * (b \<sqinter> c)
[PROOF STEP]
apply (subgoal_tac "a * (b \<sqinter> c) = (a * (b * (b r\<rightarrow> c))) \<squnion>1 (a * (c * (c r\<rightarrow> b)))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b))) \<Longrightarrow> a * b \<sqinter> (a * c) \<le> a * (b \<sqinter> c)
 2. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b))) \<Longrightarrow> a * b \<sqinter> (a * c) \<le> a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
 2. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> a * b \<sqinter> (a * c) \<le> a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
 2. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (rule_tac y = "(((a * b) \<sqinter> (a * c)) * (b r\<rightarrow> c)) \<squnion>1 (((a * b) \<sqinter> (a * c)) * (c r\<rightarrow> b))" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. True \<Longrightarrow> a * b \<sqinter> (a * c) \<le> a * b \<sqinter> (a * c) * (b r\<rightarrow> c) \<squnion>1 (a * b \<sqinter> (a * c) * (c r\<rightarrow> b))
 2. True \<Longrightarrow> a * b \<sqinter> (a * c) * (b r\<rightarrow> c) \<squnion>1 (a * b \<sqinter> (a * c) * (c r\<rightarrow> b)) \<le> a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
 3. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (subst sup_times [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. True \<Longrightarrow> a * b \<sqinter> (a * c) \<le> a * b \<sqinter> (a * c) * ((b r\<rightarrow> c) \<squnion>1 (c r\<rightarrow> b))
 2. True \<Longrightarrow> a * b \<sqinter> (a * c) * (b r\<rightarrow> c) \<squnion>1 (a * b \<sqinter> (a * c) * (c r\<rightarrow> b)) \<le> a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
 3. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (simp add: lemma_4_5 lemma_4_5_ii)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> a * b \<sqinter> (a * c) * (b r\<rightarrow> c) \<squnion>1 (a * b \<sqinter> (a * c) * (c r\<rightarrow> b)) \<le> a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
 2. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (simp add: mult.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a * b \<sqinter> (a * c) * (b r\<rightarrow> c) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b)) \<and> a * b \<sqinter> (a * c) * (c r\<rightarrow> b) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 2. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a * b \<sqinter> (a * c) * (b r\<rightarrow> c) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 2. a * b \<sqinter> (a * c) * (c r\<rightarrow> b) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 3. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (rule_tac y = "a * b * (b r\<rightarrow> c)" in order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. a * b \<sqinter> (a * c) * (b r\<rightarrow> c) \<le> a * b * (b r\<rightarrow> c)
 2. a * b * (b r\<rightarrow> c) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 3. a * b \<sqinter> (a * c) * (c r\<rightarrow> b) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 4. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a * b * (b r\<rightarrow> c) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 2. a * b \<sqinter> (a * c) * (c r\<rightarrow> b) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 3. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a * b \<sqinter> (a * c) * (c r\<rightarrow> b) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 2. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (rule_tac y = "a * c * (c r\<rightarrow> b)" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a * b \<sqinter> (a * c) * (c r\<rightarrow> b) \<le> a * c * (c r\<rightarrow> b)
 2. a * c * (c r\<rightarrow> b) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 3. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a * c * (c r\<rightarrow> b) \<le> a * b * (b r\<rightarrow> c) \<squnion>1 (a * c * (c r\<rightarrow> b))
 2. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (b \<sqinter> c) = a * (b * (b r\<rightarrow> c)) \<squnion>1 (a * (c * (c r\<rightarrow> b)))
[PROOF STEP]
apply (simp add: inf_r_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (b \<sqinter> c) = a * (b \<sqinter> c) \<squnion>1 (a * (c \<sqinter> b))
[PROOF STEP]
apply (subgoal_tac "b \<sqinter> c = c \<sqinter> b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c = c \<sqinter> b \<Longrightarrow> a * (b \<sqinter> c) = a * (b \<sqinter> c) \<squnion>1 (a * (c \<sqinter> b))
 2. b \<sqinter> c = c \<sqinter> b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> c = c \<sqinter> b
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c \<le> c \<sqinter> b
 2. c \<sqinter> b \<le> b \<sqinter> c
[PROOF STEP]
by simp_all


[STATEMENT]
lemma lemma_4_8_ii: "(b \<sqinter> c) * a = (b * a) \<sqinter> (c * a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> c * a = b * a \<sqinter> (c * a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c * a \<le> b * a \<sqinter> (c * a)
 2. b * a \<sqinter> (c * a) \<le> b \<sqinter> c * a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * a \<sqinter> (c * a) \<le> b \<sqinter> c * a
[PROOF STEP]
apply (subgoal_tac "(b \<sqinter> c) * a = (((b l\<rightarrow> c) * b) * a) \<squnion>1 (((c l\<rightarrow> b) * c) * a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a) \<Longrightarrow> b * a \<sqinter> (c * a) \<le> b \<sqinter> c * a
 2. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a) \<Longrightarrow> b * a \<sqinter> (c * a) \<le> (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
 2. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> b * a \<sqinter> (c * a) \<le> (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
 2. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (rule_tac y = "((b l\<rightarrow> c) * ((b * a) \<sqinter> (c * a))) \<squnion>1 ((c l\<rightarrow> b) * ((b * a) \<sqinter> (c * a)))" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. True \<Longrightarrow> b * a \<sqinter> (c * a) \<le> (b l\<rightarrow> c) * (b * a \<sqinter> (c * a)) \<squnion>1 ((c l\<rightarrow> b) * (b * a \<sqinter> (c * a)))
 2. True \<Longrightarrow> (b l\<rightarrow> c) * (b * a \<sqinter> (c * a)) \<squnion>1 ((c l\<rightarrow> b) * (b * a \<sqinter> (c * a))) \<le> (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
 3. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (subst sup_times_right [THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. True \<Longrightarrow> b * a \<sqinter> (c * a) \<le> (b l\<rightarrow> c) \<squnion>1 (c l\<rightarrow> b) * (b * a \<sqinter> (c * a))
 2. True \<Longrightarrow> (b l\<rightarrow> c) * (b * a \<sqinter> (c * a)) \<squnion>1 ((c l\<rightarrow> b) * (b * a \<sqinter> (c * a))) \<le> (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
 3. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (simp add: lemma_4_5_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True \<Longrightarrow> (b l\<rightarrow> c) * (b * a \<sqinter> (c * a)) \<squnion>1 ((c l\<rightarrow> b) * (b * a \<sqinter> (c * a))) \<le> (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
 2. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b l\<rightarrow> c) * (b * a \<sqinter> (c * a)) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a)) \<and> (c l\<rightarrow> b) * (b * a \<sqinter> (c * a)) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a))
 2. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (b l\<rightarrow> c) * (b * a \<sqinter> (c * a)) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a))
 2. (c l\<rightarrow> b) * (b * a \<sqinter> (c * a)) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a))
 3. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (rule_tac y = "(b l\<rightarrow> c) * (b * a)" in order_trans)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (b l\<rightarrow> c) * (b * a \<sqinter> (c * a)) \<le> (b l\<rightarrow> c) * (b * a)
 2. (b l\<rightarrow> c) * (b * a) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a))
 3. (c l\<rightarrow> b) * (b * a \<sqinter> (c * a)) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a))
 4. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (c l\<rightarrow> b) * (b * a \<sqinter> (c * a)) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a))
 2. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (rule_tac y = "(c l\<rightarrow> b) * (c * a)" in order_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (c l\<rightarrow> b) * (b * a \<sqinter> (c * a)) \<le> (c l\<rightarrow> b) * (c * a)
 2. (c l\<rightarrow> b) * (c * a) \<le> (b l\<rightarrow> c) * (b * a) \<squnion>1 ((c l\<rightarrow> b) * (c * a))
 3. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> c * a = (b l\<rightarrow> c) * b * a \<squnion>1 ((c l\<rightarrow> b) * c * a)
[PROOF STEP]
apply (simp add: inf_l_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> c * a = b \<sqinter> c * a \<squnion>1 (c \<sqinter> b * a)
[PROOF STEP]
apply (subgoal_tac "b \<sqinter> c = c \<sqinter> b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c = c \<sqinter> b \<Longrightarrow> b \<sqinter> c * a = b \<sqinter> c * a \<squnion>1 (c \<sqinter> b * a)
 2. b \<sqinter> c = c \<sqinter> b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> c = c \<sqinter> b
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b \<sqinter> c \<le> c \<sqinter> b
 2. c \<sqinter> b \<le> b \<sqinter> c
[PROOF STEP]
by simp_all


[STATEMENT]
lemma lemma_4_8_iii: "(a l\<rightarrow> b) l\<rightarrow> (b l\<rightarrow> a) = b l\<rightarrow> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) l\<rightarrow> b l\<rightarrow> a = b l\<rightarrow> a
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> b) l\<rightarrow> b l\<rightarrow> a \<le> b l\<rightarrow> a
 2. b l\<rightarrow> a \<le> (a l\<rightarrow> b) l\<rightarrow> b l\<rightarrow> a
[PROOF STEP]
apply (cut_tac a = a and b = b in lemma_4_5_i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> b) \<squnion>1 (b l\<rightarrow> a) = (1::'a) \<Longrightarrow> (a l\<rightarrow> b) l\<rightarrow> b l\<rightarrow> a \<le> b l\<rightarrow> a
 2. b l\<rightarrow> a \<le> (a l\<rightarrow> b) l\<rightarrow> b l\<rightarrow> a
[PROOF STEP]
apply (unfold sup1_def right_lesseq, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b l\<rightarrow> a) r\<rightarrow> (a l\<rightarrow> b) l\<rightarrow> b l\<rightarrow> a = (1::'a)
[PROOF STEP]
by (simp add: lemma_2_5_9_a)


[STATEMENT]
lemma lemma_4_8_iv: "(a r\<rightarrow> b) r\<rightarrow> (b r\<rightarrow> a) = b r\<rightarrow> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) r\<rightarrow> b r\<rightarrow> a = b r\<rightarrow> a
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a r\<rightarrow> b) r\<rightarrow> b r\<rightarrow> a \<le> b r\<rightarrow> a
 2. b r\<rightarrow> a \<le> (a r\<rightarrow> b) r\<rightarrow> b r\<rightarrow> a
[PROOF STEP]
apply (cut_tac a = a and b = b in lemma_4_5_ii)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a r\<rightarrow> b) \<squnion>2 (b r\<rightarrow> a) = (1::'a) \<Longrightarrow> (a r\<rightarrow> b) r\<rightarrow> b r\<rightarrow> a \<le> b r\<rightarrow> a
 2. b r\<rightarrow> a \<le> (a r\<rightarrow> b) r\<rightarrow> b r\<rightarrow> a
[PROOF STEP]
apply (unfold sup2_def left_lesseq, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b r\<rightarrow> a) l\<rightarrow> (a r\<rightarrow> b) r\<rightarrow> b r\<rightarrow> a = (1::'a)
[PROOF STEP]
by (simp add: lemma_2_5_9_b)


[STATEMENT]
lemma impl_one_bl [simp]: "a l\<rightarrow> a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (rule bounded_lattice.order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a l\<rightarrow> a \<le> (1::'a)
 2. (1::'a) \<le> a l\<rightarrow> a
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> a l\<rightarrow> a
[PROOF STEP]
apply (subst left_residual_bl [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) * a \<le> a
[PROOF STEP]
by simp


[STATEMENT]
lemma impr_one_bl [simp]: "a r\<rightarrow> a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (rule bounded_lattice.order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a r\<rightarrow> a \<le> (1::'a)
 2. (1::'a) \<le> a r\<rightarrow> a
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<le> a r\<rightarrow> a
[PROOF STEP]
apply (subst right_residual_bl [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (1::'a) \<le> a
[PROOF STEP]
by simp


[STATEMENT]
lemma impl_ded_bl: "((a * b) l\<rightarrow> c) = (a l\<rightarrow> (b l\<rightarrow> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * b l\<rightarrow> c = a l\<rightarrow> b l\<rightarrow> c
[PROOF STEP]
apply (rule bounded_lattice.order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c
 2. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (case_tac "(a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c)
      \<and> ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = (((a * b l\<rightarrow> c) * a) * b \<le> c)
      \<and> (((a * b l\<rightarrow> c) * a) * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c)
      \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = ((a * b l\<rightarrow> c) \<le> (a * b l\<rightarrow> c))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) \<and> ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a * b \<le> c) \<and> ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c) \<Longrightarrow> a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c
 2. \<not> ((a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) \<and> ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a * b \<le> c) \<and> ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)) \<Longrightarrow> a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c
 3. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> ((a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) \<and> ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a * b \<le> c) \<and> ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)) \<Longrightarrow> a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c
 2. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) \<and> ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a * b \<le> c) \<and> ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)
 2. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a * b l\<rightarrow> c \<le> a l\<rightarrow> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c)
 2. ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a * b \<le> c) \<and> ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)
 3. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (simp add: left_residual_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a * b \<le> c) \<and> ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)
 2. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ((a * b l\<rightarrow> c) * a \<le> b l\<rightarrow> c) = ((a * b l\<rightarrow> c) * a * b \<le> c)
 2. ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)
 3. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (simp add: left_residual_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c) \<and> ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)
 2. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ((a * b l\<rightarrow> c) * a * b \<le> c) = ((a * b l\<rightarrow> c) * (a * b) \<le> c)
 2. ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)
 3. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((a * b l\<rightarrow> c) * (a * b) \<le> c) = (a * b l\<rightarrow> c \<le> a * b l\<rightarrow> c)
 2. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (simp add: left_residual_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> b l\<rightarrow> c \<le> a * b l\<rightarrow> c
[PROOF STEP]
apply (simp add: left_residual_bl [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b l\<rightarrow> c) * (a * b) \<le> c
[PROOF STEP]
apply (rule_tac y="(b l\<rightarrow> c) * b" in bounded_lattice.order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> b l\<rightarrow> c) * (a * b) \<le> (b l\<rightarrow> c) * b
 2. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply (simp add: mult.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a l\<rightarrow> b l\<rightarrow> c) * a * b \<le> (b l\<rightarrow> c) * b
 2. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply (subst inf_l_bl_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<sqinter> (b l\<rightarrow> c) * b \<le> (b l\<rightarrow> c) * b
 2. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply (subst bounded_lattice.inf_commute)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b l\<rightarrow> c) \<sqinter> a * b \<le> (b l\<rightarrow> c) * b
 2. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply (subst inf_l_bl_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((b l\<rightarrow> c) l\<rightarrow> a) * (b l\<rightarrow> c) * b \<le> (b l\<rightarrow> c) * b
 2. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply (subst mult.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ((b l\<rightarrow> c) l\<rightarrow> a) * ((b l\<rightarrow> c) * b) \<le> (b l\<rightarrow> c) * b
 2. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply (subst left_residual_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b l\<rightarrow> c) l\<rightarrow> a \<le> (b l\<rightarrow> c) * b l\<rightarrow> (b l\<rightarrow> c) * b
 2. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b l\<rightarrow> c) * b \<le> c
[PROOF STEP]
apply (subst left_residual_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b l\<rightarrow> c \<le> b l\<rightarrow> c
[PROOF STEP]
by simp


[STATEMENT]
lemma impr_ded_bl: "(b * a r\<rightarrow> c) = (a r\<rightarrow> (b r\<rightarrow> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * a r\<rightarrow> c = a r\<rightarrow> b r\<rightarrow> c
[PROOF STEP]
apply (rule bounded_lattice.order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c
 2. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (case_tac "(b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c) = (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c)
      \<and> (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c)
      \<and> (b * ( a* (b * a r\<rightarrow> c)) \<le> c) = ((b * a) * (b * a r\<rightarrow> c) \<le> c)
      \<and> ((b * a) * (b * a r\<rightarrow> c) \<le> c) = ((b * a r\<rightarrow> c) \<le> (b * a r\<rightarrow> c))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c) = (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) \<and> (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c) \<and> (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c) \<Longrightarrow> b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c
 2. \<not> ((b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c) = (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) \<and> (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c) \<and> (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)) \<Longrightarrow> b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c
 3. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> ((b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c) = (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) \<and> (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c) \<and> (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)) \<Longrightarrow> b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c
 2. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c) = (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) \<and> (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c) \<and> (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)
 2. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (b * a r\<rightarrow> c \<le> a r\<rightarrow> b r\<rightarrow> c) = (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c)
 2. (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c) \<and> (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)
 3. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (simp add: right_residual_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c) \<and> (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)
 2. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (a * (b * a r\<rightarrow> c) \<le> b r\<rightarrow> c) = (b * (a * (b * a r\<rightarrow> c)) \<le> c)
 2. (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)
 3. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (simp add: right_residual_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c) \<and> (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)
 2. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (b * (a * (b * a r\<rightarrow> c)) \<le> c) = (b * a * (b * a r\<rightarrow> c) \<le> c)
 2. (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)
 3. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b * a * (b * a r\<rightarrow> c) \<le> c) = (b * a r\<rightarrow> c \<le> b * a r\<rightarrow> c)
 2. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (simp add: right_residual_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a r\<rightarrow> b r\<rightarrow> c \<le> b * a r\<rightarrow> c
[PROOF STEP]
apply (simp add: right_residual_bl [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * a * (a r\<rightarrow> b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (rule_tac y="b * (b r\<rightarrow> c)" in bounded_lattice.order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b * a * (a r\<rightarrow> b r\<rightarrow> c) \<le> b * (b r\<rightarrow> c)
 2. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b * (a * (a r\<rightarrow> b r\<rightarrow> c)) \<le> b * (b r\<rightarrow> c)
 2. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (subst inf_r_bl_def [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b * (a \<sqinter> (b r\<rightarrow> c)) \<le> b * (b r\<rightarrow> c)
 2. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (subst bounded_lattice.inf_commute)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b * ((b r\<rightarrow> c) \<sqinter> a) \<le> b * (b r\<rightarrow> c)
 2. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (subst inf_r_bl_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b * ((b r\<rightarrow> c) * ((b r\<rightarrow> c) r\<rightarrow> a)) \<le> b * (b r\<rightarrow> c)
 2. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (subst mult.assoc [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b * (b r\<rightarrow> c) * ((b r\<rightarrow> c) r\<rightarrow> a) \<le> b * (b r\<rightarrow> c)
 2. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (subst right_residual_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (b r\<rightarrow> c) r\<rightarrow> a \<le> b * (b r\<rightarrow> c) r\<rightarrow> b * (b r\<rightarrow> c)
 2. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * (b r\<rightarrow> c) \<le> c
[PROOF STEP]
apply (subst right_residual_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b r\<rightarrow> c \<le> b r\<rightarrow> c
[PROOF STEP]
by simp


[STATEMENT]
lemma lesseq_impl_bl: "(a \<le> b) = (a l\<rightarrow> b = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<le> b) = (a l\<rightarrow> b = (1::'a))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> a l\<rightarrow> b = (1::'a)
 2. a l\<rightarrow> b = (1::'a) \<Longrightarrow> a \<le> b
[PROOF STEP]
apply (rule  bounded_lattice.order.antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a \<le> b \<Longrightarrow> a l\<rightarrow> b \<le> (1::'a)
 2. a \<le> b \<Longrightarrow> (1::'a) \<le> a l\<rightarrow> b
 3. a l\<rightarrow> b = (1::'a) \<Longrightarrow> a \<le> b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> (1::'a) \<le> a l\<rightarrow> b
 2. a l\<rightarrow> b = (1::'a) \<Longrightarrow> a \<le> b
[PROOF STEP]
apply (simp add: left_residual_bl [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a l\<rightarrow> b = (1::'a) \<Longrightarrow> a \<le> b
[PROOF STEP]
apply (subgoal_tac "1 \<le> a l\<rightarrow> b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a l\<rightarrow> b = (1::'a); (1::'a) \<le> a l\<rightarrow> b\<rbrakk> \<Longrightarrow> a \<le> b
 2. a l\<rightarrow> b = (1::'a) \<Longrightarrow> (1::'a) \<le> a l\<rightarrow> b
[PROOF STEP]
apply (subst (asm) left_residual_bl [THEN sym])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a l\<rightarrow> b = (1::'a); (1::'a) * a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b
 2. a l\<rightarrow> b = (1::'a) \<Longrightarrow> (1::'a) \<le> a l\<rightarrow> b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma lemma_4_12_i_ii: "a \<noteq> 1 \<Longrightarrow> filterof({a}) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> filterof {a} = UNIV
[PROOF STEP]
apply (cut_tac strong_simple)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (1::'a); properfilters = {{1::'a}}\<rbrakk> \<Longrightarrow> filterof {a} = UNIV
[PROOF STEP]
apply (simp add: properfilters_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}\<rbrakk> \<Longrightarrow> filterof {a} = UNIV
[PROOF STEP]
apply (subgoal_tac "filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}; filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}\<rbrakk> \<Longrightarrow> filterof {a} = UNIV
 2. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}\<rbrakk> \<Longrightarrow> filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{F \<in> filters. F \<noteq> UNIV} = {{1::'a}}; filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}; True\<rbrakk> \<Longrightarrow> filterof {a} = UNIV
 2. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}\<rbrakk> \<Longrightarrow> filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}
[PROOF STEP]
apply (drule drop_assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}; True; True\<rbrakk> \<Longrightarrow> filterof {a} = UNIV
 2. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}\<rbrakk> \<Longrightarrow> filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}\<rbrakk> \<Longrightarrow> filterof {a} \<notin> {F \<in> filters. F \<noteq> UNIV}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}\<rbrakk> \<Longrightarrow> filterof {a} \<noteq> {1::'a}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}; filterof {a} = {1::'a}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "a \<in> filterof {a}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}; filterof {a} = {1::'a}; a \<in> filterof {a}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}; filterof {a} = {1::'a}\<rbrakk> \<Longrightarrow> a \<in> filterof {a}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}; filterof {a} = {1::'a}\<rbrakk> \<Longrightarrow> a \<in> filterof {a}
[PROOF STEP]
apply (subst filterof_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> (1::'a); {F \<in> filters. F \<noteq> UNIV} = {{1::'a}}; filterof {a} = {1::'a}\<rbrakk> \<Longrightarrow> a \<in> \<Inter> {F \<in> filters. {a} \<subseteq> F}
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_12_i_iii: "a \<noteq> 1 \<Longrightarrow> (\<exists> n . a ^ n \<le> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> \<exists>n. a ^ n \<le> b
[PROOF STEP]
apply (drule lemma_4_12_i_ii)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterof {a} = UNIV \<Longrightarrow> \<exists>n. a ^ n \<le> b
[PROOF STEP]
apply (simp add: prop_3_2_i)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {aa. \<exists>n. a ^ n \<le> aa} = UNIV \<Longrightarrow> \<exists>n. a ^ n \<le> b
[PROOF STEP]
by blast


[STATEMENT]
lemma lemma_4_12_i_iv: "a \<noteq> 1 \<Longrightarrow> (\<exists> n . a l-n\<rightarrow> b = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> \<exists>n. a l-n\<rightarrow> b = (1::'a)
[PROOF STEP]
apply (subst lemma_2_4_7_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> \<exists>n. a ^ n l\<rightarrow> b = (1::'a)
[PROOF STEP]
apply (subst left_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> \<exists>n. a ^ n \<le> b
[PROOF STEP]
by (simp add: lemma_4_12_i_iii)


[STATEMENT]
lemma lemma_4_12_i_v: "a \<noteq> 1 \<Longrightarrow> (\<exists> n . a r-n\<rightarrow> b = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> \<exists>n. a r-n\<rightarrow> b = (1::'a)
[PROOF STEP]
apply (subst lemma_2_4_7_b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> \<exists>n. a ^ n r\<rightarrow> b = (1::'a)
[PROOF STEP]
apply (subst right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (1::'a) \<Longrightarrow> \<exists>n. a ^ n \<le> b
[PROOF STEP]
by (simp add: lemma_4_12_i_iii)


[STATEMENT]
lemma (in pseudo_hoop_algebra) [simp]: "{1} \<in> filters"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {1::'a} \<in> filters
[PROOF STEP]
apply (simp add: filters_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b\<ge>1::'a. b = (1::'a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. (1::'a) \<le> b \<Longrightarrow> b = (1::'a)
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. (1::'a) \<le> b \<Longrightarrow> b \<le> (1::'a)
 2. \<And>b. (1::'a) \<le> b \<Longrightarrow> (1::'a) \<le> b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma (in pseudo_hoop_algebra) power_impl: "b l\<rightarrow> a = a \<Longrightarrow> b ^ n l\<rightarrow> a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b l\<rightarrow> a = a \<Longrightarrow> b ^ n l\<rightarrow> a = a
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b l\<rightarrow> a = a \<Longrightarrow> b ^ 0 l\<rightarrow> a = a
 2. \<And>n. \<lbrakk>b l\<rightarrow> a = a; b ^ n l\<rightarrow> a = a\<rbrakk> \<Longrightarrow> b ^ Suc n l\<rightarrow> a = a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b l\<rightarrow> a = a; b ^ n l\<rightarrow> a = a\<rbrakk> \<Longrightarrow> b ^ Suc n l\<rightarrow> a = a
[PROOF STEP]
by (simp add: left_impl_ded)


[STATEMENT]
lemma (in pseudo_hoop_algebra) power_impr: "b r\<rightarrow> a = a \<Longrightarrow> b ^ n r\<rightarrow> a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b r\<rightarrow> a = a \<Longrightarrow> b ^ n r\<rightarrow> a = a
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. b r\<rightarrow> a = a \<Longrightarrow> b ^ 0 r\<rightarrow> a = a
 2. \<And>n. \<lbrakk>b r\<rightarrow> a = a; b ^ n r\<rightarrow> a = a\<rbrakk> \<Longrightarrow> b ^ Suc n r\<rightarrow> a = a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b r\<rightarrow> a = a; b ^ n r\<rightarrow> a = a\<rbrakk> \<Longrightarrow> b ^ Suc n r\<rightarrow> a = a
[PROOF STEP]
by (simp add: right_impl_ded)


[STATEMENT]
lemma lemma_4_13_i: "b l\<rightarrow> a = a \<Longrightarrow> a = 1 \<or> b = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b l\<rightarrow> a = a \<Longrightarrow> a = (1::'a) \<or> b = (1::'a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b l\<rightarrow> a = a; b \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply (drule_tac a = b and b = a in lemma_4_12_i_iii)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b l\<rightarrow> a = a; \<exists>n. b ^ n \<le> a\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b l\<rightarrow> a = a; b ^ n \<le> a\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply (subst (asm) left_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b l\<rightarrow> a = a; b ^ n l\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply (drule_tac n = n in power_impl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b ^ n l\<rightarrow> a = (1::'a); b ^ n l\<rightarrow> a = a\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma lemma_4_13_ii: "b r\<rightarrow> a = a \<Longrightarrow> a = 1 \<or> b = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b r\<rightarrow> a = a \<Longrightarrow> a = (1::'a) \<or> b = (1::'a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b r\<rightarrow> a = a; b \<noteq> (1::'a)\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply (drule_tac a = b and b = a in lemma_4_12_i_iii)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b r\<rightarrow> a = a; \<exists>n. b ^ n \<le> a\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b r\<rightarrow> a = a; b ^ n \<le> a\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply (subst (asm) right_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b r\<rightarrow> a = a; b ^ n r\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
apply (drule_tac n = n in power_impr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>b ^ n r\<rightarrow> a = (1::'a); b ^ n r\<rightarrow> a = a\<rbrakk> \<Longrightarrow> a = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "(a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply (case_tac "a = b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a = b \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
 2. a \<noteq> b \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply (cut_tac x = a and y =b in linear)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; a \<le> b \<or> b \<le> a\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; a \<le> b\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
 2. \<lbrakk>a \<noteq> b; b \<le> a\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply (subst (asm) left_lesseq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; a l\<rightarrow> b = (1::'a)\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
 2. \<lbrakk>a \<noteq> b; b \<le> a\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply (simp add: lemma_2_10_24)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b \<le> a\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply (subst (asm) left_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b l\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> (b l\<rightarrow> a) r\<rightarrow> a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b l\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> a
[PROOF STEP]
apply (subst left_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b l\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (cut_tac b = "((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> a" and a = "a l\<rightarrow> b" in left_impl_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; b l\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> (((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> a) l\<rightarrow> a l\<rightarrow> b = a l\<rightarrow> b
 2. \<lbrakk>a \<noteq> b; b l\<rightarrow> a = (1::'a); a l\<rightarrow> b = (1::'a) \<or> ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (simp add: lemma_2_10_32)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b l\<rightarrow> a = (1::'a); a l\<rightarrow> b = (1::'a) \<or> ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> ((a l\<rightarrow> b) r\<rightarrow> b) l\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (simp add: left_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b \<le> a; a \<le> b \<or> (a l\<rightarrow> b) r\<rightarrow> b \<le> a\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> a
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b \<le> a; a \<le> b\<rbrakk> \<Longrightarrow> (a l\<rightarrow> b) r\<rightarrow> b \<le> a
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; a \<le> b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "(a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (case_tac "a = b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a = b \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
 2. a \<noteq> b \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (cut_tac x = a and y =b in linear)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; a \<le> b \<or> b \<le> a\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; a \<le> b\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
 2. \<lbrakk>a \<noteq> b; b \<le> a\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (subst (asm) right_lesseq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; a r\<rightarrow> b = (1::'a)\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
 2. \<lbrakk>a \<noteq> b; b \<le> a\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; a r\<rightarrow> b = (1::'a)\<rbrakk> \<Longrightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
 2. \<lbrakk>a \<noteq> b; b \<le> a\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (simp add: lemma_2_10_26)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b \<le> a\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> (b r\<rightarrow> a) l\<rightarrow> a
[PROOF STEP]
apply (unfold right_lesseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b r\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> (b r\<rightarrow> a) l\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (cut_tac b = "((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> a" and a = "a r\<rightarrow> b" in right_impl_one)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> b; b r\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> (((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> a) r\<rightarrow> a r\<rightarrow> b = a r\<rightarrow> b
 2. \<lbrakk>a \<noteq> b; b r\<rightarrow> a = (1::'a); a r\<rightarrow> b = (1::'a) \<or> ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> (b r\<rightarrow> a) l\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (simp add: lemma_2_10_33)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b r\<rightarrow> a = (1::'a); a r\<rightarrow> b = (1::'a) \<or> ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> a = (1::'a)\<rbrakk> \<Longrightarrow> ((a r\<rightarrow> b) l\<rightarrow> b) r\<rightarrow> (b r\<rightarrow> a) l\<rightarrow> a = (1::'a)
[PROOF STEP]
apply (simp add: right_lesseq [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b \<le> a; a \<le> b \<or> (a r\<rightarrow> b) l\<rightarrow> b \<le> a\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> a
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> b; b \<le> a; a \<le> b\<rbrakk> \<Longrightarrow> (a r\<rightarrow> b) l\<rightarrow> b \<le> a
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> a; a \<le> b\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_left_isotone:
  "x \<le> y \<Longrightarrow> x * z \<le> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x * z \<le> y * z
[PROOF STEP]
using mult_right_dist_sup sup_right_divisibility
[PROOF STATE]
proof (prove)
using this:
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
(?x \<le> ?y) = (\<exists>z. z \<squnion> ?x = ?y)

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x * z \<le> y * z
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_right_isotone:
  "x \<le> y \<Longrightarrow> z * x \<le> z * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> z * x \<le> z * y
[PROOF STEP]
using mult_left_sub_dist_sup sup.bounded_iff sup_right_divisibility
[PROOF STATE]
proof (prove)
using this:
?x * ?y \<squnion> ?x * ?z \<le> ?x * (?y \<squnion> ?z)
(?b \<squnion> ?c \<le> ?a) = (?b \<le> ?a \<and> ?c \<le> ?a)
(?x \<le> ?y) = (\<exists>z. z \<squnion> ?x = ?y)

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> z * x \<le> z * y
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_isotone:
  "w \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> w * x \<le> y * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> w * x \<le> y * z
[PROOF STEP]
using order_trans mult_left_isotone mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. \<lbrakk>w \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> w * x \<le> y * z
[PROOF STEP]
by blast


[STATEMENT]
lemma affine_isotone:
  "isotone (\<lambda>x . y * x \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isotone (\<lambda>x. y * x \<squnion> z)
[PROOF STEP]
using isotone_def mult_right_isotone sup_left_isotone
[PROOF STATE]
proof (prove)
using this:
isotone ?f \<equiv> \<forall>x y. x \<le> y \<longrightarrow> ?f x \<le> ?f y
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?x \<le> ?y \<Longrightarrow> ?x \<squnion> ?z \<le> ?y \<squnion> ?z

goal (1 subgoal):
 1. isotone (\<lambda>x. y * x \<squnion> z)
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_left_sub_dist_sup_left:
  "x * y \<le> x * (y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<le> x * (y \<squnion> z)
[PROOF STEP]
by (simp add: mult_right_isotone)


[STATEMENT]
lemma mult_left_sub_dist_sup_right:
  "x * z \<le> x * (y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<le> x * (y \<squnion> z)
[PROOF STEP]
by (simp add: mult_right_isotone)


[STATEMENT]
lemma mult_right_sub_dist_sup_left:
  "x * z \<le> (x \<squnion> y) * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * z \<le> (x \<squnion> y) * z
[PROOF STEP]
by (simp add: mult_left_isotone)


[STATEMENT]
lemma mult_right_sub_dist_sup_right:
  "y * z \<le> (x \<squnion> y) * z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * z \<le> (x \<squnion> y) * z
[PROOF STEP]
by (simp add: mult_left_isotone)


[STATEMENT]
lemma case_split_left:
  assumes "1 \<le> w \<squnion> z"
      and "w * x \<le> y"
      and "z * x \<le> y"
    shows "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
have "(w \<squnion> z) * x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<squnion> z) * x \<le> y
[PROOF STEP]
by (simp add: assms(2-3) mult_right_dist_sup)
[PROOF STATE]
proof (state)
this:
(w \<squnion> z) * x \<le> y

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(w \<squnion> z) * x \<le> y

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by (metis assms(1) dual_order.trans mult_left_one mult_left_isotone)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma case_split_left_equal:
  "w \<squnion> z = 1 \<Longrightarrow> w * x = w * y \<Longrightarrow> z * x = z * y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<squnion> z = (1::'a); w * x = w * y; z * x = z * y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (metis mult_left_one mult_right_dist_sup)