FunctionalCompleteness
Difficulty: optional — 7 definitions, 2 abbreviations, 8 lemmas, 0 theorems, 0 examples.
A set of connectives is functionally complete when every truth table is the truth table of some formula built only from that set. Negation, conjunction, and disjunction together are functionally complete: the canonical disjunctive normal form witnesses this for any truth table. A row of the truth table where the function is true becomes a conjunction of literals (an atom, or its negation, matching that row); the function itself becomes the disjunction of those rows.
The next chapter builds on this to show that the Sheffer stroke alone is already functionally complete.
Logic.PropositionalLogic.BoolFun
A Boolean function taking \(n\) Boolean arguments.
abbrev Logic.PropositionalLogic.BoolFun (n : ℕ) : Type
Show details
| Logic.PropositionalLogic.BoolFun n = ((Fin n → Bool) → Bool)
Complexity: 9 (size of the value term)
Outer dependencies: (none)
Logic.PropositionalLogic.Formula.witness
The distinguished atom used to build a tautology and a contradiction below: since there is at least one argument (\(n + 1\) of them), there is always at least one atom to use.
abbrev Logic.PropositionalLogic.Formula.witness✝ {n : ℕ} : Fin (n + 1)
Show details
| Logic.PropositionalLogic.Formula.witness✝ = ⟨0, ⋯⟩
Complexity: 43 (size of the value term)
Outer dependencies: (none)
Lean core dependencies: Fin, Nat, Nat.succ_pos
Logic.PropositionalLogic.Formula.verum'
A tautology: true under every valuation. The base case for a (possibly empty) conjunction.
def Logic.PropositionalLogic.Formula.verum'✝ {n : ℕ} : Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details
| Logic.PropositionalLogic.Formula.verum'✝ = (Logic.PropositionalLogic.Formula.atom Logic.PropositionalLogic.Formula.witness✝).imp (Logic.PropositionalLogic.Formula.atom Logic.PropositionalLogic.Formula.witness✝)
Complexity: 142 (size of the value term)
Outer dependencies: Logic.PropositionalLogic.Formula
Inner dependencies: Logic.PropositionalLogic.Formula.witness
Logic.PropositionalLogic.Formula.val_verum'
theorem Logic.PropositionalLogic.Formula.val_verum'✝ {n : ℕ} (w : Logic.PropositionalLogic.Valuation (Fin (n + 1))) : Logic.PropositionalLogic.Formula.val w Logic.PropositionalLogic.Formula.verum'✝ = true
Show details
fun {n} w => of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Logic.PropositionalLogic.Formula.val.eq_5 w (Logic.PropositionalLogic.Formula.atom 0) (Logic.PropositionalLogic.Formula.atom 0)) (Bool.not_or_self (w 0)))) true) (eq_self true))
Complexity: 1351 (size of the value term)
Dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Formula.verum', Logic.PropositionalLogic.Valuation
Logic.PropositionalLogic.Formula.falsum'
A contradiction: false under every valuation. The base case for a (possibly empty) disjunction.
def Logic.PropositionalLogic.Formula.falsum'✝ {n : ℕ} : Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details
| Logic.PropositionalLogic.Formula.falsum'✝ = (Logic.PropositionalLogic.Formula.atom Logic.PropositionalLogic.Formula.witness✝).and (Logic.PropositionalLogic.Formula.atom Logic.PropositionalLogic.Formula.witness✝).neg
Complexity: 172 (size of the value term)
Outer dependencies: Logic.PropositionalLogic.Formula
Inner dependencies: Logic.PropositionalLogic.Formula.witness
Logic.PropositionalLogic.Formula.val_falsum'
theorem Logic.PropositionalLogic.Formula.val_falsum'✝ {n : ℕ} (w : Logic.PropositionalLogic.Valuation (Fin (n + 1))) : Logic.PropositionalLogic.Formula.val w Logic.PropositionalLogic.Formula.falsum'✝ = false
Show details
fun {n} w => of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Logic.PropositionalLogic.Formula.val.eq_3 w (Logic.PropositionalLogic.Formula.atom 0) (Logic.PropositionalLogic.Formula.atom 0).neg) (Bool.and_not_self (w 0)))) false) (eq_self false))
Complexity: 1469 (size of the value term)
Dependencies: Logic.PropositionalLogic.Formula.falsum', Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation
Logic.PropositionalLogic.Formula.bigAnd
The conjunction of a list of formulas: true exactly when every formula in the list is. Unfolds via the already-simp List.foldr equations, so it needs no separate step lemmas.
def Logic.PropositionalLogic.Formula.bigAnd {n : ℕ} (l : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))) : Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details
| Logic.PropositionalLogic.Formula.bigAnd l = List.foldr Logic.PropositionalLogic.Formula.and Logic.PropositionalLogic.Formula.verum'✝ l
Complexity: 273 (size of the value term)
Outer dependencies: Logic.PropositionalLogic.Formula
Inner dependencies: Logic.PropositionalLogic.Formula.verum'
Lean core dependencies: Fin, List, List.foldr, Nat
Logic.PropositionalLogic.Formula.bigAnd_val
theorem Logic.PropositionalLogic.Formula.bigAnd_val {n : ℕ} (l : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))) (w : Logic.PropositionalLogic.Valuation (Fin (n + 1))) : Logic.PropositionalLogic.Formula.val w (Logic.PropositionalLogic.Formula.bigAnd l) = true ↔ ∀ φ ∈ l, Logic.PropositionalLogic.Formula.val w φ = true
Show details
fun {n} l w => id (List.rec (of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Logic.PropositionalLogic.Formula.val_verum'✝ w)) true) (eq_self true))) (Eq.trans (forall_congr fun φ => Eq.trans (implies_congr List.not_mem_nil._simp_1 (Eq.refl (Logic.PropositionalLogic.Formula.val w φ = true))) IsEmpty.forall_iff._simp_1) (implies_true (Logic.PropositionalLogic.Formula (Fin (n + 1)))))) (iff_self True))) (fun φ l ih => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (Eq.trans (congrFun' (congrArg Eq (Logic.PropositionalLogic.Formula.val.eq_3 w φ (List.foldr Logic.PropositionalLogic.Formula.and Logic.PropositionalLogic.Formula.verum'✝ l))) true) (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val w φ) (Logic.PropositionalLogic.Formula.val w (List.foldr Logic.PropositionalLogic.Formula.and Logic.PropositionalLogic.Formula.verum'✝ l)))) (congrArg (And (Logic.PropositionalLogic.Formula.val w φ = true)) (propext ih)))) (Eq.trans (forall_congr fun φ_1 => implies_congr List.mem_cons._simp_1 (Eq.refl (Logic.PropositionalLogic.Formula.val w φ_1 = true))) forall_eq_or_imp._simp_1)) (iff_self (Logic.PropositionalLogic.Formula.val w φ = true ∧ ∀ φ ∈ l, Logic.PropositionalLogic.Formula.val w φ = true)))) l)
Complexity: 12574 (size of the value term)
Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.bigAnd, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation
Proof dependencies: Logic.PropositionalLogic.Formula.val_verum', Logic.PropositionalLogic.Formula.verum'
Lean core dependencies: And, Bool, Bool.and, Bool.and_eq_true, Eq, Eq.trans, False, Fin, Iff, List, List.foldr, Nat, Or, True, congr, congrArg, congrFun', eq_self, forall_congr, id, iff_self, implies_congr, implies_true, of_eq_true
Logic.PropositionalLogic.Formula.bigOr
The disjunction of a list of formulas: true exactly when some formula in the list is.
def Logic.PropositionalLogic.Formula.bigOr {n : ℕ} (l : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))) : Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details
| Logic.PropositionalLogic.Formula.bigOr l = List.foldr Logic.PropositionalLogic.Formula.or Logic.PropositionalLogic.Formula.falsum'✝ l
Complexity: 303 (size of the value term)
Outer dependencies: Logic.PropositionalLogic.Formula
Inner dependencies: Logic.PropositionalLogic.Formula.falsum'
Lean core dependencies: Fin, List, List.foldr, Nat
Logic.PropositionalLogic.Formula.bigOr_val
theorem Logic.PropositionalLogic.Formula.bigOr_val {n : ℕ} (l : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))) (w : Logic.PropositionalLogic.Valuation (Fin (n + 1))) : Logic.PropositionalLogic.Formula.val w (Logic.PropositionalLogic.Formula.bigOr l) = true ↔ ∃ φ ∈ l, Logic.PropositionalLogic.Formula.val w φ = true
Show details
fun {n} l w => id (List.rec (of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Logic.PropositionalLogic.Formula.val_falsum'✝ w)) true) Bool.false_eq_true)) (Eq.trans (congrArg Exists (funext fun φ => Eq.trans (congrFun' (congrArg And List.not_mem_nil._simp_1) (Logic.PropositionalLogic.Formula.val w φ = true)) (false_and (Logic.PropositionalLogic.Formula.val w φ = true)))) exists_false._simp_1)) (iff_self False))) (fun φ l ih => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (Eq.trans (congrFun' (congrArg Eq (Logic.PropositionalLogic.Formula.val.eq_4 w φ (List.foldr Logic.PropositionalLogic.Formula.or Logic.PropositionalLogic.Formula.falsum'✝ l))) true) (Bool.or_eq_true (Logic.PropositionalLogic.Formula.val w φ) (Logic.PropositionalLogic.Formula.val w (List.foldr Logic.PropositionalLogic.Formula.or Logic.PropositionalLogic.Formula.falsum'✝ l)))) (congrArg (Or (Logic.PropositionalLogic.Formula.val w φ = true)) (propext ih)))) (Eq.trans (congrArg Exists (funext fun φ_1 => congrFun' (congrArg And List.mem_cons._simp_1) (Logic.PropositionalLogic.Formula.val w φ_1 = true))) exists_eq_or_imp._simp_1)) (iff_self (Logic.PropositionalLogic.Formula.val w φ = true ∨ ∃ φ ∈ l, Logic.PropositionalLogic.Formula.val w φ = true)))) l)
Complexity: 14624 (size of the value term)
Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.bigOr, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation
Proof dependencies: Logic.PropositionalLogic.Formula.falsum', Logic.PropositionalLogic.Formula.val_falsum'
Logic.PropositionalLogic.Formula.literal
The literal for atom \(i\) under valuation \(v\): the atom itself if \(v\) makes it true, its negation otherwise.
def Logic.PropositionalLogic.Formula.literal {n : ℕ} (v : Logic.PropositionalLogic.Valuation (Fin (n + 1))) (i : Fin (n + 1)) : Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details
| Logic.PropositionalLogic.Formula.literal v i = if v i = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg
Complexity: 203 (size of the value term)
Outer dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Valuation
Logic.PropositionalLogic.Formula.literal_val
theorem Logic.PropositionalLogic.Formula.literal_val {n : ℕ} (v w : Logic.PropositionalLogic.Valuation (Fin (n + 1))) (i : Fin (n + 1)) : Logic.PropositionalLogic.Formula.val w (Logic.PropositionalLogic.Formula.literal v i) = true ↔ w i = v i
Show details
fun {n} v w i => id (Bool.casesOn (motive := fun t => v i = t → (Logic.PropositionalLogic.Formula.val w (if v i = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ w i = v i)) (v i) (fun h => Eq.ndrec (motive := fun x => v i = x → (Logic.PropositionalLogic.Formula.val w (if x = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ w i = x)) (fun hv => Bool.casesOn (motive := fun t => w i = t → (Logic.PropositionalLogic.Formula.val w (if false = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ w i = false)) (w i) (fun h => Eq.ndrec (motive := fun x => w i = x → (Logic.PropositionalLogic.Formula.val w (if false = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ x = false)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Logic.PropositionalLogic.Formula.val w) (ite_cond_eq_false (Logic.PropositionalLogic.Formula.atom i) (Logic.PropositionalLogic.Formula.atom i).neg Bool.false_eq_true)) (Logic.PropositionalLogic.Formula.val.eq_2 w (Logic.PropositionalLogic.Formula.atom i))) (Eq.trans (congrArg not hw) Bool.not_false))) true) (eq_self true))) (eq_self false)) (iff_self True))) (Eq.symm h) (Eq.refl (w i))) (fun h => Eq.ndrec (motive := fun x => w i = x → (Logic.PropositionalLogic.Formula.val w (if false = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ x = false)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Logic.PropositionalLogic.Formula.val w) (ite_cond_eq_false (Logic.PropositionalLogic.Formula.atom i) (Logic.PropositionalLogic.Formula.atom i).neg Bool.false_eq_true)) (Logic.PropositionalLogic.Formula.val.eq_2 w (Logic.PropositionalLogic.Formula.atom i))) (Eq.trans (congrArg not hw) Bool.not_true))) true) Bool.false_eq_true)) Bool.true_eq_false) (iff_self False))) (Eq.symm h) (Eq.refl (w i))) (Eq.refl (w i))) (Eq.symm h) (Eq.refl (v i))) (fun h => Eq.ndrec (motive := fun x => v i = x → (Logic.PropositionalLogic.Formula.val w (if x = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ w i = x)) (fun hv => Bool.casesOn (motive := fun t => w i = t → (Logic.PropositionalLogic.Formula.val w (if true = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ w i = true)) (w i) (fun h => Eq.ndrec (motive := fun x => w i = x → (Logic.PropositionalLogic.Formula.val w (if true = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ x = true)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Logic.PropositionalLogic.Formula.val w) (ite_cond_eq_true (Logic.PropositionalLogic.Formula.atom i) (Logic.PropositionalLogic.Formula.atom i).neg (eq_self true))) (Logic.PropositionalLogic.Formula.val.eq_1 w i)) hw)) true) Bool.false_eq_true)) Bool.false_eq_true) (iff_self False))) (Eq.symm h) (Eq.refl (w i))) (fun h => Eq.ndrec (motive := fun x => w i = x → (Logic.PropositionalLogic.Formula.val w (if true = true then Logic.PropositionalLogic.Formula.atom i else (Logic.PropositionalLogic.Formula.atom i).neg) = true ↔ x = true)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Logic.PropositionalLogic.Formula.val w) (ite_cond_eq_true (Logic.PropositionalLogic.Formula.atom i) (Logic.PropositionalLogic.Formula.atom i).neg (eq_self true))) (Logic.PropositionalLogic.Formula.val.eq_1 w i)) hw)) true) (eq_self true))) (eq_self true)) (iff_self True))) (Eq.symm h) (Eq.refl (w i))) (Eq.refl (w i))) (Eq.symm h) (Eq.refl (v i))) (Eq.refl (v i)))
Complexity: 11857 (size of the value term)
Dependencies: Logic.PropositionalLogic.Formula.literal, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation
Proof dependencies: Logic.PropositionalLogic.Formula
Lean core dependencies: Bool, Bool.false_eq_true, Bool.not, Bool.not_false, Bool.not_true, Bool.true_eq_false, Eq, Eq.symm, Eq.trans, False, Fin, Iff, Nat, True, congr, congrArg, congrFun', eq_self, id, iff_self, ite, ite_cond_eq_false, ite_cond_eq_true, of_eq_true
Logic.PropositionalLogic.Formula.minterm
The minterm for \(v\): the conjunction of every atom’s literal under \(v\), true exactly at \(v\) itself.
def Logic.PropositionalLogic.Formula.minterm {n : ℕ} (v : Logic.PropositionalLogic.Valuation (Fin (n + 1))) : Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details
| Logic.PropositionalLogic.Formula.minterm v = Logic.PropositionalLogic.Formula.bigAnd (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1)))
Complexity: 129 (size of the value term)
Outer dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Valuation
Inner dependencies: Logic.PropositionalLogic.Formula.bigAnd, Logic.PropositionalLogic.Formula.literal
Lean core dependencies: Fin, List.finRange, List.map, Nat
Logic.PropositionalLogic.Formula.minterm_val
theorem Logic.PropositionalLogic.Formula.minterm_val {n : ℕ} (v w : Logic.PropositionalLogic.Valuation (Fin (n + 1))) : Logic.PropositionalLogic.Formula.val w (Logic.PropositionalLogic.Formula.minterm v) = true ↔ w = v
Show details
fun {n} v w => Eq.mpr (id (congrFun' (congrArg Iff (Eq.trans (Logic.PropositionalLogic.Formula.minterm_val._simp_1_2 (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))) w) Logic.PropositionalLogic.Formula.minterm_val._simp_1_3)) (w = v))) { mp := fun h => funext fun i => (Logic.PropositionalLogic.Formula.literal_val v w i).mp (h i (List.mem_finRange i)), mpr := fun heq i x => Eq.mpr (id (congrArg (fun _a => Logic.PropositionalLogic.Formula.val _a (Logic.PropositionalLogic.Formula.literal v i) = true) heq)) ((Logic.PropositionalLogic.Formula.literal_val v v i).mpr rfl) }
Complexity: 3281 (size of the value term)
Dependencies: Logic.PropositionalLogic.Formula.minterm, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation
Proof dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.bigAnd, Logic.PropositionalLogic.Formula.bigAnd_val, Logic.PropositionalLogic.Formula.literal, Logic.PropositionalLogic.Formula.literal_val
Logic.PropositionalLogic.Formula.dnf
Completeness of \(\{\lnot, \land, \lor\}\). The canonical disjunctive normal form for a Boolean function: the disjunction, over every row where the function is true, of that row’s minterm.
def Logic.PropositionalLogic.Formula.dnf {n : ℕ} (f : Logic.PropositionalLogic.BoolFun (n + 1)) : Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details
| Logic.PropositionalLogic.Formula.dnf f = Logic.PropositionalLogic.Formula.bigOr (List.map Logic.PropositionalLogic.Formula.minterm (List.filter f Finset.univ.toList))
Complexity: 343 (size of the value term)
Outer dependencies: Logic.PropositionalLogic.BoolFun, Logic.PropositionalLogic.Formula
Inner dependencies: Logic.PropositionalLogic.Formula.bigOr, Logic.PropositionalLogic.Formula.minterm, Logic.PropositionalLogic.Valuation
Mathlib dependencies: Finset.toList, Finset.univ
Lean core dependencies: Bool, Fin, List.filter, List.map, Nat
Logic.PropositionalLogic.Formula.dnf_val
theorem Logic.PropositionalLogic.Formula.dnf_val {n : ℕ} (f : Logic.PropositionalLogic.BoolFun (n + 1)) (w : Logic.PropositionalLogic.Valuation (Fin (n + 1))) : Logic.PropositionalLogic.Formula.val w (Logic.PropositionalLogic.Formula.dnf f) = true ↔ f w = true
Show details
fun {n} f w => id (Eq.mpr (id (congrArg (fun _a => _a ↔ f w = true) (propext (Logic.PropositionalLogic.Formula.bigOr_val (List.map Logic.PropositionalLogic.Formula.minterm (List.filter f Finset.univ.toList)) w)))) { mp := fun a => Exists.casesOn a fun φ h => And.casesOn h fun hφmem hφval => Exists.casesOn (List.mem_map.mp hφmem) fun v h => And.casesOn h fun hvmem right => Eq.ndrec (motive := fun φ => φ ∈ List.map Logic.PropositionalLogic.Formula.minterm (List.filter f Finset.univ.toList) → Logic.PropositionalLogic.Formula.val w φ = true → f w = true) (fun hφmem hφval => And.casesOn (List.mem_filter.mp hvmem) fun left hv2 => Eq.mpr (id (congrArg (fun _a => f _a = true) ((Logic.PropositionalLogic.Formula.minterm_val v w).mp hφval))) hv2) right hφmem hφval, mpr := fun hf => Exists.intro (Logic.PropositionalLogic.Formula.minterm w) ⟨List.mem_map.mpr (Exists.intro w ⟨List.mem_filter.mpr ⟨Finset.mem_toList.mpr (Finset.mem_univ w), hf⟩, rfl⟩), (Logic.PropositionalLogic.Formula.minterm_val w w).mpr rfl⟩ })
Complexity: 20061 (size of the value term)
Dependencies: Logic.PropositionalLogic.BoolFun, Logic.PropositionalLogic.Formula.dnf, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation
Proof dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.bigOr, Logic.PropositionalLogic.Formula.bigOr_val, Logic.PropositionalLogic.Formula.minterm, Logic.PropositionalLogic.Formula.minterm_val
Mathlib dependencies: Finset, Finset.mem_toList, Finset.mem_univ, Finset.toList, Finset.univ
Logic.PropositionalLogic.Formula.exists_andOrNot_of_boolFun
Every Boolean function of \(n + 1\) arguments is the truth table of some formula using only negation, conjunction, and disjunction.
theorem Logic.PropositionalLogic.Formula.exists_andOrNot_of_boolFun {n : ℕ} (f : Logic.PropositionalLogic.BoolFun (n + 1)) : ∃ φ, ∀ (w : Logic.PropositionalLogic.Valuation (Fin (n + 1))), Logic.PropositionalLogic.Formula.val w φ = f w
Show details
fun {n} f => Exists.intro (Logic.PropositionalLogic.Formula.dnf f) fun w => Bool.eq_iff_iff.mpr (Logic.PropositionalLogic.Formula.dnf_val f w)
Complexity: 355 (size of the value term)
Dependencies: Logic.PropositionalLogic.BoolFun, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation
Proof dependencies: Logic.PropositionalLogic.Formula.dnf, Logic.PropositionalLogic.Formula.dnf_val
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.