Theory CEM

section ‹ Closed Extensional Mereology ›

(*<*)
theory CEM
  imports CM EM
begin
(*>*)

text ‹ Closed extensional mereology combines closed mereology with extensional mereology.\footnote{
See \<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"casati_parts_1999"› p. 43.} ›  

locale CEM = CM + EM

text ‹ Likewise, closed minimal mereology combines closed mereology with minimal mereology.\footnote{
See \<^cite>‹"casati_parts_1999"› p. 43.} ›

locale CMM = CM + MM

text ‹ But famously closed minimal mereology and closed extensional mereology are the same theory,
because in closed minimal mereology product closure and weak supplementation entail strong
supplementation.\footnote{See \<^cite>‹"simons_parts:_1987"› p. 31 and \<^cite>‹"casati_parts_1999"› p. 44.} ›

sublocale CMM ⊆ CEM
proof
  fix x y
  show strong_supplementation: "¬ P x y ⟹ (∃ z. P z x ∧ ¬ O z y)"
  proof -
    assume "¬ P x y"
    show "∃ z. P z x ∧ ¬ O z y"
    proof cases
      assume "O x y"
      with ‹¬ P x y› have "¬ P x y ∧ O x y"..
      hence "PP (x ⊗ y) x" by (rule nonpart_implies_proper_product)
      hence "∃ z. P z x ∧ ¬ O z (x ⊗ y)" by (rule weak_supplementation)
      then obtain z where z: "P z x ∧ ¬ O z (x ⊗ y)"..
      hence "¬ O z y" by (rule disjoint_from_second_factor)
      moreover from z have "P z x"..
      hence  "P z x ∧ ¬ O z y"
        using ‹¬ O z y›..
      thus "∃ z. P z x ∧ ¬ O z y"..
    next
      assume "¬ O x y"
      with part_reflexivity have "P x x ∧ ¬ O x y"..
      thus "(∃ z. P z x ∧ ¬ O z y)"..
    qed
  qed
qed

sublocale CEM ⊆ CMM..

subsection ‹ Sums ›

context CEM
begin

lemma sum_intro:
   "(∀ w. O w z ⟷ (O w x ∨ O w y)) ⟹ x ⊕ y = z"
proof -
  assume sum: "∀ w. O w z ⟷ (O w x ∨ O w y)"
  hence "(THE v. ∀ w. O w v ⟷ (O w x ∨ O w y)) = z"
  proof (rule the_equality)
    fix a
    assume a: "∀ w. O w a ⟷ (O w x ∨ O w y)"
    have "∀ w. O w a ⟷ O w z"
    proof
      fix w
      from sum have "O w z ⟷ (O w x ∨ O w y)"..
      moreover from a have "O w a ⟷ (O w x ∨ O w y)"..
      ultimately show "O w a ⟷ O w z" by (rule ssubst)
      qed
      with overlap_extensionality show "a = z"..
  qed
  thus "x ⊕ y = z"
    using sum_eq by (rule subst)
qed

lemma sum_idempotence: "x ⊕ x = x"
proof -
  have "∀ w. O w x ⟷ (O w x ∨ O w x)"
  proof
    fix w
    show "O w x ⟷ (O w x ∨ O w x)"
    proof (rule iffI)
      assume "O w x"
      thus "O w x ∨ O w x"..
    next
      assume "O w x ∨ O w x"
      thus "O w x" by (rule disjE)
    qed
  qed
  thus "x ⊕ x = x" by (rule sum_intro)
qed

lemma part_sum_identity: "P y x ⟹ x ⊕ y = x"
proof -
  assume "P y x"
  have "∀ w. O w x ⟷ (O w x ∨ O w y)"
  proof
    fix w
    show "O w x ⟷ (O w x ∨ O w y)"
    proof
      assume "O w x"
      thus "O w x ∨ O w y"..
    next
      assume "O w x ∨ O w y"
      thus "O w x"
      proof
        assume "O w x"
        thus "O w x".
      next
        assume "O w y"
        with ‹P y x› show "O w x" 
          by (rule overlap_monotonicity)
      qed
    qed
  qed
  thus "x ⊕ y = x" by (rule sum_intro)
qed

lemma sum_character: "∀ w. O w (x ⊕ y) ⟷ (O w x ∨ O w y)"
proof -
  from sum_closure have "(∃ z. ∀ w. O w z ⟷ (O w x ∨ O w y))".
  then obtain a where a: "∀ w. O w a ⟷ (O w x ∨ O w y)"..
  hence "x ⊕ y = a" by (rule sum_intro)
  thus "∀ w. O w (x ⊕ y) ⟷ (O w x ∨ O w y)"
    using a by (rule ssubst)
qed

lemma sum_overlap: "O w (x ⊕ y) ⟷ (O w x ∨ O w y)" 
  using sum_character..

lemma sum_part_character:  
  "P w (x ⊕ y) ⟷ (∀ v. O v w ⟶ O v x ∨ O v y)"
proof
  assume "P w (x ⊕ y)"
  show "∀ v. O v w ⟶ O v x ∨ O v y"
  proof
    fix v
    show "O v w ⟶ O v x ∨ O v y"
    proof
      assume "O v w"    
      with ‹P w (x ⊕ y)› have "O v (x ⊕ y)"
        by (rule overlap_monotonicity)
      with sum_overlap show "O v x ∨ O v y"..
    qed
  qed
next
  assume right: "∀ v. O v w ⟶ O v x ∨ O v y"
  have "∀ v. O v w ⟶ O v (x ⊕ y)"
  proof
    fix v
    from right have "O v w ⟶ O v x ∨ O v y"..
    with sum_overlap show "O v w ⟶ O v (x ⊕ y)" 
      by (rule ssubst)
  qed
  with part_overlap_eq show "P w (x ⊕ y)"..
qed

lemma sum_commutativity: "x ⊕ y = y ⊕ x"
proof -
  from sum_character have "∀ w. O w (y ⊕ x) ⟷ O w y ∨ O w x".
  hence "∀ w. O w (y ⊕ x) ⟷ O w x ∨ O w y" by metis
  thus "x ⊕ y = y ⊕ x" by (rule sum_intro)
qed

