Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Apply unknownprop_9155775841857cb348ae79731186aa077c95466dd39af675bcbf421e2bc4c9da with x0, 80242.. (f4dc0.. x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: and (and (80242.. (f4dc0.. x0)) (∀ x1 . prim1 x1 (23e07.. x0) ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1))) (∀ x1 . prim1 x1 (5246e.. x0) ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0)).
Apply H1 with 02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..) ⟶ 80242.. (f4dc0.. x0).
Assume H2: and (80242.. (f4dc0.. x0)) (∀ x1 . prim1 x1 (23e07.. x0) ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1)).
Apply H2 with (∀ x1 . prim1 x1 (5246e.. x0) ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0)) ⟶ 02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..) ⟶ 80242.. (f4dc0.. x0).
Assume H3: 80242.. (f4dc0.. x0).
Assume H4: ∀ x1 . prim1 x1 (23e07.. x0) ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1).
Assume H5: ∀ x1 . prim1 x1 (5246e.. x0) ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0).
Assume H6: 02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..).
The subproof is completed by applying H3.
■