LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm

theorem carry_comm {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : Carry i X Y ↔ Carry i Y X

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

theorem str_add_comm {num str : Type} [M : V0ExtModel num str] {X Y : str} : X + Y = Y + X

theorem str_add_comm_strengthened_v0 {num str : Type} [M : V0ExtModel num str] {X Y : str} : X + Y = Y + X

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