lemma first_summand_overlap: "O z x ⟹ O z (x ⊕ y)"
proof -
  assume "O z x"
  hence "O z x ∨ O z y"..
  with sum_overlap show "O z (x ⊕ y)"..
qed

lemma first_summand_disjointness: "¬ O z (x ⊕ y) ⟹ ¬ O z x"
proof -
  assume "¬ O z (x ⊕ y)"
  show "¬ O z x"
  proof
    assume "O z x"
    hence "O z (x ⊕ y)" by (rule first_summand_overlap)
    with ‹¬ O z (x ⊕ y)› show "False"..
  qed
qed

lemma first_summand_in_sum: "P x (x ⊕ y)"
proof -
  have "∀ w. O w x ⟶ O w (x ⊕ y)"
  proof
    fix w
    show "O w x ⟶ O w (x ⊕ y)"
    proof
      assume "O w x"
      thus "O w (x ⊕ y)"
        by (rule first_summand_overlap)
    qed
  qed
  with part_overlap_eq show "P x (x ⊕ y)"..
qed

lemma common_first_summand: "P x (x ⊕ y) ∧ P x (x ⊕ z)"
proof
  from first_summand_in_sum show "P x (x ⊕ y)".
  from first_summand_in_sum show "P x (x ⊕ z)".
qed

lemma common_first_summand_overlap: "O (x ⊕ y) (x ⊕ z)"
proof -
  from first_summand_in_sum have "P x (x ⊕ y)".
  moreover from first_summand_in_sum have "P x (x ⊕ z)".
  ultimately have "P x (x ⊕ y) ∧ P x (x ⊕ z)"..
  hence "∃ v. P v (x ⊕ y) ∧ P v (x ⊕ z)"..
  with overlap_eq show ?thesis..
qed

lemma second_summand_overlap: "O z y ⟹ O z (x ⊕ y)"
proof -
  assume "O z y"
  from sum_character have "O z (x ⊕ y) ⟷ (O z x ∨ O z y)"..
  moreover from ‹O z y› have "O z x ∨ O z y"..
  ultimately show "O z (x ⊕ y)"..
qed

lemma second_summand_disjointness: "¬ O z (x ⊕ y) ⟹ ¬ O z y"
proof -
  assume "¬ O z (x ⊕ y)"
  show "¬ O z y"
  proof
    assume  "O z y"
    hence "O z (x ⊕ y)" 
      by (rule second_summand_overlap)
    with ‹¬ O z (x ⊕ y)› show False..
  qed
qed

lemma second_summand_in_sum: "P y (x ⊕ y)"
proof -
  have "∀ w. O w y ⟶ O w (x ⊕ y)"
  proof
    fix w
    show "O w y ⟶ O w (x ⊕ y)"
    proof
      assume "O w y"
      thus "O w (x ⊕ y)"
        by (rule second_summand_overlap)
    qed
  qed
  with part_overlap_eq show "P y (x ⊕ y)"..
qed

lemma second_summands_in_sums: "P y (x ⊕ y) ∧ P v (z ⊕ v)"
proof
  show "P y (x ⊕ y)" using second_summand_in_sum.
  show "P v (z ⊕ v)" using second_summand_in_sum.
qed

lemma disjoint_from_sum: "¬ O z (x ⊕ y) ⟷ ¬ O z x ∧ ¬ O z y"
proof -
  from sum_character have "O z (x ⊕ y) ⟷ (O z x ∨ O z y)"..
  thus ?thesis by simp
qed

lemma summands_part_implies_sum_part: 
  "P x z ∧ P y z ⟹ P (x ⊕ y) z"
proof -
  assume antecedent: "P x z ∧ P y z"
  have "∀ w. O w (x ⊕ y) ⟶ O w z"
  proof
    fix w
    have w: "O w (x ⊕ y) ⟷ (O w x ∨ O w y)"
      using sum_character..
    show "O w (x ⊕ y) ⟶ O w z"
    proof
      assume "O w (x ⊕ y)"
      with w have "O w x ∨ O w y"..
      thus "O w z"
      proof
        from antecedent have "P x z"..
        moreover assume "O w x"
        ultimately show "O w z"
          by (rule overlap_monotonicity)
      next
        from antecedent have "P y z"..
        moreover assume "O w y"
        ultimately show "O w z"
          by (rule overlap_monotonicity)
      qed
    qed
  qed
  with part_overlap_eq show "P (x ⊕ y) z"..
qed

lemma sum_part_implies_summands_part: 
  "P (x ⊕ y) z ⟹ P x z ∧ P y z"
proof -
  assume antecedent: "P (x ⊕ y) z"
  show "P x z ∧ P y z"
  proof
    from first_summand_in_sum show "P x z"
      using antecedent by (rule part_transitivity)
  next
    from second_summand_in_sum show "P y z"
      using antecedent by (rule part_transitivity)
  qed
qed

lemma in_second_summand: "P z (x ⊕ y) ∧ ¬ O z x ⟹ P z y"
proof -
  assume antecedent: "P z (x ⊕ y) ∧ ¬ O z x"
  hence "P z (x ⊕ y)"..
  show "P z y"
  proof (rule ccontr)
    assume "¬ P z y"
    hence "∃ v. P v z ∧ ¬ O v y"
      by (rule strong_supplementation)
    then obtain v where v: "P v z ∧ ¬ O v y"..
    hence "¬ O v y"..
    from v have "P v z"..
    hence "P v (x ⊕ y)"
      using ‹P z (x ⊕ y)› by (rule part_transitivity)
    hence "O v (x ⊕ y)" by (rule part_implies_overlap)
    from sum_character have "O v (x ⊕ y) ⟷ O v x ∨ O v y"..
    hence "O v x ∨ O v y" using ‹O v (x ⊕ y)›..
    thus "False"
    proof (rule disjE)
      from antecedent have "¬ O z x"..
      moreover assume "O v x"
      hence "O x v" by (rule overlap_symmetry)
      with ‹P v z› have "O x z"
        by (rule overlap_monotonicity)
      hence "O z x" by (rule overlap_symmetry)
      ultimately show "False"..
    next
      assume "O v y"
      with ‹¬ O v y› show "False"..
    qed
  qed
qed

lemma disjoint_second_summands:
  "P v (x ⊕ y) ∧ P v (x ⊕ z) ⟹ ¬ O y z ⟹ P v x"
