∀x (¬Strike(x) ∨ Contract(x)) ⇒Report(x)
Eliminate ⇒
∀x ¬(¬Strike(x) ∨ Contract(x))∨Report(x)
Push negation inside
∀x Strike(x) ∧¬Contract(x)∨Report(x)
is this correct?
∀x (¬Strike(x) ∨ Contract(x)) ⇒Report(x)
Eliminate ⇒
∀x ¬(¬Strike(x) ∨ Contract(x))∨Report(x)
Push negation inside
∀x Strike(x) ∧¬Contract(x)∨Report(x)
is this correct?
Copyright © 2021 JogjaFile Inc.
The procedure is not wrong, although the names for the justification names are off. Well, it is clear what you mean, so that's not too wrong. However, it is better to get the terminology down.
Additionally, to derive a Conjunctive Normal Form you need just one more step. You want a conjunction of disjuncts.
$$\def\Strike{\operatorname{Strike}}\def\Contract{\operatorname{Contract}}\def\Report{\operatorname{Report}} {\forall x~(\neg\Strike(x) \lor \Contract(x)~\to~ \Report(x))\\\quad\Updownarrow\quad\text{Implication Equivalence}\\\forall x~(\neg(\neg\Strike(x)\lor\Contract(x))\lor\Report(x))\\\quad\Updownarrow\quad\text{de Morgan's Duality}\\\forall x~((\Strike(x)\land\neg\Contract(x))\lor\Report(x))\\\quad\Updownarrow\quad\text{Distribution}\\\bbox[border:dotted navy 1pt]{\phantom{\forall x~((\Strike(x)\lor\Report(x))\land(\neg\Contract(x)\lor\Report(x)))}}}$$