Quelle  GEM.thy

section ‹ General Extensional Mereology ›

(*<*)
theory GEM
  imports GMM CEM
begin (*>*)

text ‹ The theory of \emph{general extensional mereology}, also known as \emph{classical extensional
 } adds general mereology to extensional mereology.\footnote{For this axiomatization see
 cite‹"varzi_parts_1996"› p. 265 and cite‹"casati_parts_1999"› p. 46.} ›

locale GEM = GM + EM +
  assumes sum_eq: "x ⊕ y = (THE z. ∀v. O v z ⟷ O v x ∨ O v y)" 
  assumes product_eq: 
    "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
  assumes difference_eq: 
    "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
  assumes complement_eq: "←- x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
  assumes universe_eq: "u = (THE x. ∀y. P y x)"
  assumes fusion_eq: "∃x. F x ==>
    (σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"
  assumes general_product_eq: "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)"

sublocale GEM ⊆ GMM
proof
qed

subsection ‹ General Sums ›

context GEM
begin

lemma fusion_intro: 
"(∀y. O y z ⟷ (∃x. F x ∧ O y x)) ==> (σ x. F x) = z"
proof -
  assume antecedent: "(∀y. O y z ⟷ (∃x. F x ∧ O y x))"
  hence "(THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z)) = z"
  proof (rule the_equality)
    fix a
    assume a: "(∀y. O y a ⟷ (∃x. F x ∧ O y x))"
    have "∀x. O x a ⟷ O x z"
    proof
      fix b     
      from antecedent have "O b z ⟷ (∃x. F x ∧ O b x)"..
      moreover from a have "O b a ⟷ (∃x. F x ∧ O b x)"..
      ultimately show "O b a ⟷ O b z" by (rule ssubst)
    qed
    with overlap_extensionality show "a = z"..
  qed
  moreover from antecedent have "O z z ⟷ (∃x. F x ∧ O z x)"..
  hence "∃x. F x ∧ O z x" using overlap_reflexivity..
  hence "∃x. F x" by auto
  hence "(σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"
    by (rule fusion_eq)
  ultimately show "(σ v. F v) = z" by (rule subst)
qed

lemma fusion_idempotence: "(σ x. z = x) = z"
proof -
  have "∀y. O y z ⟷ (∃x. z = x ∧ O y x)"
  proof
    fix y
    show "O y z ⟷ (∃x. z = x ∧ O y x)"
    proof
      assume "O y z"
      with refl have "z = z ∧ O y z"..
      thus "∃x. z = x ∧ O y x"..
    next
      assume "∃x. z = x ∧ O y x"
      then obtain x where x: "z = x ∧ O y x"..
      hence "z = x"..
      moreover from x have "O y x"..
      ultimately show "O y z" by (rule ssubst)
    qed
  qed
  thus "(σ x. z = x) = z"
    by (rule fusion_intro)
qed

text ‹ The whole is the sum of its parts. ›

lemma fusion_absorption: "(σ x. P x z) = z"
proof -
  have "(∀y. O y z ⟷ (∃x. P x z ∧ O y x))"
  proof
    fix y
    show "O y z ⟷ (∃x. P x z ∧ O y x)"
    proof
      assume "O y z"
      with part_reflexivity have "P z z ∧ O y z"..
      thus "∃x. P x z ∧ O y x"..
    next
      assume "∃x. P x z ∧ O y x"
      then obtain x where x: "P x z ∧ O y x"..
      hence "P x z"..
      moreover from x have "O y x"..
      ultimately show "O y z" by (rule overlap_monotonicity)
    qed
  qed
  thus "(σ x. P x z) = z"
    by (rule fusion_intro)
qed

lemma part_fusion: "P w (σ v. P v x) ==> P w x"
proof -
  assume "P w (σ v. P v x)"
  with fusion_absorption show "P w x" by (rule subst)
qed

lemma fusion_character: 
  "∃x. F x ==> (∀y. O y (σ v. F v) ⟷ (∃x. F x ∧ O y x))"
proof -
  assume "∃x. F x"
  hence "∃z. ∀y. O y z ⟷ (∃x. F x ∧ O y x)"
    by (rule fusion)
  then obtain z where z: "∀y. O y z ⟷ (∃x. F x ∧ O y x)"..
  hence "(σ v. F v) = z " by (rule fusion_intro)
  thus "∀y. O y (σ v. F v) ⟷ (∃x. F x ∧ O y x)" using z by (rule ssubst)
qed

text ‹ The next lemma characterises fusions in terms of parthood.\footnote{See cite‹"pontow_note_2004"› pp. 202-9.} ›

lemma fusion_part_character: "∃x. F x ==>
  (∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v)))"
proof -
  assume "(∃x. F x)"
  hence F: "∀y. O y (σ v. F v) ⟷ (∃x. F x ∧ O y x)"
    by (rule fusion_character)
  show "∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
  proof
    fix y
    show "P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
    proof
      assume "P y (σ v. F v)"
      show "∀w. P w y ⟶ (∃v. F v ∧ O w v)"
      proof
        fix w
        from F have w: "O w (σ v. F v) ⟷ (∃x. F x ∧ O w x)"..
        show "P w y ⟶ (∃v. F v ∧ O w v)"
        proof
          assume "P w y"
          hence "P w (σ v. F v)" using ‹P y (σ v. F v)›
            by (rule part_transitivity)
          hence "O w (σ v. F v)" by (rule part_implies_overlap)
          with w show "∃x. F x ∧ O w x"..
        qed
      qed
    next
      assume right: "∀w. P w y ⟶ (∃v. F v ∧ O w v)"
      show "P y (σ v. F v)"
      proof (rule ccontr)
        assume "¬ P y (σ v. F v)"
        hence "∃v. P v y ∧ ¬ O v (σ v. F v)"
          by (rule strong_supplementation)
        then obtain v where v: "P v y ∧ ¬ O v (σ v. F v)"..
        hence "¬ O v (σ v. F v)"..
        from right have "P v y ⟶ (∃w. F w ∧ O v w)"..
        moreover from v have "P v y"..
        ultimately have "∃w. F w ∧ O v w"..
        from F have "O v (σ v. F v) ⟷ (∃x. F x ∧ O v x)"..
        hence "O v (σ v. F v)" using ‹∃w. F w ∧ O v w›..
        with ‹¬ O v (σ v. F v)› show "False"..
      qed
    qed
  qed
qed

lemma fusion_part: "F x ==> P x (σ x. F x)"
proof -
  assume "F x"
  hence "∃x. F x"..
  hence "∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
    by (rule fusion_part_character)
  hence "P x (σ v. F v) ⟷ (∀w. P w x ⟶ (∃v. F v ∧ O w v))"..
  moreover have "∀w. P w x ⟶ (∃v. F v ∧ O w v)"
  proof
    fix w
    show "P w x ⟶ (∃v. F v ∧ O w v)"
    proof
      assume "P w x"
      hence "O w x" by (rule part_implies_overlap)
      with ‹F x› have "F x ∧ O w x"..
      thus "∃v. F v ∧ O w v"..
    qed
  qed
  ultimately show "P x (σ v. F v)"..