proof -
  assume antecedent: "P v (x ⊕ y) ∧ P v (x ⊕ z)"
  hence "P v (x ⊕ z)"..
  assume "¬ O y z"
  show "P v x"
  proof (rule ccontr)
    assume "¬ P v x"
    hence "∃ w. P w v ∧ ¬ O w x" by (rule strong_supplementation)
    then obtain w where w: "P w v ∧ ¬ O w x"..
    hence "¬ O w x"..
    from w have "P w v"..
    moreover from antecedent have "P v (x ⊕ z)"..
    ultimately have "P w (x ⊕ z)" by (rule part_transitivity)
    hence "P w (x ⊕ z) ∧ ¬ O w x" using ‹¬ O w x›.. 
    hence "P w z" by (rule in_second_summand)
    from antecedent have "P v (x ⊕ y)"..
    with ‹P w v› have "P w (x ⊕ y)" by (rule part_transitivity)
    hence "P w (x ⊕ y) ∧ ¬ O w x" using ‹¬ O w x›..
    hence "P w y" by (rule in_second_summand)
    hence "P w y ∧ P w z" using ‹P w z›..
    hence "∃ w. P w y ∧ P w z"..
    with overlap_eq have "O y z"..
    with ‹¬ O y z› show "False"..
  qed
qed

lemma right_associated_sum:
  "O w (x ⊕ (y ⊕ z)) ⟷ O w x ∨ (O w y ∨ O w z)"
proof -
  from sum_character have "O w (y ⊕ z) ⟷ O w y ∨ O w z"..
  moreover from sum_character have
    "O w (x ⊕ (y ⊕ z)) ⟷ (O w x ∨ O w (y ⊕ z))"..
  ultimately show ?thesis
    by (rule subst)
qed

lemma left_associated_sum: 
  "O w ((x ⊕ y) ⊕ z) ⟷ (O w x ∨ O w y) ∨ O w z"
proof -
  from sum_character have "O w (x ⊕ y) ⟷ (O w x ∨ O w y)"..
  moreover from sum_character have
    "O w ((x ⊕ y) ⊕ z) ⟷ O w (x ⊕ y) ∨ O w z"..
  ultimately show ?thesis
    by (rule subst)
qed

theorem sum_associativity: "x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
proof -
  have  "∀ w. O w (x ⊕ (y ⊕ z)) ⟷ O w ((x ⊕ y) ⊕ z)"
  proof
    fix w
    have "O w (x ⊕ (y ⊕ z)) ⟷ (O w x ∨ O w y) ∨ O w z"
      using right_associated_sum by simp
    with left_associated_sum show 
      "O w (x ⊕ (y ⊕ z)) ⟷ O w ((x ⊕ y) ⊕ z)" by (rule ssubst)
  qed
  with overlap_extensionality show "x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"..
qed

subsection ‹ Distributivity ›

text ‹ The proofs in this section are adapted from \<^cite>‹"pietruszczak_metamereology_2018"› pp. 102-4.  ›

lemma common_summand_in_product: "P x ((x ⊕ y) ⊗ (x ⊕ z))"
    using common_first_summand by (rule common_part_in_product)

lemma product_in_first_summand:
  "¬ O y z ⟹ P ((x ⊕ y) ⊗ (x ⊕ z)) x"
proof -
  assume "¬ O y z"
  have "∀ v. P v ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ P v x"
  proof
    fix v
    show "P v ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ P v x"
    proof
      assume "P v ((x ⊕ y) ⊗ (x ⊕ z))"
      with common_first_summand_overlap have 
        "P v (x ⊕ y) ∧ P v (x ⊕ z)" by (rule product_part_in_factors)
      thus "P v x" using ‹¬ O y z›  by (rule disjoint_second_summands)
    qed
  qed
  hence "P ((x ⊕ y) ⊗ (x ⊕ z)) ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ 
    P ((x ⊕ y) ⊗ (x ⊕ z)) x"..
  thus "P ((x ⊕ y) ⊗ (x ⊕ z)) x" using part_reflexivity..
qed
  
lemma product_is_first_summand: 
  "¬ O y z ⟹ (x ⊕ y) ⊗ (x ⊕ z) = x"
proof -
  assume "¬ O y z"
  hence "P ((x ⊕ y) ⊗ (x ⊕ z)) x"
    by (rule product_in_first_summand)
  thus "(x ⊕ y) ⊗ (x ⊕ z) = x"
    using common_summand_in_product
    by (rule part_antisymmetry)
qed

lemma sum_over_product_left: "O y z ⟹ P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))"
proof -
  assume "O y z"
  hence "P (y ⊗ z) ((x ⊕ y) ⊗ (x ⊕ z))" using second_summands_in_sums
    by (rule part_product_in_whole_product)
  with common_summand_in_product have
    "P x ((x ⊕ y) ⊗ (x ⊕ z)) ∧ P (y ⊗ z) ((x ⊕ y) ⊗ (x ⊕ z))"..
  thus "P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))"
    by (rule summands_part_implies_sum_part)
qed

lemma sum_over_product_right: 
  "O y z ⟹ P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
proof -
  assume "O y z"
  show "P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
  proof (rule ccontr)
    assume "¬ P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
    hence "∃ v. P v ((x ⊕ y) ⊗ (x ⊕ z)) ∧ ¬ O v (x ⊕ (y ⊗ z))"
      by (rule strong_supplementation)
    then obtain v where v: 
      "P v ((x ⊕ y) ⊗ (x ⊕ z)) ∧ ¬ O v (x ⊕ (y ⊗ z))"..
    hence " ¬ O v (x ⊕ (y ⊗ z))"..
    with disjoint_from_sum have vd: "¬ O v x ∧ ¬ O v (y ⊗ z)"..
    hence "¬ O v (y ⊗ z)"..
    from vd have "¬ O v x"..
    from v have "P v ((x ⊕ y) ⊗ (x ⊕ z))"..
    with common_first_summand_overlap have 
      vs: "P v (x ⊕ y) ∧ P v (x ⊕ z)" by (rule product_part_in_factors)
    hence "P v (x ⊕ y)"..
    hence "P v (x ⊕ y) ∧ ¬ O v x" using ‹¬ O v x›..
    hence "P v y" by (rule in_second_summand)
    moreover from vs have "P v (x ⊕ z)"..
    hence "P v (x ⊕ z) ∧ ¬ O v x" using ‹¬ O v x›..
    hence "P v z" by (rule in_second_summand)
    ultimately have "P v y ∧ P v z"..    
    hence "P v (y ⊗ z)" by (rule common_part_in_product)
    hence "O v (y ⊗ z)" by (rule part_implies_overlap)
    with ‹¬ O v (y ⊗ z)› show "False"..
  qed
