Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_a84c26fe1e8eab090e46587a2dce33d43adea76dac76ef9e457538086747ff10 with λ x0 . f4dc0.. (f4dc0.. x0) = x0.
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 02b90.. x0 x1.
Assume H1: ∀ x2 . prim1 x2 x0 ⟶ f4dc0.. (f4dc0.. x2) = x2.
Assume H2: ∀ x2 . prim1 x2 x1 ⟶ f4dc0.. (f4dc0.. x2) = x2.
Apply H0 with f4dc0.. (f4dc0.. (02a50.. x0 x1)) = 02a50.. x0 x1.
Assume H3: and (∀ x2 . prim1 x2 x0 ⟶ 80242.. x2) (∀ x2 . prim1 x2 x1 ⟶ 80242.. x2).
Apply H3 with (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3) ⟶ f4dc0.. (f4dc0.. (02a50.. x0 x1)) = 02a50.. x0 x1.
Assume H4: ∀ x2 . prim1 x2 x0 ⟶ 80242.. x2.
Assume H5: ∀ x2 . prim1 x2 x1 ⟶ 80242.. x2.
Assume H6: ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. (f4dc0.. (f4dc0.. (02a50.. x0 x1))))) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) (f4dc0.. (f4dc0.. (02a50.. x0 x1))))
Apply unknownprop_34fa0f857eadb854ca355983a4ae0231c847f4ec451cfc0522270cf37c3c2aff with x0, x1, f4dc0.. (f4dc0.. (02a50.. x0 x1)) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L9.
Let x2 of type ι be given.
Assume H10: prim1 x2 x0.
Apply H1 with x2, λ x3 x4 . 099f3.. x3 (f4dc0.. (f4dc0.. (02a50.. x0 x1))) leaving 2 subgoals.
The subproof is completed by applying H10.
Claim L11: 80242.. x2
Apply H4 with x2.
The subproof is completed by applying H10.
Claim L12: 80242.. (f4dc0.. x2)
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with x2.
The subproof is completed by applying L11.
Apply unknownprop_3cc82c9758d3882690e6647e4154486613d1a5c615c0651627364410273ab026 with f4dc0.. (02a50.. x0 x1), f4dc0.. x2 leaving 3 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L12.
Apply unknownprop_3cc82c9758d3882690e6647e4154486613d1a5c615c0651627364410273ab026 with x2, 02a50.. x0 x1 leaving 3 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L7.
Apply unknownprop_9d3d7e3a3303096ebb406ebd4ae6c5aff572ffe215624d21fe33216d8b0e1bc7 with x0, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H10.
Let x2 of type ι be given.
Assume H10: prim1 x2 x1.
Apply H2 with x2, λ x3 x4 . ... leaving 2 subgoals.
...
...
Apply L10 with f4dc0.. (f4dc0.. (02a50.. x0 x1)) = 02a50.. x0 x1.
Assume H11: Subq (e4431.. (02a50.. x0 x1)) (e4431.. (f4dc0.. (f4dc0.. (02a50.. x0 x1)))).
Assume H12: SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) (f4dc0.. (f4dc0.. (02a50.. x0 x1))).
Let x2 of type ι → ι → ο be given.
Apply unknownprop_c3102c186c7aa1001a5c1b1b7ecab6b25bcd639e713104221ece8bf414726a69 with 02a50.. x0 x1, f4dc0.. (f4dc0.. (02a50.. x0 x1)), λ x3 x4 . x2 x4 x3 leaving 4 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L9.
Apply set_ext with e4431.. (02a50.. x0 x1), e4431.. (f4dc0.. (f4dc0.. (02a50.. x0 x1))) leaving 2 subgoals.
The subproof is completed by applying H11.
Apply Subq_tra with e4431.. (f4dc0.. (f4dc0.. (02a50.. x0 x1))), e4431.. (f4dc0.. (02a50.. x0 x1)), e4431.. (02a50.. x0 x1) leaving 2 subgoals.
Apply unknownprop_15318642c6583c8aaae77c99bf38263533e68b4d16b9781fdcb393bd0698deae with f4dc0.. (02a50.. x0 x1).
The subproof is completed by applying L8.
Apply unknownprop_15318642c6583c8aaae77c99bf38263533e68b4d16b9781fdcb393bd0698deae with 02a50.. x0 x1.
The subproof is completed by applying L7.
The subproof is completed by applying H12.
■