qed

lemma common_part_fusion: 
  "O x y ==> (∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y))"
proof -
  assume "O x y"
  with overlap_eq have "∃z. (P z x ∧ P z y)"..
  hence sum: "(∀w. P w (σ v. (P v x ∧ P v y)) ⟷
    (∀z. P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v)))"
    by (rule fusion_part_character)
  show "∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y)"
  proof
    fix w
    from sum have w: "P w (σ v. (P v x ∧ P v y))
      ⟷ (∀z. P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v))"..
    show "P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y)"
    proof
      assume "P w (σ v. (P v x ∧ P v y))"
      with w have bla: 
        "(∀z. P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v))"..
      show "P w x ∧ P w y" 
      proof
        show "P w x"
        proof (rule ccontr)
          assume "¬ P w x"
          hence "∃z. P z w ∧ ¬ O z x"
            by (rule strong_supplementation)
          then obtain z where z: "P z w ∧ ¬ O z x"..
          hence "¬ O z x"..
          from bla have "P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v)"..
          moreover from z have "P z w"..
          ultimately have "∃v. (P v x ∧ P v y) ∧ O z v"..
          then obtain v where v: "(P v x ∧ P v y) ∧ O z v"..
          hence "P v x ∧ P v y"..
          hence "P v x"..
          moreover from v have "O z v"..
          ultimately have "O z x"
            by (rule overlap_monotonicity)
          with ‹¬ O z x› show "False"..
        qed
        show "P w y"
        proof (rule ccontr)
          assume "¬ P w y"
          hence "∃z. P z w ∧ ¬ O z y"
            by (rule strong_supplementation)
          then obtain z where z: "P z w ∧ ¬ O z y"..
          hence "¬ O z y"..
          from bla have "P z w ⟶ (∃v. (P v x ∧ P v y) ∧ O z v)"..
          moreover from z have "P z w"..
          ultimately have "∃v. (P v x ∧ P v y) ∧ O z v"..
          then obtain v where v: "(P v x ∧ P v y) ∧ O z v"..
          hence "P v x ∧ P v y"..
          hence "P v y"..
          moreover from v have "O z v"..
          ultimately have "O z y"
            by (rule overlap_monotonicity)
          with ‹¬ O z y› show "False"..
        qed
      qed
    next
      assume "P w x ∧ P w y"
      thus "P w (σ v. (P v x ∧ P v y))"
        by (rule fusion_part)
    qed
  qed
qed

theorem product_closure: 
  "O x y ==> (∃z. ∀w. P w z ⟷ (P w x ∧ P w y))"
proof -
  assume "O x y"
  hence "(∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y))"
    by (rule common_part_fusion)
  thus "∃z. ∀w. P w z ⟷ (P w x ∧ P w y)"..
qed

end

sublocale GEM ⊆ CEM
proof
  fix x y
  show "∃z. ∀w. O w z = (O w x ∨ O w y)" 
    using sum_closure.
  show "x ⊕ y = (THE z. ∀v. O v z ⟷ O v x ∨ O v y)" 
    using sum_eq.
  show "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)" 
    using product_eq.
  show "O x y ==> (∃z. ∀w. P w z = (P w x ∧ P w y))" 
    using product_closure.
qed

context GEM
begin

corollary "O x y ==> x ⊗ y = (σ v. P v x ∧ P v y)"
proof -
  assume "O x y"
  hence "(∀w. P w (σ v. (P v x ∧ P v y)) ⟷ (P w x ∧ P w y))"
    by (rule common_part_fusion)
  thus "x ⊗ y = (σ v. P v x ∧ P v y)" by (rule product_intro)
qed

lemma disjoint_fusion:
  "∃w. ¬ O w x ==> (∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x)"
proof -
  assume antecedent: "∃w. ¬ O w x"
  hence "∀y. O y (σ v. ¬ O v x) ⟷ (∃v. ¬ O v x ∧ O y v)"
    by (rule fusion_character)
  hence x: "O x (σ v. ¬ O v x) ⟷ (∃v. ¬ O v x ∧ O x v)"..
  show "∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x"
  proof
    fix y
    show "P y (σ z. ¬ O z x) ⟷ ¬ O y x"
    proof
      assume "P y (σ z. ¬ O z x)"
      moreover have "¬ O x (σ z. ¬ O z x)"
      proof
        assume "O x (σ z. ¬ O z x)"
        with x have "(∃v. ¬ O v x ∧ O x v)"..
        then obtain v where v: "¬ O v x ∧ O x v"..
        hence "¬ O v x"..
        from v have "O x v"..
        hence "O v x" by (rule overlap_symmetry)
        with ‹¬ O v x› show "False"..
      qed
      ultimately have "¬ O x y"
        by (rule disjoint_demonotonicity)
      thus "¬ O y x" by (rule disjoint_symmetry)
    next
      assume "¬ O y x"
      thus "P y (σ v. ¬ O v x)"
        by (rule fusion_part)
    qed
  qed
qed

theorem complement_closure: 
  "∃w. ¬ O w x ==> (∃z. ∀w. P w z ⟷ ¬ O w x)"
proof -
  assume "(∃w. ¬ O w x)"
  hence "∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x"
    by (rule disjoint_fusion)
  thus "∃z. ∀w. P w z ⟷ ¬ O w x"..
qed

end

sublocale GEM ⊆ CEMC
proof
  fix x y
  show "←- x = (THE z. ∀w. P w z ⟷ ¬ O w x)" 
    using complement_eq.
  show "(∃w. ¬ O w x) ==> (∃z. ∀w. P w z = (¬ O w x))" 
    using complement_closure.
  show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))" 
    using difference_eq.
  show "u = (THE x. ∀y. P y x)"
    using universe_eq.
qed

context GEM
begin

corollary complement_is_disjoint_fusion: 
  "∃w. ¬ O w x ==> ←- x = (σ z. ¬ O z x)"
proof -
  assume "∃w. ¬ O w x"
  hence "∀w. P w (σ z. ¬ O z x) ⟷ ¬ O w x"
    by (rule disjoint_fusion)
  thus "←- x = (σ z. ¬ O z x)"
    by (rule complement_intro)
qed

theorem strong_fusion: "∃x. F x ==>
  ∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
