Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ba9d8.. x0.
Let x1 of type ι be given.
Assume H1: ba9d8.. x1.
Let x2 of type ι be given.
Assume H2: ba9d8.. x2.
Apply unknownprop_d018bd0ff7e1673bb0aea059ead181f579bde1ee59189802e506bc50bc706f38 with 616bf.. x0 x1, x2, λ x3 x4 . x4 = 616bf.. (14149.. x0 x2) (14149.. x1 x2) leaving 3 subgoals.
Apply unknownprop_6ea59642454c806d36d2cfe931420377c027fcaf6c044cc84fb5291b346de8a0 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_d018bd0ff7e1673bb0aea059ead181f579bde1ee59189802e506bc50bc706f38 with x0, x2, λ x3 x4 . 14149.. x2 (616bf.. x0 x1) = 616bf.. x4 (14149.. x1 x2) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_d018bd0ff7e1673bb0aea059ead181f579bde1ee59189802e506bc50bc706f38 with x1, x2, λ x3 x4 . 14149.. x2 (616bf.. x0 x1) = 616bf.. (14149.. x2 x0) x4 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_f3c9cd006b0ca49dbaea87eee344eae5f575e10742b8882573411ba536c6d868 with x2, x0, x1 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.