theorem Eq511.rule_0_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (old_0 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X0 X1 X3 ∨ X2 = X3) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_12 : ∀ (X0 X1 X2 X3 X4 X5 : G), ¬old X0 X1 X2 ∨ ¬old X0 X3 X2 ∨ ¬old X4 X0 X1 ∨ ¬old X5 X0 X3 ∨ X4 = X5) (old_15 : ∀ (X0 X1 X2 X3 X4 : G), ¬old X0 X1 X0 ∨ ¬old X0 X2 X3 ∨ ¬old X3 X0 X1 ∨ ¬old X4 X0 X2 ∨ X0 = X4) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (imp_new_2 : ∀ (X Y Z X2 : G), a ≠ X ∨ c ≠ Y ∨ ¬old Z a X2 ∨ ¬old a X2 b ∨ new X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_1_3 : ∀ (X Y Z : G), old a (sF0 X Y Z) b ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (imp_new_4 : ∀ (X Y Z X3 : G), b ≠ X ∨ c ≠ Y ∨ ¬old a X3 a ∨ ¬old b X3 a ∨ ¬old Z b X3 ∨ new X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_2 : ∀ (X Y Z : G), a = Z ∨ ¬sP4 X Y Z) (rule_def_4_3 : ∀ (X Y Z : G), old a (sF4 X Y Z) a ∨ ¬sP4 X Y Z) (rule_def_4_4 : ∀ (X Y Z : G), old b a (sF4 X Y Z) ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 X3 : G) : ¬new X0 X1 X2 ∨ ¬new X0 X1 X3 ∨ X2 = X3

theorem Eq511.rule_1_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (prev_0 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X1 X2 ∨ ¬new X0 X1 X3 ∨ X2 = X3) (old_1 : ∀ (X0 X1 X2 X3 X4 : G), ¬old X0 X1 X2 ∨ ¬old X1 X2 X3 ∨ ¬old X1 X3 X4 ∨ old X1 X4 X0) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_10 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X0 ∨ ¬old X2 X0 X3 ∨ ¬old X3 X0 X1 ∨ old X0 X0 X2) (old_11 : ∀ (X0 X1 X2 X3 X4 : G), ¬old X0 X1 X2 ∨ ¬old X3 X0 X1 ∨ ¬old X4 X0 X2 ∨ old X0 X3 X4) (old_14 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X0 X3 X0 ∨ ¬old X1 X0 X3 ∨ old X0 X2 X0) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (imp_new_2 : ∀ (X Y Z X2 : G), a ≠ X ∨ c ≠ Y ∨ ¬old Z a X2 ∨ ¬old a X2 b ∨ new X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_1_3 : ∀ (X Y Z : G), old a (sF0 X Y Z) b ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (imp_new_4 : ∀ (X Y Z X3 : G), b ≠ X ∨ c ≠ Y ∨ ¬old a X3 a ∨ ¬old b X3 a ∨ ¬old Z b X3 ∨ new X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_2 : ∀ (X Y Z : G), a = Z ∨ ¬sP4 X Y Z) (rule_def_4_3 : ∀ (X Y Z : G), old a (sF4 X Y Z) a ∨ ¬sP4 X Y Z) (rule_def_4_4 : ∀ (X Y Z : G), old b a (sF4 X Y Z) ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (imp_new_0 : ∀ (X Y Z : G), ¬old X Y Z ∨ new X Y Z) (X0 X1 X2 X3 X4 : G) : ¬new X0 X1 X2 ∨ ¬new X1 X2 X3 ∨ ¬new X1 X3 X4 ∨ new X1 X4 X0

theorem Eq511.rule_2_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (old_2 : ∀ (X0 X1 : G), ¬old X0 X1 X1 ∨ old X1 X0 X1) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_2 : ∀ (X Y Z : G), a = Z ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (imp_new_0 : ∀ (X Y Z : G), ¬old X Y Z ∨ new X Y Z) (X0 X1 : G) : ¬new X0 X1 X1 ∨ new X1 X0 X1

theorem Eq511.rule_3_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (old_3 : ∀ (X0 X1 : G), ¬old X0 X1 X0 ∨ ¬old X1 X0 X1 ∨ old X0 X0 X0) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (imp_new_0 : ∀ (X Y Z : G), ¬old X Y Z ∨ new X Y Z) (X0 X1 : G) : ¬new X0 X1 X0 ∨ ¬new X1 X0 X1 ∨ new X0 X0 X0

theorem Eq511.rule_4_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 X3 X4 : G) : ¬new X0 X1 X2 ∨ ¬new X3 X0 X4 ∨ ¬new X3 X1 X2 ∨ new X0 X3 X4

theorem Eq511.rule_5_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (old_5 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X0 X1 ∨ ¬old X0 X1 X2 ∨ ¬old X3 X0 X2 ∨ X1 = X3) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_10 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X0 ∨ ¬old X2 X0 X3 ∨ ¬old X3 X0 X1 ∨ old X0 X0 X2) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_1_3 : ∀ (X Y Z : G), old a (sF0 X Y Z) b ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_4 : ∀ (X Y Z : G), old b a (sF4 X Y Z) ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 X3 : G) : ¬new X0 X0 X1 ∨ ¬new X0 X1 X2 ∨ ¬new X3 X0 X2 ∨ X1 = X3

