Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply unknownprop_1fe1f9b87156c35e13519655d4a61e2c6dea7ba3e9716ca13f2c1f009fc9c17d with x0, λ x1 x2 . or (and (x1 = 4a7ef..) (x2 = x0)) (∃ x3 x4 . and (and (x1 = 4ae4a.. x3) (x2 = prim3 x4)) (aa8d2.. x3 x0 x4)) leaving 2 subgoals.
Apply orIL with and (4a7ef.. = 4a7ef..) (x0 = x0), ∃ x1 x2 . and (and (4a7ef.. = 4ae4a.. x1) (x0 = prim3 x2)) (aa8d2.. x1 x0 x2).
Apply andI with 4a7ef.. = 4a7ef.., x0 = x0 leaving 2 subgoals.
Let x1 of type ιιο be given.
Assume H0: x1 4a7ef.. 4a7ef...
The subproof is completed by applying H0.
Let x1 of type ιιο be given.
Assume H0: x1 x0 x0.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H0: ba9d8.. x1.
Let x2 of type ι be given.
Assume H1: aa8d2.. x1 x0 x2.
Assume H2: (λ x3 x4 . or (and (x3 = 4a7ef..) (x4 = x0)) (∃ x5 x6 . and (and (x3 = 4ae4a.. x5) (x4 = prim3 x6)) (aa8d2.. x5 x0 x6))) x1 x2.
Apply orIR with and (4ae4a.. x1 = 4a7ef..) (prim3 x2 = x0), ∃ x3 x4 . and (and (4ae4a.. x1 = 4ae4a.. x3) (prim3 x2 = prim3 x4)) (aa8d2.. x3 x0 x4).
Let x3 of type ο be given.
Assume H3: ∀ x4 . (∃ x5 . and (and (4ae4a.. x1 = 4ae4a.. x4) (prim3 x2 = prim3 x5)) (aa8d2.. x4 x0 x5))x3.
Apply H3 with x1.
Let x4 of type ο be given.
Assume H4: ∀ x5 . and (and (4ae4a.. x1 = 4ae4a.. x1) (prim3 x2 = prim3 x5)) (aa8d2.. x1 x0 x5)x4.
Apply H4 with x2.
Apply and3I with 4ae4a.. x1 = 4ae4a.. x1, prim3 x2 = prim3 x2, aa8d2.. x1 x0 x2 leaving 3 subgoals.
Let x5 of type ιιο be given.
Assume H5: x5 (4ae4a.. x1) (4ae4a.. x1).
The subproof is completed by applying H5.
Let x5 of type ιιο be given.
Assume H5: x5 (prim3 x2) (prim3 x2).
The subproof is completed by applying H5.
The subproof is completed by applying H1.