Proofgold Signed Transaction

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition f3993.. := λ x0 : ι → ο . λ x1 : (ι → ο) → ο . λ x2 : (ι → ι → ο) → ο . λ x3 . λ x4 x5 : ι → ι → ι . and (and (and (and (and (x2 (λ x6 x7 . x0 (x4 x6 x7))) (x1 (λ x6 . x1 (λ x7 . x0 (x5 x6 x7))))) (x1 (λ x6 . x4 x6 x3 = x6))) (x2 (λ x6 x7 . x4 x6 x7 = x4 x7 x6))) (x1 (λ x6 . x1 (λ x7 . x4 (x5 x6 x7) x7 = x6)))) (x1 (λ x6 . x1 (λ x7 . x5 (x4 x6 x7) x7 = x6)))
Definition c1ee3.. := λ x0 : ι → ο . λ x1 : (ι → ο) → ο . λ x2 : (ι → ι → ο) → ο . λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . λ x17 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x18 : ι → ι → ι . λ x19 . x18 (x18 (x17 (x17 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) (x17 x4 x11 x3 x16 x12 x13 x8 x14 x15 x7 x10 x6 x5 x9) (x17 x5 x3 x15 x14 x13 x9 x11 x7 x6 x10 x4 x8 x16 x12) (x17 x6 x16 x14 x3 x9 x10 x7 x4 x5 x11 x8 x12 x13 x15) (x17 x7 x12 x13 x9 x15 x3 x6 x16 x8 x5 x14 x10 x11 x4) (x17 x8 x13 x9 x10 x3 x5 x4 x11 x12 x15 x7 x16 x14 x6) (x17 x9 x8 x11 x7 x6 x4 x13 x12 x14 x16 x15 x5 x3 x10) (x17 x10 x14 x7 x4 x16 x11 x12 x13 x3 x8 x6 x15 x9 x5) (x17 x11 x15 x6 x5 x8 x12 x14 x3 x10 x13 x16 x9 x4 x7) (x17 x12 x7 x10 x11 x5 x15 x16 x8 x13 x3 x9 x4 x6 x14) (x17 x13 x10 x4 x8 x14 x7 x15 x6 x16 x9 x5 x11 x12 x3) (x17 x14 x6 x8 x12 x10 x16 x5 x15 x9 x4 x11 x3 x7 x13) (x17 x15 x5 x16 x13 x11 x14 x3 x9 x4 x6 x12 x7 x10 x8) (x17 x16 x9 x12 x15 x4 x6 x10 x5 x7 x14 x3 x13 x8 x11)) x19)
Definition f5650.. := λ x0 : ι → ο . λ x1 : (ι → ο) → ο . λ x2 : (ι → ι → ο) → ο . λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . λ x17 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x18 : ι → ι → ι . λ x19 . x18 (x18 (x17 (x17 x3 x5 x4 x6 x8 x7 x15 x11 x10 x12 x16 x14 x9 x13) (x17 x4 x3 x13 x10 x16 x9 x8 x6 x15 x14 x5 x12 x11 x7) (x17 x5 x15 x3 x11 x12 x8 x14 x16 x6 x7 x13 x9 x4 x10) (x17 x6 x14 x11 x3 x9 x16 x7 x13 x5 x15 x10 x4 x12 x8) (x17 x7 x12 x10 x9 x3 x13 x6 x5 x16 x4 x8 x15 x14 x11) (x17 x8 x9 x14 x13 x11 x3 x4 x12 x7 x10 x6 x5 x16 x15) (x17 x9 x16 x8 x7 x6 x5 x3 x15 x14 x13 x12 x11 x10 x4) (x17 x10 x13 x12 x8 x14 x6 x16 x3 x11 x5 x4 x7 x15 x9) (x17 x11 x4 x9 x12 x15 x10 x5 x8 x3 x6 x14 x13 x7 x16) (x17 x12 x7 x16 x14 x4 x11 x10 x9 x8 x3 x15 x6 x13 x5) (x17 x13 x8 x7 x15 x5 x4 x9 x10 x12 x11 x3 x16 x6 x14) (x17 x14 x10 x6 x5 x13 x15 x11 x4 x9 x16 x7 x3 x8 x12) (x17 x15 x11 x5 x16 x7 x12 x13 x14 x4 x8 x9 x10 x3 x6) (x17 x16 x6 x15 x4 x10 x14 x12 x7 x13 x9 x11 x8 x5 x3)) x19)
Definition 2e6fa.. := λ x0 : ι → ο . λ x1 : (ι → ο) → ο . λ x2 : (ι → ι → ο) → ο . λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . λ x17 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x18 x19 x20 : ι → ι → ι . λ x21 x22 x23 . x20 (x19 (x19 x23 x21) x22) (x19 x21 x22)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known and6I^and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ and (and (and (and (and x0 x1) x2) x3) x4) x5
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known and5I^and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Theorem eeafe.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ο) → ο . ∀ x2 : (ι → ι → ο) → ο . ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ (∀ x17 : ι → ο . x17 x3 ⟶ x17 x4 ⟶ x17 x5 ⟶ x17 x6 ⟶ x17 x7 ⟶ x17 x8 ⟶ x17 x9 ⟶ x17 x10 ⟶ x17 x11 ⟶ x17 x12 ⟶ x17 x13 ⟶ x17 x14 ⟶ x17 x15 ⟶ x17 x16 ⟶ x1 x17) ⟶ (∀ x17 : ι → ι → ο . x17 x3 x3 ⟶ x17 x3 x4 ⟶ x17 x3 x5 ⟶ x17 x3 x6 ⟶ x17 x3 x7 ⟶ x17 x3 x8 ⟶ x17 x3 x9 ⟶ x17 x3 x10 ⟶ x17 x3 x11 ⟶ x17 x3 x12 ⟶ x17 x3 x13 ⟶ x17 x3 x14 ⟶ x17 x3 x15 ⟶ x17 x3 x16 ⟶ x17 x4 x3 ⟶ x17 x4 x4 ⟶ x17 x4 x5 ⟶ x17 x4 x6 ⟶ x17 x4 x7 ⟶ x17 x4 x8 ⟶ x17 x4 x9 ⟶ x17 x4 x10 ⟶ x17 x4 x11 ⟶ x17 x4 x12 ⟶ x17 x4 x13 ⟶ x17 x4 x14 ⟶ x17 x4 x15 ⟶ x17 x4 x16 ⟶ x17 x5 x3 ⟶ x17 x5 x4 ⟶ x17 x5 x5 ⟶ x17 x5 x6 ⟶ x17 x5 x7 ⟶ x17 x5 x8 ⟶ x17 x5 x9 ⟶ x17 x5 x10 ⟶ x17 x5 x11 ⟶ x17 x5 x12 ⟶ x17 x5 x13 ⟶ x17 x5 x14 ⟶ x17 x5 x15 ⟶ x17 x5 x16 ⟶ x17 x6 x3 ⟶ x17 x6 x4 ⟶ x17 x6 x5 ⟶ x17 x6 x6 ⟶ x17 x6 x7 ⟶ x17 x6 x8 ⟶ x17 x6 x9 ⟶ x17 x6 x10 ⟶ x17 x6 x11 ⟶ x17 x6 x12 ⟶ x17 x6 x13 ⟶ x17 x6 x14 ⟶ x17 x6 x15 ⟶ x17 x6 x16 ⟶ x17 x7 x3 ⟶ x17 x7 x4 ⟶ x17 x7 x5 ⟶ x17 x7 x6 ⟶ x17 x7 x7 ⟶ x17 x7 x8 ⟶ x17 x7 x9 ⟶ x17 x7 x10 ⟶ x17 x7 x11 ⟶ x17 x7 x12 ⟶ x17 x7 x13 ⟶ x17 x7 x14 ⟶ x17 x7 x15 ⟶ x17 x7 x16 ⟶ x17 x8 x3 ⟶ x17 x8 x4 ⟶ x17 x8 x5 ⟶ x17 x8 x6 ⟶ x17 x8 x7 ⟶ x17 x8 x8 ⟶ x17 x8 x9 ⟶ x17 x8 x10 ⟶ x17 x8 x11 ⟶ x17 x8 x12 ⟶ x17 x8 x13 ⟶ x17 x8 x14 ⟶ x17 x8 x15 ⟶ x17 x8 x16 ⟶ x17 x9 x3 ⟶ x17 x9 x4 ⟶ x17 x9 x5 ⟶ x17 x9 x6 ⟶ x17 x9 x7 ⟶ x17 x9 x8 ⟶ x17 x9 x9 ⟶ x17 x9 x10 ⟶ x17 x9 x11 ⟶ x17 x9 x12 ⟶ x17 x9 x13 ⟶ x17 x9 x14 ⟶ x17 x9 x15 ⟶ x17 x9 x16 ⟶ x17 x10 x3 ⟶ x17 x10 x4 ⟶ x17 x10 x5 ⟶ x17 x10 x6 ⟶ x17 x10 x7 ⟶ x17 x10 x8 ⟶ x17 x10 x9 ⟶ x17 x10 x10 ⟶ x17 x10 x11 ⟶ x17 x10 x12 ⟶ x17 x10 x13 ⟶ x17 x10 x14 ⟶ x17 x10 x15 ⟶ x17 x10 x16 ⟶ x17 x11 x3 ⟶ x17 x11 x4 ⟶ x17 x11 x5 ⟶ x17 x11 x6 ⟶ x17 x11 x7 ⟶ x17 x11 x8 ⟶ x17 x11 x9 ⟶ x17 x11 x10 ⟶ x17 x11 x11 ⟶ x17 x11 x12 ⟶ x17 x11 x13 ⟶ x17 x11 x14 ⟶ x17 x11 x15 ⟶ x17 x11 x16 ⟶ x17 x12 x3 ⟶ x17 x12 x4 ⟶ x17 x12 x5 ⟶ x17 x12 x6 ⟶ x17 x12 x7 ⟶ x17 x12 x8 ⟶ x17 x12 x9 ⟶ x17 x12 x10 ⟶ x17 x12 x11 ⟶ x17 x12 x12 ⟶ x17 x12 x13 ⟶ x17 x12 x14 ⟶ x17 x12 x15 ⟶ x17 x12 x16 ⟶ x17 x13 x3 ⟶ x17 x13 x4 ⟶ x17 x13 x5 ⟶ x17 x13 x6 ⟶ x17 x13 x7 ⟶ x17 x13 x8 ⟶ x17 x13 x9 ⟶ x17 x13 x10 ⟶ x17 x13 x11 ⟶ x17 x13 x12 ⟶ x17 x13 x13 ⟶ x17 x13 x14 ⟶ x17 x13 x15 ⟶ x17 x13 x16 ⟶ x17 x14 x3 ⟶ x17 x14 x4 ⟶ x17 x14 x5 ⟶ x17 x14 x6 ⟶ x17 x14 x7 ⟶ x17 x14 x8 ⟶ x17 x14 x9 ⟶ x17 x14 x10 ⟶ x17 x14 x11 ⟶ x17 x14 x12 ⟶ x17 x14 x13 ⟶ x17 x14 x14 ⟶ x17 x14 x15 ⟶ x17 x14 x16 ⟶ x17 x15 x3 ⟶ x17 x15 x4 ⟶ x17 x15 x5 ⟶ x17 x15 x6 ⟶ x17 x15 x7 ⟶ x17 x15 x8 ⟶ x17 x15 x9 ⟶ x17 x15 x10 ⟶ x17 x15 x11 ⟶ x17 x15 x12 ⟶ x17 x15 x13 ⟶ x17 x15 x14 ⟶ x17 x15 x15 ⟶ x17 x15 x16 ⟶ x17 x16 x3 ⟶ x17 x16 x4 ⟶ x17 x16 x5 ⟶ x17 x16 x6 ⟶ x17 x16 x7 ⟶ x17 x16 x8 ⟶ x17 x16 x9 ⟶ x17 x16 x10 ⟶ x17 x16 x11 ⟶ x17 x16 x12 ⟶ x17 x16 x13 ⟶ x17 x16 x14 ⟶ x17 x16 x15 ⟶ x17 x16 x16 ⟶ x1 (λ x18 . x1 (x17 x18))) ⟶ (∀ x17 : ι → ι → ο . x17 x3 x4 ⟶ x17 x3 x5 ⟶ x17 x4 x5 ⟶ x17 x3 x6 ⟶ x17 x4 x6 ⟶ x17 x5 x6 ⟶ x17 x3 x7 ⟶ x17 x4 x7 ⟶ x17 x5 x7 ⟶ x17 x6 x7 ⟶ x17 x3 x8 ⟶ x17 x4 x8 ⟶ x17 x5 x8 ⟶ x17 x6 x8 ⟶ x17 x7 x8 ⟶ x17 x3 x9 ⟶ x17 x4 x9 ⟶ x17 x5 x9 ⟶ x17 x6 x9 ⟶ x17 x7 x9 ⟶ x17 x8 x9 ⟶ x17 x3 x10 ⟶ x17 x4 x10 ⟶ x17 x5 x10 ⟶ x17 x6 x10 ⟶ x17 x7 x10 ⟶ x17 x8 x10 ⟶ x17 x9 x10 ⟶ x17 x3 x11 ⟶ x17 x4 x11 ⟶ x17 x5 x11 ⟶ x17 x6 x11 ⟶ x17 x7 x11 ⟶ x17 x8 x11 ⟶ x17 x9 x11 ⟶ x17 x10 x11 ⟶ x17 x3 x12 ⟶ x17 x4 x12 ⟶ x17 x5 x12 ⟶ x17 x6 x12 ⟶ x17 x7 x12 ⟶ x17 x8 x12 ⟶ x17 x9 x12 ⟶ x17 x10 x12 ⟶ x17 x11 x12 ⟶ x17 x3 x13 ⟶ x17 x4 x13 ⟶ x17 x5 x13 ⟶ x17 x6 x13 ⟶ x17 x7 x13 ⟶ x17 x8 x13 ⟶ x17 x9 x13 ⟶ x17 x10 x13 ⟶ x17 x11 x13 ⟶ x17 x12 x13 ⟶ x17 x3 x14 ⟶ x17 x4 x14 ⟶ x17 x5 x14 ⟶ x17 x6 x14 ⟶ x17 x7 x14 ⟶ x17 x8 x14 ⟶ x17 x9 x14 ⟶ x17 x10 x14 ⟶ x17 x11 x14 ⟶ x17 x12 x14 ⟶ x17 x13 x14 ⟶ x17 x3 x15 ⟶ x17 x4 x15 ⟶ x17 x5 x15 ⟶ x17 x6 x15 ⟶ x17 x7 x15 ⟶ x17 x8 x15 ⟶ x17 x9 x15 ⟶ x17 x10 x15 ⟶ x17 x11 x15 ⟶ x17 x12 x15 ⟶ x17 x13 x15 ⟶ x17 x14 x15 ⟶ x17 x3 x16 ⟶ x17 x4 x16 ⟶ x17 x5 x16 ⟶ x17 x6 x16 ⟶ x17 x7 x16 ⟶ x17 x8 x16 ⟶ x17 x9 x16 ⟶ x17 x10 x16 ⟶ x17 x11 x16 ⟶ x17 x12 x16 ⟶ x17 x13 x16 ⟶ x17 x14 x16 ⟶ x17 x15 x16 ⟶ x2 x17) ⟶ ∀ x17 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x18 : ι → ι → ι . (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x3 = x19) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x4 = x20) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x5 = x21) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x6 = x22) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x7 = x23) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x8 = x24) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x9 = x25) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x10 = x26) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x11 = x27) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x12 = x28) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x13 = x29) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x14 = x30) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x15 = x31) ⟶ (∀ x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 . x18 (x17 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32) x16 = x32) ⟶ ∀ x19 : ο . (∀ x20 : ι → ι → ι . (∀ x21 : ο . (∀ x22 : ι → ι → ι . and (f3993.. x0 x1 x2 x3 x20 x22) (∀ x23 : ο . (∀ x24 . (∀ x25 : ο . (∀ x26 . (∀ x27 : ο . (∀ x28 . (∀ x29 : ο . (∀ x30 . (∀ x31 : ο . (∀ x32 . and (and (and (and (and (and (x0 x24) (x0 x26)) (x0 x28)) (x0 x30)) (x0 x32)) (and (and (and (and (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x22 x3 x30) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x3 x32) x28 (x20 x24 (x22 x3 x28))) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x3 x32) x28 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x22 x3 x30) (x20 x24 (x22 x3 x28)))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 x24 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x28 (x22 x3 x32) x28) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x28 (x22 x3 x32) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 x24 x28))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x20 x24 (x22 x3 x28)) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) x26 x26) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) x26 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x20 x24 (x22 x3 x28)) (x20 x24 (x22 x3 x28)) x26))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x32 (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) (x20 x24 (x22 x3 x28)) (x22 x3 x32)) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 (x22 x24 x26) (x20 x24 (x22 x3 x28)) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x32 (x22 x3 x32)))) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x32) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x30) x26) = 2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x30) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x32 (x22 x3 x32) x26)))) (and (x20 x30 (x20 (x20 (x22 x3 x28) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x26 x28)) x32) = x4) (x20 (x20 x30 (x20 (x22 x3 x28) (2e6fa.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x20 x22 x24 x26 x28))) x32 = x5)) ⟶ x31) ⟶ x31) ⟶ x29) ⟶ x29) ⟶ x27) ⟶ x27) ⟶ x25) ⟶ x25) ⟶ x23) ⟶ x23) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19 (proof)