qed

text ‹ Sums distribute over products. ›

theorem sum_over_product: 
    "O y z ⟹ x ⊕ (y ⊗ z) = (x ⊕ y) ⊗ (x ⊕ z)"
proof -
  assume "O y z"
  hence "P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))"
    by (rule sum_over_product_left)
  moreover have "P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))"
    using ‹O y z› by (rule sum_over_product_right)
  ultimately show "x ⊕ (y ⊗ z) = (x ⊕ y) ⊗ (x ⊕ z)"
    by (rule part_antisymmetry)
qed

lemma product_in_factor_by_sum:
  "O x y ⟹ P (x ⊗ y) (x ⊗ (y ⊕ z))"
proof -
  assume "O x y"
  hence "P (x ⊗ y) x" 
    by (rule product_in_first_factor)
  moreover have "P (x ⊗ y) y" 
    using ‹O x y› by (rule product_in_second_factor)
  hence "P (x ⊗ y) (y ⊕ z)" 
    using first_summand_in_sum by (rule part_transitivity)
  with ‹P (x ⊗ y) x› have "P (x ⊗ y) x ∧ P (x ⊗ y) (y ⊕ z)"..
  thus "P (x ⊗ y) (x ⊗ (y ⊕ z))" 
    by (rule common_part_in_product)
qed

lemma product_of_first_summand:
  "O x y ⟹ ¬ O x z ⟹ P (x ⊗ (y ⊕ z)) (x ⊗ y)"
proof -
  assume "O x y"
  hence "O x (y ⊕ z)"
    by (rule first_summand_overlap)
  assume "¬ O x z"
  show "P (x ⊗ (y ⊕ z)) (x ⊗ y)"
  proof (rule ccontr)
    assume "¬ P (x ⊗ (y ⊕ z)) (x ⊗ y)"
    hence "∃ v. P v (x ⊗ (y ⊕ z)) ∧ ¬ O v (x ⊗ y)"
      by (rule strong_supplementation)
    then obtain v where v: "P v (x ⊗ (y ⊕ z)) ∧ ¬ O v (x ⊗ y)"..
    hence "P v (x ⊗ (y ⊕ z))"..
    with ‹O x (y ⊕ z)› have "P v x ∧ P v (y ⊕ z)"
      by (rule product_part_in_factors)
    hence "P v x"..
    moreover from v have "¬ O v (x ⊗ y)"..
    ultimately have  "P v x ∧ ¬ O v (x ⊗ y)"..
    hence "¬ O v y" by (rule disjoint_from_second_factor)
    from ‹P v x ∧ P v (y ⊕ z)› have "P v (y ⊕ z)"..
    hence "P v (y ⊕ z) ∧ ¬ O v y" using ‹¬ O v y›..
    hence "P v z" by (rule in_second_summand)
    with ‹P v x› have "P v x ∧ P v z"..
    hence "∃ v. P v x ∧ P v z"..
    with overlap_eq have "O x z"..
    with ‹¬ O x z› show "False"..
  qed
qed

theorem disjoint_product_over_sum: 
  "O x y ⟹ ¬ O x z ⟹ x ⊗ (y ⊕ z) = x ⊗ y"
proof -
  assume "O x y"
  moreover assume "¬ O x z"
  ultimately have "P (x ⊗ (y ⊕ z)) (x ⊗ y)" 
    by (rule product_of_first_summand)
  moreover have "P (x ⊗ y)(x ⊗ (y ⊕ z))"
    using ‹O x y› by (rule product_in_factor_by_sum)
  ultimately show "x ⊗ (y ⊕ z) = x ⊗ y"
    by (rule part_antisymmetry)
qed

lemma product_over_sum_left:
  "O x y ∧ O x z ⟹ P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
proof -
  assume "O x y ∧ O x z"
  hence "O x y"..
  hence "O x (y ⊕ z)" by (rule first_summand_overlap)
  show "P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
  proof (rule ccontr)
    assume "¬ P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
    hence "∃ v. P v (x ⊗ (y ⊕ z)) ∧ ¬ O v ((x ⊗ y) ⊕ (x ⊗ z))"
      by (rule strong_supplementation)
    then obtain v where v: 
      "P v (x ⊗ (y ⊕ z)) ∧ ¬ O v ((x ⊗ y) ⊕ (x ⊗ z))"..
    hence "¬ O v ((x ⊗ y) ⊕ (x ⊗ z))"..
    with disjoint_from_sum have oxyz:
      "¬ O v (x ⊗ y) ∧ ¬ O v (x ⊗ z)"..
    from v have "P v (x ⊗ (y ⊕ z))"..
    with ‹O x (y ⊕ z)› have pxyz: "P v x ∧ P v (y ⊕ z)"
      by (rule product_part_in_factors)
    hence "P v x"..
    moreover from oxyz have "¬ O v (x ⊗ y)"..
    ultimately have "P v x ∧ ¬ O v (x ⊗ y)"..
    hence "¬ O v y" by (rule disjoint_from_second_factor)
    from oxyz have "¬ O v (x ⊗ z)"..
    with ‹P v x› have "P v x ∧ ¬ O v (x ⊗ z)"..
    hence "¬ O v z" by (rule disjoint_from_second_factor)
    with ‹¬ O v y› have "¬ O v y ∧ ¬ O v z"..
    with disjoint_from_sum have "¬ O v (y ⊕ z)"..
    from pxyz have "P v (y ⊕ z)"..
    hence "O v (y ⊕ z)" by (rule part_implies_overlap)
    with ‹¬ O v (y ⊕ z)› show "False"..
  qed
qed

lemma product_over_sum_right:
  "O x y ∧ O x z ⟹ P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))" 
