Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ba9d8.. x0.
Apply unknownprop_bebd867283cf8e42ab0a6fcae40b7b03bd53172bba6a0231eb1c5875aaddede9 with x0, x1, prim0 (aa8d2.. (4ae4a.. x0) x1), prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 (prim0 (aa8d2.. x0 x1)) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_90bcc02ecc46b92df3edbe0008c0f8bb530ab6a017204b007fade1bade9af775 with 4ae4a.. x0, x1.
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with x0.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1: (λ x3 . and (prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 x3) (aa8d2.. x0 x1 x3)) x2.
Apply H1 with prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 (prim0 (aa8d2.. x0 x1)).
Assume H2: prim0 (aa8d2.. (4ae4a.. x0) x1) = prim3 x2.
Assume H3: aa8d2.. x0 x1 x2.
Apply H2 with λ x3 x4 . x4 = prim3 (prim0 (aa8d2.. x0 x1)).
Claim L4: prim0 (aa8d2.. x0 x1) = x2
Apply unknownprop_9c1354c1627b000b8714ed09b0e535b241e3434601d3939b6f5f152d11f41e1c with x1, x0, prim0 (aa8d2.. x0 x1), x2 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_90bcc02ecc46b92df3edbe0008c0f8bb530ab6a017204b007fade1bade9af775 with x0, x1.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply L4 with λ x3 x4 . prim3 x2 = prim3 x4.
Let x3 of type ιιο be given.
Assume H5: x3 (prim3 x2) (prim3 x2).
The subproof is completed by applying H5.