LeanPool.FormalizationOfBoundedArithmetic.V0StrAddAssoc

theorem add_assoc_bit_bool {A B C D X Y Z : Prop} : (Xor A B ↔ Xor C D) → (Xor (Xor (Xor (Xor X Y) C) Z) D ↔ Xor (Xor X (Xor (Xor Y Z) A)) B)

theorem carry_pair_step_bool {A B C D X Y Z : Prop} : (A ∧ B ↔ C ∧ D) → (Xor A B ↔ Xor C D) → (Maj A Y Z ∧ Maj B X (Xor (Xor Y Z) A) ↔ Maj C X Y ∧ Maj D (Xor (Xor X Y) C) Z) ∧ (Xor (Maj A Y Z) (Maj B X (Xor (Xor Y Z) A)) ↔ Xor (Maj C X Y) (Maj D (Xor (Xor X Y) C) Z))

def CarryAssocPred {num str : Type} [M : V0ExtModel num str] (X Y Z : str) (i : num) : Prop

Strong carry invariant used to prove associativity of string addition.

Equations

• CarryAssocPred X Y Z i = ((Carry i Y Z ∧ Carry i X (Y + Z) ↔ Carry i X Y ∧ Carry i (X + Y) Z) ∧ (Xor (Carry i Y Z) (Carry i X (Y + Z)) ↔ Xor (Carry i X Y) (Carry i (X + Y) Z)))

theorem carry_assoc_induction {num str : Type} [M : V0ExtModel num str] {X Y Z : str} : CarryAssocPred X Y Z 0 → (∀ (i : num), CarryAssocPred X Y Z i → CarryAssocPred X Y Z (i + 1)) → ∀ (i : num), CarryAssocPred X Y Z i

Induction step supplied by the strengthened V0Model interface.

This calls the bundled field V0Model.prop_induction_ax. The displayed predicate is the stronger Cook–Nguyen carry invariant built from bounded formulas, but this file does not derive the induction principle from a separate raw V0 axiom class.

theorem carry_pair_assoc {num str : Type} [M : V0ExtModel num str] {X Y Z : str} {i : num} : (Carry i Y Z ∧ Carry i X (Y + Z) ↔ Carry i X Y ∧ Carry i (X + Y) Z) ∧ (Xor (Carry i Y Z) (Carry i X (Y + Z)) ↔ Xor (Carry i X Y) (Carry i (X + Y) Z))

theorem str_add_assoc {num str : Type} [M : V0ExtModel num str] {X Y Z : str} : X + Y + Z = X + (Y + Z)

Associativity of string addition for V0ExtModel.

The theorem is stated for the enriched extension model whose parent V0Model already bundles the propositional induction/order/algebra fields used above. It is not advertised here as a derivation from only the raw finite V0 comprehension axioms.

theorem str_add_assoc_strengthened_v0 {num str : Type} [M : V0ExtModel num str] {X Y Z : str} : X + Y + Z = X + (Y + Z)

Named alias emphasizing that this theorem is conditional on the strengthened V0 extension.