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.
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Apply unknownprop_025381747cb997774d510d08999871dcc335b332fa7ba883a4b4899fbfe1e3a2 with bc82c.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying L4.
Let x2 of type ι be given.
Assume H6: prim1 x2 (56ded.. (e4431.. (bc82c.. x0 x1))).
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with e4431.. (bc82c.. x0 x1), x2, 099f3.. x2 (bc82c.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H6.
Assume H7: prim1 (e4431.. x2) (e4431.. (bc82c.. x0 x1)).
Assume H8: ordinal (e4431.. x2).
Assume H9: 80242.. x2.
Assume H10: 1beb9.. (e4431.. x2) x2.
Apply unknownprop_5e27941980fd82e6bd970186ba0607de8244696a96acf12736011288a143d4ba with x2, bc82c.. x0 x1, 099f3.. x2 (bc82c.. x0 x1) leaving 4 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying L4.
Assume H11: or (099f3.. x2 (bc82c.. x0 x1)) (x2 = bc82c.. x0 x1).
Apply H11 with 099f3.. x2 (bc82c.. x0 x1) leaving 2 subgoals.
Assume H12: 099f3.. x2 (bc82c.. x0 x1).
The subproof is completed by applying H12.
Assume H12: x2 = bc82c.. x0 x1.
Apply FalseE with 099f3.. x2 (bc82c.. x0 x1).
Apply In_irref with e4431.. x2.
Apply H12 with λ x3 x4 . prim1 (e4431.. x2) (e4431.. x4).
The subproof is completed by applying H7.
Assume H11: 099f3.. (bc82c.. x0 x1) x2.
Apply FalseE with 099f3.. x2 (bc82c.. x0 x1).
Apply unknownprop_360dad628eb310c4b99b99306a537b749071911afda713bd180f99c61063736f with x0, x1, False leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H12: and (∀ x3 . prim1 x3 (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (bc82c.. x0))) ⟶ 80242.. x3) (∀ x3 . prim1 x3 4a7ef.. ⟶ 80242.. x3).
Apply H12 with (∀ x3 . prim1 x3 (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (bc82c.. x0))) ⟶ ∀ x4 . prim1 x4 4a7ef.. ⟶ 099f3.. x3 x4) ⟶ False.
Assume H13: ∀ x3 . prim1 x3 (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) ⟶ 80242.. x3.
Assume H14: ∀ x3 . prim1 x3 4a7ef.. ⟶ 80242.. x3.
Assume H15: ∀ x3 . prim1 x3 (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (bc82c.. x0))) ⟶ ∀ x4 . prim1 x4 4a7ef.. ⟶ 099f3.. x3 x4.
Apply unknownprop_e277188ae242e07bd6727f267e38747aecd739d129890076e65b92339f7beb98 with 0ac37.. (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (56ded.. x1) (λ x3 . bc82c.. x0 x3)), 4a7ef.., False leaving 2 subgoals.
Apply unknownprop_360dad628eb310c4b99b99306a537b749071911afda713bd180f99c61063736f with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H16: and (and (and (80242.. (02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (56ded.. x1) (bc82c.. x0))) 4a7ef..)) (prim1 (e4431.. ...) ...)) ...) ....
...
■