Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: prim1 x0 (56ded.. 48ef8..).
Let x1 of type ι be given.
Assume H1: prim1 x1 (56ded.. 48ef8..).
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with 48ef8.., x0, prim1 (bc82c.. x0 x1) (56ded.. 48ef8..) leaving 3 subgoals.
The subproof is completed by applying unknownprop_324ce453d59dc0cec2287cf76ff2a387a8fc967ae0f5a05b7a0d78c03b03044e.
The subproof is completed by applying H0.
Assume H2: prim1 (e4431.. x0) 48ef8...
Assume H3: ordinal (e4431.. x0).
Assume H4: 80242.. x0.
Assume H5: 1beb9.. (e4431.. x0) x0.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with 48ef8.., x1, prim1 (bc82c.. x0 x1) (56ded.. 48ef8..) leaving 3 subgoals.
The subproof is completed by applying unknownprop_324ce453d59dc0cec2287cf76ff2a387a8fc967ae0f5a05b7a0d78c03b03044e.
The subproof is completed by applying H1.
Assume H6: prim1 (e4431.. x1) 48ef8...
Assume H7: ordinal (e4431.. x1).
Assume H8: 80242.. x1.
Assume H9: 1beb9.. (e4431.. x1) x1.
Apply unknownprop_5a5c48612170d465714265799d25003db15da4f2d5d05eaf9fa403276d7d9f0a with 48ef8.., bc82c.. x0 x1, e4431.. (bc82c.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying unknownprop_324ce453d59dc0cec2287cf76ff2a387a8fc967ae0f5a05b7a0d78c03b03044e.
Claim L10: ordinal (e4431.. (bc82c.. x0 x1))
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with bc82c.. x0 x1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply ordinal_In_Or_Subq with e4431.. (bc82c.. x0 x1), 48ef8.., prim1 (e4431.. (bc82c.. x0 x1)) 48ef8.. leaving 4 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_324ce453d59dc0cec2287cf76ff2a387a8fc967ae0f5a05b7a0d78c03b03044e.
Assume H11: prim1 (e4431.. (bc82c.. x0 x1)) 48ef8...
The subproof is completed by applying H11.
Assume H11: Subq 48ef8.. (e4431.. (bc82c.. x0 x1)).
Apply In_irref with bc82c.. (e4431.. x0) (e4431.. x1), prim1 (e4431.. (bc82c.. x0 x1)) 48ef8...
Apply unknownprop_a603fab6a3bb62686be57b2e17a4ac9ff228cebdbc1fe59040d5ebbf3fd37549 with x0, x1, bc82c.. (e4431.. x0) (e4431.. x1) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply H11 with bc82c.. (e4431.. x0) (e4431.. x1).
Apply unknownprop_41bcf069d1a354a3112d597edcb9cf73b44b8483bc4b8c2cc4d5df12d42e0ad7 with e4431.. x0, e4431.. x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply unknownprop_90012ae02c7e97888ea4d0a930b01b500b9d0d1d1a0841df69b82a77726b906b with bc82c.. x0 x1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
■