Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Let x1 of type ο be given.
Assume H1: ∀ x2 x3 . 02b90.. x2 x3 ⟶ (∀ x4 . prim1 x4 x2 ⟶ prim1 (e4431.. x4) (e4431.. x0)) ⟶ (∀ x4 . prim1 x4 x3 ⟶ prim1 (e4431.. x4) (e4431.. x0)) ⟶ x0 = 02a50.. x2 x3 ⟶ x1.
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Apply H1 with 1216a.. (56ded.. (e4431.. x0)) (λ x2 . 099f3.. x2 x0), 1216a.. (56ded.. (e4431.. x0)) (λ x2 . 099f3.. x0 x2) leaving 4 subgoals.
Apply and3I with ∀ x2 . prim1 x2 (1216a.. (56ded.. (e4431.. x0)) (λ x3 . 099f3.. x3 x0)) ⟶ 80242.. x2, ∀ x2 . prim1 x2 (1216a.. (56ded.. (e4431.. x0)) (λ x3 . 099f3.. x0 x3)) ⟶ 80242.. x2, ∀ x2 . prim1 x2 (1216a.. (56ded.. (e4431.. x0)) (λ x3 . 099f3.. x3 x0)) ⟶ ∀ x3 . prim1 x3 (1216a.. (56ded.. (e4431.. x0)) (λ x4 . 099f3.. x0 x4)) ⟶ 099f3.. x2 x3 leaving 3 subgoals.
Let x2 of type ι be given.
Assume H6: prim1 x2 (1216a.. (56ded.. (e4431.. x0)) (λ x3 . 099f3.. x3 x0)).
Apply L4 with x2, 80242.. x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: and (80242.. x2) (prim1 (e4431.. x2) (e4431.. x0)).
Assume H8: 099f3.. x2 x0.
Apply H7 with 80242.. x2.
Assume H9: 80242.. x2.
Assume H10: prim1 (e4431.. x2) (e4431.. x0).
The subproof is completed by applying H9.
Let x2 of type ι be given.
Assume H6: prim1 x2 (1216a.. (56ded.. (e4431.. x0)) (λ x3 . 099f3.. x0 x3)).
Apply L5 with x2, 80242.. x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: and (80242.. x2) (prim1 (e4431.. x2) (e4431.. x0)).
Assume H8: 099f3.. x0 x2.
Apply H7 with 80242.. x2.
Assume H9: 80242.. x2.
Assume H10: prim1 (e4431.. x2) (e4431.. x0).
The subproof is completed by applying H9.
Let x2 of type ι be given.
Assume H6: prim1 x2 (1216a.. (56ded.. (e4431.. x0)) (λ x3 . 099f3.. x3 x0)).
Let x3 of type ι be given.
Assume H7: prim1 x3 (1216a.. (56ded.. (e4431.. x0)) (λ x4 . 099f3.. x0 x4)).
Apply L4 with x2, 099f3.. x2 x3 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H8: and (80242.. x2) (prim1 (e4431.. x2) (e4431.. x0)).
Apply H8 with 099f3.. x2 x0 ⟶ 099f3.. x2 x3.
Assume H9: 80242.. x2.
Assume H10: prim1 (e4431.. x2) (e4431.. x0).
Assume H11: 099f3.. x2 x0.
Apply L5 with x3, 099f3.. x2 x3 leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H12: and (80242.. x3) (prim1 (e4431.. x3) (e4431.. x0)).
Apply H12 with 099f3.. x0 x3 ⟶ 099f3.. x2 x3.
Assume H13: 80242.. x3.
Assume H14: prim1 ... ....
...
...
...
...
■