Formulas on bit vectors

The vocabulary in which the describer of the succinct Cook–Levin theorem is written (planning/succinct-cook-levin.md, S3): a field is a list of formulas read as a binary number, least significant bit first (Fml.val); the fields of an index are slices of the input bits (Fml.field); and the tests on fields are conjunctions and disjunctions (andList, orList), equality with a constant or another field (eqConst, eqFields), comparison (ltConst, ltFields), addition of a constant with its carry (addBits, addConstRel), subtraction of a constant by the two's complement (subConstBits), padding (padTo) and a multiplexer (mux). Every test is defined by a fold or a structural recursion whose program is the same fold (FmlProg.lean), and every semantics lemma is an equation on val.

Values of bit strings

theorem MIPRE.SAT.bitsVal_cons' (b : Bool) (l : Cost.BitStr) : Cost.bitsVal (b :: l) = 2 * Cost.bitsVal l + b.toNat

theorem MIPRE.SAT.bitsVal_lt (l : Cost.BitStr) : Cost.bitsVal l < 2 ^ List.length l

theorem MIPRE.SAT.bitsVal_append (l₁ l₂ : Cost.BitStr) : Cost.bitsVal (l₁ ++ l₂) = Cost.bitsVal l₁ + 2 ^ List.length l₁ * Cost.bitsVal l₂

theorem MIPRE.SAT.bitsVal_replicate_false (n : ℕ) : Cost.bitsVal (List.replicate n false) = 0

theorem MIPRE.SAT.bitsVal_injective {l₁ l₂ : Cost.BitStr} : List.length l₁ = List.length l₂ → Cost.bitsVal l₁ = Cost.bitsVal l₂ → l₁ = l₂

Equal-length bit strings with equal values are equal.

theorem MIPRE.SAT.bitsVal_take (l : Cost.BitStr) (n : ℕ) : Cost.bitsVal (List.take n l) = Cost.bitsVal l % 2 ^ n

theorem MIPRE.SAT.bitsVal_map_not (l : Cost.BitStr) : Cost.bitsVal (List.map not l) + Cost.bitsVal l + 1 = 2 ^ List.length l

theorem MIPRE.SAT.length_incBits_ge (l : Cost.BitStr) : List.length l ≤ List.length (Cost.incBits l)

theorem MIPRE.SAT.bitsVal_incBits (l : Cost.BitStr) : Cost.bitsVal (Cost.incBits l) = Cost.bitsVal l + 1

def MIPRE.SAT.padBits (W : ℕ) (l : Cost.BitStr) : Cost.BitStr

The bits of a number, padded to W bits with zeros (least significant bit first).

Equations

• MIPRE.SAT.padBits W l = l ++ List.replicate (W - List.length l) false

theorem MIPRE.SAT.length_padBits (W : ℕ) (l : Cost.BitStr) (h : List.length l ≤ W) : List.length (padBits W l) = W

theorem MIPRE.SAT.bitsVal_padBits (W : ℕ) (l : Cost.BitStr) : Cost.bitsVal (padBits W l) = Cost.bitsVal l

def MIPRE.SAT.twosComp (c : Cost.BitStr) : Cost.BitStr

The two's complement of a W-bit string: 2^W - v modulo 2^W.

Equations

• MIPRE.SAT.twosComp c = List.take (List.length c) (MIPRE.Cost.incBits (List.map not c))

theorem MIPRE.SAT.length_twosComp (c : Cost.BitStr) : List.length (twosComp c) = List.length c

theorem MIPRE.SAT.bitsVal_twosComp (c : Cost.BitStr) : Cost.bitsVal (twosComp c) = (2 ^ List.length c - Cost.bitsVal c) % 2 ^ List.length c

Basic connectives

def MIPRE.SAT.Fml.xnor (f g : Fml) : Fml

Equivalence.

Equations

• f.xnor g = (f.and g).or (f.not.and g.not)

theorem MIPRE.SAT.Fml.eval_xnor (f g : Fml) (x : ℕ → Bool) : eval x (f.xnor g) = (eval x f == eval x g)

def MIPRE.SAT.Fml.xor (f g : Fml) : Fml

Exclusive or.

Equations

• f.xor g = (f.and g.not).or (f.not.and g)

theorem MIPRE.SAT.Fml.eval_xor (f g : Fml) (x : ℕ → Bool) : eval x (f.xor g) = (eval x f != eval x g)

