集合と写像の証明

次を示す。

• f(A)＼f(P) ⊆ f(A＼P)

下に、清書したフォワードプルーフ。作業的にはバックワード探索をしている。

使う（一部未使用）定義、論理法則、推論規則：

• DefSetInc: A⊆B :⇔ ∀x.(x∈A ⇒ x∈B)
• DefSetDiff: X = A＼B :⇔ ∀x.(x∈X ⇔ (x∈A ∧ ¬(x∈B)))
• DefSetDiff: x∈A＼B :⇔ x∈A ∧ ¬(x∈B)
• DefMapImage: y∈f(A) :⇔ ∃x.(x∈A ∧ f(x) = y)
• LawDeMor: ¬(A∧B) ⇔ ¬A∨¬B
• LawDeMor: ¬(A∨B) ⇔ ¬A∧¬B
• LawDeMor: ¬∀x.P ⇔ ∃x.¬P
• LawDeMor: ¬∃x.P ⇔ ∀x.¬P
• LawContrapo: (A⇒B) ⇔ (¬B⇒A)
• LawConjAssoc: (A∧B)∧C ⇔ A∧(B∧C)
• LawConjComm: A∧B ⇔ B∧A
• RuleDisjNeg: A∨B, ¬B |- A

// SerND 差集合の像
put
 f(A)＼f(P) ⊆ f(A＼P) ---(goal)
proof of (goal)
 assume
  y∈(f(A)＼f(P)) ---(ass)
 expand by DefSetDiff
  y∈f(A) ∧ ¬(y∈f(P))
 expand $.1 by DefMapImage; expnad $.2.1 by DefMapImage
  ∃x.(x∈A ∧ f(x) = y) ∧ ¬(∃x.(x∈P ∧ f(x) = y)
 apply LawDeMor to $.2
  ∃x.(x∈A ∧ f(x) = y) ∧ ∀x.(¬(x∈P) ∨ ¬(f(x) = y)) ---(ass')
 select $.1
  ∃x.(x∈A ∧ f(x) = y)
 choice a
    a∈A ∧ f(a) = y ---(ch)
   select $.2 of (ass')
    ∀x.(¬(x∈P) ∨ ¬(f(x) = y))
   instantiate by a
    ¬(a∈P) ∨ ¬(f(a) = y) ---(inst)
   select $.2 of (ch)
    f(a) = y ---(ch2)
   call RuleDistNeg[(inst), (ch2)]
    ¬(a∈P)
   concat with (ch)
    ¬(a∈P) ∧ (a∈A ∧ f(a) = y)
   rewrite by LawConjAsoc, LawConjComm
    (a∈A ∧ ¬(a∈P)) ∧ f(a) = y
   introduce existential witness a
    ∃x.((x∈A ∧ ¬(x∈P)) ∧ f(x) = y)
 end choice
  ∃x.((x∈A ∧ ¬(x∈P)) ∧ f(x) = y)
 contract $.1.1 by DefSetDiff
  ∃x.(x∈A＼P ∧ f(x) = y)
 contract by DefMapImage
  y∈f(A＼P)
 use condition (ass)
  y∈(f(A)＼f(P)) ⇒ y∈f(A＼P)
 contract by Def SetInc
  f(A)＼f(P) ⊆ f(A＼P)
end proof of (goal)