proof -
  assume "∃x. F x"
  have "(∀y. F y ⟶ P y (σ v. F v)) ∧
     (∀y. P y (σ v. F v) ⟶ (∃z. F z ∧ O y z))"
  proof
    show "∀y. F y ⟶ P y (σ v. F v)"
    proof
      fix y
      show "F y ⟶ P y (σ v. F v)"
      proof
        assume "F y"
        thus "P y (σ v. F v)"
          by (rule fusion_part)
      qed
    qed
  next
    have "(∀y. P y (σ v. F v) ⟷
      (∀w. P w y ⟶ (∃v. F v ∧ O w v)))"
      using ‹∃x. F x› by (rule fusion_part_character)
    hence "P (σ v. F v) (σ v. F v) ⟷ (∀w. P w (σ v. F v) ⟶
      (∃v. F v ∧ O w v))"..
    thus "∀w. P w (σ v. F v) ⟶ (∃v. F v ∧ O w v)" using part_reflexivity..
  qed
  thus ?thesis..
qed

theorem strong_fusion_eq: "∃x. F x ==> (σ x. F x) =
  (THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))"
proof -
  assume "∃x. F x"
  have "(THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))) = (σ x. F x)" 
  proof (rule the_equality)
    show "(∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"
    proof
      show "∀y. F y ⟶ P y (σ x. F x)"
      proof
        fix y
        show "F y ⟶ P y (σ x. F x)"
        proof
          assume "F y"
          thus "P y (σ x. F x)"
            by (rule fusion_part)
        qed
      qed
    next
      show "(∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"
      proof
        fix y
        show "P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)"
        proof
          have  "∀y. P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"
            using ‹∃x. F x› by (rule fusion_part_character)
          hence "P y (σ v. F v) ⟷ (∀w. P w y ⟶ (∃v. F v ∧ O w v))"..
          moreover assume "P y (σ x. F x)"
          ultimately have "∀w. P w y ⟶ (∃v. F v ∧ O w v)"..
          hence "P y y ⟶ (∃v. F v ∧ O y v)"..
          thus "∃v. F v ∧ O y v" using part_reflexivity..
        qed
      qed
    qed
  next
    fix x
    assume x: "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
    have "∀y. O y x ⟷ (∃z. F z ∧ O y z)"
    proof
      fix y
      show "O y x ⟷ (∃z. F z ∧ O y z)"
      proof
        assume "O y x"
        with overlap_eq have "∃v. P v y ∧ P v x"..
        then obtain v where v: "P v y ∧ P v x"..
        from x have "∀y. P y x ⟶ (∃z. F z ∧ O y z)"..
        hence "P v x ⟶ (∃z. F z ∧ O v z)"..
        moreover from v have "P v x"..
        ultimately have "∃z. F z ∧ O v z"..
        then obtain z where z: "F z ∧ O v z"..
        hence "F z"..
        from v have "P v y"..
        moreover from z have "O v z"..
        hence "O z v" by (rule overlap_symmetry)
        ultimately have "O z y" by (rule overlap_monotonicity)
        hence "O y z" by (rule overlap_symmetry)
        with ‹F z› have "F z ∧ O y z"..
        thus "∃z. F z ∧ O y z"..
      next
        assume "∃z. F z ∧ O y z"
        then obtain z where z: "F z ∧ O y z"..
        from x have "∀y. F y ⟶ P y x"..
        hence "F z ⟶ P z x"..
        moreover from z have "F z"..
        ultimately have "P z x"..
        moreover from z have "O y z"..
        ultimately show "O y x"
          by (rule overlap_monotonicity)
      qed
    qed
    hence "(σ x. F x) = x"
      by (rule fusion_intro)
    thus "x = (σ x. F x)"..
  qed
  thus ?thesis..
qed

lemma strong_sum_eq: "x ⊕ y = (THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y))"
proof -
  have "(THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)) = x ⊕ y"
  proof (rule the_equality)
    show "(P x (x ⊕ y) ∧ P y (x ⊕ y)) ∧ (∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y)"
    proof
      show "P x (x ⊕ y) ∧ P y (x ⊕ y)"
        proof
          show "P x (x ⊕ y)" using first_summand_in_sum.
          show "P y (x ⊕ y)" using second_summand_in_sum.
        qed
      show "∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y"
      proof
        fix w
        show "P w (x ⊕ y) ⟶ O w x ∨ O w y"
        proof
          assume "P w (x ⊕ y)"
          hence "O w (x ⊕ y)" by (rule part_implies_overlap)
          with sum_overlap show "O w x ∨ O w y"..
        qed
      qed
    qed
    fix z
    assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
    hence "P x z ∧ P y z"..
    have "∀w. O w z ⟷ (O w x ∨ O w y)"
    proof
      fix w
      show "O w z ⟷ (O w x ∨ O w y)"
      proof
        assume "O w z"
        with overlap_eq have "∃v. P v w ∧ P v z"..
        then obtain v where v: "P v w ∧ P v z"..
        hence "P v w"..
        from z have "∀w. P w z ⟶ O w x ∨ O w y"..
        hence "P v z ⟶ O v x ∨ O v y"..
        moreover from v have "P v z"..
        ultimately have "O v x ∨ O v y"..
        thus "O w x ∨ O w y"
        proof
          assume "O v x"
          hence "O x v" by (rule overlap_symmetry)
          with ‹P v w› have "O x w" by (rule overlap_monotonicity)
          hence "O w x" by (rule overlap_symmetry)
          thus "O w x ∨ O w y"..
        next
          assume "O v y"
          hence "O y v" by (rule overlap_symmetry)
          with ‹P v w› have "O y w" by (rule overlap_monotonicity)
          hence "O w y" by (rule overlap_symmetry)
          thus "O w x ∨ O w y"..
        qed
      next
        assume "O w x ∨ O w y"
        thus "O w z"
        proof
          from ‹P x z ∧ P y z› have "P x z"..
          moreover assume "O w x"
          ultimately show "O w z"
            by (rule overlap_monotonicity)
        next
          from ‹P x z ∧ P y z› have "P y z"..
          moreover assume "O w y"
          ultimately show "O w z"
            by (rule overlap_monotonicity)
        qed
      qed
    qed
    hence "x ⊕ y = z" by (rule sum_intro)
    thus "z = x ⊕ y"..
  qed
  thus ?thesis..
qed

subsection ‹ General Products ›

lemma general_product_intro: "(∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)) ==> (π x. F x) = x"
proof -
  assume "∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)"
  hence "(σ x. ∀y. F y ⟶ P x y) = x" by (rule fusion_intro)
  with general_product_eq show "(π x. F x) = x" by (rule ssubst)
qed

lemma general_product_idempotence: "(π z. z = x) = x"
proof -
  have "∀y. O y x ⟷ (∃z. (∀y. y = x ⟶ P z y) ∧ O y z)"
    by (meson overlap_eq part_reflexivity part_transitivity)
  thus "(π z. z = x) = x" by (rule general_product_intro)
qed

