[STATEMENT]
theorem (in field)
  assumes "finite S"
  assumes "S \<subseteq> carrier R"
  assumes "f ` S \<subseteq> carrier R"
  shows
    interpolate_poly: "interpolate S f \<in> carrier (poly_ring R)" and
    interpolate_degree: "degree (interpolate S f) \<le> card S - 1" and
    interpolate_eval: "\<And>s. s \<in> S \<Longrightarrow> eval (interpolate S f) s = f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpolate S f \<in> carrier (poly_ring R) &&& degree (interpolate S f) \<le> card S - 1 &&& (\<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. interpolate S f \<in> carrier (poly_ring R)
 2. degree (interpolate S f) \<le> card S - 1
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
interpret r:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. interpolate S f \<in> carrier (poly_ring R)
 2. degree (interpolate S f) \<le> card S - 1
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have a:"\<And>x. x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {x}) x \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {x}) x \<in> carrier (poly_ring R)
[PROOF STEP]
by (meson lagrange_poly assms Diff_iff finite_Diff in_mono insertI1 subset_insertI2 subset_insert_iff)
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {?x}) ?x \<in> carrier (poly_ring R)

goal (3 subgoals):
 1. interpolate S f \<in> carrier (poly_ring R)
 2. degree (interpolate S f) \<le> card S - 1
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have b:"\<And>x. x \<in> S \<Longrightarrow> f x \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> f x \<in> carrier R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
S \<subseteq> carrier R
f ` S \<subseteq> carrier R

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> f x \<in> carrier R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> f ?x \<in> carrier R

goal (3 subgoals):
 1. interpolate S f \<in> carrier (poly_ring R)
 2. degree (interpolate S f) \<le> card S - 1
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have c:"\<And>x. x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {x}) x) \<le> card S - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {x}) x) \<le> card S - 1
[PROOF STEP]
by (metis (full_types) lagrange_degree  DiffI Diff_insert_absorb assms(1) assms(2)
        card_Diff_singleton finite_insert insert_subset mk_disjoint_insert)
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {?x}) ?x) \<le> card S - 1

goal (3 subgoals):
 1. interpolate S f \<in> carrier (poly_ring R)
 2. degree (interpolate S f) \<le> card S - 1
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have d: "\<And>x. x \<in> S \<Longrightarrow>
    degree (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) \<le> (card S - 1) + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) \<le> card S - 1 + 0
[PROOF STEP]
using poly_of_const_in_carrier[OF b] poly_mult_degree_le[OF a] c poly_of_const_def
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> S \<Longrightarrow> poly_of_const (f ?x1) \<in> carrier (poly_ring R)
\<lbrakk>?x1 \<in> S; ?y \<in> carrier (poly_ring R); degree (lagrange_basis_polynomial (S - {?x1}) ?x1) \<le> ?n; degree ?y \<le> ?m\<rbrakk> \<Longrightarrow> degree (lagrange_basis_polynomial (S - {?x1}) ?x1 \<otimes>\<^bsub>poly_ring R\<^esub> ?y) \<le> ?n + ?m
?x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {?x}) ?x) \<le> card S - 1
poly_of_const = (\<lambda>k. local.normalize [k])

goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) \<le> card S - 1 + 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> degree (lagrange_basis_polynomial (S - {?x}) ?x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f ?x)) \<le> card S - 1 + 0

goal (3 subgoals):
 1. interpolate S f \<in> carrier (poly_ring R)
 2. degree (interpolate S f) \<le> card S - 1
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
show "interpolate S f \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpolate S f \<in> carrier (poly_ring R)
[PROOF STEP]
using interpolate_def poly_of_const_in_carrier a b
[PROOF STATE]
proof (prove)
using this:
interpolate ?S ?f = (\<Oplus>\<^bsub>poly_ring R\<^esub>s\<in>?S. lagrange_basis_polynomial (?S - {s}) s \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (?f s))
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {?x}) ?x \<in> carrier (poly_ring R)
?x \<in> S \<Longrightarrow> f ?x \<in> carrier R

goal (1 subgoal):
 1. interpolate S f \<in> carrier (poly_ring R)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
interpolate S f \<in> carrier (poly_ring R)

goal (2 subgoals):
 1. degree (interpolate S f) \<le> card S - 1
 2. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
show "degree (interpolate S f) \<le> card S - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (interpolate S f) \<le> card S - 1
[PROOF STEP]
using poly_sum_degree_le[OF assms(1) d] poly_of_const_in_carrier[OF b] interpolate_def a
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> S \<Longrightarrow> ?x1 x \<in> S; \<And>x. x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {?x1 x}) (?x1 x) \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f (?x1 x)) \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (\<Oplus>\<^bsub>poly_ring R\<^esub>x\<in>S. lagrange_basis_polynomial (S - {?x1 x}) (?x1 x) \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f (?x1 x))) \<le> card S - 1 + 0
?x1 \<in> S \<Longrightarrow> poly_of_const (f ?x1) \<in> carrier (poly_ring R)
interpolate ?S ?f = (\<Oplus>\<^bsub>poly_ring R\<^esub>s\<in>?S. lagrange_basis_polynomial (?S - {s}) s \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (?f s))
?x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {?x}) ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (interpolate S f) \<le> card S - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (interpolate S f) \<le> card S - 1

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have e:"subring (carrier R) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subring (carrier R) R
[PROOF STEP]
using carrier_is_subring assms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
finite S
S \<subseteq> carrier R
f ` S \<subseteq> carrier R