proof -
  assume antecedent: "O x y ∧ O x z"
  have "P (x ⊗ y) (x ⊗ (y ⊕ z)) ∧ P (x ⊗ z) (x ⊗ (y ⊕ z))"
  proof
    from antecedent have "O x y"..
    thus "P (x ⊗ y) (x ⊗ (y ⊕ z))"
      by (rule  product_in_factor_by_sum)
  next
    from antecedent have "O x z"..
    hence "P (x ⊗ z) (x ⊗ (z ⊕ y))"
      by (rule  product_in_factor_by_sum)
    with sum_commutativity show "P (x ⊗ z) (x ⊗ (y ⊕ z))"
      by (rule subst)
  qed
  thus "P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))"
    by (rule summands_part_implies_sum_part)
qed

theorem product_over_sum: 
  "O x y ∧ O x z ⟹ x ⊗ (y ⊕ z) = (x ⊗ y) ⊕ (x ⊗ z)"
proof -
  assume antecedent: "O x y ∧ O x z"
  hence "P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))"
    by (rule product_over_sum_left)
  moreover have "P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))"
    using antecedent by (rule product_over_sum_right)
  ultimately show "x ⊗ (y ⊕ z) = (x ⊗ y) ⊕ (x ⊗ z)"
    by (rule part_antisymmetry)
qed

lemma joint_identical_sums: 
  "v ⊕ w = x ⊕ y ⟹ O x v ∧ O x w ⟹ ((x ⊗ v) ⊕ (x ⊗ w)) = x"
proof -
  assume "v ⊕ w = x ⊕ y"
  moreover assume "O x v ∧ O x w"
  hence "x ⊗ (v ⊕ w) = x ⊗ v ⊕ x ⊗ w"
    by (rule product_over_sum)
  ultimately have "x ⊗ (x ⊕ y) = x ⊗ v ⊕ x ⊗ w" by (rule subst)
  moreover have "(x ⊗ (x ⊕ y)) = x" using first_summand_in_sum
    by (rule part_product_identity)
  ultimately show "((x ⊗ v) ⊕ (x ⊗ w)) = x" by (rule subst)
qed

lemma disjoint_identical_sums: 
  "v ⊕ w = x ⊕ y ⟹ ¬ O y v ∧ ¬ O w x ⟹ x = v ∧ y = w"
proof -
  assume identical: "v ⊕ w = x ⊕ y"
  assume disjoint: "¬ O y v ∧ ¬ O w x"
  show "x = v ∧ y = w"
  proof
    from disjoint have "¬ O y v"..
    hence "(x ⊕ y) ⊗ (x ⊕ v) = x"
      by (rule product_is_first_summand)
    with identical have "(v ⊕ w) ⊗ (x ⊕ v) = x"
      by (rule ssubst)
    moreover from disjoint have "¬ O w x"..
    hence "(v ⊕ w) ⊗ (v ⊕ x) = v"
      by (rule product_is_first_summand)
    with sum_commutativity have "(v ⊕ w) ⊗ (x ⊕ v) = v" 
      by (rule subst)
    ultimately show "x = v" by (rule subst)
  next
    from disjoint have "¬ O w x"..
    hence "(y ⊕ w) ⊗ (y ⊕ x) = y"
      by (rule product_is_first_summand)
    moreover from disjoint have "¬ O y v"..
    hence "(w ⊕ y) ⊗ (w ⊕ v) = w"
      by (rule product_is_first_summand)
    with sum_commutativity have "(w ⊕ y) ⊗ (v ⊕ w) = w" 
      by (rule subst)
    with identical have "(w ⊕ y) ⊗ (x ⊕ y) = w" 
      by (rule subst)
    with sum_commutativity have "(w ⊕ y) ⊗ (y ⊕ x) = w" 
      by (rule subst)
    with sum_commutativity have "(y ⊕ w) ⊗ (y ⊕ x) = w" 
      by (rule subst)
    ultimately show "y = w" 
      by (rule subst)
  qed
qed

end

subsection ‹ Differences ›

locale CEMD = CEM + CMD
begin

lemma plus_minus: "PP y x ⟹ y ⊕ (x ⊖ y) = x"
proof -
  assume "PP y x"
  hence "∃ z. P z x ∧ ¬ O z y" by (rule weak_supplementation)
  hence xmy:"∀ w. P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)"
    by (rule difference_character)
  have "∀ w. O w x ⟷ (O w y ∨ O w (x ⊖ y))"
  proof
    fix w
    from xmy have w: "P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)"..
    show "O w x ⟷ (O w y ∨ O w (x ⊖ y))"
    proof
      assume "O w x"
      with overlap_eq have "∃ v. P v w ∧ P v x"..
      then obtain v where v: "P v w ∧ P v x"..
      hence "P v w"..
      from v have "P v x"..
      show "O w y ∨ O w (x ⊖ y)"
      proof cases
        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 y ∨ O w (x ⊖ y)"..
      next
        from xmy have "P v (x ⊖ y) ⟷ (P v x ∧ ¬ O v y)"..
        moreover assume "¬ O v y"
        with ‹P v x› have  "P v x ∧ ¬ O v y"..
        ultimately have "P v (x ⊖ y)"..
        with ‹P v w› have "P v w ∧ P v (x ⊖ y)"..
        hence "∃ v. P v w ∧ P v (x ⊖ y)"..
        with overlap_eq have "O w (x ⊖ y)"..
        thus "O w y ∨ O w (x ⊖ y)"..
      qed
    next
      assume "O w y ∨ O w (x ⊖ y)"
      thus "O w x"
      proof
        from ‹PP y x› have "P y x"
          by (rule proper_implies_part)
        moreover assume "O w y"
        ultimately show "O w x"
          by (rule overlap_monotonicity)
      next
        assume "O w (x ⊖ y)"
        with overlap_eq have "∃ v. P v w ∧ P v (x ⊖ y)"..
        then obtain v where v: "P v w ∧ P v (x ⊖ y)"..
        hence "P v w"..
        from xmy have "P v (x ⊖ y) ⟷ (P v x ∧ ¬ O v y)"..
        moreover from v have "P v (x ⊖ y)"..
        ultimately have "P v x ∧ ¬ O v y"..
        hence "P v x"..
        with ‹P v w› have "P v w ∧ P v x"..
        hence "∃ v. P v w ∧ P v x"..
        with overlap_eq show "O w x"..
      qed
    qed
  qed
  thus "y ⊕ (x ⊖ y) = x"
    by (rule sum_intro)