lemma general_product_absorption: "(π z. P x z) = x"
proof -
  have "∀y. O y x ⟷ (∃z. (∀y. P x y ⟶ P z y) ∧ O y z)"
    by (meson overlap_eq part_reflexivity part_transitivity)
  thus "(π z. P x z) = x" by (rule general_product_intro)
qed

lemma general_product_character: "∃z. ∀y. F y ⟶ P z y ==>
  ∀y. O y (π x. F x) ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)"
proof -
  assume "(∃z. ∀y. F y ⟶ P z y)"
  hence "(∃x. ∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z))"
    by (rule fusion)
  then obtain x where x: 
    "∀y. O y x ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z)"..
  hence "(π x. F x) = x" by (rule general_product_intro)
  thus "(∀y. O y (π x. F x) ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z))"
    using x by (rule ssubst)
qed

corollary "¬ (∃x. F x) ==> u = (π x. F x)"
proof -
  assume antecedent: "¬ (∃x. F x)"
  have "∀y. P y (π x. F x)"
  proof
    fix y
    show "P y (π x. F x)"
    proof (rule ccontr)
      assume "¬ P y (π x. F x)"
     hence "∃z. P z y ∧ ¬ O z (π x. F x)" by (rule strong_supplementation)
      then obtain z where z: "P z y ∧ ¬ O z (π x. F x)"..
      hence "¬ O z (π x. F x)"..
      from antecedent have bla: "∀ y. F y ⟶ P z y" by simp 
      hence "∃ v. ∀ y. F y ⟶ P v y"..
      hence "(∀y. O y (π x. F x) ⟷ (∃z. (∀y. F y ⟶ P z y) ∧ O y z))" by (rule general_product_character)
      hence "O z (π x. F x) ⟷ (∃v. (∀y. F y ⟶ P v y) ∧ O z v)"..
      moreover from bla have  "(∀ y. F y ⟶ P z y) ∧ O z z" 
        using overlap_reflexivity..
      hence "∃ v. (∀ y. F y ⟶ P v y) ∧ O z v"..
      ultimately have "O z (π x. F x)"..
      with ‹¬ O z (π x. F x)› show "False"..
    qed
  qed
  thus "u = (π x. F x)"
    by (rule universe_intro)
qed

end

subsection ‹ Strong Fusion ›

text ‹ An alternative axiomatization of general extensional mereology adds a stronger version of the
  axiom to minimal mereology, with correspondingly stronger definitions of sums and general
 .\footnote{See cite‹"tarski_foundations_1983"› p. 25. The proofs in this section are adapted
  cite‹"hovda_what_2009"›.} ›

locale GEM1 = MM + 
  assumes strong_fusion: "∃x. F x ==> ∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
  assumes strong_sum_eq: "x ⊕ y = (THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y))"
  assumes product_eq: 
    "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)"
  assumes difference_eq: 
    "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))"
  assumes complement_eq: "←- x = (THE z. ∀w. P w z ⟷ ¬ O w x)"
  assumes universe_eq: "u = (THE x. ∀y. P y x)"
  assumes strong_fusion_eq:  "∃x. F x ==> (σ x. F x) = (THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))"
  assumes general_product_eq: "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)"
begin

theorem fusion: 
  "∃x. φ x ==> (∃z. ∀y. O y z ⟷ (∃x. φ x ∧ O y x))"
proof -
  assume "∃x. φ x"
  hence "∃x. (∀y. φ y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. φ z ∧ O y z))" by (rule strong_fusion)
  then obtain x where x: 
    "(∀y. φ y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. φ z ∧ O y z))"..
  have "∀y. O y x ⟷ (∃v. φ v ∧ O y v)"
  proof
    fix y
    show "O y x ⟷ (∃v. φ v ∧ O y v)"
    proof
      assume "O y x"
      with overlap_eq have "∃z. P z y ∧ P z x"..
      then obtain z where z: "P z y ∧ P z x"..
      hence "P z x"..
      from x have "∀y. P y x ⟶ (∃v. φ v ∧ O y v)"..
      hence "P z x ⟶ (∃v. φ v ∧ O z v)"..
      hence "∃v. φ v ∧ O z v" using ‹P z x›..
      then obtain v where v: "φ v ∧ O z v"..
      hence "O z v"..
      with overlap_eq have "∃w. P w z ∧ P w v"..
      then obtain w where w: "P w z ∧ P w v"..
      hence "P w z"..
      moreover from z have "P z y"..
      ultimately have "P w y"
        by (rule part_transitivity)
      moreover from w have "P w v"..
      ultimately have "P w y ∧ P w v"..
      hence "∃w. P w y ∧ P w v"..
      with overlap_eq have "O y v"..
      from v have "φ v"..
      hence "φ v ∧ O y v" using ‹O y v›..
      thus "∃v. φ v ∧ O y v"..
    next
      assume "∃v. φ v ∧ O y v"
      then obtain v where v: "φ v ∧ O y v"..
      hence "O y v"..
      with overlap_eq have "∃z. P z y ∧ P z v"..
      then obtain z where z: "P z y ∧ P z v"..
      hence "P z v"..
      from x have "∀y. φ y ⟶ P y x"..
      hence "φ v ⟶ P v x"..
      moreover from v have "φ v"..
      ultimately have "P v x"..
      with ‹P z v› have "P z x"
        by (rule part_transitivity)
      from z have "P z y"..
      thus "O y x" using ‹P z x›
        by (rule overlap_intro)
    qed
  qed
  thus "(∃z. ∀y. O y z ⟷ (∃x. φ x ∧ O y x))"..
qed

lemma pair: "∃v. (∀w. (w = x ∨ w = y) ⟶ P w v) ∧ (∀w. P w v ⟶ (∃z. (z = x ∨ z = y) ∧ O w z))"
proof -
  have "x = x"..
  hence "x = x ∨ x = y"..
  hence "∃v. v = x ∨ v = y"..
  thus ?thesis
    by (rule strong_fusion)
qed

lemma or_id: "(v = x ∨ v = y) ∧ O w v ==> O w x ∨ O w y"
proof -
  assume v: "(v = x ∨ v = y) ∧ O w v"
  hence "O w v"..
  from v have "v = x ∨ v = y"..
  thus "O w x ∨ O w y"
  proof
    assume "v = x"
    hence "O w x" using ‹O w v› by (rule subst)
    thus "O w x ∨ O w y"..
  next
    assume "v = y"
    hence "O w y" using ‹O w v› by (rule subst)
    thus "O w x ∨ O w y"..
  qed
qed

lemma strong_sum_closure: 
  "∃z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
