Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ο be given.
Let x1 of type ο be given.
Assume H0: not (and x0 x1).
Apply xm with x0, or (not x0) (not x1) leaving 2 subgoals.
Assume H1: x0.
Apply xm with x1, or (not x0) (not x1) leaving 2 subgoals.
Assume H2: x1.
Apply H0 with or (not x0) (not x1).
Apply andI with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Assume H2: not x1.
Apply orIR with not x0, not x1.
The subproof is completed by applying H2.
Assume H1: not x0.
Apply orIL with not x0, not x1.
The subproof is completed by applying H1.
■