MatchingLogic.EntryIII.CanonicalChoice

theorem MatchingLogic.Provable.and_decide {S : Signature} {Gamma : Set (Pattern S ℕ)} (Phi psi : Pattern S ℕ) : Provable Gamma (Phi.imp ((Phi.and psi).or (Phi.and psi.nt)))

Propositional decision while retaining the current finite-stage conjunction: Phi -> (Phi and psi) or (Phi and not psi).

theorem MatchingLogic.IsMCS.app_choice_at {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) {sigma : S.Sym} (args : Fin (S.arity sigma) → Pattern S ℕ) (i : Fin (S.arity sigma)) (psi : Pattern S ℕ) (happ : Pattern.app sigma args ∈ Gamma) : ∃ (b : Bool), Pattern.app sigma (Function.update args i ((args i).and (if b = true then psi else psi.nt))) ∈ Gamma

The one-coordinate distribution step. It is the binary branching node in the source's 2^n disjunction argument.

theorem MatchingLogic.IsMCS.app_joint_choice {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) {sigma : S.Sym} (Phi : Fin (S.arity sigma) → Pattern S ℕ) (psi : Pattern S ℕ) (happ : Pattern.app sigma Phi ∈ Gamma) : ∃ (choose : Fin (S.arity sigma) → Bool), (Pattern.app sigma fun (i : Fin (S.arity sigma)) => (Phi i).and (if choose i = true then psi else psi.nt)) ∈ Gamma

Joint finite-product decision used in every stage of the n-ary canonical Existence Lemma. This includes the nullary case.

theorem MatchingLogic.IsMCS.exists_joint_choice {S : Signature} {Gamma : Set (Pattern S ℕ)} (hM : IsMCS Gamma) {sigma : S.Sym} (L : Fin (S.arity sigma) → List (Pattern S ℕ)) (psi : Pattern S ℕ) (happ : (Pattern.app sigma fun (i : Fin (S.arity sigma)) => conj (L i)) ∈ Gamma) : ∃ (choose : Fin (S.arity sigma) → Bool), (Pattern.app sigma fun (i : Fin (S.arity sigma)) => (conj (L i)).and (if choose i = true then psi else psi.nt)) ∈ Gamma

List-conjunction specialization consumed directly by the simultaneous finite-stage construction in the canonical Existence Lemma.