proof -
  from pair obtain z where z: "(∀w. (w = x ∨ w = y) ⟶ P w z) ∧ (∀w. P w z ⟶ (∃v. (v = x ∨ v = y) ∧ O w v))"..
  have "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
  proof
    from z have allw: "∀w. (w = x ∨ w = y) ⟶ P w z"..
    hence "x = x ∨ x = y ⟶ P x z"..
    moreover have "x = x ∨ x = y" using refl..
    ultimately have "P x z"..
    from allw have "y = x ∨ y = y ⟶ P y z"..
    moreover have "y = x ∨ y = y" using refl..
    ultimately have "P y z"..
    with ‹P x z› show "P x z ∧ P y z"..
  next
    show "∀w. P w z ⟶ O w x ∨ O w y"
    proof
      fix w
      show "P w z ⟶ O w x ∨ O w y"
      proof
        assume "P w z"
        from z have "∀w. P w z ⟶ (∃v. (v = x ∨ v = y) ∧ O w v)"..
        hence "P w z ⟶ (∃v. (v = x ∨ v = y) ∧ O w v)"..
        hence "∃v. (v = x ∨ v = y) ∧ O w v" using ‹P w z›..
        then obtain v where v: "(v = x ∨ v = y) ∧ O w v"..
        thus "O w x ∨ O w y" by (rule or_id)
      qed
    qed
  qed
  thus ?thesis..
qed

end 

sublocale GEM1 ⊆ GMM
proof
  fix x y φ
  show "(∃x. φ x) ==> (∃z. ∀y. O y z ⟷ (∃x. φ x ∧ O y x))" using fusion.
qed

context GEM1
begin

lemma least_upper_bound:
  assumes sf: 
    "((∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))"
  shows lub: 
      "(∀y. F y ⟶ P y x) ∧ (∀z. (∀y. F y ⟶ P y z) ⟶ P x z)"
proof
 from sf show "∀y. F y ⟶ P y x"..
next
 show "(∀z. (∀y. F y ⟶ P y z) ⟶ P x z)"
 proof
  fix z
  show "(∀y. F y ⟶ P y z) ⟶ P x z"
  proof
   assume z: "∀y. F y ⟶ P y z"
   from pair obtain v where v: "(∀w. (w = x ∨ w = z) ⟶ P w v) ∧ (∀w. P w v ⟶ (∃y. (y = x ∨ y = z) ∧ O w y))"..
   hence left: "(∀w. (w = x ∨ w = z) ⟶ P w v)"..
   hence "(x = x ∨ x = z) ⟶ P x v"..
   moreover have "x = x ∨ x = z" using refl..
   ultimately have "P x v"..
   have "z = v"
   proof (rule ccontr)
    assume "z ≠ v"
    from left have "z = x ∨ z = z ⟶ P z v"..
    moreover have "z = x ∨ z = z" using refl..
    ultimately have "P z v"..
    hence "P z v ∧ z ≠ v" using ‹z ≠ v›..
    with nip_eq have "PP z v"..
    hence "∃w. P w v ∧ ¬ O w z" by (rule weak_supplementation)
    then obtain w where w: "P w v ∧ ¬ O w z"..
    hence "P w v"..
    from v have right: 
      "∀w. P w v ⟶ (∃y. (y = x ∨ y = z) ∧ O w y)"..
    hence "P w v ⟶ (∃y. (y = x ∨ y = z) ∧ O w y)"..
    hence "∃y. (y = x ∨ y = z) ∧ O w y" using ‹P w v›..
    then obtain s where s: "(s = x ∨ s = z) ∧ O w s"..
    hence "s = x ∨ s = z"..
    thus "False"
    proof
     assume "s = x"
     moreover from s have "O w s"..
     ultimately have "O w x" by (rule subst)
     with overlap_eq have "∃t. P t w ∧ P t x"..
     then obtain t where t: "P t w ∧ P t x"..
     hence "P t x"..
     from sf have "(∀y. P y x ⟶ (∃z. F z ∧ O y z))"..
     hence "P t x ⟶ (∃z. F z ∧ O t z)"..
     hence "∃z. F z ∧ O t z" using ‹P t x›..
     then obtain a where a: "F a ∧ O t a"..
     hence "F a"..
     from sf have ub: "∀y. F y ⟶ P y x"..
     hence "F a ⟶ P a x"..
     hence "P a x" using ‹F a›..
     moreover from a have "O t a"..
     ultimately have "O t x"
      by (rule overlap_monotonicity)
     from t have "P t w"..
     moreover have "O z t"
     proof -
      from z have "F a ⟶ P a z"..
      moreover from a have "F a"..
      ultimately have "P a z"..
      moreover from a have "O t a"..
      ultimately have "O t z"
       by (rule overlap_monotonicity)
      thus "O z t" by (rule overlap_symmetry)
     qed
     ultimately have "O z w"
      by (rule overlap_monotonicity)
     hence "O w z" by (rule overlap_symmetry)
     from w have "¬ O w z"..
     thus "False" using ‹O w z›..
    next
     assume "s = z"
     moreover from s have "O w s"..
     ultimately have "O w z" by (rule subst)
     from w have "¬ O w z"..
     thus "False" using ‹O w z›..
    qed
   qed
   thus "P x z" using ‹P x v› by (rule ssubst)
  qed
 qed
qed

corollary strong_fusion_intro:  "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)) ==> (σ x. F x) = x"
proof -
  assume antecedent: "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
  with least_upper_bound have lubx: 
    "(∀y. F y ⟶ P y x) ∧ (∀z. (∀y. F y ⟶ P y z) ⟶ P x z)".
  from antecedent have "∀y. P y x ⟶ (∃z. F z ∧ O y z)"..
  hence "P x x ⟶ (∃z. F z ∧ O x z)"..
  hence "∃z. F z ∧ O x z" using part_reflexivity..
  then obtain z where z: "F z ∧ O x z"..
  hence "F z"..
  hence "∃z. F z"..
  hence "(σ x. F x) = (THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion_eq)
  moreover have "(THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))) = x"
  proof (rule the_equality)
    show "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
      using antecedent.
  next
    fix w
    assume w: 
      "(∀y. F y ⟶ P y w) ∧ (∀y. P y w ⟶ (∃z. F z ∧ O y z))"
    with least_upper_bound have lubw:
      "(∀y. F y ⟶ P y w) ∧ (∀z. (∀y. F y ⟶ P y z) ⟶ P w z)".
    hence "(∀z. (∀y. F y ⟶ P y z) ⟶ P w z)"..
    hence "(∀y. F y ⟶ P y x) ⟶ P w x"..
    moreover from antecedent have "∀y. F y ⟶ P y x"..
    ultimately have "P w x"..
    from lubx have "(∀z. (∀y. F y ⟶ P y z) ⟶ P x z)"..
    hence "(∀y. F y ⟶ P y w) ⟶ P x w"..
    moreover from lubw have "(∀y. F y ⟶ P y w)"..
    ultimately have "P x w"..
    with ‹P w x› show "w = x"
      by (rule part_antisymmetry)
  qed
  ultimately show "(σ x. F x) = x" by (rule ssubst)
