Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 430d6.. x0.
Apply H0 with λ x1 . x1 = 9f84a.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Assume H1: ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ prim1 (x2 x3 x4) x1.
Let x3 of type ι → ι → ι be given.
Assume H2: ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ prim1 (x3 x4 x5) x1.
Let x4 of type ι → ι → ο be given.
Let x5 of type ι → ο be given.
Apply unknownprop_9cdbbf0280d75590ed17418626d1f22d357a0ce58946a65813e86c8ab25fade8 with x1, x2, x3, x4, x5, λ x6 x7 . 9f84a.. x1 x2 x3 x4 x5 = 9f84a.. x6 (e3162.. (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_2bf737aa06993cd59c6c8744a0ff0eef275f559126ef8d03887b3c6e6e3059e0 with x1, x2, e3162.. (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, decode_p (f482f.. (9f84a.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_d301693eb1fa0da7f271198093e9f6d03844da17df8460c814a3c7e04330e1bd with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_f9ab74e6a825d231a8f13599dca1474efce0a9e0d29b33944ec2c0009892b1c3 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Let x7 of type ι be given.
Assume H4: prim1 x7 x1.
Apply unknownprop_c1ac95df319708a0a9776f296ca0a8170fd3188b34ed6996bb4a1132ca15ce9d with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x4 x6 x7.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Apply unknownprop_820bbb9f006ad1aaef2209a7aabb86b72b74c78c861a4ac2924950cfccbc7e42 with x1, x2, x3, x4, x5, x6, λ x7 x8 : ο . iff (x5 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying iff_refl with x5 x6.
■