qed

end

subsection ‹ The Universe ›

locale CEMU = CEM + CMU
begin

lemma something_disjoint: "x ≠ u ⟹ (∃ v. ¬ O v x)"
proof -
  assume "x ≠ u"
  with universe_character have "P x u ∧ x ≠ u"..
  with nip_eq have "PP x u"..
  hence "∃ v. P v u ∧ ¬ O v x"
    by (rule weak_supplementation)
  then obtain v where "P v u ∧ ¬ O v x"..
  hence "¬ O v x"..
  thus "∃ v. ¬ O v x"..
qed

lemma overlaps_universe: "O x u"
proof -
  from universe_character have "P x u".
  thus "O x u" by (rule part_implies_overlap)
qed

lemma universe_absorbing: "x ⊕ u = u"
proof -
  from universe_character have "P (x ⊕ u) u".
  thus "x ⊕ u = u" using second_summand_in_sum
    by (rule part_antisymmetry)
qed

lemma second_summand_not_universe: "x ⊕ y ≠ u ⟹ y ≠ u"
proof -
  assume antecedent: "x ⊕ y ≠ u"
  show "y ≠ u"
  proof
    assume "y = u"
    hence "x ⊕ u ≠ u" using antecedent by (rule subst)
    thus "False" using universe_absorbing..
  qed
qed

lemma first_summand_not_universe: "x ⊕ y ≠ u ⟹ x ≠ u"
proof -
  assume "x ⊕ y ≠ u"
  with sum_commutativity have "y ⊕ x ≠ u" by (rule subst)
  thus "x ≠ u" by (rule second_summand_not_universe)
qed

end

subsection ‹ Complements ›

locale CEMC = CEM + CMC + 
  assumes universe_eq: "u = (THE x. ∀ y. P y x)"
begin

lemma complement_sum_character: "∀ y. P y (x ⊕ (─x))"
proof
  fix y
  have "∀ v. O v y ⟶ O v x ∨ O v (─x)"
  proof
    fix v
    show "O v y ⟶ O v x ∨ O v (─x)"
    proof
      assume "O v y"
      show "O v x ∨ O v (─x)"
        using or_complement_overlap..
    qed
  qed
  with sum_part_character show "P y (x ⊕ (─x))"..
qed

lemma universe_closure: "∃ x. ∀ y. P y x"
  using complement_sum_character by (rule exI)

end

sublocale CEMC ⊆ CEMU
proof
  show "u = (THE z. ∀w. P w z)" using universe_eq.
  show "∃ x. ∀ y. P y x" using universe_closure.
qed

sublocale CEMC ⊆ CEMD
proof
qed

context CEMC
begin

corollary universe_is_complement_sum: "u = x ⊕ (─x)"
  using complement_sum_character by (rule universe_intro)

lemma strong_complement_character: 
  "x ≠ u ⟹ (∀ v. P v (─x) ⟷ ¬ O v x)"
proof -
  assume "x ≠ u"
  hence "∃ v. ¬ O v x" by (rule something_disjoint)
  thus "∀ v. P v (─x) ⟷ ¬ O v x" by (rule complement_character)
qed

lemma complement_part_not_part: "x ≠ u ⟹ P y (─x) ⟹ ¬ P y x"
proof -
  assume "x ≠ u"
  hence "∀ w. P w (─x) ⟷ ¬ O w x"
    by (rule strong_complement_character)
  hence y: "P y (─x) ⟷ ¬ O y x"..
  moreover assume "P y (─x)"
  ultimately have "¬ O y x"..
  thus "¬ P y x" 
    by (rule disjoint_implies_not_part)
qed

lemma complement_involution: "x ≠ u ⟹ x = ─(─x)"
proof -
  assume "x ≠ u"
  have "¬ P u x"
  proof
    assume "P u x"
    with universe_character have "x = u"
      by (rule part_antisymmetry)
    with ‹x ≠ u› show "False"..
  qed
  hence "∃ v. P v u ∧ ¬ O v x"
    by (rule strong_supplementation)
  then obtain v where v: "P v u ∧ ¬ O v x"..
  hence "¬ O v x"..
  hence "∃ v. ¬ O v x"..
  hence notx: "∀ w. P w (─x) ⟷ ¬ O w x"
    by (rule complement_character)
  have "─x ≠ u"
  proof
    assume "─x = u"
    hence "∀ w. P w u ⟷ ¬ O w x" using notx by (rule subst)
    hence "P x u ⟷ ¬ O x x"..
    hence "¬ O x x" using universe_character..
    thus "False" using overlap_reflexivity..
  qed  
  have "¬ P u (─x)"
  proof
    assume "P u (─x)"
    with universe_character have "─x = u"
      by (rule part_antisymmetry)
    with ‹─x ≠ u› show "False"..
  qed
  hence "∃ v. P v u ∧ ¬ O v (─x)"
    by (rule strong_supplementation)
  then obtain w where w: "P w u ∧ ¬ O w (─x)"..
  hence "¬ O w (─x)"..
  hence "∃ v. ¬ O v (─x)"..
  hence notnotx: "∀ w. P w (─(─x)) ⟷ ¬ O w (─x)"
    by (rule complement_character)
  hence "P x (─(─x)) ⟷ ¬ O x (─x)"..
  moreover have "¬ O x (─x)"
  proof
    assume "O x (─x)"
    with overlap_eq have "∃ s. P s x ∧ P s (─x)"..
    then obtain s where s: "P s x ∧ P s (─x)"..
    hence "P s x"..
    hence "O s x" by (rule part_implies_overlap)
    from notx have "P s (─x) ⟷ ¬ O s x"..
    moreover from s have "P s (─x)"..     
    ultimately have "¬ O s x"..
    thus "False" using ‹O s x›..
  qed
  ultimately have "P x (─(─x))"..
  moreover have "P (─(─x)) x"
  proof (rule ccontr)
    assume "¬ P (─(─x)) x"
    hence "∃ s. P s (─(─x)) ∧ ¬ O s x"
      by (rule strong_supplementation)
    then obtain s where s: "P s (─(─x)) ∧ ¬ O s x"..
    hence "¬ O s x"..
    from notnotx have "P s (─(─x)) ⟷ (¬ O s (─x))"..
    moreover from s have "P s (─(─x))"..
    ultimately have "¬ O s (─x)"..
    from or_complement_overlap have "O s x ∨ O s (─x)"..
    thus "False"
    proof
      assume "O s x"
      with ‹¬ O s x› show "False"..
    next
      assume "O s (─x)"
      with ‹¬ O s (─x )› show "False"..
    qed
  qed 
  ultimately show "x = ─(─x)"
    by (rule part_antisymmetry)