goal (1 subgoal):
 1. subring (carrier R) R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subring (carrier R) R

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
show "\<And>s. s \<in> S \<Longrightarrow> eval (interpolate S f) s = f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
assume f:"s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
interpret s:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p s)
[PROOF STEP]
using eval_cring_hom[OF e] assms f
[PROOF STATE]
proof (prove)
using this:
?a \<in> carrier R \<Longrightarrow> ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p ?a)
finite S
S \<subseteq> carrier R
f ` S \<subseteq> carrier R
s \<in> S

goal (1 subgoal):
 1. ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have g:"\<And>i. i \<in> S \<Longrightarrow>
         eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s =
         (if s = i then f s else \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
assume i_in_S: "i \<in> S"
[PROOF STATE]
proof (state)
this:
i \<in> S

goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
have "eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s =
        eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i
[PROOF STEP]
using b i_in_S poly_of_const_in_carrier
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> f ?x \<in> carrier R
i \<in> S
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i
[PROOF STEP]
by (simp add: s.hom_mult[OF a] eval_poly_of_const)
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i

goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i

goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
have "... = (if s = i then f s else \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i = (if s = i then f s else \<zero>)
[PROOF STEP]
using b i_in_S poly_of_const_in_carrier assms f
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> f ?x \<in> carrier R
i \<in> S
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
finite S
S \<subseteq> carrier R
f ` S \<subseteq> carrier R
s \<in> S

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i = (if s = i then f s else \<zero>)
[PROOF STEP]
apply (cases "s=i", simp, subst lagrange_one, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> i; \<And>x. x \<in> S \<Longrightarrow> f x \<in> carrier R; i \<in> S; \<And>s. s \<in> carrier R \<Longrightarrow> poly_of_const s \<in> carrier (poly_ring R); finite S; S \<subseteq> carrier R; f ` S \<subseteq> carrier R; s \<in> S\<rbrakk> \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i = \<zero>
[PROOF STEP]
by (subst lagrange_zero, auto)
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial (S - {i}) i) s \<otimes> f i = (if s = i then f s else \<zero>)

goal (1 subgoal):
 1. \<And>i. i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
show
        "eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s =
         (if s = i then f s else \<zero>)"
[PROOF STATE]
proof (prove)
using this:
local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial (S - {i}) i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f i)) s = (if s = i then f s else \<zero>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {?i}) ?i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f ?i)) s = (if s = ?i then f s else \<zero>)

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have "eval (interpolate S f) s =
    (\<Oplus>x\<in>S. eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval (interpolate S f) s = (\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s)
[PROOF STEP]
using  poly_of_const_in_carrier[OF b] a e
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> S \<Longrightarrow> poly_of_const (f ?x1) \<in> carrier (poly_ring R)
?x \<in> S \<Longrightarrow> lagrange_basis_polynomial (S - {?x}) ?x \<in> carrier (poly_ring R)
subring (carrier R) R

goal (1 subgoal):
 1. local.eval (interpolate S f) s = (\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s)
[PROOF STEP]
by (simp add: interpolate_def s.hom_finsum[OF Pi_I] comp_def)
[PROOF STATE]
proof (state)
this:
local.eval (interpolate S f) s = (\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s)

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.eval (interpolate S f) s = (\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s)

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have "... =  (\<Oplus>x\<in>S. if s = x then f s else \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s) = (\<Oplus>x\<in>S. if s = x then f s else \<zero>)
[PROOF STEP]
using b g
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> f ?x \<in> carrier R
?i \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial (S - {?i}) ?i \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f ?i)) s = (if s = ?i then f s else \<zero>)

goal (1 subgoal):
 1. (\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s) = (\<Oplus>x\<in>S. if s = x then f s else \<zero>)
[PROOF STEP]
by (simp cong: finsum_cong)
[PROOF STATE]
proof (state)
this:
(\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s) = (\<Oplus>x\<in>S. if s = x then f s else \<zero>)

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>x\<in>S. local.eval (lagrange_basis_polynomial (S - {x}) x \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (f x)) s) = (\<Oplus>x\<in>S. if s = x then f s else \<zero>)

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
have "... = f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>x\<in>S. if s = x then f s else \<zero>) = f s
[PROOF STEP]
using finsum_singleton[OF f assms(1)] f assms
[PROOF STATE]
proof (prove)
using this:
?f \<in> S \<rightarrow> carrier R \<Longrightarrow> (\<Oplus>j\<in>S. if s = j then ?f j else \<zero>) = ?f s
s \<in> S
finite S
S \<subseteq> carrier R
f ` S \<subseteq> carrier R

goal (1 subgoal):
 1. (\<Oplus>x\<in>S. if s = x then f s else \<zero>) = f s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Oplus>x\<in>S. if s = x then f s else \<zero>) = f s

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (interpolate S f) s = f s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.eval (interpolate S f) s = f s
[PROOF STEP]
show "eval (interpolate S f) s = f s"
[PROOF STATE]
proof (prove)
using this:
local.eval (interpolate S f) s = f s

goal (1 subgoal):
 1. local.eval (interpolate S f) s = f s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.eval (interpolate S f) s = f s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?s \<in> S \<Longrightarrow> local.eval (interpolate S f) ?s = f ?s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cont_edom[THEN cont_compose, simp, cont2cont]:
  "cont (\<lambda> f. edom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont edom