def MIPRE.SAT.Fml.mux (s a b : Fml) : Fml

The multiplexer if s then a else b.

Equations

• s.mux a b = (s.and a).or (s.not.and b)

theorem MIPRE.SAT.Fml.eval_mux (s a b : Fml) (x : ℕ → Bool) : eval x (s.mux a b) = if eval x s = true then eval x a else eval x b

def MIPRE.SAT.Fml.andList (l : List Fml) : Fml

Conjunction of a list, as a fold.

Equations

• MIPRE.SAT.Fml.andList l = List.foldl MIPRE.SAT.Fml.and (MIPRE.SAT.Fml.const true) l

theorem MIPRE.SAT.Fml.eval_foldl_and (l : List Fml) (init : Fml) (x : ℕ → Bool) : eval x (List.foldl and init l) = (eval x init && l.all fun (x_1 : Fml) => eval x x_1)

theorem MIPRE.SAT.Fml.eval_andList (l : List Fml) (x : ℕ → Bool) : eval x (andList l) = l.all fun (x_1 : Fml) => eval x x_1

theorem MIPRE.SAT.Fml.eval_andList_eq_true (l : List Fml) (x : ℕ → Bool) : eval x (andList l) = true ↔ ∀ f ∈ l, eval x f = true

def MIPRE.SAT.Fml.orList (l : List Fml) : Fml

Disjunction of a list, as a fold.

Equations

• MIPRE.SAT.Fml.orList l = List.foldl MIPRE.SAT.Fml.or (MIPRE.SAT.Fml.const false) l

theorem MIPRE.SAT.Fml.eval_foldl_or (l : List Fml) (init : Fml) (x : ℕ → Bool) : eval x (List.foldl or init l) = (eval x init || l.any fun (x_1 : Fml) => eval x x_1)

theorem MIPRE.SAT.Fml.eval_orList (l : List Fml) (x : ℕ → Bool) : eval x (orList l) = l.any fun (x_1 : Fml) => eval x x_1

theorem MIPRE.SAT.Fml.eval_orList_eq_true (l : List Fml) (x : ℕ → Bool) : eval x (orList l) = true ↔ ∃ f ∈ l, eval x f = true

Fields

def MIPRE.SAT.Fml.bitsOf (fs : List Fml) (x : ℕ → Bool) : Cost.BitStr

The bits of a field: the values of its formulas, least significant first.

Equations

• MIPRE.SAT.Fml.bitsOf fs x = List.map (fun (x_1 : MIPRE.SAT.Fml) => MIPRE.SAT.Fml.eval x x_1) fs

def MIPRE.SAT.Fml.val (fs : List Fml) (x : ℕ → Bool) : ℕ

The value of a field.

Equations

• MIPRE.SAT.Fml.val fs x = MIPRE.Cost.bitsVal (MIPRE.SAT.Fml.bitsOf fs x)

@[simp]

theorem MIPRE.SAT.Fml.bitsOf_nil (x : ℕ → Bool) : bitsOf [] x = []

@[simp]

theorem MIPRE.SAT.Fml.bitsOf_cons (f : Fml) (fs : List Fml) (x : ℕ → Bool) : bitsOf (f :: fs) x = eval x f :: bitsOf fs x

@[simp]

theorem MIPRE.SAT.Fml.length_bitsOf (fs : List Fml) (x : ℕ → Bool) : List.length (bitsOf fs x) = fs.length

theorem MIPRE.SAT.Fml.val_cons (f : Fml) (fs : List Fml) (x : ℕ → Bool) : val (f :: fs) x = 2 * val fs x + (eval x f).toNat

theorem MIPRE.SAT.Fml.val_lt (fs : List Fml) (x : ℕ → Bool) : val fs x < 2 ^ fs.length

def MIPRE.SAT.Fml.field (a W : ℕ) : List Fml

The field of W input bits starting at bit a.

Equations

