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.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Assume H2: 80242.. x2.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with x0, x1, x2, λ x3 x4 . x4 = bc82c.. x1 (bc82c.. x0 x2) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with x1, x0, x2, λ x3 x4 . bc82c.. (bc82c.. x0 x1) x2 = x4 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
set y3 to be bc82c.. (bc82c.. x0 x1) x2
set y4 to be bc82c.. (bc82c.. x2 x1) y3
Claim L3: ∀ x5 : ι → ο . x5 y4x5 y3
Let x5 of type ιο be given.
Assume H3: x5 (bc82c.. (bc82c.. y3 x2) y4).
set y6 to be λ x6 . x5
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with x2, y3, λ x7 x8 . y6 (bc82c.. x7 y4) (bc82c.. x8 y4) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Let x5 of type ιιο be given.
Apply L3 with λ x6 . x5 x6 y4x5 y4 x6.
Assume H4: x5 y4 y4.
The subproof is completed by applying H4.