qed

lemma strong_fusion_character: "∃x. F x ==> ((∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)))"
proof -
  assume "∃x. F x"
  hence "(∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion)
  then obtain x where x: 
    "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"..
  hence "(σ x. F x) = x" by (rule strong_fusion_intro)
  thus ?thesis using x by (rule ssubst)
qed

lemma F_in: "∃x. F x ==> (∀y. F y ⟶ P y (σ x. F x))"
proof -
  assume "∃x. F x"
  hence "((∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion_character)
 thus "∀y. F y ⟶ P y (σ x. F x)"..
qed

lemma parts_overlap_Fs:
  "∃x. F x ==> (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"
proof -
  assume "∃x. F x"
  hence "((∀y. F y ⟶ P y (σ x. F x)) ∧ (∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)))" by (rule strong_fusion_character)
  thus "(∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z))"..
qed

lemma in_strong_fusion: "P z (σ x. z = x)"
proof -
  have "∃y. z = y" using refl..
  hence "∀y. z = y ⟶ P y (σ x. z = x)"
    by (rule F_in)
  hence "z = z ⟶ P z (σ x. z = x)"..
  thus "P z (σ x. z = x)" using refl..
qed

lemma strong_fusion_in: "P (σ x. z = x) z"
proof -
  have "∃y. z = y" using refl..
  hence sf:
    "(∀y. z = y ⟶ P y (σ x. z = x)) ∧ (∀y. P y (σ x. z = x) ⟶ (∃v. z = v ∧ O y v))"
    by (rule strong_fusion_character)
  with least_upper_bound have lub: "(∀y. z = y ⟶ P y (σ x. z = x)) ∧ (∀v. (∀y. z = y ⟶ P y v) ⟶ P (σ x. z = x) v)".
  hence "(∀v. (∀y. z = y ⟶ P y v) ⟶ P (σ x. z = x) v)"..
  hence "(∀y. z = y ⟶ P y z) ⟶ P (σ x. z = x) z"..
  moreover have "(∀y. z = y ⟶ P y z)"
  proof
    fix y
    show "z = y ⟶ P y z"
    proof
      assume "z = y"
      thus "P y z" using part_reflexivity by (rule subst)
    qed
  qed
  ultimately show "P (σ x. z = x) z"..
qed

lemma strong_fusion_idempotence: "(σ x. z = x) = z"
 using strong_fusion_in in_strong_fusion by (rule part_antisymmetry)

subsection ‹ Strong Sums ›

lemma pair_fusion: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y) ⟶ (σ z. z = x ∨ z = y) = z"
proof
 assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
  have "(∀v. v = x ∨ v = y ⟶ P v z) ∧ (∀v. P v z ⟶ (∃z. (z = x ∨ z = y) ∧ O v z))"
 proof
  show "∀v. v = x ∨ v = y ⟶ P v z"
  proof
   fix w
   from z have "P x z ∧ P y z"..
   show "w = x ∨ w = y ⟶ P w z"
   proof
    assume "w = x ∨ w = y"
    thus "P w z"
    proof
     assume "w = x"
     moreover from ‹P x z ∧ P y z› have "P x z"..
     ultimately show "P w z" by (rule ssubst)
    next
     assume "w = y"
     moreover from ‹P x z ∧ P y z› have "P y z"..
     ultimately show "P w z" by (rule ssubst)
    qed
   qed
  qed
  show "∀v. P v z ⟶ (∃z. (z = x ∨ z = y) ∧ O v z)"
  proof
   fix v
   show "P v z ⟶ (∃z. (z = x ∨ z = y) ∧ O v z)"
   proof
    assume "P v z"
    from z have "∀w. P w z ⟶ O w x ∨ O w y"..
    hence "P v z ⟶ O v x ∨ O v y"..
    hence "O v x ∨ O v y" using ‹P v z›..
    thus "∃z. (z = x ∨ z = y) ∧ O v z"
    proof
     assume "O v x"
     have "x = x ∨ x = y" using refl.. 
     hence "(x = x ∨ x = y) ∧ O v x" using ‹O v x›..
     thus "∃z. (z = x ∨ z = y) ∧ O v z"..
    next
     assume "O v y"
     have "y = x ∨ y = y" using refl..
     hence "(y = x ∨ y = y) ∧ O v y" using ‹O v y›..
     thus "∃z. (z = x ∨ z = y) ∧ O v z"..
    qed
   qed
  qed
 qed
  thus "(σ z. z = x ∨ z = y) = z"
    by (rule strong_fusion_intro)
qed

corollary strong_sum_fusion: "x ⊕ y = (σ z. z = x ∨ z = y)"
proof -
  have "(THE z. (P x z ∧ P y z) ∧
    (∀w. P w z ⟶ O w x ∨ O w y)) = (σ z. z = x ∨ z = y)"
  proof (rule the_equality)
    have "x = x ∨ x = y" using refl..
    hence exz: "∃z. z = x ∨ z = y"..
    hence allw: "(∀w. w = x ∨ w = y ⟶ P w (σ z. z = x ∨ z = y))"
      by (rule F_in)
    show "(P x (σ z. z = x ∨ z = y) ∧ P y (σ z. z = x ∨ z = y)) ∧
      (∀w. P w (σ z. z = x ∨ z = y) ⟶ O w x ∨ O w y)"
    proof
      show "(P x (σ z. z = x ∨ z = y) ∧ P y (σ z. z = x ∨ z = y))"
      proof
        from allw have "x = x ∨ x = y ⟶ P x (σ z. z = x ∨ z = y)"..
        thus "P x (σ z. z = x ∨ z = y)" 
          using ‹x = x ∨ x = y›..
      next
        from allw have "y = x ∨ y = y ⟶ P y (σ z. z = x ∨ z = y)"..
        moreover have "y = x ∨ y = y" 
          using refl..
        ultimately show "P y (σ z. z = x ∨ z = y)"..
      qed
    next
      show "∀w. P w (σ z. z = x ∨ z = y) ⟶ O w x ∨ O w y"
      proof
        fix w
        show "P w (σ z. z = x ∨ z = y) ⟶ O w x ∨ O w y"
        proof
          have "∀v. P v (σ z. z = x ∨ z = y) ⟶ (∃z. (z = x ∨ z = y) ∧ O v z)" using exz by (rule parts_overlap_Fs)
          hence "P w (σ z. z = x ∨ z = y) ⟶ (∃z. (z = x ∨ z = y) ∧ O w z)"..
          moreover assume "P w (σ z. z = x ∨ z = y)"
          ultimately have "(∃z. (z = x ∨ z = y) ∧ O w z)"..
          then obtain z where z: "(z = x ∨ z = y) ∧ O w z"..
          thus "O w x ∨ O w y" by (rule or_id)
        qed
      qed
    qed
  next
    fix z
    assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
    with pair_fusion have "(σ z. z = x ∨ z = y) = z"..
    thus "z = (σ z. z = x ∨ z = y)"..
  qed
  with strong_sum_eq show "x ⊕ y = (σ z. z = x ∨ z = y)" 
    by (rule ssubst)
