Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ο be given.
Claim L0: (λ x1 . or (x1 = 4a7ef..) x0) 4a7ef..
Apply orIL with 4a7ef.. = 4a7ef.., x0.
Let x1 of type ιιο be given.
Assume H0: x1 4a7ef.. 4a7ef...
The subproof is completed by applying H0.
Claim L1: or (prim0 (λ x1 . or (x1 = 4a7ef..) x0) = 4a7ef..) x0
Apply Eps_i_ax with λ x1 . or (x1 = 4a7ef..) x0, 4a7ef...
The subproof is completed by applying L0.
Claim L2: (λ x1 . or (not (x1 = 4a7ef..)) x0) (91630.. 4a7ef..)
Apply orIL with not (91630.. 4a7ef.. = 4a7ef..), x0.
Assume H2: 91630.. 4a7ef.. = 4a7ef...
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with 4a7ef...
Apply H2 with λ x1 x2 . prim1 4a7ef.. x1.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with 4a7ef...
Claim L3: or (not (prim0 (λ x1 . or (not (x1 = 4a7ef..)) x0) = 4a7ef..)) x0
Apply Eps_i_ax with λ x1 . or (not (x1 = 4a7ef..)) x0, 91630.. 4a7ef...
The subproof is completed by applying L2.
Apply L1 with or x0 (not x0) leaving 2 subgoals.
Assume H4: prim0 (λ x1 . or (x1 = 4a7ef..) x0) = 4a7ef...
Apply L3 with or x0 (not x0) leaving 2 subgoals.
Assume H5: not (prim0 (λ x1 . or (not (x1 = 4a7ef..)) x0) = 4a7ef..).
Apply orIR with x0, not x0.
Assume H6: x0.
Claim L7: (λ x1 . or (x1 = 4a7ef..) x0) = λ x1 . or (not (x1 = 4a7ef..)) x0
Apply pred_ext with λ x1 . or (x1 = 4a7ef..) x0, λ x1 . or (not (x1 = 4a7ef..)) x0.
Let x1 of type ι be given.
Apply iffI with (λ x2 . or (x2 = 4a7ef..) x0) x1, (λ x2 . or (not (x2 = 4a7ef..)) x0) x1 leaving 2 subgoals.
Assume H7: (λ x2 . or (x2 = 4a7ef..) x0) x1.
Apply orIR with not (x1 = 4a7ef..), x0.
The subproof is completed by applying H6.
Assume H7: (λ x2 . or (not (x2 = 4a7ef..)) x0) x1.
Apply orIR with x1 = 4a7ef.., x0.
The subproof is completed by applying H6.
Apply H5.
Apply L7 with λ x1 x2 : ι → ο . prim0 x1 = 4a7ef...
The subproof is completed by applying H4.
Assume H5: x0.
Apply orIL with x0, not x0.
The subproof is completed by applying H5.
Assume H4: x0.
Apply orIL with x0, not x0.
The subproof is completed by applying H4.