Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι → ι → ο be given.
Assume H0: ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 (x1 x4) ⟶ iff (x2 x4 x5) (x3 x4 x5).
Apply unknownprop_30ac4ff63aadd043c27cf069c3bf27e9414e186b180e64da8c2794e499eb075b with 38062.. x0 x1 x2, 38062.. x0 x1 x3 leaving 3 subgoals.
The subproof is completed by applying unknownprop_127ccbdbe2b5e92784c84de059cb9a6959d210ccb5f39b5b516a20d9a10c3042 with x0, x1, x2.
The subproof is completed by applying unknownprop_127ccbdbe2b5e92784c84de059cb9a6959d210ccb5f39b5b516a20d9a10c3042 with x0, x1, x3.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply iffI with prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x2), prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x3) leaving 2 subgoals.
Assume H1: prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x2).
Apply unknownprop_0d0b4194fab77127c359e0ea4da0082fbc6cb63a1f3d2bf9d40caed8dc882254 with x0, x1, x2, x4, x5, prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: and (prim1 x4 x0) (prim1 x5 (x1 x4)).
Assume H3: x2 x4 x5.
Apply H2 with prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x3).
Assume H4: prim1 x4 x0.
Assume H5: prim1 x5 (x1 x4).
Apply unknownprop_f0ee0e0da1b09f2dfb62d73da9f7b08ad931aaf047c3bc215bf1dd6e512c41c1 with x0, x1, x3, x4, x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H0 with x4, x5, x3 x4 x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H6: x2 x4 x5 ⟶ x3 x4 x5.
Assume H7: x3 x4 x5 ⟶ x2 x4 x5.
Apply H6.
The subproof is completed by applying H3.
Assume H1: prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x3).
Apply unknownprop_0d0b4194fab77127c359e0ea4da0082fbc6cb63a1f3d2bf9d40caed8dc882254 with x0, x1, x3, x4, x5, prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: and (prim1 x4 x0) (prim1 x5 (x1 x4)).
Assume H3: x3 x4 x5.
Apply H2 with prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (38062.. x0 x1 x2).
Assume H4: prim1 x4 x0.
Assume H5: prim1 x5 (x1 x4).
Apply unknownprop_f0ee0e0da1b09f2dfb62d73da9f7b08ad931aaf047c3bc215bf1dd6e512c41c1 with x0, x1, x2, x4, x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H0 with x4, x5, x2 x4 x5 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H6: x2 x4 x5 ⟶ x3 x4 x5.
Assume H7: x3 x4 x5 ⟶ x2 x4 x5.
...
■