theorem Eq511.rule_6_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (prev_0 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X1 X2 ∨ ¬new X0 X1 X3 ∨ X2 = X3) (old_2 : ∀ (X0 X1 : G), ¬old X0 X1 X1 ∨ old X1 X0 X1) (old_6 : ∀ (X0 X1 X2 X3 X4 : G), ¬old X0 X1 X2 ∨ ¬old X1 X2 X3 ∨ ¬old X2 X1 X3 ∨ ¬old X4 X0 X1 ∨ old X0 X4 X1) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (imp_new_0 : ∀ (X Y Z : G), ¬old X Y Z ∨ new X Y Z) (X0 X1 X2 X3 X4 : G) : ¬new X0 X1 X2 ∨ ¬new X1 X2 X3 ∨ ¬new X2 X1 X3 ∨ ¬new X4 X0 X1 ∨ new X0 X4 X1

theorem Eq511.rule_7_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (prev_1 : ∀ (X0 X1 X2 X3 X4 : G), ¬new X0 X1 X2 ∨ ¬new X1 X2 X3 ∨ ¬new X1 X3 X4 ∨ new X1 X4 X0) (prev_4 : ∀ (X0 X1 X2 X3 X4 : G), ¬new X0 X1 X2 ∨ ¬new X3 X0 X4 ∨ ¬new X3 X1 X2 ∨ new X0 X3 X4) (X0 X1 X2 X3 X4 : G) : ¬new X0 X1 X2 ∨ ¬new X0 X3 X0 ∨ ¬new X1 X3 X0 ∨ ¬new X4 X1 X3 ∨ new X1 X2 X4

theorem Eq511.rule_8_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 X3 : G) : ¬new X0 X1 X2 ∨ ¬new X3 X1 X2 ∨ X3 = X0

theorem Eq511.rule_9_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_9 : ∀ (X0 X1 X2 : G), ¬old X0 X1 X0 ∨ ¬old X0 X2 X0 ∨ ¬old X2 X0 X1 ∨ X1 = X2) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 : G) : ¬new X0 X1 X0 ∨ ¬new X0 X2 X0 ∨ ¬new X2 X0 X1 ∨ X1 = X2

theorem Eq511.rule_10_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_10 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X0 ∨ ¬old X2 X0 X3 ∨ ¬old X3 X0 X1 ∨ old X0 X0 X2) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_4 : ∀ (X Y Z : G), old b a (sF4 X Y Z) ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (imp_new_0 : ∀ (X Y Z : G), ¬old X Y Z ∨ new X Y Z) (X0 X1 X2 X3 : G) : ¬new X0 X1 X0 ∨ ¬new X2 X0 X3 ∨ ¬new X3 X0 X1 ∨ new X0 X0 X2

theorem Eq511.rule_11_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (prev_2 : ∀ (X0 X1 : G), ¬new X0 X1 X1 ∨ new X1 X0 X1) (prev_5 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X0 X1 ∨ ¬new X0 X1 X2 ∨ ¬new X3 X0 X2 ∨ X1 = X3) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_11 : ∀ (X0 X1 X2 X3 X4 : G), ¬old X0 X1 X2 ∨ ¬old X3 X0 X1 ∨ ¬old X4 X0 X2 ∨ old X0 X3 X4) (imp_new_1 : ∀ (X Y Z : G), a ≠ X ∨ b ≠ Y ∨ c ≠ Z ∨ new X Y Z) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (imp_new_0 : ∀ (X Y Z : G), ¬old X Y Z ∨ new X Y Z) (X0 X1 X2 X3 X4 : G) : ¬new X0 X1 X2 ∨ ¬new X3 X0 X1 ∨ ¬new X4 X0 X2 ∨ new X0 X3 X4

