Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Assume H2: 80242.. x2.
Assume H3: 80242.. x3.
Assume H4: fe4bb.. x0 x2.
Assume H5: fe4bb.. x1 x3.
Apply unknownprop_5f01c21b20f5151eb58230694adfaac0cd3dc9203ea975568057400d5e0e5f7a with bc82c.. x0 x1, bc82c.. x2 x1, bc82c.. x2 x3 leaving 5 subgoals.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x2, x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x2, x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_7a8a09f739ce2b80076d5abc4f8aa49cc67deae8353a3a5f1876e1562db9a7cf with x0, x1, x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply unknownprop_785de96e0736c15754c7d7b1a8c7a8a67f701ffa3e6f8320bf2fa437af385e9c with x2, x1, x3 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H5.