Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . and (x6 = x1 (x1 x5 (x1 x7 (x1 (x1 (x1 (x1 x6 (x1 (x1 x5 (x1 x5 (x1 (x1 x5 (x1 (x4 x5) (x1 (x1 x7 (x1 x6 (x1 x6 x6))) x5))) (x1 (x4 (x1 (x1 (x4 x7) x5) (x1 x5 x5))) (x1 x6 (x1 x6 (x1 (x1 (x1 x5 (x1 (x1 x5 (x1 (x4 x6) x7)) (x4 (x1 x7 x5)))) x6) (x4 (x1 (x1 x7 (x1 x5 (x1 (x4 (x1 x5 x7)) x5))) (x1 (x1 (x1 x6 (x1 (x4 x5) x6)) x6) (x4 (x4 (x1 (x1 (x1 (x1 x5 (x1 (x1 x6 (x1 (x1 x7 x5) x7)) x6)) x7) (x1 x7 (x1 x5 x5))) x6))))))))))))) (x1 (x1 (x1 (x1 (x1 x6 (x1 x5 x5)) (x4 (x4 (x1 x7 (x4 (x4 (x1 x7 x5))))))) x5) x6) (x1 x6 x7)))) x5) x5) (x4 x6)))) (x1 (x1 (x4 (x1 (x4 (x1 (x1 (x1 (x1 x7 (x1 (x4 (x4 (x1 (x1 x5 x6) x7))) (x4 (x1 x5 x5)))) x5) (x4 x5)) (x1 (x1 (x1 (x1 (x1 x5 x7) (x4 (x4 (x4 x7)))) x7) x6) x5))) (x1 (x1 (x1 x6 x5) (x4 x6)) x6))) x7) x6)) (∃ x8 . x3 (x4 x5)).
Claim L1: and (0 = 0) (∃ x0 . False)
The subproof is completed by applying H0 with λ x0 x1 . False, λ x0 x1 . 0, λ x0 . False, λ x0 . False, λ x0 . 0, 0, 0, 0.
Claim L2: ∃ x0 . False
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with 0 = 0, ∃ x0 . False.
The subproof is completed by applying L1.
Claim L3: (∀ x0 . FalseFalse)False
The subproof is completed by applying L2 with False.
Claim L4: ∀ x0 . FalseFalse
Let x0 of type ι be given.
The subproof is completed by applying FalseE.
Apply L3.
The subproof is completed by applying L4.