def Std.Sat.CNF.Clause.maxLiteral (c : Clause Nat) : Option Nat

Obtain the literal with the largest identifier in c.

theorem Std.Sat.CNF.Clause.of_maxLiteral_eq_some {maxLit : Nat} (c : Clause Nat) (h : c.maxLiteral = some maxLit) (lit : Nat) : Mem lit c → lit ≤ maxLit

theorem Std.Sat.CNF.Clause.maxLiteral_eq_some_of_mem {l : Nat} (c : Clause Nat) (h : Mem l c) : ∃ (maxLit : Nat), c.maxLiteral = some maxLit

theorem Std.Sat.CNF.Clause.of_maxLiteral_eq_none (c : Clause Nat) (h : c.maxLiteral = none) (lit : Nat) : ¬Mem lit c

def Std.Sat.CNF.maxLiteral (f : CNF Nat) : Option Nat

Obtain the literal with the largest identifier in f.

theorem Std.Sat.CNF.of_maxLiteral_eq_some' {maxLit localMax : Nat} (f : CNF Nat) (h : f.maxLiteral = some maxLit) (clause : Clause Nat) : clause ∈ f → clause.maxLiteral = some localMax → localMax ≤ maxLit

theorem Std.Sat.CNF.of_maxLiteral_eq_some {maxLit : Nat} (f : CNF Nat) (h : f.maxLiteral = some maxLit) (lit : Nat) : Mem lit f → lit ≤ maxLit

theorem Std.Sat.CNF.of_maxLiteral_eq_none (f : CNF Nat) (h : f.maxLiteral = none) (lit : Nat) : ¬Mem lit f

def Std.Sat.CNF.numLiterals (f : CNF Nat) : Nat

An upper bound for the amount of distinct literals in f.

theorem Std.Sat.CNF.lt_numLiterals {v : Nat} {f : CNF Nat} (h : Mem v f) : v < f.numLiterals

theorem Std.Sat.CNF.numLiterals_pos {v : Nat} {f : CNF Nat} (h : Mem v f) : 0 < f.numLiterals

def Std.Sat.CNF.relabelFin (f : CNF Nat) : CNF (Fin f.numLiterals)

Relabel f to a CNF formula with a known upper bound for its literals.

This operation might be useful when e.g. using the literals to index into an array of known size without conducting bounds checks.

@[simp]

theorem Std.Sat.CNF.unsat_relabelFin {f : CNF Nat} : f.relabelFin.Unsat ↔ f.Unsat