qed

lemma part_complement_reversal: "y ≠ u ⟹ P x y ⟹ P (─y) (─x)"
proof - 
  assume "y ≠ u"
  hence ny: "∀ w. P w (─y) ⟷ ¬ O w y"
    by (rule strong_complement_character)
  assume "P x y"
  have "x ≠ u"
  proof
    assume "x = u"
    hence "P u y" using ‹P x y› by (rule subst)
    with universe_character have "y = u"
      by (rule part_antisymmetry)
    with ‹y ≠ u› show "False"..
  qed
  hence "∀ w. P w (─x) ⟷ ¬ O w x"
    by (rule strong_complement_character)
  hence "P (─y) (─x) ⟷ ¬ O (─y) x"..
  moreover have "¬ O (─y) x"
  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"..
    hence "P v (─y)"..
    from ny have "P v (─y) ⟷ ¬ O v y"..
    hence "¬ O v y" using ‹P v (─y)›..
    moreover from v have "P v x"..
    hence "P v y" using ‹P x y›
      by (rule part_transitivity)
    hence "O v y" 
      by (rule part_implies_overlap)
    ultimately show "False"..
  qed
  ultimately show "P (─y) (─x)"..
qed

lemma complements_overlap: "x ⊕ y ≠ u ⟹ O(─x)(─y)"
proof -
  assume "x ⊕ y ≠ u"
  hence "∃ z. ¬ O z (x ⊕ y)"
    by (rule something_disjoint)
  then obtain z where z:"¬ O z (x ⊕ y)"..
  hence "¬ O z x" by (rule first_summand_disjointness)
  hence "P z (─x)" by (rule complement_part)
  moreover from z have "¬ O z y" 
    by (rule second_summand_disjointness)
  hence "P z (─y)" by (rule complement_part)
  ultimately show "O(─x)(─y)"
    by (rule overlap_intro)
qed

lemma sum_complement_in_complement_product: 
  "x ⊕ y ≠ u ⟹ P(─(x ⊕ y))(─x ⊗ ─y)"
proof -
  assume "x ⊕ y ≠ u"
  hence "O (─x) (─y)"
    by (rule complements_overlap)
  hence "∀ w. P w (─x ⊗ ─y) ⟷ (P w (─x) ∧ P w (─y))"
    by (rule product_character)
  hence "P(─(x ⊕ y))(─x ⊗ ─y)⟷(P(─(x ⊕ y))(─x) ∧ P(─(x ⊕ y))(─y))"..
  moreover have "P (─(x ⊕ y))(─x) ∧ P (─(x ⊕ y))(─y)"
  proof
    show "P (─(x ⊕ y))(─x)" using ‹x ⊕ y ≠ u› first_summand_in_sum
      by (rule part_complement_reversal)
  next
    show  "P (─(x ⊕ y))(─y)" using ‹x ⊕ y ≠ u› second_summand_in_sum
      by (rule part_complement_reversal)
  qed
  ultimately show "P (─(x ⊕ y))(─x ⊗ ─y)"..
qed

lemma complement_product_in_sum_complement: 
  "x ⊕ y ≠ u ⟹ P(─x ⊗ ─y)(─(x ⊕ y))"
proof -
  assume "x ⊕ y ≠ u"
  hence "∀w. P w (─(x ⊕ y)) ⟷ ¬ O w (x ⊕ y)"
    by (rule strong_complement_character)
  hence "P (─x ⊗ ─y) (─(x ⊕ y)) ⟷ (¬ O (─x ⊗ ─y) (x ⊕ y))"..
  moreover have "¬ O (─x ⊗ ─y) (x ⊕ y)"
  proof
    have "O(─x)(─y)" using ‹x ⊕ y ≠ u› by (rule complements_overlap)
    hence p: "∀ v. P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))" 
      by (rule product_character)
    have "O(─x ⊗ ─y)(x ⊕ y) ⟷ (O(─x ⊗ ─y) x ∨ O(─x ⊗ ─y)y)"
      using sum_character..
    moreover assume "O (─x ⊗ ─y)(x ⊕ y)"
    ultimately have "O (─x ⊗ ─y) x ∨ O (─x ⊗ ─y) y"..
    thus "False"
    proof
      assume "O (─x ⊗ ─y) x"
      with overlap_eq have "∃ v. P v (─x ⊗ ─y) ∧ P v x"..
      then obtain v where v: "P v (─x ⊗ ─y) ∧ P v x"..
      hence "P v (─x ⊗ ─y)"..
      from p have "P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))"..
      hence "P v (─x) ∧ P v (─y)" using ‹P v (─x ⊗ ─y)›..
      hence "P v (─x)"..
      have "x ≠ u" using ‹x ⊕ y ≠ u›
        by (rule first_summand_not_universe)
      hence "∀w. P w (─x) ⟷ ¬ O w x"
        by (rule strong_complement_character)
      hence "P v (─x) ⟷ ¬ O v x"..
      hence "¬ O v x" using ‹P v (─x)›..
      moreover from v have "P v x"..
      hence "O v x" by (rule part_implies_overlap)
      ultimately show "False"..
    next 
      assume "O (─x ⊗ ─y) y"
      with overlap_eq have "∃ v. P v (─x ⊗ ─y) ∧ P v y"..
      then obtain v where v: "P v (─x ⊗ ─y) ∧ P v y"..
      hence "P v (─x ⊗ ─y)"..
      from p have "P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))"..
      hence "P v (─x) ∧ P v (─y)" using ‹P v (─x ⊗ ─y)›..
      hence "P v (─y)"..
      have "y ≠ u" using ‹x ⊕ y ≠ u›
        by (rule second_summand_not_universe)
      hence "∀w. P w (─y) ⟷ ¬ O w y"
        by (rule strong_complement_character)
      hence "P v (─y) ⟷ ¬ O v y"..
      hence "¬ O v y" using ‹P v (─y)›..
      moreover from v have "P v y"..
      hence "O v y" by (rule part_implies_overlap)
      ultimately show "False"..
    qed
  qed
  ultimately show "P (─x ⊗ ─y) (─(x ⊕ y))"..