• MIPRE.SAT.Fml.field a W = List.map MIPRE.SAT.Fml.inp (List.range' a W)

@[simp]

theorem MIPRE.SAT.Fml.length_field (a W : ℕ) : (field a W).length = W

theorem MIPRE.SAT.Fml.bitsOf_field (a W : ℕ) (x : ℕ → Bool) : bitsOf (field a W) x = List.map x (List.range' a W)

def MIPRE.SAT.Fml.constBits (c : Cost.BitStr) : List Fml

Constant bits as formulas.

Equations

• MIPRE.SAT.Fml.constBits c = List.map MIPRE.SAT.Fml.const c

@[simp]

theorem MIPRE.SAT.Fml.length_constBits (c : Cost.BitStr) : (constBits c).length = List.length c

theorem MIPRE.SAT.Fml.bitsOf_constBits (c : Cost.BitStr) (x : ℕ → Bool) : bitsOf (constBits c) x = c

def MIPRE.SAT.Fml.padTo (W : ℕ) (fs : List Fml) : List Fml

Padding a field to W bits with zeros.

Equations

• MIPRE.SAT.Fml.padTo W fs = fs ++ List.replicate (W - fs.length) (MIPRE.SAT.Fml.const false)

theorem MIPRE.SAT.Fml.length_padTo (W : ℕ) (fs : List Fml) (h : fs.length ≤ W) : (padTo W fs).length = W

theorem MIPRE.SAT.Fml.bitsOf_padTo (W : ℕ) (fs : List Fml) (x : ℕ → Bool) : bitsOf (padTo W fs) x = padBits W (bitsOf fs x)

theorem MIPRE.SAT.Fml.val_padTo (W : ℕ) (fs : List Fml) (x : ℕ → Bool) : val (padTo W fs) x = val fs x

Equality

def MIPRE.SAT.Fml.eqStep (acc : Fml) (p : Fml × Bool) : Fml

The step of the equality test with a constant.

Equations

• acc.eqStep p = acc.and (if p.2 = true then p.1 else p.1.not)

def MIPRE.SAT.Fml.eqConst (fs : List Fml) (c : Cost.BitStr) : Fml

The field fs equals the constant c (of the same length).

Equations

• MIPRE.SAT.Fml.eqConst fs c = List.foldl MIPRE.SAT.Fml.eqStep (MIPRE.SAT.Fml.const true) (fs.zip c)

theorem MIPRE.SAT.Fml.eval_foldl_eqStep (fs : List Fml) (c : Cost.BitStr) : fs.length = List.length c → ∀ (init : Fml) (x : ℕ → Bool), eval x (List.foldl eqStep init (fs.zip c)) = (eval x init && decide (bitsOf fs x = c))

theorem MIPRE.SAT.Fml.eval_eqConst (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) (x : ℕ → Bool) : eval x (eqConst fs c) = decide (bitsOf fs x = c)

theorem MIPRE.SAT.Fml.eval_eqConst_iff (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) (x : ℕ → Bool) : eval x (eqConst fs c) = true ↔ val fs x = Cost.bitsVal c

def MIPRE.SAT.Fml.eqFStep (acc : Fml) (p : Fml × Fml) : Fml

The step of the equality test of two fields.

Equations

• acc.eqFStep p = acc.and (p.1.xnor p.2)

def MIPRE.SAT.Fml.eqFields (fs gs : List Fml) : Fml

The fields fs and gs (of the same length) are equal.

Equations

• MIPRE.SAT.Fml.eqFields fs gs = List.foldl MIPRE.SAT.Fml.eqFStep (MIPRE.SAT.Fml.const true) (fs.zip gs)

theorem MIPRE.SAT.Fml.eval_foldl_eqFStep (fs gs : List Fml) : fs.length = gs.length → ∀ (init : Fml) (x : ℕ → Bool), eval x (List.foldl eqFStep init (fs.zip gs)) = (eval x init && decide (bitsOf fs x = bitsOf gs x))

theorem MIPRE.SAT.Fml.eval_eqFields (fs gs : List Fml) (h : fs.length = gs.length) (x : ℕ → Bool) : eval x (eqFields fs gs) = decide (bitsOf fs x = bitsOf gs x)

theorem MIPRE.SAT.Fml.eval_eqFields_iff (fs gs : List Fml) (h : fs.length = gs.length) (x : ℕ → Bool) : eval x (eqFields fs gs) = true ↔ val fs x = val gs x

Comparison

def MIPRE.SAT.Fml.ltStep (lt : Fml) (p : Fml × Bool) : Fml

The step of the comparison with a constant, least significant bit first: the prefix is below the constant's prefix iff this bit is below, or equal with the lower bits below.

Equations

• lt.ltStep p = (p.1.not.and (MIPRE.SAT.Fml.const p.2)).or ((p.1.xnor (MIPRE.SAT.Fml.const p.2)).and lt)

def MIPRE.SAT.Fml.ltConst (fs : List Fml) (c : Cost.BitStr) : Fml

The field fs is below the constant c (of the same length).

Equations

• MIPRE.SAT.Fml.ltConst fs c = List.foldl MIPRE.SAT.Fml.ltStep (MIPRE.SAT.Fml.const false) (fs.zip c)

theorem MIPRE.SAT.Fml.eval_foldl_ltStep (fs : List Fml) (c : Cost.BitStr) : fs.length = List.length c → ∀ (init : Fml) (x : ℕ → Bool), eval x (List.foldl ltStep init (fs.zip c)) = true ↔ val fs x < Cost.bitsVal c ∨ val fs x = Cost.bitsVal c ∧ eval x init = true

theorem MIPRE.SAT.Fml.eval_ltConst_iff (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) (x : ℕ → Bool) : eval x (ltConst fs c) = true ↔ val fs x < Cost.bitsVal c

def MIPRE.SAT.Fml.ltFStep (lt : Fml) (p : Fml × Fml) : Fml

The step of the comparison of two fields.

Equations

• lt.ltFStep p = (p.1.not.and p.2).or ((p.1.xnor p.2).and lt)

def MIPRE.SAT.Fml.ltFields (fs gs : List Fml) : Fml

The field fs is below the field gs (of the same length).

Equations

• MIPRE.SAT.Fml.ltFields fs gs = List.foldl MIPRE.SAT.Fml.ltFStep (MIPRE.SAT.Fml.const false) (fs.zip gs)

theorem MIPRE.SAT.Fml.eval_foldl_ltFStep (fs gs : List Fml) : fs.length = gs.length → ∀ (init : Fml) (x : ℕ → Bool), eval x (List.foldl ltFStep init (fs.zip gs)) = true ↔ val fs x < val gs x ∨ val fs x = val gs x ∧ eval x init = true

theorem MIPRE.SAT.Fml.eval_ltFields_iff (fs gs : List Fml) (h : fs.length = gs.length) (x : ℕ → Bool) : eval x (ltFields fs gs) = true ↔ val fs x < val gs x

Addition of a constant

def MIPRE.SAT.Fml.sum3 (f b c : Fml) : Fml

The sum bit of a full adder.

Equations

• f.sum3 b c = (f.xor b).xor c

def MIPRE.SAT.Fml.maj3 (f b c : Fml) : Fml

The carry bit of a full adder.

Equations

• f.maj3 b c = (f.and b).or ((f.or b).and c)

theorem MIPRE.SAT.Fml.eval_sum3_maj3 (f b c : Fml) (x : ℕ → Bool) : (eval x (f.sum3 b c)).toNat + 2 * (eval x (f.maj3 b c)).toNat = (eval x f).toNat + (eval x b).toNat + (eval x c).toNat

def MIPRE.SAT.Fml.addBits : List Fml → Cost.BitStr → Fml → List Fml × Fml

The sum of a field and a constant (of the same length) with a carry in: the sum bits and the carry out.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.SAT.Fml.addBits x✝² x✝¹ x✝ = ([], x✝)

theorem MIPRE.SAT.Fml.length_addBits (fs : List Fml) (c : Cost.BitStr) : fs.length = List.length c → ∀ (cin : Fml), (addBits fs c cin).1.length = fs.length

theorem MIPRE.SAT.Fml.val_addBits (fs : List Fml) (c : Cost.BitStr) : fs.length = List.length c → ∀ (cin : Fml) (x : ℕ → Bool), val (addBits fs c cin).1 x + 2 ^ fs.length * (eval x (addBits fs c cin).2).toNat = val fs x + Cost.bitsVal c + (eval x cin).toNat

The adder identity: sum + 2^W · carry = fs + c + cin.

def MIPRE.SAT.Fml.addConstBits (fs : List Fml) (c : Cost.BitStr) : List Fml

The sum bits of a field and a constant.

Equations

• MIPRE.SAT.Fml.addConstBits fs c = (MIPRE.SAT.Fml.addBits fs c (MIPRE.SAT.Fml.const false)).1

def MIPRE.SAT.Fml.addConstCarry (fs : List Fml) (c : Cost.BitStr) : Fml

The carry out of the sum of a field and a constant.

Equations

• MIPRE.SAT.Fml.addConstCarry fs c = (MIPRE.SAT.Fml.addBits fs c (MIPRE.SAT.Fml.const false)).2

theorem MIPRE.SAT.Fml.length_addConstBits (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) : (addConstBits fs c).length = fs.length

theorem MIPRE.SAT.Fml.val_addConstBits (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) (x : ℕ → Bool) : val (addConstBits fs c) x + 2 ^ fs.length * (eval x (addConstCarry fs c)).toNat = val fs x + Cost.bitsVal c

theorem MIPRE.SAT.Fml.val_addConstBits_mod (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) (x : ℕ → Bool) : val (addConstBits fs c) x = (val fs x + Cost.bitsVal c) % 2 ^ fs.length

def MIPRE.SAT.Fml.addConstRel (fs gs : List Fml) (c : Cost.BitStr) : Fml

gs = fs + c, exactly: the sum bits agree and there is no carry out.

Equations

• MIPRE.SAT.Fml.addConstRel fs gs c = (MIPRE.SAT.Fml.eqFields gs (MIPRE.SAT.Fml.addConstBits fs c)).and (MIPRE.SAT.Fml.addConstCarry fs c).not

theorem MIPRE.SAT.Fml.eval_addConstRel_iff (fs gs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) (hg : gs.length = fs.length) (x : ℕ → Bool) : eval x (addConstRel fs gs c) = true ↔ val gs x = val fs x + Cost.bitsVal c

Subtraction of a constant

def MIPRE.SAT.Fml.subConstBits (fs : List Fml) (c : Cost.BitStr) : List Fml

The difference fs - c by the two's complement, correct when c ≤ fs.

Equations

• MIPRE.SAT.Fml.subConstBits fs c = MIPRE.SAT.Fml.addConstBits fs (MIPRE.SAT.twosComp c)

theorem MIPRE.SAT.Fml.length_subConstBits (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) : (subConstBits fs c).length = fs.length

theorem MIPRE.SAT.Fml.val_subConstBits (fs : List Fml) (c : Cost.BitStr) (h : fs.length = List.length c) (x : ℕ → Bool) (hc : Cost.bitsVal c ≤ val fs x) : val (subConstBits fs c) x = val fs x - Cost.bitsVal c

Input bounds

theorem MIPRE.SAT.Fml.InputsLt.xnor {n : ℕ} {f g : Fml} (hf : InputsLt n f) (hg : InputsLt n g) : InputsLt n (f.xnor g)

theorem MIPRE.SAT.Fml.InputsLt.xor {n : ℕ} {f g : Fml} (hf : InputsLt n f) (hg : InputsLt n g) : InputsLt n (f.xor g)

theorem MIPRE.SAT.Fml.InputsLt.mux {n : ℕ} {s a b : Fml} (hs : InputsLt n s) (ha : InputsLt n a) (hb : InputsLt n b) : InputsLt n (s.mux a b)

theorem MIPRE.SAT.Fml.InputsLt.foldl_and {n : ℕ} (l : List Fml) (init : Fml) (hi : InputsLt n init) (hl : ∀ f ∈ l, InputsLt n f) : InputsLt n (List.foldl and init l)

theorem MIPRE.SAT.Fml.InputsLt.andList {n : ℕ} (l : List Fml) (hl : ∀ f ∈ l, InputsLt n f) : InputsLt n (Fml.andList l)

theorem MIPRE.SAT.Fml.InputsLt.foldl_or {n : ℕ} (l : List Fml) (init : Fml) (hi : InputsLt n init) (hl : ∀ f ∈ l, InputsLt n f) : InputsLt n (List.foldl or init l)

theorem MIPRE.SAT.Fml.InputsLt.orList {n : ℕ} (l : List Fml) (hl : ∀ f ∈ l, InputsLt n f) : InputsLt n (Fml.orList l)

theorem MIPRE.SAT.Fml.InputsLt.field {n a W : ℕ} (h : a + W ≤ n) (f : Fml) : f ∈ Fml.field a W → InputsLt n f

theorem MIPRE.SAT.Fml.InputsLt.constBits {n : ℕ} (c : Cost.BitStr) (f : Fml) : f ∈ Fml.constBits c → InputsLt n f

theorem MIPRE.SAT.Fml.InputsLt.padTo {n W : ℕ} {fs : List Fml} (h : ∀ f ∈ fs, InputsLt n f) (f : Fml) : f ∈ Fml.padTo W fs → InputsLt n f

theorem MIPRE.SAT.Fml.InputsLt.foldl_zip {n : ℕ} {γ : Type u_1} (step : Fml → Fml × γ → Fml) (hstep : ∀ (acc : Fml) (p : Fml × γ), InputsLt n acc → InputsLt n p.1 → InputsLt n (step acc p)) (fs : List Fml) (c : List γ) (init : Fml) (hi : InputsLt n init) (hl : ∀ f ∈ fs, InputsLt n f) : InputsLt n (List.foldl step init (fs.zip c))

theorem MIPRE.SAT.Fml.InputsLt.eqConst {n : ℕ} {fs : List Fml} (c : Cost.BitStr) (h : ∀ f ∈ fs, InputsLt n f) : InputsLt n (Fml.eqConst fs c)

theorem MIPRE.SAT.Fml.InputsLt.foldl_zip₂ {n : ℕ} (step : Fml → Fml × Fml → Fml) (hstep : ∀ (acc : Fml) (p : Fml × Fml), InputsLt n acc → InputsLt n p.1 → InputsLt n p.2 → InputsLt n (step acc p)) (fs gs : List Fml) (init : Fml) (hi : InputsLt n init) (hf : ∀ f ∈ fs, InputsLt n f) (hg : ∀ f ∈ gs, InputsLt n f) : InputsLt n (List.foldl step init (fs.zip gs))

theorem MIPRE.SAT.Fml.InputsLt.eqFields {n : ℕ} {fs gs : List Fml} (h : ∀ f ∈ fs, InputsLt n f) (hg : ∀ f ∈ gs, InputsLt n f) : InputsLt n (Fml.eqFields fs gs)

theorem MIPRE.SAT.Fml.InputsLt.ltConst {n : ℕ} {fs : List Fml} (c : Cost.BitStr) (h : ∀ f ∈ fs, InputsLt n f) : InputsLt n (Fml.ltConst fs c)

theorem MIPRE.SAT.Fml.InputsLt.ltFields {n : ℕ} {fs gs : List Fml} (h : ∀ f ∈ fs, InputsLt n f) (hg : ∀ f ∈ gs, InputsLt n f) : InputsLt n (Fml.ltFields fs gs)

theorem MIPRE.SAT.Fml.InputsLt.sum3 {n : ℕ} {f b c : Fml} (hf : InputsLt n f) (hb : InputsLt n b) (hc : InputsLt n c) : InputsLt n (f.sum3 b c)

theorem MIPRE.SAT.Fml.InputsLt.maj3 {n : ℕ} {f b c : Fml} (hf : InputsLt n f) (hb : InputsLt n b) (hc : InputsLt n c) : InputsLt n (f.maj3 b c)

theorem MIPRE.SAT.Fml.InputsLt.addBits {n : ℕ} (fs : List Fml) (c : Cost.BitStr) (cin : Fml) : (∀ f ∈ fs, InputsLt n f) → InputsLt n cin → (∀ f ∈ (Fml.addBits fs c cin).1, InputsLt n f) ∧ InputsLt n (Fml.addBits fs c cin).2

theorem MIPRE.SAT.Fml.InputsLt.addConstBits {n : ℕ} {fs : List Fml} (c : Cost.BitStr) (h : ∀ f ∈ fs, InputsLt n f) (f : Fml) : f ∈ Fml.addConstBits fs c → InputsLt n f

theorem MIPRE.SAT.Fml.InputsLt.addConstCarry {n : ℕ} {fs : List Fml} (c : Cost.BitStr) (h : ∀ f ∈ fs, InputsLt n f) : InputsLt n (Fml.addConstCarry fs c)

theorem MIPRE.SAT.Fml.InputsLt.addConstRel {n : ℕ} {fs gs : List Fml} (c : Cost.BitStr) (h : ∀ f ∈ fs, InputsLt n f) (hg : ∀ f ∈ gs, InputsLt n f) : InputsLt n (Fml.addConstRel fs gs c)

theorem MIPRE.SAT.Fml.InputsLt.subConstBits {n : ℕ} {fs : List Fml} (c : Cost.BitStr) (h : ∀ f ∈ fs, InputsLt n f) (f : Fml) : f ∈ Fml.subConstBits fs c → InputsLt n f