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: ordinal x1.
Apply and3I with ∀ x2 . prim1 x2 (0ac37.. (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (56ded.. x1) (λ x3 . bc82c.. x0 x3))) ⟶ 80242.. x2, ∀ x2 . prim1 x2 4a7ef.. ⟶ 80242.. x2, ∀ x2 . prim1 x2 (0ac37.. (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (56ded.. x1) (λ x3 . bc82c.. x0 x3))) ⟶ ∀ x3 . prim1 x3 4a7ef.. ⟶ 099f3.. x2 x3 leaving 3 subgoals.
Let x2 of type ι be given.
Assume H2: prim1 x2 (0ac37.. (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (56ded.. x1) (λ x3 . bc82c.. x0 x3))).
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with 94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1), 94f9e.. (56ded.. x1) (λ x3 . bc82c.. x0 x3), x2, 80242.. x2 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: prim1 x2 (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with 56ded.. x0, λ x3 . bc82c.. x3 x1, x2, 80242.. x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H4: prim1 x3 (56ded.. x0).
Assume H5: x2 = bc82c.. x3 x1.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with x0, x3, 80242.. x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Assume H6: prim1 (e4431.. x3) x0.
Assume H7: ordinal (e4431.. x3).
Assume H8: 80242.. x3.
Assume H9: 1beb9.. (e4431.. x3) x3.
Apply H5 with λ x4 x5 . 80242.. x5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x3, x1 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with x1.
The subproof is completed by applying H1.
Assume H3: prim1 x2 (94f9e.. (56ded.. x1) (λ x3 . bc82c.. x0 x3)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with 56ded.. x1, λ x3 . bc82c.. x0 x3, x2, 80242.. x2 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H4: prim1 x3 (56ded.. x1).
Assume H5: x2 = bc82c.. x0 x3.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with x1, x3, 80242.. x2 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Assume H6: prim1 (e4431.. x3) x1.
Assume H7: ordinal (e4431.. x3).
Assume H8: 80242.. x3.
Assume H9: 1beb9.. (e4431.. x3) x3.
Apply H5 with λ x4 x5 . 80242.. x5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x0, x3 leaving 2 subgoals.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with x0.
The subproof is completed by applying H0.
The subproof is completed by applying H8.
Let x2 of type ι be given.
Assume H2: prim1 x2 4a7ef...
Apply FalseE with 80242.. x2.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x2.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Assume H2: prim1 x2 (0ac37.. (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (56ded.. x1) (λ x3 . bc82c.. x0 x3))).
Let x3 of type ι be given.
Assume H3: prim1 x3 4a7ef...
Apply FalseE with 099f3.. x2 x3.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x3.
The subproof is completed by applying H3.
■