Proofgold Address

Param f482f.. : ι → ι → ι
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Known 03651.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 7d2e2.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) 4a7ef.. = x0 (proof)
Known ff451.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known 5c667.. : 4ae4a.. 4a7ef.. = 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem 504a8.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. 4a7ef..) = x1 (proof)
Known a7963.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known 3a2b6.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known f9d2f.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem fb20c.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known 9044c.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known 57b7e.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known daead.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 0c325.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Theorem 431f3.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Known 3b34e.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known 37f0a.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known d1b49.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 05e02.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known 2f510.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0
Theorem ffdcd.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x4 (proof)
Known 652a2.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem d842e.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) 4a7ef.. = x0 (proof)
Known 71fcb.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem df2aa.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. 4a7ef..) = x1 (proof)
Known 7f899.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 3956e.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known d88ba.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem c9d91.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Known 15e7b.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem e2ad4.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x4 (proof)
Known 98e34.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Known 3dae7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known a82a2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 7fa57.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known 67cbd.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0
Known e25a7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0
Theorem 7039d.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x5 (proof)
Known b9890.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 9619e.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) 4a7ef.. = x0 (proof)
Known 102c8.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 31081.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. 4a7ef..) = x1 (proof)
Known 28cca.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 3daa5.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known 57aad.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem bb257.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Known ea5d5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 85552.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x4 (proof)
Known 1ceed.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 33c62.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x5 (proof)
Known 57cc6.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Known cdcd4.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 31e4d.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 5ccd2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known 7357c.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0
Known d13e3.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0
Known 2d896.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0
Theorem 7a7b6.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x6 (proof)