7 Prove each of the following laws of Binary Theory using the proof format given in Subsection 1.0.1, and any laws listed in Section 11.4. Do not use the Completion Rule.
(a)
§
(b) §
(c) §
if a then a else ¬a fi = a=a
=⊤
OR if a then a else ¬a fi
if a then a else ¬a fi
= a∧a ∨ ¬a∧¬a
= a ∨ ¬a =⊤
OR if a then a else ¬a fi
= if a then ⊤ else ¬⊥ fi
= if a then ⊤ else ⊤ fi =⊤
ifbthencelse¬cfi = ifcthenbelse¬bfi
if b then c else ¬c fi
= b∧c ∨ ¬b∧¬c
= c∧b ∨ ¬c∧¬b
= ifcthenbelse¬bfi
ifb∧cthenPelseQfi = ifbthenifcthenPelseQfielseQfi
if b then if c then P else Q fi else Q fi
= b ∧ (c∧P ∨ ¬c∧Q) ∨ ¬b∧Q
= b∧c∧P ∨ b∧¬c∧Q ∨ ¬b∧Q
= b∧c∧P ∨ (b∧¬c ∨ ¬b) ∧ Q
= b∧c∧P ∨ (¬b ∨ b∧¬c) ∧ Q
= b∧c∧P ∨ (¬b ∨ b)∧(¬b ∨ ¬c)∧Q
= b∧c∧P ∨ ⊤∧¬(b∧c)∧Q
= b∧c∧P ∨ ¬(b∧c)∧Q
= ifb∧cthenPelseQfi
case analysis, twice distribution distribution symmetry distribution excluded middle, duality identity case analysis
one-case reflexive
case analysis idempotencetwice excluded middle
context binary law generic case idempotent law
case analysis symmetry twice case analysis
(d) §
(e) §
(f) §
ifb∨cthenPelseQfi = ifbthenPelseifcthenPelseQfifi ifbthenPelseifcthenPelseQfifi caseanalysistwice
= b∧P ∨ ¬b∧(c∧P ∨ ¬c∧Q)
= b∧P ∨ ¬b∧c∧P ∨ ¬b∧¬c∧Q
= (b ∨ ¬b∧c)∧P ∨ ¬b∧¬c∧Q
= (b ∨ ¬b)∧(b ∨ c)∧P ∨ ¬(b ∨ c)∧Q
= (b ∨ c)∧P ∨ ¬(b ∨ c)∧Q
= ifb∨cthenPelseQfi
distribute factor (undistribute) distribute, duality excluded middle and identity case analysis
ifbthenPelseifbthenQelseRfifi = ifbthenPelseRfi
ifbthenPelseifbthenQelseRfifi context
= ifbthenPelseif⊥thenQelseRfifi casebase
= ifbthenPelseRfi
if if b then c else d fi then P else Q fi
= ifbthenifcthenPelseQfielseifdthenPelseQfifi
if if b then c else d fi then P else Q fi
= ifbthencelsedfi∧P ∨ ¬ifbthencelsedfi∧Q
= if b then c∧P else d∧P fi ∨ if b then ¬c∧Q else ¬d∧Q fi
case analysis distribute distribute
= =
(g)
=
§
=
=
= =
(h)
=
§
=
= =
if b then c∧P ∨ ¬c∧Q else d∧P ∨ ¬d∧Q fi case analysis ifbthenifcthenPelseQfielseifdthenPelseQfifi
ifbthenifcthenPelseRfielseifcthenQelseRfifi ifcthenifbthenPelseQfielseRfi ifbthenifcthenPelseRfielseifcthenQelseRfifi caseidempotent ifcthenifbthenifcthenPelseRfielseifcthenQelseRfi
else if b then if c then P else R fi else if c then Q else R fi fi fi context ifcthenifbthenif⊤thenPelseRfielseif⊤thenQelseRfi
else if b then if ⊥ then P else R fi else if ⊥ then Q else R fi fi fi case base ifcthenifbthenPelseQfielseifbthenRelseRfifi caseidempotent ifcthenifbthenPelseQfielseRfi
ifbthenifcthenPelseRfielseifdthenQelseRfifi
if if b then c else d fi then if b then P else Q fi else R fi
if if b then c else d fi then if b then P else Q fi else R fi case analysis law ifbthencelsedfi∧ifbthenPelseQfi ∨ ¬ifbthencelsedfi∧R
four case distributive laws if b then c∧P ∨ ¬c∧R else d∧Q ∨ ¬d∧R fi case analysis law twice
ifbthenifcthenPelseRfielseifdthenQelseRfifi