[STATEMENT]
lemma right_total_semigroup_add_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "right_total A" "bi_unique A"
  shows "((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add
[PROOF STEP]
proof (intro rel_funI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (A ===> A ===> A) x y \<Longrightarrow> semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (A ===> A ===> A) x y \<Longrightarrow> semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
assume xy[transfer_rule]: "(A ===> A ===> A) x y"
[PROOF STATE]
proof (state)
this:
(A ===> A ===> A) x y

goal (1 subgoal):
 1. \<And>x y. (A ===> A ===> A) x y \<Longrightarrow> semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
show "semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y
[PROOF STEP]
unfolding semigroup_add_on_with_def class.semigroup_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>a b c. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> c \<in> Collect (Domainp A) \<longrightarrow> x (x a b) c = x a (x b c)) \<and> (\<forall>a b. a \<in> Collect (Domainp A) \<longrightarrow> b \<in> Collect (Domainp A) \<longrightarrow> x a b \<in> Collect (Domainp A))) = (\<forall>a b c. y (y a b) c = y a (y b c))
[PROOF STEP]
by transfer (auto intro!: Domainp_apply2I[OF xy])
[PROOF STATE]
proof (state)
this:
semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y

goal:
No subgoals!
[PROOF STEP]
qed