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: 80242.. x1.
Assume H2: prim1 (e4431.. x1) x0.
Claim L3: 80242.. x0
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with x0.
The subproof is completed by applying H0.
Claim L4: e4431.. x0 = x0
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with x0.
The subproof is completed by applying H0.
Apply unknownprop_5e27941980fd82e6bd970186ba0607de8244696a96acf12736011288a143d4ba with x1, x0, 099f3.. x1 x0 leaving 4 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with x0.
The subproof is completed by applying H0.
Assume H5: or (099f3.. x1 x0) (x1 = x0).
Apply H5 with 099f3.. x1 x0 leaving 2 subgoals.
Assume H6: 099f3.. x1 x0.
The subproof is completed by applying H6.
Assume H6: x1 = x0.
Apply FalseE with 099f3.. x1 x0.
Apply In_irref with x0.
Apply L4 with λ x2 x3 . prim1 x2 x0.
Apply H6 with λ x2 x3 . prim1 (e4431.. x2) x0.
The subproof is completed by applying H2.
Assume H5: 099f3.. x0 x1.
Apply FalseE with 099f3.. x1 x0.
Apply unknownprop_334a5a4dfd5441f12538cd3c70458238b05308c372afbd4cf94b09dd8e7afe85 with x0, x1, False leaving 6 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Let x2 of type ι be given.
Apply L4 with λ x3 x4 . 80242.. x2prim1 (e4431.. x2) (d3786.. x4 (e4431.. x1))SNoEq_ (e4431.. x2) x2 x0SNoEq_ (e4431.. x2) x2 x1099f3.. x0 x2099f3.. x2 x1nIn (e4431.. x2) x0prim1 (e4431.. x2) x1False.
Assume H6: 80242.. x2.
Assume H7: prim1 (e4431.. x2) (d3786.. x0 (e4431.. x1)).
Assume H8: SNoEq_ (e4431.. x2) x2 x0.
Assume H9: SNoEq_ (e4431.. x2) x2 x1.
Assume H10: 099f3.. x0 x2.
Assume H11: 099f3.. x2 x1.
Assume H12: nIn (e4431.. x2) x0.
Apply FalseE with prim1 (e4431.. x2) x1False.
Apply H12.
Apply unknownprop_badc5b9f63c74f1108fd64d39c5dff780b186073e78615613501a542df505687 with x0, e4431.. x1, e4431.. x2.
The subproof is completed by applying H7.
Apply L4 with λ x2 x3 . prim1 x3 (e4431.. x1)SNoEq_ x3 x0 x1prim1 x3 x1False.
Assume H6: prim1 x0 (e4431.. x1).
Apply FalseE with SNoEq_ x0 x0 x1prim1 x0 x1False.
Apply unknownprop_f1a526a64fd91875cd825eea7f2e7776b7f0e7be5dcee74dc03af1d7886d1eb6 with x0, e4431.. x1 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H2.
Apply L4 with λ x2 x3 . prim1 (e4431.. x1) x3SNoEq_ (e4431.. x1) x0 x1nIn (e4431.. x1) x0False.
Assume H6: prim1 (e4431.. x1) x0.
Assume H7: SNoEq_ (e4431.. x1) x0 x1.
Assume H8: nIn (e4431.. x1) x0.
Apply H8.
The subproof is completed by applying H6.