[PROOF STEP]
apply (rule set_contI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. chain Y \<Longrightarrow> edom (\<Squnion>i. Y i) = \<Union> (edom ` range Y)
[PROOF STEP]
apply (auto simp add: edom_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Y x. \<lbrakk>chain Y; (\<Squnion>x. Y x) x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> \<exists>xa. Y xa x \<noteq> \<bottom>
 2. \<And>Y x xa. \<lbrakk>chain Y; Y xa x \<noteq> \<bottom>; (\<Squnion>x. Y x) x = \<bottom>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis ch2ch_fun lub_eq_bottom_iff lub_fun)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y x xa. \<lbrakk>chain Y; Y xa x \<noteq> \<bottom>; (\<Squnion>x. Y x) x = \<bottom>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis ch2ch_fun lub_eq_bottom_iff lub_fun)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bdia_bmod_comp: "(\<langle>R| f x) = \<otimes> (\<lambda>y x z. (x,y) \<in> R) f c1 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<langle>R| f x = \<otimes> (\<lambda>y x z. (x, y) \<in> R) f c1 x
[PROOF STEP]
by (simp add: bdia_def bmod_comp_def c1_def)


[STATEMENT]
lemma bmod_fdia_comp: "\<otimes> R f g x = |{(x,(y,z)) |x y z. R x y z}\<rangle> (\<lambda>(x,y). (f x) \<cdot> (g y)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<otimes> R f g x =  |{(x, y, z) |x y z. R x y z}\<rangle> (\<lambda>(x, y). f x \<cdot> g y) x
[PROOF STEP]
by (simp add: fdia_def bmod_comp_def)


[STATEMENT]
lemma bmod_fdia_comp_var:
  "\<otimes> R f g x = |{(x,(y,z)) |x y z. R x y z}\<rangle> (\<lambda>(x,y). (\<lambda>(v,w).(v \<cdot> w)) (f x,g y)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<otimes> R f g x =  |{(x, y, z) |x y z. R x y z}\<rangle> (\<lambda>(x, y). case (f x, g y) of (v, w) \<Rightarrow> v \<cdot> w) x
[PROOF STEP]
by (simp add: fdia_def bmod_comp_def)


[STATEMENT]
lemma fdia_im: "( |R\<rangle> f x) = \<Squnion>(f ` R `` {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |R\<rangle> f x = \<Squnion>(f ` R `` {x})
[PROOF STEP]
apply (simp add: fdia_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>{f y |y. (x, y) \<in> R} = \<Squnion>(f ` R `` {x})
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Squnion>{f y |y. (x, y) \<in> R} \<le> \<Squnion>(f ` R `` {x})
 2. \<Squnion>(f ` R `` {x}) \<le> \<Squnion>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (intro Sup_least, clarsimp simp: SUP_upper)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>(f ` R `` {x}) \<le> \<Squnion>{f y |y. (x, y) \<in> R}
[PROOF STEP]
by (intro SUP_least Sup_upper, force)


[STATEMENT]
lemma fdia_un_rel: "fdia (R \<union> S) = fdia R \<squnion> fdia S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdia (R \<union> S) = fdia R \<squnion> fdia S
[PROOF STEP]
apply (simp add: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xa.  |R \<union> S\<rangle> x xa =  |R\<rangle> x xa \<squnion>  |S\<rangle> x xa
[PROOF STEP]
by (clarsimp simp: fun_eq_iff fdia_im SUP_union Un_Image)


[STATEMENT]
lemma fdia_Un_rel: "( |\<Union>\<R>\<rangle> f x) = \<Squnion>{|R\<rangle> f x |R. R \<in> \<R>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |\<Union> \<R>\<rangle> f x = \<Squnion>{ |R\<rangle> f x |R. R \<in> \<R>}
[PROOF STEP]
apply (simp add: fdia_im)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>(f ` \<Union> \<R> `` {x}) = \<Squnion>{\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>}
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Squnion>(f ` \<Union> \<R> `` {x}) \<le> \<Squnion>{\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>}
 2. \<Squnion>{\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>} \<le> \<Squnion>(f ` \<Union> \<R> `` {x})
[PROOF STEP]
apply (intro SUP_least, safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa X. \<lbrakk>(x, xa) \<in> X; X \<in> \<R>\<rbrakk> \<Longrightarrow> f xa \<le> \<Squnion>{\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>}
 2. \<Squnion>{\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>} \<le> \<Squnion>(f ` \<Union> \<R> `` {x})
[PROOF STEP]
apply (rule Sup_upper2, force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa X. \<lbrakk>(x, xa) \<in> X; X \<in> \<R>\<rbrakk> \<Longrightarrow> f xa \<le> \<Squnion>(f ` X `` {x})
 2. \<Squnion>{\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>} \<le> \<Squnion>(f ` \<Union> \<R> `` {x})
[PROOF STEP]
apply (rule SUP_upper, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>{\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>} \<le> \<Squnion>(f ` \<Union> \<R> `` {x})
[PROOF STEP]
apply (rule Sup_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {\<Squnion>(f ` R `` {x}) |R. R \<in> \<R>} \<Longrightarrow> xa \<le> \<Squnion>(f ` \<Union> \<R> `` {x})
[PROOF STEP]
by (clarsimp simp: Image_mono SUP_subset_mono Sup_upper)


[STATEMENT]
lemma fdia_sup_fun: "fdia R (f \<squnion> g) = fdia R f \<squnion> fdia R g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdia R (f \<squnion> g) = fdia R f \<squnion> fdia R g
[PROOF STEP]
by (simp add: fun_eq_iff fdia_im complete_lattice_class.SUP_sup_distrib)


[STATEMENT]
lemma fdia_Sup_fun: "( |R\<rangle> (\<Squnion>\<F>) x) = \<Squnion>{|R\<rangle> f x |f. f \<in> \<F>} "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |R\<rangle> \<Squnion>\<F> x = \<Squnion>{ |R\<rangle> f x |f. f \<in> \<F>}
[PROOF STEP]
apply (simp add: fdia_im)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x) = \<Squnion>{\<Squnion>(f ` R `` {x}) |f. f \<in> \<F>}
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x) \<le> \<Squnion>{\<Squnion>(f ` R `` {x}) |f. f \<in> \<F>}
 2. \<Squnion>{\<Squnion>(f ` R `` {x}) |f. f \<in> \<F>} \<le> (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x)
[PROOF STEP]
apply (rule SUP_least)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa f. \<lbrakk>xa \<in> R `` {x}; f \<in> \<F>\<rbrakk> \<Longrightarrow> f xa \<le> \<Squnion>{\<Squnion>(f ` R `` {x}) |f. f \<in> \<F>}
 2. \<Squnion>{\<Squnion>(f ` R `` {x}) |f. f \<in> \<F>} \<le> (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x)
[PROOF STEP]
apply (rule Sup_upper2, force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa f. \<lbrakk>xa \<in> R `` {x}; f \<in> \<F>\<rbrakk> \<Longrightarrow> f xa \<le> \<Squnion>(f ` R `` {x})
 2. \<Squnion>{\<Squnion>(f ` R `` {x}) |f. f \<in> \<F>} \<le> (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x)
[PROOF STEP]
apply (rule SUP_upper, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>{\<Squnion>(f ` R `` {x}) |f. f \<in> \<F>} \<le> (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x)
[PROOF STEP]
apply (rule Sup_least, safe)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa f. f \<in> \<F> \<Longrightarrow> \<Squnion>(f ` R `` {x}) \<le> (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x)
[PROOF STEP]
apply (rule SUP_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa f xaa. \<lbrakk>f \<in> \<F>; xaa \<in> R `` {x}\<rbrakk> \<Longrightarrow> f xaa \<le> (SUP x\<in>R `` {x}. SUP f\<in>\<F>. f x)
[PROOF STEP]
by (simp add: SUP_upper2)


[STATEMENT]
lemma fdia_seq: "fdia (R ; S) f x  = fdia R (fdia S f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |R ; S\<rangle> f x =  |R\<rangle> fdia S f x
[PROOF STEP]
by (simp add: fdia_im relcomp_Image, metis Image_eq_UN SUP_UNION)


[STATEMENT]
lemma fdia_Id [simp]: "( |Id\<rangle> f x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |Id\<rangle> f x = f x
[PROOF STEP]
by (simp add: fdia_def)


[STATEMENT]
lemma fdia_fbox_demorgan: "( |R\<rangle> (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - |R] (\<lambda>y. -f y) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |R\<rangle> f x = - |R] (\<lambda>y. - f y) x
[PROOF STEP]
apply (simp add: fbox_def fdia_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>{f y |y. (x, y) \<in> R} = - \<Sqinter>{- f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Squnion>{f y |y. (x, y) \<in> R} \<le> - \<Sqinter>{- f y |y. (x, y) \<in> R}
 2. - \<Sqinter>{- f y |y. (x, y) \<in> R} \<le> \<Squnion>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (rule Sup_least)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {f y |y. (x, y) \<in> R} \<Longrightarrow> xa \<le> - \<Sqinter>{- f y |y. (x, y) \<in> R}
 2. - \<Sqinter>{- f y |y. (x, y) \<in> R} \<le> \<Squnion>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (simp add: Inf_lower compl_le_swap1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<Sqinter>{- f y |y. (x, y) \<in> R} \<le> \<Squnion>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (simp add: uminus_Inf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>(uminus ` {- f y |y. (x, y) \<in> R}) \<le> \<Squnion>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (rule SUP_least; intro Sup_upper)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {- f y |y. (x, y) \<in> R} \<Longrightarrow> - xa \<in> {f y |y. (x, y) \<in> R}
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_fdia_demorgan: "( |R] (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - |R\<rangle> (\<lambda>y. -f y) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |R] f x = -  |R\<rangle> (\<lambda>y. - f y) x
[PROOF STEP]
apply (simp add: fbox_def fdia_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter>{f y |y. (x, y) \<in> R} = - \<Squnion>{- f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Sqinter>{f y |y. (x, y) \<in> R} \<le> - \<Squnion>{- f y |y. (x, y) \<in> R}
 2. - \<Squnion>{- f y |y. (x, y) \<in> R} \<le> \<Sqinter>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (simp add: uminus_Sup)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Sqinter>{f y |y. (x, y) \<in> R} \<le> \<Sqinter>(uminus ` {- f y |y. (x, y) \<in> R})
 2. - \<Squnion>{- f y |y. (x, y) \<in> R} \<le> \<Sqinter>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (rule INF_greatest; rule Inf_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {- f y |y. (x, y) \<in> R} \<Longrightarrow> - xa \<in> {f y |y. (x, y) \<in> R}
 2. - \<Squnion>{- f y |y. (x, y) \<in> R} \<le> \<Sqinter>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<Squnion>{- f y |y. (x, y) \<in> R} \<le> \<Sqinter>{f y |y. (x, y) \<in> R}
[PROOF STEP]
apply (rule Inf_greatest)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {f y |y. (x, y) \<in> R} \<Longrightarrow> - \<Squnion>{- f y |y. (x, y) \<in> R} \<le> xa
[PROOF STEP]
by (simp add: Sup_upper compl_le_swap2)


[STATEMENT]
lemma bdia_bbox_demorgan: "(\<langle>R| (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - [R| (\<lambda>y. -f y) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<langle>R| f x = - [R| (\<lambda>y. - f y) x
[PROOF STEP]
apply (simp add: bbox_def bdia_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>{f xa |xa. (xa, x) \<in> R} = - \<Sqinter>{- f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Squnion>{f xa |xa. (xa, x) \<in> R} \<le> - \<Sqinter>{- f xa |xa. (xa, x) \<in> R}
 2. - \<Sqinter>{- f xa |xa. (xa, x) \<in> R} \<le> \<Squnion>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (rule Sup_least)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {f xa |xa. (xa, x) \<in> R} \<Longrightarrow> xa \<le> - \<Sqinter>{- f xa |xa. (xa, x) \<in> R}
 2. - \<Sqinter>{- f xa |xa. (xa, x) \<in> R} \<le> \<Squnion>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (simp add: Inf_lower compl_le_swap1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<Sqinter>{- f xa |xa. (xa, x) \<in> R} \<le> \<Squnion>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (simp add: uminus_Inf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion>(uminus ` {- f xa |xa. (xa, x) \<in> R}) \<le> \<Squnion>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (rule SUP_least; intro Sup_upper)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {- f xa |xa. (xa, x) \<in> R} \<Longrightarrow> - xa \<in> {f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
by auto


[STATEMENT]
lemma bbox_bdia_demorgan: "( [R| (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - \<langle>R| (\<lambda>y. -f y) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [R| f x = -  \<langle>R| (\<lambda>y. - f y) x
[PROOF STEP]
apply (simp add: bbox_def bdia_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter>{f xa |xa. (xa, x) \<in> R} = - \<Squnion>{- f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Sqinter>{f xa |xa. (xa, x) \<in> R} \<le> - \<Squnion>{- f xa |xa. (xa, x) \<in> R}
 2. - \<Squnion>{- f xa |xa. (xa, x) \<in> R} \<le> \<Sqinter>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (simp add: uminus_Sup)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Sqinter>{f xa |xa. (xa, x) \<in> R} \<le> \<Sqinter>(uminus ` {- f xa |xa. (xa, x) \<in> R})
 2. - \<Squnion>{- f xa |xa. (xa, x) \<in> R} \<le> \<Sqinter>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (rule INF_greatest; rule Inf_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {- f xa |xa. (xa, x) \<in> R} \<Longrightarrow> - xa \<in> {f xa |xa. (xa, x) \<in> R}
 2. - \<Squnion>{- f xa |xa. (xa, x) \<in> R} \<le> \<Sqinter>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<Squnion>{- f xa |xa. (xa, x) \<in> R} \<le> \<Sqinter>{f xa |xa. (xa, x) \<in> R}
[PROOF STEP]
apply (rule Inf_greatest)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {f xa |xa. (xa, x) \<in> R} \<Longrightarrow> - \<Squnion>{- f xa |xa. (xa, x) \<in> R} \<le> xa
[PROOF STEP]
by (simp add: Sup_upper compl_le_swap2)


[STATEMENT]
lemma fdia_bdia_conv: "( |R\<rangle> f x) = \<langle>converse R| f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  |R\<rangle> f x =  \<langle>R\<inverse>| f x
[PROOF STEP]
by (simp add: fdia_def bdia_def)


[STATEMENT]
lemma fbox_bbox_conv: "( |R] f x) = [converse R| f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |R] f x = [R\<inverse>| f x
[PROOF STEP]
by (simp add: fbox_def bbox_def)


[STATEMENT]
lemma fdia_bbox_galois: "(\<forall>x. ( |R\<rangle> f x) \<le> g x) \<longleftrightarrow> (\<forall>x. f x \<le> [R| g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x.  |R\<rangle> f x \<le> g x) = (\<forall>x. f x \<le> [R| g x)
[PROOF STEP]
apply (standard, simp_all add: fdia_def bbox_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x. \<Squnion>{f y |y. (x, y) \<in> R} \<le> g x \<Longrightarrow> \<forall>x. f x \<le> \<Sqinter>{g xa |xa. (xa, x) \<in> R}
 2. \<forall>x. f x \<le> \<Sqinter>{g xa |xa. (xa, x) \<in> R} \<Longrightarrow> \<forall>x. \<Squnion>{f y |y. (x, y) \<in> R} \<le> g x
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>x. \<Squnion>{f y |y. (x, y) \<in> R} \<le> g x \<Longrightarrow> f x \<le> \<Sqinter>{g xa |xa. (xa, x) \<in> R}
 2. \<And>x. \<forall>x. f x \<le> \<Sqinter>{g xa |xa. (xa, x) \<in> R} \<Longrightarrow> \<Squnion>{f y |y. (x, y) \<in> R} \<le> g x
[PROOF STEP]
apply (rule Inf_greatest)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>x. \<Squnion>{f y |y. (x, y) \<in> R} \<le> g x; xa \<in> {g xa |xa. (xa, x) \<in> R}\<rbrakk> \<Longrightarrow> f x \<le> xa
 2. \<And>x. \<forall>x. f x \<le> \<Sqinter>{g xa |xa. (xa, x) \<in> R} \<Longrightarrow> \<Squnion>{f y |y. (x, y) \<in> R} \<le> g x
[PROOF STEP]
apply (force simp: Sup_le_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x. f x \<le> \<Sqinter>{g xa |xa. (xa, x) \<in> R} \<Longrightarrow> \<Squnion>{f y |y. (x, y) \<in> R} \<le> g x
[PROOF STEP]
apply (rule Sup_least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>x. f x \<le> \<Sqinter>{g xa |xa. (xa, x) \<in> R}; xa \<in> {f y |y. (x, y) \<in> R}\<rbrakk> \<Longrightarrow> xa \<le> g x
[PROOF STEP]
by (force simp: le_Inf_iff)


[STATEMENT]
lemma dia_conjugate:
  "(\<forall>x. ( |R\<rangle> (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) \<sqinter> g x = \<bottom>) \<longleftrightarrow> (\<forall>x. f x \<sqinter> (\<langle>R| g x) = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x.  |R\<rangle> f x \<sqinter> g x = \<bottom>) = (\<forall>x. f x \<sqinter>  \<langle>R| g x = \<bottom>)
[PROOF STEP]
by (simp add: meet_shunt fdia_bbox_galois bdia_bbox_demorgan)


[STATEMENT]
lemma box_conjugate:
  "(\<forall>x. ( |R] (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) \<squnion> g x = \<top>) \<longleftrightarrow> (\<forall>x. f x \<squnion> ([R| g x) = \<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
have "(\<forall>x. ( |R] f x) \<squnion> g x = \<top>) \<longleftrightarrow> (\<forall>x. -g x \<le> |R] f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. - g x \<le> |R] f x)
[PROOF STEP]
by (simp add: join_shunt sup_commute)
[PROOF STATE]
proof (state)
this:
(\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. - g x \<le> |R] f x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. - g x \<le> |R] f x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>x. -g x \<le> - |R\<rangle> (\<lambda>y. -f y) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. - g x \<le> |R] f x) = (\<forall>x. - g x \<le> -  |R\<rangle> (\<lambda>y. - f y) x)
[PROOF STEP]
by (simp add: fbox_fdia_demorgan)
[PROOF STATE]
proof (state)
this:
(\<forall>x. - g x \<le> |R] f x) = (\<forall>x. - g x \<le> -  |R\<rangle> (\<lambda>y. - f y) x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x. - g x \<le> |R] f x) = (\<forall>x. - g x \<le> -  |R\<rangle> (\<lambda>y. - f y) x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>x. ( |R\<rangle> (\<lambda>y. -f y) x) \<le> g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. - g x \<le> -  |R\<rangle> (\<lambda>y. - f y) x) = (\<forall>x.  |R\<rangle> (\<lambda>y. - f y) x \<le> g x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. - g x \<le> -  |R\<rangle> (\<lambda>y. - f y) x) = (\<forall>x.  |R\<rangle> (\<lambda>y. - f y) x \<le> g x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>x. - g x \<le> -  |R\<rangle> (\<lambda>y. - f y) x) = (\<forall>x.  |R\<rangle> (\<lambda>y. - f y) x \<le> g x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>x. -f x \<le> [R| g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x.  |R\<rangle> (\<lambda>y. - f y) x \<le> g x) = (\<forall>x. - f x \<le> [R| g x)
[PROOF STEP]
by (simp add: fdia_bbox_galois)
[PROOF STATE]
proof (state)
this:
(\<forall>x.  |R\<rangle> (\<lambda>y. - f y) x \<le> g x) = (\<forall>x. - f x \<le> [R| g x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. - f x \<le> [R| g x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. - f x \<le> [R| g x)

goal (1 subgoal):
 1. (\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)
[PROOF STEP]
by (simp add: join_shunt)
[PROOF STATE]
proof (state)
this:
(\<forall>x. |R] f x \<squnion> g x = \<top>) = (\<forall>x. f x \<squnion> [R| g x = \<top>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (Var ''x'') = 26"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (\<epsilon> ''x'') = 26
[PROOF STEP]
by auto


[STATEMENT]
lemma "eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (Fun ''one'' []) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (Fun ''one'' []) = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma "eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (Fun ''mul'' [Var ''y'',Var ''y'']) = 25"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (Fun ''mul'' [\<epsilon> ''y'', \<epsilon> ''y'']) = 25
[PROOF STEP]
by auto


[STATEMENT]
lemma
  "eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''], Fun ''one'' []]) = 26"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>t E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t (Fun ''add'' [Fun ''mul'' [\<epsilon> ''y'', \<epsilon> ''y''], Fun ''one'' []]) = 26
[PROOF STEP]
by auto


[STATEMENT]
lemma "eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t (Pos ''greater'' [Var ''x'', Var ''y'']) = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t (Pos ''greater'' [\<epsilon> ''x'', \<epsilon> ''y'']) = True
[PROOF STEP]
by auto


[STATEMENT]
lemma "eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t (Neg ''less'' [Var ''x'', Var ''y'']) = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t (Neg ''less'' [\<epsilon> ''x'', \<epsilon> ''y'']) = True
[PROOF STEP]
by auto


[STATEMENT]
lemma "eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t (Pos ''less'' [Var ''x'', Var ''y'']) = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t (Pos ''less'' [\<epsilon> ''x'', \<epsilon> ''y'']) = False
[PROOF STEP]
by auto


[STATEMENT]
lemma "eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t
       (Pos ''equals''
         [Fun ''add'' [Fun ''mul'' [Var ''y'',Var ''y''],Fun ''one'' []]
         ,Var ''x'']
       ) = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval\<^sub>l E\<^sub>n\<^sub>a\<^sub>t F\<^sub>n\<^sub>a\<^sub>t G\<^sub>n\<^sub>a\<^sub>t (Pos ''equals'' [Fun ''add'' [Fun ''mul'' [\<epsilon> ''y'', \<epsilon> ''y''], Fun ''one'' []], \<epsilon> ''x'']) = True
[PROOF STEP]
by auto


[STATEMENT]
theorem empty_mgu:
  assumes "unifier\<^sub>l\<^sub>s \<epsilon> L"
  shows "mgu\<^sub>l\<^sub>s \<epsilon> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s \<epsilon> L
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s \<epsilon> L

goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s \<epsilon> L
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def mgu\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<epsilon> = l'

goal (1 subgoal):
 1. (\<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l \<epsilon> = l') \<and> (\<forall>u. (\<exists>l'. \<forall>l\<in>L. l \<cdot>\<^sub>l u = l') \<longrightarrow> (\<exists>i. u = \<epsilon> \<cdot> i))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l' u l'a. \<lbrakk>\<forall>l\<in>L. l \<cdot>\<^sub>l \<epsilon> = l'; \<forall>l\<in>L. l \<cdot>\<^sub>l u = l'a\<rbrakk> \<Longrightarrow> \<exists>i. u = \<epsilon> \<cdot> i
[PROOF STEP]
apply (rule_tac x=u in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l' u l'a. \<lbrakk>\<forall>l\<in>L. l \<cdot>\<^sub>l \<epsilon> = l'; \<forall>l\<in>L. l \<cdot>\<^sub>l u = l'a\<rbrakk> \<Longrightarrow> u = \<epsilon> \<cdot> u
[PROOF STEP]
using empty_comp1 empty_comp2
[PROOF STATE]
proof (prove)
using this:
?\<sigma> \<cdot> \<epsilon> = ?\<sigma>
\<epsilon> \<cdot> ?\<sigma> = ?\<sigma>

goal (1 subgoal):
 1. \<And>l' u l'a. \<lbrakk>\<forall>l\<in>L. l \<cdot>\<^sub>l \<epsilon> = l'; \<forall>l\<in>L. l \<cdot>\<^sub>l u = l'a\<rbrakk> \<Longrightarrow> u = \<epsilon> \<cdot> u
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem unifier_single: "unifier\<^sub>l\<^sub>s \<sigma> {l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s \<sigma> {l}
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. \<forall>l\<in>{l}. l \<cdot>\<^sub>l \<sigma> = l'
[PROOF STEP]
by auto


[STATEMENT]
theorem resolution_rule':
  assumes "C\<^sub>1 \<in> Cs"
  assumes "C\<^sub>2 \<in> Cs"
  assumes "applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>"
  assumes "C = {resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>}"
  shows "resolution_step Cs (Cs \<union> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_step Cs (Cs \<union> C)
[PROOF STEP]
using assms resolution_rule
[PROOF STATE]
proof (prove)
using this:
C\<^sub>1 \<in> Cs
C\<^sub>2 \<in> Cs
applicable C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>
C = {resolution C\<^sub>1 C\<^sub>2 L\<^sub>1 L\<^sub>2 \<sigma>}
\<lbrakk>?C\<^sub>1 \<in> ?Cs; ?C\<^sub>2 \<in> ?Cs; applicable ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>\<rbrakk> \<Longrightarrow> resolution_step ?Cs (?Cs \<union> {resolution ?C\<^sub>1 ?C\<^sub>2 ?L\<^sub>1 ?L\<^sub>2 ?\<sigma>})

goal (1 subgoal):
 1. resolution_step Cs (Cs \<union> C)
[PROOF STEP]
by auto


[STATEMENT]
lemma resolution_example1:
   "resolution_deriv {{NP,PQ},{NQ},{PP,PQ}}
                              {{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
have "resolution_step
          {{NP,PQ},{NQ},{PP,PQ}}
         ({{NP,PQ},{NQ},{PP,PQ}} \<union> {{NP}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} ({{NP, PQ}, {NQ}, {PP, PQ}} \<union> {{NP}})
[PROOF STEP]
apply (rule resolution_rule'[of "{NP,PQ}" _ "{NQ}" "{PQ}" "{NQ}" \<epsilon>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {NP, PQ} \<in> {{NP, PQ}, {NQ}, {PP, PQ}}
 2. {NQ} \<in> {{NP, PQ}, {NQ}, {PP, PQ}}
 3. applicable {NP, PQ} {NQ} {PQ} {NQ} \<epsilon>
 4. {{NP}} = {resolution {NP, PQ} {NQ} {PQ} {NQ} \<epsilon>}
[PROOF STEP]
unfolding applicable_def vars\<^sub>l\<^sub>s_def  vars\<^sub>l_def
              NQ_def NP_def PQ_def PP_def resolution_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}}
 2. {Neg ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}}
 3. {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Neg ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<and> {Neg ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''Q'' [Fun ''d'' []]} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Pos ''Q'' [Fun ''d'' []]} \<union> {Neg ''Q'' [Fun ''d'' []]}\<^sup>C)
 4. {{Neg ''P'' [Fun ''c'' []]}} = {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} - {Pos ''Q'' [Fun ''d'' []]} \<union> ({Neg ''Q'' [Fun ''d'' []]} - {Neg ''Q'' [Fun ''d'' []]}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
using unifier_single empty_mgu
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s ?\<sigma> {?l}
unifier\<^sub>l\<^sub>s \<epsilon> ?L \<Longrightarrow> mgu\<^sub>l\<^sub>s \<epsilon> ?L

goal (4 subgoals):
 1. {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}}
 2. {Neg ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}}
 3. {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Neg ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<and> {Neg ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''Q'' [Fun ''d'' []]} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Pos ''Q'' [Fun ''d'' []]} \<union> {Neg ''Q'' [Fun ''d'' []]}\<^sup>C)
 4. {{Neg ''P'' [Fun ''c'' []]}} = {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} - {Pos ''Q'' [Fun ''d'' []]} \<union> ({Neg ''Q'' [Fun ''d'' []]} - {Neg ''Q'' [Fun ''d'' []]}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
using empty_subls
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s ?\<sigma> {?l}
unifier\<^sub>l\<^sub>s \<epsilon> ?L \<Longrightarrow> mgu\<^sub>l\<^sub>s \<epsilon> ?L
?L \<cdot>\<^sub>l\<^sub>s \<epsilon> = ?L

goal (4 subgoals):
 1. {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}}
 2. {Neg ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}}
 3. {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Neg ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<and> {Neg ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''Q'' [Fun ''d'' []]} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Pos ''Q'' [Fun ''d'' []]} \<union> {Neg ''Q'' [Fun ''d'' []]}\<^sup>C)
 4. {{Neg ''P'' [Fun ''c'' []]}} = {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} - {Pos ''Q'' [Fun ''d'' []]} \<union> ({Neg ''Q'' [Fun ''d'' []]} - {Neg ''Q'' [Fun ''d'' []]}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} ({{NP, PQ}, {NQ}, {PP, PQ}} \<union> {{NP}})

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} ({{NP, PQ}, {NQ}, {PP, PQ}} \<union> {{NP}})
[PROOF STEP]
have "resolution_step
          {{NP,PQ},{NQ},{PP,PQ}}
         ({{NP,PQ},{NQ},{PP,PQ},{NP}})"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} ({{NP, PQ}, {NQ}, {PP, PQ}} \<union> {{NP}})

goal (1 subgoal):
 1. resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP}} \<union> {{PP}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}} \<union> {{PP}})
[PROOF STEP]
apply (rule resolution_rule'[of "{NQ}" _ "{PP,PQ}" "{NQ}" "{PQ}" \<epsilon>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {NQ} \<in> {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}
 2. {PP, PQ} \<in> {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}
 3. applicable {NQ} {PP, PQ} {NQ} {PQ} \<epsilon>
 4. {{PP}} = {resolution {NQ} {PP, PQ} {NQ} {PQ} \<epsilon>}
[PROOF STEP]
unfolding applicable_def vars\<^sub>l\<^sub>s_def  vars\<^sub>l_def
              NQ_def NP_def PQ_def PP_def resolution_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Neg ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}}
 2. {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}}
 3. {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''Q'' [Fun ''d'' []]} \<and> {Pos ''Q'' [Fun ''d'' []]} \<subseteq> {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''Q'' [Fun ''d'' []]} \<union> {Pos ''Q'' [Fun ''d'' []]}\<^sup>C)
 4. {{Pos ''P'' [Fun ''c'' []]}} = {{Neg ''Q'' [Fun ''d'' []]} - {Neg ''Q'' [Fun ''d'' []]} \<union> ({Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} - {Pos ''Q'' [Fun ''d'' []]}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
using unifier_single empty_mgu empty_subls
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s ?\<sigma> {?l}
unifier\<^sub>l\<^sub>s \<epsilon> ?L \<Longrightarrow> mgu\<^sub>l\<^sub>s \<epsilon> ?L
?L \<cdot>\<^sub>l\<^sub>s \<epsilon> = ?L

goal (4 subgoals):
 1. {Neg ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}}
 2. {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}}
 3. {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> {Pos ''Q'' [Fun ''d'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''Q'' [Fun ''d'' []]} \<subseteq> {Neg ''Q'' [Fun ''d'' []]} \<and> {Pos ''Q'' [Fun ''d'' []]} \<subseteq> {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''Q'' [Fun ''d'' []]} \<union> {Pos ''Q'' [Fun ''d'' []]}\<^sup>C)
 4. {{Pos ''P'' [Fun ''c'' []]}} = {{Neg ''Q'' [Fun ''d'' []]} - {Neg ''Q'' [Fun ''d'' []]} \<union> ({Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]} - {Pos ''Q'' [Fun ''d'' []]}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}} \<union> {{PP}})

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}} \<union> {{PP}})
[PROOF STEP]
have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP}})"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}} \<union> {{PP}})

goal (1 subgoal):
 1. resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP},{PP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP}} \<union> {{}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} \<union> {{}})
[PROOF STEP]
apply (rule resolution_rule'[of "{NP}" _ "{PP}" "{NP}" "{PP}" \<epsilon>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {NP} \<in> {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}
 2. {PP} \<in> {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}
 3. applicable {NP} {PP} {NP} {PP} \<epsilon>
 4. {{}} = {resolution {NP} {PP} {NP} {PP} \<epsilon>}
[PROOF STEP]
unfolding applicable_def vars\<^sub>l\<^sub>s_def  vars\<^sub>l_def
              NQ_def NP_def PQ_def PP_def resolution_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Neg ''P'' [Fun ''c'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}, {Pos ''P'' [Fun ''c'' []]}}
 2. {Pos ''P'' [Fun ''c'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}, {Pos ''P'' [Fun ''c'' []]}}
 3. {Neg ''P'' [Fun ''c'' []]} \<noteq> {} \<and> {Pos ''P'' [Fun ''c'' []]} \<noteq> {} \<and> {Neg ''P'' [Fun ''c'' []]} \<noteq> {} \<and> {Pos ''P'' [Fun ''c'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''P'' [Fun ''c'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Pos ''P'' [Fun ''c'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''P'' [Fun ''c'' []]} \<subseteq> {Neg ''P'' [Fun ''c'' []]} \<and> {Pos ''P'' [Fun ''c'' []]} \<subseteq> {Pos ''P'' [Fun ''c'' []]} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''P'' [Fun ''c'' []]} \<union> {Pos ''P'' [Fun ''c'' []]}\<^sup>C)
 4. {{}} = {{Neg ''P'' [Fun ''c'' []]} - {Neg ''P'' [Fun ''c'' []]} \<union> ({Pos ''P'' [Fun ''c'' []]} - {Pos ''P'' [Fun ''c'' []]}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
using unifier_single empty_mgu
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s ?\<sigma> {?l}
unifier\<^sub>l\<^sub>s \<epsilon> ?L \<Longrightarrow> mgu\<^sub>l\<^sub>s \<epsilon> ?L

goal (4 subgoals):
 1. {Neg ''P'' [Fun ''c'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}, {Pos ''P'' [Fun ''c'' []]}}
 2. {Pos ''P'' [Fun ''c'' []]} \<in> {{Neg ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''Q'' [Fun ''d'' []]}, {Pos ''P'' [Fun ''c'' []], Pos ''Q'' [Fun ''d'' []]}, {Neg ''P'' [Fun ''c'' []]}, {Pos ''P'' [Fun ''c'' []]}}
 3. {Neg ''P'' [Fun ''c'' []]} \<noteq> {} \<and> {Pos ''P'' [Fun ''c'' []]} \<noteq> {} \<and> {Neg ''P'' [Fun ''c'' []]} \<noteq> {} \<and> {Pos ''P'' [Fun ''c'' []]} \<noteq> {} \<and> (\<Union>l\<in>{Neg ''P'' [Fun ''c'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) \<inter> (\<Union>l\<in>{Pos ''P'' [Fun ''c'' []]}. vars\<^sub>t\<^sub>s (get_terms l)) = {} \<and> {Neg ''P'' [Fun ''c'' []]} \<subseteq> {Neg ''P'' [Fun ''c'' []]} \<and> {Pos ''P'' [Fun ''c'' []]} \<subseteq> {Pos ''P'' [Fun ''c'' []]} \<and> mgu\<^sub>l\<^sub>s \<epsilon> ({Neg ''P'' [Fun ''c'' []]} \<union> {Pos ''P'' [Fun ''c'' []]}\<^sup>C)
 4. {{}} = {{Neg ''P'' [Fun ''c'' []]} - {Neg ''P'' [Fun ''c'' []]} \<union> ({Pos ''P'' [Fun ''c'' []]} - {Pos ''P'' [Fun ''c'' []]}) \<cdot>\<^sub>l\<^sub>s \<epsilon>}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} \<union> {{}})

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} \<union> {{}})
[PROOF STEP]
have "resolution_step
         {{NP,PQ},{NQ},{PP,PQ},{NP},{PP}}
        ({{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}})"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} ({{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} \<union> {{}})

goal (1 subgoal):
 1. resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
have "resolution_deriv {{NP,PQ},{NQ},{PP,PQ}}
                         {{NP,PQ},{NQ},{PP,PQ},{NP},{PP},{}}"
[PROOF STATE]
proof (prove)
using this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
unfolding resolution_deriv_def
[PROOF STATE]
proof (prove)
using this:
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}}
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}}
resolution_step {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}

goal (1 subgoal):
 1. resolution_step\<^sup>*\<^sup>* {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}

goal (1 subgoal):
 1. resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
resolution_deriv {{NP, PQ}, {NQ}, {PP, PQ}} {{NP, PQ}, {NQ}, {PP, PQ}, {NP}, {PP}, {}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mguPaaPax_mgu: "mgu\<^sub>l\<^sub>s mguPaaPax {Paa,Pax}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}
[PROOF STEP]
let ?\<sigma> = "\<lambda>x. if x = ''x'' then Fun ''a'' [] else Var x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}
[PROOF STEP]
have a: "unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else Var x) {Paa,Pax}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Paa, Pax}
[PROOF STEP]
unfolding Paa_def Pax_def unifier\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l'. \<forall>l\<in>{Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']}. l \<cdot>\<^sub>l (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) = l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Paa, Pax}

goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}
[PROOF STEP]
have b: "\<forall>u. unifier\<^sub>l\<^sub>s u {Paa,Pax} \<longrightarrow> (\<exists>i. u = ?\<sigma> \<cdot> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i)
[PROOF STEP]
proof (rule;rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<Longrightarrow> \<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<Longrightarrow> \<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i
[PROOF STEP]
assume "unifier\<^sub>l\<^sub>s u {Paa,Pax}"
[PROOF STATE]
proof (state)
this:
unifier\<^sub>l\<^sub>s u {Paa, Pax}

goal (1 subgoal):
 1. \<And>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<Longrightarrow> \<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s u {Paa, Pax}
[PROOF STEP]
have uuu: "u ''x'' = Fun ''a'' []"
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s u {Paa, Pax}

goal (1 subgoal):
 1. u ''x'' = Fun ''a'' []
[PROOF STEP]
unfolding unifier\<^sub>l\<^sub>s_def Paa_def Pax_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l'. \<forall>l\<in>{Pos ''a'' [Fun ''a'' []], Pos ''a'' [\<epsilon> ''x'']}. l \<cdot>\<^sub>l u = l'

goal (1 subgoal):
 1. u ''x'' = Fun ''a'' []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u ''x'' = Fun ''a'' []

goal (1 subgoal):
 1. \<And>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<Longrightarrow> \<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i
[PROOF STEP]
have "?\<sigma> \<cdot> u = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u = u
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
assume "x=''x''"
[PROOF STATE]
proof (state)
this:
x = ''x''

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = ''x''

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
have "(?\<sigma> \<cdot> u) ''x'' =  Fun ''a'' []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) ''x'' = Fun ''a'' []
[PROOF STEP]
unfolding composition_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ''x'' = ''x'' then Fun ''a'' [] else \<epsilon> ''x'') \<cdot>\<^sub>t u = Fun ''a'' []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) ''x'' = Fun ''a'' []

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = ''x''
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) ''x'' = Fun ''a'' []
[PROOF STEP]
have "(?\<sigma> \<cdot> u) x = u x"
[PROOF STATE]
proof (prove)
using this:
x = ''x''
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) ''x'' = Fun ''a'' []

goal (1 subgoal):
 1. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
using uuu
[PROOF STATE]
proof (prove)
using this:
x = ''x''
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) ''x'' = Fun ''a'' []
u ''x'' = Fun ''a'' []

goal (1 subgoal):
 1. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x = ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x = ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
assume "x\<noteq>''x''"
[PROOF STATE]
proof (state)
this:
x \<noteq> ''x''

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> ''x''
[PROOF STEP]
have "(?\<sigma> \<cdot> u) x = (\<epsilon> x) \<cdot>\<^sub>t u"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> ''x''

goal (1 subgoal):
 1. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = \<epsilon> x \<cdot>\<^sub>t u
[PROOF STEP]
unfolding composition_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> ''x''

goal (1 subgoal):
 1. (if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot>\<^sub>t u = \<epsilon> x \<cdot>\<^sub>t u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = \<epsilon> x \<cdot>\<^sub>t u

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = \<epsilon> x \<cdot>\<^sub>t u
[PROOF STEP]
have "(?\<sigma> \<cdot> u) x = u x"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = \<epsilon> x \<cdot>\<^sub>t u

goal (1 subgoal):
 1. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x \<noteq> ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal (1 subgoal):
 1. \<And>x. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
x \<noteq> ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
show "(?\<sigma> \<cdot> u) x = u x"
[PROOF STATE]
proof (prove)
using this:
x = ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
x \<noteq> ''x'' \<Longrightarrow> ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal (1 subgoal):
 1. ((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u) x = u x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u = u

goal (1 subgoal):
 1. \<And>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<Longrightarrow> \<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u = u
[PROOF STEP]
have "\<exists>i. ?\<sigma> \<cdot> i = u"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> u = u

goal (1 subgoal):
 1. \<exists>i. (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i = u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i = u

goal (1 subgoal):
 1. \<And>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<Longrightarrow> \<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i = u
[PROOF STEP]
show "\<exists>i. u = ?\<sigma> \<cdot> i"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i = u

goal (1 subgoal):
 1. \<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i)

goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Paa, Pax}
\<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Paa, Pax}
\<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i)

goal (1 subgoal):
 1. mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}
[PROOF STEP]
unfolding mgu\<^sub>l\<^sub>s_def
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Paa, Pax}
\<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i)

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s mguPaaPax {Paa, Pax} \<and> (\<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = mguPaaPax \<cdot> i))
[PROOF STEP]
unfolding mguPaaPax_def
[PROOF STATE]
proof (prove)
using this:
unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Paa, Pax}
\<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i)

goal (1 subgoal):
 1. unifier\<^sub>l\<^sub>s (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) {Paa, Pax} \<and> (\<forall>u. unifier\<^sub>l\<^sub>s u {Paa, Pax} \<longrightarrow> (\<exists>i. u = (\<lambda>x. if x = ''x'' then Fun ''a'' [] else \<epsilon> x) \<cdot> i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mgu\<^sub>l\<^sub>s mguPaaPax {Paa, Pax}

goal:
No subgoals!
[PROOF STEP]
qed