qed

corollary strong_sum_intro: 
  "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y) ⟶ x ⊕ y = z"
proof
  assume z: "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
  with pair_fusion have "(σ z. z = x ∨ z = y) = z"..
  with strong_sum_fusion show "(x ⊕ y) = z" 
    by (rule ssubst)
qed

corollary strong_sum_character: "(P x (x ⊕ y) ∧ P y (x ⊕ y)) ∧ (∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y)"
proof -
  from strong_sum_closure obtain z where z: 
    "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"..
 with strong_sum_intro have "x ⊕ y = z"..
 thus ?thesis using z by (rule ssubst)
qed

corollary summands_in: "(P x (x ⊕ y) ∧ P y (x ⊕ y))"
  using strong_sum_character..

corollary first_summand_in: "P x (x ⊕ y)" using summands_in..

corollary second_summand_in: "P y (x ⊕ y)" using summands_in..

corollary sum_part_overlap: "(∀w. P w (x ⊕ y) ⟶ O w x ∨ O w y)" using strong_sum_character..

lemma strong_sum_absorption: "y = (x ⊕ y) ==> P x y"
proof -
 assume "y = (x ⊕ y)"
 thus "P x y" using first_summand_in by (rule ssubst)
qed

theorem strong_supplementation: "¬ P x y ==> (∃z. P z x ∧ ¬ O z y)"
proof -
 assume "¬ P x y"
 have "¬ (∀z. P z x ⟶ O z y)"
 proof
  assume z: "∀z. P z x ⟶ O z y"
  have "(∀v. y = v ⟶ P v (x ⊕ y)) ∧
    (∀v. P v (x ⊕ y) ⟶ (∃z. y = z ∧ O v z))"
  proof
   show "∀v. y = v ⟶ P v (x ⊕ y)"
   proof
    fix v
    show "y = v ⟶ P v (x ⊕ y)"
    proof
     assume "y = v"
     thus "P v (x ⊕ y)" 
       using second_summand_in by (rule subst)
    qed
   qed
   show "∀v. P v (x ⊕ y) ⟶ (∃z. y = z ∧ O v z)"
   proof
    fix v
    show "P v (x ⊕ y) ⟶ (∃z. y = z ∧ O v z)"
    proof
     assume "P v (x ⊕ y)"
     moreover from sum_part_overlap have
       "P v (x ⊕ y) ⟶ O v x ∨ O v y"..
     ultimately have "O v x ∨ O v y" by (rule rev_mp)
     hence "O v y"
     proof
      assume "O v x"
      with overlap_eq have "∃w. P w v ∧ P w x"..
      then obtain w where w: "P w v ∧ P w x"..
      from z have "P w x ⟶ O w y"..
      moreover from w have "P w x"..
      ultimately have "O w y"..
      with overlap_eq have "∃t. P t w ∧ P t y"..
      then obtain t where t: "P t w ∧ P t y"..
      hence "P t w"..
      moreover from w have "P w v"..
      ultimately have "P t v"
        by (rule part_transitivity)
      moreover from t have "P t y"..
      ultimately show "O v y"
        by (rule overlap_intro)
     next
      assume "O v y"
      thus "O v y".
     qed
     with refl have "y = y ∧ O v y"..
     thus "∃z. y = z ∧ O v z"..
    qed
   qed
  qed
  hence  "(σ z. y = z) = (x ⊕ y)" by (rule strong_fusion_intro)
  with strong_fusion_idempotence have "y = x ⊕ y" by (rule subst)
  hence "P x y" by (rule strong_sum_absorption)
  with ‹¬ P x y› show "False"..
 qed
 thus "∃z. P z x ∧ ¬ O z y" by simp
qed

lemma sum_character: "∀v. O v (x ⊕ y) ⟷ (O v x ∨ O v y)"
proof
  fix v
  show "O v (x ⊕ y) ⟷ (O v x ∨ O v y)"
  proof
    assume "O v (x ⊕ y)"
    with overlap_eq have "∃w. P w v ∧ P w (x ⊕ y)"..
    then obtain w where w: "P w v ∧ P w (x ⊕ y)"..
    hence "P w v"..
    have "P w (x ⊕ y) ⟶ O w x ∨ O w y" using sum_part_overlap..
    moreover from w have "P w (x ⊕ y)"..
    ultimately have "O w x ∨ O w y"..
    thus "O v x ∨ O v y"
    proof
      assume "O w x"
      hence "O x w"
        by (rule overlap_symmetry)
      with ‹P w v› have "O x v"
        by (rule overlap_monotonicity)
      hence "O v x"
        by (rule overlap_symmetry)
      thus "O v x ∨ O v y"..
    next
      assume "O w y"
      hence "O y w"
        by (rule overlap_symmetry)
      with ‹P w v› have "O y v"
        by (rule overlap_monotonicity)
      hence "O v y" by (rule overlap_symmetry)
      thus "O v x ∨ O v y"..
    qed
  next
    assume "O v x ∨ O v y"
    thus "O v (x ⊕ y)"
    proof
      assume "O v x"
      with overlap_eq have "∃w. P w v ∧ P w x"..
      then obtain w where w: "P w v ∧ P w x"..
      hence "P w v"..
      moreover from w have "P w x"..
      hence "P w (x ⊕ y)" using first_summand_in
        by (rule part_transitivity)
      ultimately show "O v (x ⊕ y)"
        by (rule overlap_intro)
    next
      assume "O v y"
      with overlap_eq have "∃w. P w v ∧ P w y"..
      then obtain w where w: "P w v ∧ P w y"..
      hence "P w v"..
      moreover from w have "P w y"..
      hence "P w (x ⊕ y)" using second_summand_in
        by (rule part_transitivity)
      ultimately show "O v (x ⊕ y)"
        by (rule overlap_intro)
    qed
  qed
qed