qed

theorem sum_complement_is_complements_product:
  "x ⊕ y ≠ u ⟹ ─(x ⊕ y) = (─x ⊗ ─y)"
proof -
  assume "x ⊕ y ≠ u"
  show "─(x ⊕ y) = (─x ⊗ ─y)"
  proof (rule part_antisymmetry)
    show "P (─ (x ⊕ y)) (─ x ⊗ ─ y)" using  ‹x ⊕ y ≠ u›
      by (rule sum_complement_in_complement_product)
    show "P (─ x ⊗ ─ y) (─ (x ⊕ y))" using ‹x ⊕ y ≠ u›
      by (rule complement_product_in_sum_complement)
  qed
qed

lemma complement_sum_in_product_complement: 
  "O x y ⟹ x ≠ u ⟹ y ≠ u ⟹ P ((─x) ⊕ (─y))(─(x ⊗ y))"
proof -
  assume "O x y"
  assume "x ≠ u"
  assume "y ≠ u"
  have "x ⊗ y ≠ u"
  proof
    assume "x ⊗ y = u"
    with ‹O x y› have "x = u"
      by (rule product_universe_implies_factor_universe)
    with ‹x ≠ u› show "False"..
  qed
  hence notxty: "∀ w. P w (─(x ⊗ y)) ⟷ ¬ O w (x ⊗ y)"
    by (rule strong_complement_character)
  hence "P((─x)⊕(─y))(─(x ⊗ y)) ⟷ ¬O((─x)⊕(─y))(x ⊗ y)"..
  moreover have "¬ O ((─x) ⊕ (─y)) (x ⊗ y)"
  proof
    from sum_character have 
      "∀ w. O w ((─x) ⊕ (─y)) ⟷ (O w (─x) ∨ O w (─y))".
    hence "O(x ⊗ y)((─x)⊕(─y)) ⟷ (O(x ⊗ y)(─x) ∨ O(x ⊗ y)(─y))"..
    moreover assume "O ((─x) ⊕ (─y)) (x ⊗ y)"
    hence "O (x ⊗ y) ((─x) ⊕ (─y))" by (rule overlap_symmetry)
    ultimately have "O (x ⊗ y) (─x) ∨ O (x ⊗ y) (─y)"..
    thus False
    proof
      assume "O (x ⊗ y)(─x)"
      with overlap_eq have "∃ v. P v (x ⊗ y) ∧ P v (─x)"..
      then obtain v where v: "P v (x ⊗ y) ∧ P v (─x)"..
      hence "P v (─x)"..
      with ‹x ≠ u› have "¬ P v x"
        by (rule complement_part_not_part)
      moreover from v have "P v (x ⊗ y)"..
      with ‹O x y› have "P v x" by (rule product_part_in_first_factor)
      ultimately show "False"..
    next 
      assume "O (x ⊗ y) (─y)"
      with overlap_eq have "∃ v. P v (x ⊗ y) ∧ P v (─y)"..
      then obtain v where v: "P v (x ⊗ y) ∧ P v (─y)"..
      hence "P v (─y)"..
      with ‹y ≠ u› have "¬ P v y" 
        by (rule complement_part_not_part)
      moreover from v have "P v (x ⊗ y)"..
      with ‹O x y› have "P v y" by (rule product_part_in_second_factor)
      ultimately show "False"..
    qed
  qed
  ultimately show "P ((─x) ⊕ (─y))(─(x ⊗ y))"..
qed

lemma product_complement_in_complements_sum:  
  "x ≠ u ⟹ y ≠ u ⟹ P(─(x ⊗ y))((─x) ⊕ (─y))"
proof -
  assume "x ≠ u"
  hence "x = ─(─x)"
    by (rule complement_involution)
  assume "y ≠ u"
  hence "y = ─(─y)"
    by (rule complement_involution)
  show "P (─(x ⊗ y))((─x) ⊕ (─y))"
  proof cases
    assume "─x ⊕ ─y = u"
    thus "P (─(x ⊗ y))((─x) ⊕ (─y))"
      using universe_character by (rule ssubst)
  next
    assume "─x ⊕ ─y ≠ u"
    hence "─x ⊕ ─y = ─(─(─x ⊕ ─ y))"
      by (rule complement_involution)
    moreover have "─(─x ⊕ ─y) = ─(─x) ⊗ ─(─y)" 
      using ‹─x ⊕ ─y ≠ u› 
      by (rule sum_complement_is_complements_product)
    with ‹x = ─(─x)› have  "─(─x ⊕ ─y) = x ⊗ ─(─y)" 
      by (rule ssubst)
    with ‹y = ─(─y)› have  "─(─x ⊕ ─y) = x ⊗ y" 
      by (rule ssubst)
    hence "P (─(x ⊗ y))(─(─(─x ⊕ ─y)))"
      using part_reflexivity by (rule subst)
    ultimately show "P (─(x ⊗ y))(─x ⊕ ─y)" 
      by (rule ssubst)
  qed
qed

theorem complement_of_product_is_sum_of_complements:
  "O x y ⟹ x ⊕ y ≠ u ⟹ ─(x ⊗ y) = (─x) ⊕ (─y)"
proof -
  assume "O x y"
  assume "x ⊕ y ≠ u"
  show "─(x ⊗ y) = (─x) ⊕ (─y)"
  proof (rule part_antisymmetry)
    have "x ≠ u" using ‹x ⊕ y ≠ u› 
      by (rule first_summand_not_universe)
    have "y ≠ u" using ‹x ⊕ y ≠ u› 
      by (rule second_summand_not_universe) 
    show "P (─ (x ⊗ y)) (─ x ⊕ ─ y)"
      using ‹x ≠ u› ‹y ≠ u› by (rule product_complement_in_complements_sum)
    show " P (─ x ⊕ ─ y) (─ (x ⊗ y))"
      using ‹O x y› ‹x ≠ u› ‹y ≠ u› by (rule complement_sum_in_product_complement)
  qed
qed

end

(*<*) end (*>*)