Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι be given.
Assume H1: prim1 x1 (56ded.. x0).
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with x0, x1, prim1 (f4dc0.. x1) (56ded.. x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2: prim1 (e4431.. x1) x0.
Assume H3: ordinal (e4431.. x1).
Assume H4: 80242.. x1.
Assume H5: 1beb9.. (e4431.. x1) x1.
Claim L6: 1beb9.. (e4431.. x1) (f4dc0.. x1)
Apply unknownprop_50863d4afda84f4fc301ce306d29b16ffb69c79e26e9a002d9287d32844846cb with e4431.. x1, x1 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
Apply unknownprop_5a5c48612170d465714265799d25003db15da4f2d5d05eaf9fa403276d7d9f0a with x0, f4dc0.. x1, e4431.. x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying L6.
■