LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc

theorem Xor.true1 {P Q R : Prop} : P → (Xor (Xor P Q) R ↔ ¬Xor Q R)

theorem Xor.true2 {P Q R : Prop} : Q → (Xor (Xor P Q) R ↔ ¬Xor P R)

theorem len_le_len_succ {num str : Type} [M : V0ExtModel num str] {X : str} : FirstOrder.Language.HasLen.len X ≤ FirstOrder.Language.HasLen.len (HasSucc.succ X)

theorem len_succ_le_succ {num str : Type} [M : V0ExtModel num str] {X : str} : FirstOrder.Language.HasLen.len (HasSucc.succ X) ≤ FirstOrder.Language.HasLen.len X + 1

theorem in_iff_not_notin {num str : Type} [M : V0ExtModel num str] {X : str} {j : num} : j ∈ X ↔ ¬j ∉ X

def LowestOrderZero {num str : Type} [M : V0ExtModel num str] (X : str) (m : num) : Prop

m is the least position below the string length where X has no bit.

Equations

• LowestOrderZero X m = (m ≤ FirstOrder.Language.HasLen.len X ∧ m ∉ X ∧ ∀ j < m, j ∈ X)

theorem exists_lowest_order_zero {num str : Type} [M : V0ExtModel num str] (X : str) : ∃ (m : num), LowestOrderZero X m

def LowestOrderOne {num str : Type} [M : V0ExtModel num str] (X : str) (m : num) : Prop

m is the least position below the string length where X has a bit.

Equations

• LowestOrderOne X m = (m ≤ FirstOrder.Language.HasLen.len X ∧ m ∈ X ∧ ∀ j < m, j ∉ X)

theorem exists_lowest_order_one {num str : Type} [M : V0ExtModel num str] {X : str} : 0 < FirstOrder.Language.HasLen.len X → ∃ (m : num), LowestOrderOne X m

theorem succ_le_of_lt {num str : Type} [M : V0ExtModel num str] {a b : num} (h : a < b) : a + 1 ≤ b

The discrete-successor step: a < b upgrades to a + 1 ≤ b.

theorem succ_bit_eq {num str : Type} [M : V0ExtModel num str] {X : str} {m : num} : LowestOrderZero X m → m ∈ HasSucc.succ X

theorem succ_bit_lt {num str : Type} [M : V0ExtModel num str] {X : str} {m : num} : LowestOrderZero X m → ∀ i < m, i ∉ HasSucc.succ X

theorem succ_bit_gt {num str : Type} [M : V0ExtModel num str] {X : str} {m : num} : LowestOrderZero X m → ∀ i > m, i ∈ HasSucc.succ X ↔ i ∈ X

theorem aux1 {num str : Type} [M : V0ExtModel num str] {X : str} {y min : num} : LowestOrderZero X min → y < min → y ∈ X

theorem len_succ_pos {num str : Type} [M : V0ExtModel num str] {X : str} : FirstOrder.Language.HasLen.len (HasSucc.succ X) > 0

theorem lsb_not_succ {num str : Type} [M : V0ExtModel num str] {X : str} : 0 ∈ X ↔ 0 ∉ HasSucc.succ X

theorem all_lt_mem_of_not_mem_of_mem_succ {num str : Type} [M : V0ExtModel num str] {X : str} {i : num} : i ∉ X → i ∈ HasSucc.succ X → ∀ j < i, j ∈ X

