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: 80242.. x1.
Assume H1: 80242.. x2.
Assume H2: 80242.. x3.
Assume H3: 236dc.. x0 x1 = 236dc.. x2 x3.
Let x4 of type ι be given.
Assume H4: prim1 x4 x1.
Claim L5: prim1 ((λ x5 . 15418.. x5 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4) (236dc.. x2 x3)
Apply H3 with λ x5 x6 . prim1 ((λ x7 . 15418.. x7 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4) x5.
Apply unknownprop_e4d6e0bfb4ef6d52ee13edd54a77c8cc7f0a3af8ffb1b8da66d4f98842dd28b5 with x0, 94f9e.. x1 (λ x5 . (λ x6 . 15418.. x6 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5), (λ x5 . 15418.. x5 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with x1, λ x5 . (λ x6 . 15418.. x6 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5, x4.
The subproof is completed by applying H4.
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with x2, 94f9e.. x3 (λ x5 . (λ x6 . 15418.. x6 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5), (λ x5 . 15418.. x5 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4, prim1 x4 x3 leaving 3 subgoals.
The subproof is completed by applying L5.
Assume H6: prim1 ((λ x5 . 15418.. x5 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4) x2.
Apply FalseE with prim1 x4 x3.
Apply unknownprop_4248039866c31bbba3c8ed2d0af8ec07d1aa91eb2387bfc31d9d9cb3da47787a with x2, x4 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
Assume H6: prim1 ((λ x5 . 15418.. x5 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4) (94f9e.. x3 (λ x5 . (λ x6 . 15418.. x6 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5)).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with x3, λ x5 . (λ x6 . 15418.. x6 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5, (λ x5 . 15418.. x5 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4, prim1 x4 x3 leaving 2 subgoals.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H7: prim1 x5 x3.
Assume H8: (λ x6 . 15418.. x6 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 = (λ x6 . 15418.. x6 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5.
Claim L9: x4 = x5
Apply unknownprop_432d0f2d99b37d3ef1618dbe2877026b75805afa8d003221baf0ec35833e28f8 with x1, x3, x4, x5 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
Apply L9 with λ x6 x7 . prim1 x7 x3.
The subproof is completed by applying H7.
■