section ‹ General Extensional Mereology › (*<*) theory GEM imports GMM CEM begin (*>*) text ‹ The theory of \emph{general extensional mereology}, also known as \emph{classical extensional mereology} 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 fusion axiom to minimal mereology, with correspondingly stronger definitions of sums and general sums.\footnote{See \<^cite>‹"tarski_foundations_1983"› p. 25. The proofs in this section are adapted from \<^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