theorem all_lt_not_mem_of_not_carry_of_all_lt_mem {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : ¬Carry i X Y → (∀ j < i, j ∈ Y) → ∀ j < i, j ∉ X

theorem all_lt_not_carry_of_not_carry_of_all_lt_mem {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : ¬Carry i X Y → (∀ j < i, j ∈ Y) → ∀ j < i, ¬Carry j X Y

theorem all_lt_not_mem_of_all_lt_mem_add_of_all_lt_mem {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : (∀ j < i, j ∈ Y) → (∀ j < i, j ∈ X + Y) → ∀ j < i, j ∉ X

theorem not_carry_of_all_lt_mem_add_of_all_lt_mem {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : (∀ j < i, j ∈ Y) → (∀ j < i, j ∈ X + Y) → ¬Carry i X Y

theorem not_carry_of_all_lt_mem_add {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : (∀ j < i, j ∈ X + Y) → ¬Carry i X Y

theorem all_lt_not_carry_of_all_lt_mem_add {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : (∀ j < i, j ∈ X + Y) → ∀ j < i, ¬Carry j X Y

theorem carry_succ_of_all_lt_mem_add_of_lowest_zero_lt {num str : Type} [M : V0ExtModel num str] {X Y : str} {m i : num} : LowestOrderZero Y m → m < i → (∀ j < i, j ∈ X + Y) → Carry i X (HasSucc.succ Y)

theorem prefix_zero_contradiction_of_not_carry_of_all_lt_mem {num str : Type} [M : V0ExtModel num str] {X Y : str} {i : num} : i < FirstOrder.Language.HasLen.len X + FirstOrder.Language.HasLen.len Y → (∃ j < i, j ∉ X + Y) → ¬Carry i X Y → (∀ j < i, j ∈ Y) → False

theorem not_lt_lowest_zero_of_prefix_zero_of_not_carry {num str : Type} [M : V0ExtModel num str] {X Y : str} {m i : num} : LowestOrderZero Y m → i < FirstOrder.Language.HasLen.len X + FirstOrder.Language.HasLen.len Y → (∃ j < i, j ∉ X + Y) → ¬Carry i X Y → ¬i < m

theorem not_carry_succ_of_lowest_zero_ge {num str : Type} [M : V0ExtModel num str] {X Y : str} {m i : num} : LowestOrderZero Y m → i ≤ m → ¬Carry i X (HasSucc.succ Y)

theorem carry_succ_of_carry_of_lowest_zero_lt {num str : Type} [M : V0ExtModel num str] {X Y : str} {m i : num} : LowestOrderZero Y m → m < i → Carry i X Y → Carry i X (HasSucc.succ Y)

theorem not_carry_succ_of_prefix_zero_of_not_carry_of_lowest_zero_lt {num str : Type} [M : V0ExtModel num str] {X Y : str} {m i : num} : LowestOrderZero Y m → m < i → (∃ j < i, j ∉ X + Y) → ¬Carry i X Y → ¬Carry i X (HasSucc.succ Y)

theorem not_mem_add_succ_of_not_mem_add_of_prefix_zero {num str : Type} [M : V0ExtModel num str] {X Y : str} {y : num} : y ∉ X + Y → (∃ j < y, j ∉ X + Y) → y ∉ X + HasSucc.succ Y

theorem not_mem_add_succ_of_mem_add_of_prefix_one {num str : Type} [M : V0ExtModel num str] {X Y : str} {y : num} : y ∈ X + Y → (∀ j < y, j ∈ X + Y) → y ∉ X + HasSucc.succ Y

theorem add_succ_of_succ_add_zero {num str : Type} [M : V0ExtModel num str] {X Y : str} {y : num} : y = 0 → y ∈ HasSucc.succ (X + Y) → y ∈ X + HasSucc.succ Y

theorem add_succ_of_succ_add_of_mem_add {num str : Type} [M : V0ExtModel num str] {X Y : str} {y pred_y : num} : pred_y + 1 = y → y ∈ X + Y → (∃ j < y, j ∉ X + Y) → y ∈ X + HasSucc.succ Y

theorem add_succ_of_succ_add {num str : Type} [M : V0ExtModel num str] {X Y : str} {y : num} : y ∈ HasSucc.succ (X + Y) → y ∈ X + HasSucc.succ Y

theorem succ_len_eq {num str : Type} [M : V0ExtModel num str] {X Y : str} : FirstOrder.Language.HasLen.len (X + HasSucc.succ Y) = FirstOrder.Language.HasLen.len (HasSucc.succ (X + Y))

theorem succ_add_of_add_succ {num str : Type} [M : V0ExtModel num str] {X Y : str} {y : num} : y ∈ X + HasSucc.succ Y → y ∈ HasSucc.succ (X + Y)

theorem str_succ_assoc {num str : Type} [M : V0ExtModel num str] {X Y : str} : X + HasSucc.succ Y = HasSucc.succ (X + Y)

theorem str_succ_assoc_strengthened_v0 {num str : Type} [M : V0ExtModel num str] {X Y : str} : X + HasSucc.succ Y = HasSucc.succ (X + Y)

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