lemma sum_eq: "x ⊕ y = (THE z. ∀v. O v z = (O v x ∨ O v y))"
proof -
  have "(THE z. ∀v. O v z ⟷ (O v x ∨ O v y)) = x ⊕ y"
  proof (rule the_equality)
    show "∀v. O v (x ⊕ y) ⟷ (O v x ∨ O v y)" using sum_character.
  next
    fix z
    assume z: "∀v. O v z ⟷ (O v x ∨ O v y)"
    have "(P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y)"
    proof
      show "P x z ∧ P y z"
      proof
        show "P x z"
        proof (rule ccontr)
          assume "¬ P x z"
          hence "∃v. P v x ∧ ¬ O v z"
            by (rule strong_supplementation)
          then obtain v where v: "P v x ∧ ¬ O v z"..
          hence "¬ O v z"..
          from z have "O v z ⟷ (O v x ∨ O v y)"..
          moreover from v have "P v x"..
          hence "O v x" by (rule part_implies_overlap)
          hence "O v x ∨ O v y"..
          ultimately have "O v z"..
          with ‹¬ O v z› show "False"..
        qed
      next
        show "P y z"
        proof (rule ccontr)
          assume "¬ P y z"
          hence "∃v. P v y ∧ ¬ O v z"
            by (rule strong_supplementation)
          then obtain v where v: "P v y ∧ ¬ O v z"..
          hence "¬ O v z"..
          from z have "O v z ⟷ (O v x ∨ O v y)"..
          moreover from v have "P v y"..
          hence "O v y" by (rule part_implies_overlap)
          hence "O v x ∨ O v y"..
          ultimately have "O v z"..
          with ‹¬ O v z› show "False"..
        qed
      qed
      show "∀w. P w z ⟶ (O w x ∨ O w y)"
      proof
        fix w
        show "P w z ⟶ (O w x ∨ O w y)"
        proof
          from z have "O w z ⟷ O w x ∨ O w y"..
          moreover assume "P w z"
          hence "O w z" by (rule part_implies_overlap)
          ultimately show "O w x ∨ O w y"..
        qed
      qed
    qed
    with strong_sum_intro have "x ⊕ y = z"..
    thus "z = x ⊕ y"..
  qed
  thus ?thesis..
qed

theorem fusion_eq: "∃x. F x ==>
  (σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"
proof -
  assume "∃x. F x"
  hence bla: "∀y. P y (σ x. F x) ⟶ (∃z. F z ∧ O y z)"
    by (rule parts_overlap_Fs)
  have "(THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z)) = (σ x. F x)"
  proof (rule the_equality)
    show "∀y. O y (σ x. F x) ⟷ (∃z. F z ∧ O y z)"
    proof
      fix y
      show "O y (σ x. F x) ⟷ (∃z. F z ∧ O y z)"
      proof
        assume "O y (σ x. F x)"
        with overlap_eq have "∃v. P v y ∧ P v (σ x. F x)"..
        then obtain v where v: "P v y ∧ P v (σ x. F x)"..
        hence "P v y"..
        from bla have "P v (σ x. F x) ⟶ (∃z. F z ∧ O v z)"..
        moreover from v have "P v (σ x. F x)"..
        ultimately have "(∃z. F z ∧ O v z)"..
        then obtain z where z: "F z ∧ O v z"..
        hence "F z"..
        moreover from z have "O v z"..
        hence "O z v" by (rule overlap_symmetry)
        with ‹P v y› have "O z y" by (rule overlap_monotonicity)
        hence "O y z" by (rule overlap_symmetry)
        ultimately have "F z ∧ O y z"..
        thus "(∃z. F z ∧ O y z)"..
      next
        assume "∃z. F z ∧ O y z"
        then obtain z where z: "F z ∧ O y z"..
        from‹∃x. F x› have "(∀y. F y ⟶ P y (σ x. F x))"
          by (rule F_in)
        hence "F z ⟶ P z (σ x. F x)"..
        moreover from z have "F z"..
        ultimately have "P z (σ x. F x)"..
        moreover from z have "O y z"..
        ultimately show "O y (σ x. F x)"
          by (rule overlap_monotonicity)
      qed
    qed
  next
    fix x
    assume x: "∀y. O y x ⟷ (∃v. F v ∧ O y v)"
    have "(∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z))"
    proof
      show "∀y. F y ⟶ P y x"
      proof
        fix y
        show "F y ⟶ P y x"
        proof
          assume "F y"
          show "P y x"
          proof (rule ccontr)
            assume "¬ P y x"
            hence "∃z. P z y ∧ ¬ O z x"
              by (rule strong_supplementation)
            then obtain z where z: "P z y ∧ ¬ O z x"..
            hence "¬ O z x"..
            from x have "O z x ⟷ (∃v. F v ∧ O z v)"..
            moreover from z have "P z y"..
            hence "O z y" by (rule part_implies_overlap)
            with ‹F y› have "F y ∧ O z y"..
            hence "∃y. F y ∧ O z y"..
            ultimately have "O z x"..
            with ‹¬ O z x› show "False"..
          qed
        qed
      qed
      show "∀y. P y x ⟶ (∃z. F z ∧ O y z)"
      proof
        fix y
        show "P y x ⟶ (∃z. F z ∧ O y z)"
        proof
          from x have "O y x ⟷ (∃z. F z ∧ O y z)"..
          moreover assume "P y x"
          hence "O y x" by (rule part_implies_overlap)
          ultimately show "∃z. F z ∧ O y z"..
        qed
      qed
    qed
    hence "(σ x. F x) = x"
      by (rule strong_fusion_intro)
    thus "x = (σ x. F x)"..
  qed
  thus "(σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))"..
qed

end

sublocale GEM1 ⊆ GEM
proof
  fix x y F
  show "¬ P x y ==> ∃z. P z x ∧ ¬ O z y" 
    using strong_supplementation.
  show "x ⊕ y = (THE z. ∀v. O v z ⟷ (O v x ∨ O v y))" 
    using sum_eq.
  show "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)" 
    using product_eq.
  show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))" 
    using difference_eq.
  show "←- x = (THE z. ∀w. P w z ⟷ ¬ O w x)" 
    using complement_eq.
  show "u = (THE x. ∀y. P y x)" 
    using universe_eq.
  show "∃x. F x ==> (σ x. F x) = (THE x. ∀y. O y x ⟷ (∃z. F z ∧ O y z))" using fusion_eq.
  show "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)" 
    using general_product_eq.
qed

sublocale GEM ⊆ GEM1
proof
  fix x y F
  show "∃x. F x ==> (∃x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" using strong_fusion.
  show "∃x. F x ==> (σ x. F x) = (THE x. (∀y. F y ⟶ P y x) ∧ (∀y. P y x ⟶ (∃z. F z ∧ O y z)))" using strong_fusion_eq.
  show "(π x. F x) = (σ x. ∀y. F y ⟶ P x y)" using general_product_eq.
  show "x ⊕ y = (THE z. (P x z ∧ P y z) ∧ (∀w. P w z ⟶ O w x ∨ O w y))" using strong_sum_eq.
  show "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)" 
    using product_eq.
  show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))" 
    using difference_eq.
  show "←- x = (THE z. ∀w. P w z ⟷ ¬ O w x)" using complement_eq.
  show "u = (THE x. ∀y. P y x)" using universe_eq.
qed

(*<*) end (*>*)