Removed from MATH/EECS 1019: Discrete Math

	Propositional
	- Eval/Build	If ¬α, then α → γ
	- Simplify	If ¬ β, then (γ → β iff ¬ γ)
	- Precedence & Parse Trees	¬P ∨ Q ∧ R → P ∧ Q   ≡   ((¬P)∨(Q ∧ R)) → (P ∧ Q)
	- Pleasing Father	(A ∨ B)→ C)   ≢   (A → C) ∨ (B → C)   ≡   (A ∧ B)→ C)
	Quantifiers
	- And-Or Tree Game	Prover/Adversary Game on Tree
	- Negations	¬∃xP(x) ≡ ∀x¬P(x)
	- Restricted Domain	∃x∈S,P(x) ≡ ∃x,(x∈S)∧P(x) and ∀x∈S,P(x) ≡ ∀x,(x∈S)→P(x)
	- Empty Set	∀x∈S,P(x) is true if S is empty.
	- Sets of Tuples	α is true for each tuple in S = {❬x1,y1,x2,y2❭ | x1&x2∈U, y1=y1∃, y2=y2∃(x1)}
	- Skolem/Auxiliary Functions	∀x∃yP(x,y) ⇒ P(x,y∃(x))
	- Free and Bound Variables:	α(x)∧∀xβ(x)
	- Understanding from the Inside	∀x [∃y+y=0] ≡ ∀x Property(x)
	- Constructive & Contradiction	I don't like proofs of ∀x P(x) that assume the contradiction so that it can construct an x.
		Instead, say "Let x be an arbitrary object."
	- The Proof Viewed as a Game:	Boss gives values to free variables.
		Oracle assures you of A when proving A→B.
		Prover works to prove by providing good ∃x objects.
		Adversary works to disprove by providing worst case ∀y objects.
	- Game Tree	∃Mw1∀Mb1∃Mw2∀Mb2... White-Wins(Mw1,Mb1,Mw2,Mb2,...)
	- Solution to Hard Problem	∃ solution y HardProblem(y) & ∀ potential counter examples x ¬HardProblem(x)