Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Apply unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with 1216a.. (4ae4a.. (e4431.. x0)) (λ x1 . (λ x2 . or (prim1 x2 x0) (x2 = e4431.. x0)) x1), a4c2a.. (4ae4a.. (e4431.. x0)) (λ x1 . not ((λ x2 . or (prim1 x2 x0) (x2 = e4431.. x0)) x1)) (λ x1 . (λ x2 . 15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1), e4431.. x0.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with 4ae4a.. (e4431.. x0), λ x1 . (λ x2 . or (prim1 x2 x0) (x2 = e4431.. x0)) x1, e4431.. x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with e4431.. x0.
Apply orIR with prim1 (e4431.. x0) x0, e4431.. x0 = e4431.. x0.
Let x1 of type ιιο be given.
Assume H1: x1 (e4431.. x0) (e4431.. x0).
The subproof is completed by applying H1.