theorem Eq511.rule_12_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (prev_5 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X0 X1 ∨ ¬new X0 X1 X2 ∨ ¬new X3 X0 X2 ∨ X1 = X3) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (prev_8 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X1 X2 ∨ ¬new X3 X1 X2 ∨ X3 = X0) (old_12 : ∀ (X0 X1 X2 X3 X4 X5 : G), ¬old X0 X1 X2 ∨ ¬old X0 X3 X2 ∨ ¬old X4 X0 X1 ∨ ¬old X5 X0 X3 ∨ X4 = X5) (old_15 : ∀ (X0 X1 X2 X3 X4 : G), ¬old X0 X1 X0 ∨ ¬old X0 X2 X3 ∨ ¬old X3 X0 X1 ∨ ¬old X4 X0 X2 ∨ X0 = X4) (imp_new_1 : ∀ (X Y Z : G), a ≠ X ∨ b ≠ Y ∨ c ≠ Z ∨ new X Y Z) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (imp_new_2 : ∀ (X Y Z X2 : G), a ≠ X ∨ c ≠ Y ∨ ¬old Z a X2 ∨ ¬old a X2 b ∨ new X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_1_3 : ∀ (X Y Z : G), old a (sF0 X Y Z) b ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (imp_new_4 : ∀ (X Y Z X3 : G), b ≠ X ∨ c ≠ Y ∨ ¬old a X3 a ∨ ¬old b X3 a ∨ ¬old Z b X3 ∨ new X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_2 : ∀ (X Y Z : G), a = Z ∨ ¬sP4 X Y Z) (rule_def_4_4 : ∀ (X Y Z : G), old b a (sF4 X Y Z) ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 X3 X4 X5 : G) : ¬new X0 X1 X2 ∨ ¬new X0 X3 X2 ∨ ¬new X4 X0 X1 ∨ ¬new X5 X0 X3 ∨ X4 = X5

theorem Eq511.rule_13_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (old_0 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X0 X1 X3 ∨ X2 = X3) (prev_0 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X1 X2 ∨ ¬new X0 X1 X3 ∨ X2 = X3) (prev_1 : ∀ (X0 X1 X2 X3 X4 : G), ¬new X0 X1 X2 ∨ ¬new X1 X2 X3 ∨ ¬new X1 X3 X4 ∨ new X1 X4 X0) (prev_7 : ∀ (X0 X1 X2 X3 X4 : G), ¬new X0 X1 X2 ∨ ¬new X0 X3 X0 ∨ ¬new X1 X3 X0 ∨ ¬new X4 X1 X3 ∨ new X1 X2 X4) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_14 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X0 X3 X0 ∨ ¬old X1 X0 X3 ∨ old X0 X2 X0) (imp_new_1 : ∀ (X Y Z : G), a ≠ X ∨ b ≠ Y ∨ c ≠ Z ∨ new X Y Z) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (imp_new_2 : ∀ (X Y Z X2 : G), a ≠ X ∨ c ≠ Y ∨ ¬old Z a X2 ∨ ¬old a X2 b ∨ new X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_1_3 : ∀ (X Y Z : G), old a (sF0 X Y Z) b ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (imp_new_5 : ∀ (X Y Z X3 : G), a ≠ X ∨ c ≠ Y ∨ a ≠ Z ∨ ¬old a X3 a ∨ ¬old b a X3 ∨ new X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_2 : ∀ (X Y Z : G), a = Z ∨ ¬sP4 X Y Z) (rule_def_4_3 : ∀ (X Y Z : G), old a (sF4 X Y Z) a ∨ ¬sP4 X Y Z) (rule_def_4_4 : ∀ (X Y Z : G), old b a (sF4 X Y Z) ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 X3 X4 : G) : ¬new X0 X1 X2 ∨ ¬new X0 X3 X1 ∨ ¬new X0 X4 X0 ∨ ¬new X3 X0 X4 ∨ X2 = X0

theorem Eq511.rule_14_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬old a b X0) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (prev_0 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X1 X2 ∨ ¬new X0 X1 X3 ∨ X2 = X3) (prev_4 : ∀ (X0 X1 X2 X3 X4 : G), ¬new X0 X1 X2 ∨ ¬new X3 X0 X4 ∨ ¬new X3 X1 X2 ∨ new X0 X3 X4) (prev_7 : ∀ (X0 X1 X2 X3 X4 : G), ¬new X0 X1 X2 ∨ ¬new X0 X3 X0 ∨ ¬new X1 X3 X0 ∨ ¬new X4 X1 X3 ∨ new X1 X2 X4) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_14 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X0 X3 X0 ∨ ¬old X1 X0 X3 ∨ old X0 X2 X0) (imp_new_1 : ∀ (X Y Z : G), a ≠ X ∨ b ≠ Y ∨ c ≠ Z ∨ new X Y Z) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (imp_new_2 : ∀ (X Y Z X2 : G), a ≠ X ∨ c ≠ Y ∨ ¬old Z a X2 ∨ ¬old a X2 b ∨ new X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_1_3 : ∀ (X Y Z : G), old a (sF0 X Y Z) b ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (imp_new_5 : ∀ (X Y Z X3 : G), a ≠ X ∨ c ≠ Y ∨ a ≠ Z ∨ ¬old a X3 a ∨ ¬old b a X3 ∨ new X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_3 : ∀ (X Y Z : G), old a (sF4 X Y Z) a ∨ ¬sP4 X Y Z) (rule_def_4_4 : ∀ (X Y Z : G), old b a (sF4 X Y Z) ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (imp_new_0 : ∀ (X Y Z : G), ¬old X Y Z ∨ new X Y Z) (X0 X1 X2 X3 : G) : ¬new X0 X1 X2 ∨ ¬new X0 X3 X0 ∨ ¬new X1 X0 X3 ∨ new X0 X2 X0

theorem Eq511.rule_15_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (ac : a ≠ c) (bc : c ≠ b) (p4XY : ∀ (X1 X2 : G), ¬old X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬old c X1 X2) (prev_0 : ∀ (X0 X1 X2 X3 : G), ¬new X0 X1 X2 ∨ ¬new X0 X1 X3 ∨ X2 = X3) (prev_7 : ∀ (X0 X1 X2 X3 X4 : G), ¬new X0 X1 X2 ∨ ¬new X0 X3 X0 ∨ ¬new X1 X3 X0 ∨ ¬new X4 X1 X3 ∨ new X1 X2 X4) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (old_15 : ∀ (X0 X1 X2 X3 X4 : G), ¬old X0 X1 X0 ∨ ¬old X0 X2 X3 ∨ ¬old X3 X0 X1 ∨ ¬old X4 X0 X2 ∨ X0 = X4) (imp_new_1 : ∀ (X Y Z : G), a ≠ X ∨ b ≠ Y ∨ c ≠ Z ∨ new X Y Z) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (X0 X1 X2 X3 X4 : G) : ¬new X0 X1 X0 ∨ ¬new X0 X2 X3 ∨ ¬new X3 X0 X1 ∨ ¬new X4 X0 X2 ∨ X0 = X4

theorem Eq511.rule_finite_0_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (memold : G → Prop) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (old_mem1 : ∀ (X Y Z : G), ¬old X Y Z ∨ memold X) (X Y Z : G) : ¬new X Y Z ∨ X = a ∨ X = b ∨ memold X ∨ X = c

theorem Eq511.rule_finite_1_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (memold : G → Prop) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (old_mem2 : ∀ (X Y Z : G), ¬old X Y Z ∨ memold Y) (X Y Z : G) : ¬new X Y Z ∨ Y = a ∨ Y = b ∨ memold Y ∨ Y = c

theorem Eq511.rule_finite_2_preserved (G : Type u_1) (a b c : G) (old new sP0 : G → G → G → Prop) (sF0 : G → G → G → G) (sP1 : G → G → G → Prop) (sF1 sF2 : G → G → G → G) (sP2 : G → G → G → Prop) (sF3 : G → G → G → G) (sP3 : G → G → G → Prop) (sF4 : G → G → G → G) (sP4 : G → G → G → Prop) (memold : G → Prop) (ac : a ≠ c) (p4XZ : ∀ (X1 X2 : G), ¬old X1 c X2) (old_8 : ∀ (X0 X1 X2 X3 : G), ¬old X0 X1 X2 ∨ ¬old X3 X1 X2 ∨ X3 = X0) (rule_def_0_0 : ∀ (X Y Z : G), a = X ∨ ¬sP0 X Y Z) (rule_def_0_1 : ∀ (X Y Z : G), b = Y ∨ ¬sP0 X Y Z) (rule_def_0_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP0 X Y Z) (rule_def_1_0 : ∀ (X Y Z : G), a = X ∨ ¬sP1 X Y Z) (rule_def_1_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP1 X Y Z) (rule_def_1_2 : ∀ (X Y Z : G), old Z a (sF0 X Y Z) ∨ ¬sP1 X Y Z) (rule_def_2_0 : ∀ (X Y Z : G), b = X ∨ ¬sP2 X Y Z) (rule_def_2_1 : ∀ (X Y Z : G), a = Y ∨ ¬sP2 X Y Z) (rule_def_2_2 : ∀ (X Y Z : G), c = Z ∨ ¬sP2 X Y Z) (rule_def_2_3 : ∀ (X Y Z : G), old b (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_2_4 : ∀ (X Y Z : G), old a (sF1 X Y Z) (sF2 X Y Z) ∨ ¬sP2 X Y Z) (rule_def_3_0 : ∀ (X Y Z : G), b = X ∨ ¬sP3 X Y Z) (rule_def_3_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP3 X Y Z) (rule_def_3_2 : ∀ (X Y Z : G), old a (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_3 : ∀ (X Y Z : G), old b (sF3 X Y Z) a ∨ ¬sP3 X Y Z) (rule_def_3_4 : ∀ (X Y Z : G), old Z b (sF3 X Y Z) ∨ ¬sP3 X Y Z) (rule_def_4_0 : ∀ (X Y Z : G), a = X ∨ ¬sP4 X Y Z) (rule_def_4_1 : ∀ (X Y Z : G), c = Y ∨ ¬sP4 X Y Z) (rule_def_4_2 : ∀ (X Y Z : G), a = Z ∨ ¬sP4 X Y Z) (new_imp : ∀ (X Y Z : G), ¬new X Y Z ∨ old X Y Z ∨ sP0 X Y Z ∨ sP1 X Y Z ∨ sP2 X Y Z ∨ sP3 X Y Z ∨ sP4 X Y Z) (old_mem1 : ∀ (X Y Z : G), ¬old X Y Z ∨ memold X) (old_mem3 : ∀ (X Y Z : G), ¬old X Y Z ∨ memold Z) (X Y Z : G) : ¬new X Y Z ∨ Z = a ∨ Z = b ∨ memold Z ∨ Z = c

structure Eq511.PartialSolution (G : Type u_1) : Type u_1

• R : G → G → G → Prop
• rule_0 : ∀ (X0 X1 X2 X3 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X0 X1 X3 ∨ X2 = X3
• rule_1 : ∀ (X0 X1 X2 X3 X4 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X1 X2 X3 ∨ ¬self.R X1 X3 X4 ∨ self.R X1 X4 X0
• rule_2 : ∀ (X0 X1 : G), ¬self.R X0 X1 X1 ∨ self.R X1 X0 X1
• rule_3 : ∀ (X0 X1 : G), ¬self.R X0 X1 X0 ∨ ¬self.R X1 X0 X1 ∨ self.R X0 X0 X0
• rule_4 : ∀ (X0 X1 X2 X3 X4 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X3 X0 X4 ∨ ¬self.R X3 X1 X2 ∨ self.R X0 X3 X4
• rule_5 : ∀ (X0 X1 X2 X3 : G), ¬self.R X0 X0 X1 ∨ ¬self.R X0 X1 X2 ∨ ¬self.R X3 X0 X2 ∨ X1 = X3
• rule_6 : ∀ (X0 X1 X2 X3 X4 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X1 X2 X3 ∨ ¬self.R X2 X1 X3 ∨ ¬self.R X4 X0 X1 ∨ self.R X0 X4 X1
• rule_7 : ∀ (X0 X1 X2 X3 X4 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X0 X3 X0 ∨ ¬self.R X1 X3 X0 ∨ ¬self.R X4 X1 X3 ∨ self.R X1 X2 X4
• rule_8 : ∀ (X0 X1 X2 X3 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X3 X1 X2 ∨ X3 = X0
• rule_9 : ∀ (X0 X1 X2 : G), ¬self.R X0 X1 X0 ∨ ¬self.R X0 X2 X0 ∨ ¬self.R X2 X0 X1 ∨ X1 = X2
• rule_10 : ∀ (X0 X1 X2 X3 : G), ¬self.R X0 X1 X0 ∨ ¬self.R X2 X0 X3 ∨ ¬self.R X3 X0 X1 ∨ self.R X0 X0 X2
• rule_11 : ∀ (X0 X1 X2 X3 X4 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X3 X0 X1 ∨ ¬self.R X4 X0 X2 ∨ self.R X0 X3 X4
• rule_12 : ∀ (X0 X1 X2 X3 X4 X5 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X0 X3 X2 ∨ ¬self.R X4 X0 X1 ∨ ¬self.R X5 X0 X3 ∨ X4 = X5
• rule_13 : ∀ (X0 X1 X2 X3 X4 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X0 X3 X1 ∨ ¬self.R X0 X4 X0 ∨ ¬self.R X3 X0 X4 ∨ X2 = X0
• rule_14 : ∀ (X0 X1 X2 X3 : G), ¬self.R X0 X1 X2 ∨ ¬self.R X0 X3 X0 ∨ ¬self.R X1 X0 X3 ∨ self.R X0 X2 X0
• rule_15 : ∀ (X0 X1 X2 X3 X4 : G), ¬self.R X0 X1 X0 ∨ ¬self.R X0 X2 X3 ∨ ¬self.R X3 X0 X1 ∨ ¬self.R X4 X0 X2 ∨ X0 = X4
• finsupp : Finset G
• mem_1 : ∀ (X Y Z : G), ¬self.R X Y Z ∨ X ∈ self.finsupp
• mem_2 : ∀ (X Y Z : G), ¬self.R X Y Z ∨ Y ∈ self.finsupp
• mem_3 : ∀ (X Y Z : G), ¬self.R X Y Z ∨ Z ∈ self.finsupp

theorem Eq511.PartialSolution.adjoin {G : Type u_1} (ps : Eq511.PartialSolution G) (a b c : G) (ac : a ≠ c) (bc : c ≠ b) (p3 : ∀ (X0 : G), ¬ps.R a b X0) (p4XY : ∀ (X1 X2 : G), ¬ps.R X1 X2 c) (p4XZ : ∀ (X1 X2 : G), ¬ps.R X1 c X2) (p4YZ : ∀ (X1 X2 : G), ¬ps.R c X1 X2) : ∃ (next : Eq511.PartialSolution G), next.R a b c ∧ ∀ (x y z : G), ps.R x y z → next.R x y z

noncomputable def Eq511.PartialSolution.addArbitrary {G : Type u_1} (ps : Eq511.PartialSolution G) [Infinite G] (a b : G) : Eq511.PartialSolution G

Equations

• ps.addArbitrary a b = if h : ∃ (c : G), ps.R a b c then ps else let c := ⋯.choose; let_fun hc := ⋯; ⋯.choose

theorem Eq511.PartialSolution.addArbitrary_covers {G : Type u_1} (ps : Eq511.PartialSolution G) [Infinite G] (a b : G) : ∃ (c : G), (ps.addArbitrary a b).R a b c

theorem Eq511.PartialSolution.addArbitrary_contains {G : Type u_1} (ps : Eq511.PartialSolution G) [Infinite G] (a b x y z : G) : ps.R x y z → (ps.addArbitrary a b).R x y z

noncomputable def Eq511.PartialSolution.complSeq (ps : Eq511.PartialSolution ℕ) : ℕ → Eq511.PartialSolution ℕ

Equations

• ps.complSeq 0 = ps
• ps.complSeq n.succ = (ps.complSeq n).addArbitrary (Nat.unpair n).1 (Nat.unpair n).2

theorem Eq511.PartialSolution.complSeq_exists (ps : Eq511.PartialSolution ℕ) (a b : ℕ) : ∃ (c : ℕ), (ps.complSeq (Nat.pair a b + 1)).R a b c

theorem Eq511.PartialSolution.complSeq_mono_add_one (ps : Eq511.PartialSolution ℕ) (i a b c : ℕ) (h : (ps.complSeq i).R a b c) : (ps.complSeq (i + 1)).R a b c

theorem Eq511.PartialSolution.complSeq_mono (ps : Eq511.PartialSolution ℕ) (i j : ℕ) (hij : i ≤ j) (a b c : ℕ) (h : (ps.complSeq i).R a b c) : (ps.complSeq j).R a b c

theorem Eq511.PartialSolution.complSeq_exists_of_lt (ps : Eq511.PartialSolution ℕ) (a b i : ℕ) (h : Nat.pair a b < i) : ∃ (c : ℕ), (ps.complSeq i).R a b c

noncomputable def Eq511.PartialSolution.compl (ps : Eq511.PartialSolution ℕ) (a b c : ℕ) : Prop

Equations

• ps.compl a b c = (ps.complSeq (Nat.pair a b + 1)).R a b c

theorem Eq511.PartialSolution.compl_rule0 (ps : Eq511.PartialSolution ℕ) (a b c d : ℕ) (h : ps.compl a b c) (h2 : ps.compl a b d) : c = d

theorem Eq511.PartialSolution.compl_exists (ps : Eq511.PartialSolution ℕ) (a b : ℕ) : ∃ (c : ℕ), ps.compl a b c

theorem Eq511.PartialSolution.complSeq_of_compl_of_lt (ps : Eq511.PartialSolution ℕ) (a b i : ℕ) (habi : Nat.pair a b < i) (c : ℕ) (h : ps.compl a b c) : (ps.complSeq i).R a b c

theorem Eq511.PartialSolution.complSeq_iff_of_lt (ps : Eq511.PartialSolution ℕ) (a b i : ℕ) (habi : Nat.pair a b < i) (c : ℕ) : ps.compl a b c ↔ (ps.complSeq i).R a b c

theorem Eq511.PartialSolution.compl_rule1 (ps : Eq511.PartialSolution ℕ) (X0 X1 X2 X3 X4 : ℕ) : ¬ps.compl X0 X1 X2 ∨ ¬ps.compl X1 X2 X3 ∨ ¬ps.compl X1 X3 X4 ∨ ps.compl X1 X4 X0

noncomputable def Eq511.PartialSolution.complFun (ps : Eq511.PartialSolution ℕ) (a b : ℕ) : ℕ

Equations

• ps.complFun a b = ⋯.choose

theorem Eq511.PartialSolution.complFun_eq_iff (ps : Eq511.PartialSolution ℕ) (a b c : ℕ) : ps.complFun a b = c ↔ ps.compl a b c

theorem Eq511.PartialSolution.of_R (ps : Eq511.PartialSolution ℕ) (a b c : ℕ) (h : ps.R a b c) : ps.complFun a b = c

noncomputable def Eq511.PartialSolution.toMagma (ps : Eq511.PartialSolution ℕ) : Magma ℕ

Equations

• ps.toMagma = { op := ps.complFun }

theorem Eq511.PartialSolution.toMagma_equation511 (ps : Eq511.PartialSolution ℕ) : Equation511 ℕ

noncomputable def Eq511.PartialSolution.counter614 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation614 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation614 G

noncomputable def Eq511.PartialSolution.counter714 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation714 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation714 G

noncomputable def Eq511.PartialSolution.counter1020 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation1020 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation1020 G

noncomputable def Eq511.PartialSolution.counter1223 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation1223 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation1223 G

noncomputable def Eq511.PartialSolution.counter2238 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation2238 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation2238 G

noncomputable def Eq511.PartialSolution.counter2338 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation2338 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation2338 G

noncomputable def Eq511.PartialSolution.counter2441 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation2441 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation2441 G

noncomputable def Eq511.PartialSolution.counter2847 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation2847 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation2847 G

noncomputable def Eq511.PartialSolution.counter3050 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation3050 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation3050 G

noncomputable def Eq511.PartialSolution.counter4380 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation4380 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation4380 G

noncomputable def Eq511.PartialSolution.counter4435 : Eq511.PartialSolution ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Equation511_not_implies_Equation4435 : ∃ (G : Type) (x : Magma G), Equation511 G ∧ ¬Equation4435 G