Proofgold Signed Transaction

Definition Church13_p := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x14) ⟶ x1 x0
Definition TwoRamseyGraph_3_5_Church13 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3)
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 691d6.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known 167fd.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known 8e1ba.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known e781d.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known 27109.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known 43ae5.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known 1af1a.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known cc732.. : ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ (((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) x0 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15) x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x4 x5 . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x4 x5 . x5) ⟶ False
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem f57a7.. : ∀ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ Church13_p x3 ⟶ ((λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) = x0 ⟶ ∀ x4 : ο . x4) ⟶ ((λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) = x1 ⟶ ∀ x4 : ο . x4) ⟶ ((λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) = x2 ⟶ ∀ x4 : ο . x4) ⟶ ((λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) x0 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) x1 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) x2 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 (λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) x3 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x3 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x3 = λ x5 x6 . x6) ⟶ (TwoRamseyGraph_3_5_Church13 x2 x3 = λ x5 x6 . x6) ⟶ False (proof)
Known b9bfd.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ ∀ x1 : ο . (∀ x2 x3 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x4 ⟶ Church13_p (x2 x4)) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x4 ⟶ Church13_p (x3 x4)) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x2 (x3 x4) = x4) ⟶ (∀ x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x3 (x2 x4) = x4) ⟶ (∀ x4 x5 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x4 ⟶ Church13_p x5 ⟶ TwoRamseyGraph_3_5_Church13 x4 x5 = TwoRamseyGraph_3_5_Church13 (x2 x4) (x2 x5)) ⟶ (x2 x0 = λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x5) ⟶ x1) ⟶ x1
Theorem 4a8a6.. : ∀ x0 x1 x2 x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ Church13_p x2 ⟶ Church13_p x3 ⟶ Church13_p x4 ⟶ (x0 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x0 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x2 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x3 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x0 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x2 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x3 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x1 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x2 x3 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x2 x4 = λ x6 x7 . x7) ⟶ (TwoRamseyGraph_3_5_Church13 x3 x4 = λ x6 x7 . x7) ⟶ False (proof)
Param or^or : ο → ο → ο
Known orIR^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known orIL^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem cd49f.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ or (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x3 x4 . x3) (TwoRamseyGraph_3_5_Church13 x0 x1 = λ x3 x4 . x4) (proof)
Param u1 : ι
Param u2 : ι
Param u3 : ι
Param u4 : ι
Param u5 : ι
Param u6 : ι
Param u7 : ι
Param u8 : ι
Param u9 : ι
Param u10 : ι
Param u11 : ι
Param u12 : ι
Known neq_1_0^neq_1_0 : u1 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_0^neq_2_0 : u2 = 0 ⟶ ∀ x0 : ο . x0
Known neq_3_0^neq_3_0 : u3 = 0 ⟶ ∀ x0 : ο . x0
Known neq_4_0^neq_4_0 : u4 = 0 ⟶ ∀ x0 : ο . x0
Known neq_5_0^neq_5_0 : u5 = 0 ⟶ ∀ x0 : ο . x0
Known neq_6_0^neq_6_0 : u6 = 0 ⟶ ∀ x0 : ο . x0
Known neq_7_0^neq_7_0 : u7 = 0 ⟶ ∀ x0 : ο . x0
Known neq_8_0^neq_8_0 : u8 = 0 ⟶ ∀ x0 : ο . x0
Known neq_9_0^neq_9_0 : u9 = 0 ⟶ ∀ x0 : ο . x0
Known 0e10e.. : u10 = 0 ⟶ ∀ x0 : ο . x0
Known 19f75.. : u11 = 0 ⟶ ∀ x0 : ο . x0
Known efdfc.. : u12 = 0 ⟶ ∀ x0 : ο . x0
Known neq_2_1^neq_2_1 : u2 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_1^neq_3_1 : u3 = u1 ⟶ ∀ x0 : ο . x0
Known neq_4_1^neq_4_1 : u4 = u1 ⟶ ∀ x0 : ο . x0
Known neq_5_1^neq_5_1 : u5 = u1 ⟶ ∀ x0 : ο . x0
Known neq_6_1^neq_6_1 : u6 = u1 ⟶ ∀ x0 : ο . x0
Known neq_7_1^neq_7_1 : u7 = u1 ⟶ ∀ x0 : ο . x0
Known neq_8_1^neq_8_1 : u8 = u1 ⟶ ∀ x0 : ο . x0
Known neq_9_1^neq_9_1 : u9 = u1 ⟶ ∀ x0 : ο . x0
Known d183f.. : u10 = u1 ⟶ ∀ x0 : ο . x0
Known 618f7.. : u11 = u1 ⟶ ∀ x0 : ο . x0
Known ce0cd.. : u12 = u1 ⟶ ∀ x0 : ο . x0
Known neq_3_2^neq_3_2 : u3 = u2 ⟶ ∀ x0 : ο . x0
Known neq_4_2^neq_4_2 : u4 = u2 ⟶ ∀ x0 : ο . x0
Known neq_5_2^neq_5_2 : u5 = u2 ⟶ ∀ x0 : ο . x0
Known neq_6_2^neq_6_2 : u6 = u2 ⟶ ∀ x0 : ο . x0
Known neq_7_2^neq_7_2 : u7 = u2 ⟶ ∀ x0 : ο . x0
Known neq_8_2^neq_8_2 : u8 = u2 ⟶ ∀ x0 : ο . x0
Known neq_9_2^neq_9_2 : u9 = u2 ⟶ ∀ x0 : ο . x0
Known e02d9.. : u10 = u2 ⟶ ∀ x0 : ο . x0
Known 2c42c.. : u11 = u2 ⟶ ∀ x0 : ο . x0
Known 8158b.. : u12 = u2 ⟶ ∀ x0 : ο . x0
Known neq_4_3^neq_4_3 : u4 = u3 ⟶ ∀ x0 : ο . x0
Known neq_5_3^neq_5_3 : u5 = u3 ⟶ ∀ x0 : ο . x0
Known neq_6_3^neq_6_3 : u6 = u3 ⟶ ∀ x0 : ο . x0
Known neq_7_3^neq_7_3 : u7 = u3 ⟶ ∀ x0 : ο . x0
Known neq_8_3^neq_8_3 : u8 = u3 ⟶ ∀ x0 : ο . x0
Known neq_9_3^neq_9_3 : u9 = u3 ⟶ ∀ x0 : ο . x0
Known 68152.. : u10 = u3 ⟶ ∀ x0 : ο . x0
Known b06e1.. : u11 = u3 ⟶ ∀ x0 : ο . x0
Known e015c.. : u12 = u3 ⟶ ∀ x0 : ο . x0
Known neq_5_4^neq_5_4 : u5 = u4 ⟶ ∀ x0 : ο . x0
Known neq_6_4^neq_6_4 : u6 = u4 ⟶ ∀ x0 : ο . x0
Known neq_7_4^neq_7_4 : u7 = u4 ⟶ ∀ x0 : ο . x0
Known neq_8_4^neq_8_4 : u8 = u4 ⟶ ∀ x0 : ο . x0
Known neq_9_4^neq_9_4 : u9 = u4 ⟶ ∀ x0 : ο . x0
Known 33d16.. : u10 = u4 ⟶ ∀ x0 : ο . x0
Known 6a6f1.. : u11 = u4 ⟶ ∀ x0 : ο . x0
Known 7aa79.. : u12 = u4 ⟶ ∀ x0 : ο . x0
Known neq_6_5^neq_6_5 : u6 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_5^neq_7_5 : u7 = u5 ⟶ ∀ x0 : ο . x0
Known neq_8_5^neq_8_5 : u8 = u5 ⟶ ∀ x0 : ο . x0
Known neq_9_5^neq_9_5 : u9 = u5 ⟶ ∀ x0 : ο . x0
Known a7d50.. : u10 = u5 ⟶ ∀ x0 : ο . x0
Known 1b659.. : u11 = u5 ⟶ ∀ x0 : ο . x0
Known 07eba.. : u12 = u5 ⟶ ∀ x0 : ο . x0
Known neq_7_6^neq_7_6 : u7 = u6 ⟶ ∀ x0 : ο . x0
Known neq_8_6^neq_8_6 : u8 = u6 ⟶ ∀ x0 : ο . x0
Known neq_9_6^neq_9_6 : u9 = u6 ⟶ ∀ x0 : ο . x0
Known d0401.. : u10 = u6 ⟶ ∀ x0 : ο . x0
Known 949f2.. : u11 = u6 ⟶ ∀ x0 : ο . x0
Known 0bd83.. : u12 = u6 ⟶ ∀ x0 : ο . x0
Known neq_8_7^neq_8_7 : u8 = u7 ⟶ ∀ x0 : ο . x0
Known neq_9_7^neq_9_7 : u9 = u7 ⟶ ∀ x0 : ο . x0
Known 7d7a8.. : u10 = u7 ⟶ ∀ x0 : ο . x0
Known 4abfa.. : u11 = u7 ⟶ ∀ x0 : ο . x0
Known 6a15f.. : u12 = u7 ⟶ ∀ x0 : ο . x0
Known neq_9_8^neq_9_8 : u9 = u8 ⟶ ∀ x0 : ο . x0
Known 96175.. : u10 = u8 ⟶ ∀ x0 : ο . x0
Known b3a20.. : u11 = u8 ⟶ ∀ x0 : ο . x0
Known a6a6c.. : u12 = u8 ⟶ ∀ x0 : ο . x0
Known 4fc31.. : u10 = u9 ⟶ ∀ x0 : ο . x0
Known 4f03f.. : u11 = u9 ⟶ ∀ x0 : ο . x0
Known 22885.. : u12 = u9 ⟶ ∀ x0 : ο . x0
Known ebfb7.. : u11 = u10 ⟶ ∀ x0 : ο . x0
Known 6c583.. : u12 = u10 ⟶ ∀ x0 : ο . x0
Known ab306.. : u12 = u11 ⟶ ∀ x0 : ο . x0
Theorem d7c49.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ x0 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x0 = x1 (proof)