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.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with binunion x0 (binunion x1 x2), binunion (binunion x0 x1) x2 leaving 2 subgoals.
Let x3 of type ι be given.
Assume H0: In x3 (binunion x0 (binunion x1 x2)).
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with x0, binunion x1 x2, x3, In x3 (binunion (binunion x0 x1) x2) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: In x3 x0.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with binunion x0 x1, x2, x3.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with x0, x1, x3.
The subproof is completed by applying H1.
Assume H1: In x3 (binunion x1 x2).
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with x1, x2, x3, In x3 (binunion (binunion x0 x1) x2) leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2: In x3 x1.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with binunion x0 x1, x2, x3.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with x0, x1, x3.
The subproof is completed by applying H2.
Assume H2: In x3 x2.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with binunion x0 x1, x2, x3.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H0: In x3 (binunion (binunion x0 x1) x2).
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with binunion x0 x1, x2, x3, In x3 (binunion x0 (binunion x1 x2)) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: In x3 (binunion x0 x1).
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with x0, x1, x3, In x3 (binunion x0 (binunion x1 x2)) leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2: In x3 x0.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with x0, binunion x1 x2, x3.
The subproof is completed by applying H2.
Assume H2: In x3 x1.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with x0, binunion x1 x2, x3.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with x1, x2, x3.
The subproof is completed by applying H2.
Assume H1: In x3 x2.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with x0, binunion x1 x2, x3.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with x1, x2, x3.
The subproof is completed by applying H1.
■