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: struct_b_u_p (pack_b_u_p x0 x1 x2 x3).
Apply H0 with λ x4 . x4 = pack_b_u_p x0 x1 x2 x3∀ x5 . x5x0∀ x6 . x6x0x1 x5 x6x0 leaving 2 subgoals.
Let x4 of type ι be given.
Let x5 of type ιιι be given.
Assume H1: ∀ x6 . x6x4∀ x7 . x7x4x5 x6 x7x4.
Let x6 of type ιι be given.
Assume H2: ∀ x7 . x7x4x6 x7x4.
Let x7 of type ιο be given.
Assume H3: pack_b_u_p x4 x5 x6 x7 = pack_b_u_p x0 x1 x2 x3.
Apply pack_b_u_p_inj with x4, x0, x5, x1, x6, x2, x7, x3, ∀ x8 . x8x0∀ x9 . x9x0x1 x8 x9x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Assume H4: and (and (x4 = x0) (∀ x8 . x8x4∀ x9 . x9x4x5 x8 x9 = x1 x8 x9)) (∀ x8 . x8x4x6 x8 = x2 x8).
Apply H4 with (∀ x8 . x8x4x7 x8 = x3 x8)∀ x8 . x8x0∀ x9 . x9x0x1 x8 x9x0.
Assume H5: and (x4 = x0) (∀ x8 . x8x4∀ x9 . x9x4x5 x8 x9 = x1 x8 x9).
Apply H5 with (∀ x8 . x8x4x6 x8 = x2 x8)(∀ x8 . x8x4x7 x8 = x3 x8)∀ x8 . x8x0∀ x9 . x9x0x1 x8 x9x0.
Assume H6: x4 = x0.
Assume H7: ∀ x8 . x8x4∀ x9 . x9x4x5 x8 x9 = x1 x8 x9.
Assume H8: ∀ x8 . x8x4x6 x8 = x2 x8.
Assume H9: ∀ x8 . x8x4x7 x8 = x3 x8.
Apply H6 with λ x8 x9 . ∀ x10 . x10x8∀ x11 . x11x8x1 x10 x11x8.
Let x8 of type ι be given.
Assume H10: x8x4.
Let x9 of type ι be given.
Assume H11: x9x4.
Apply H7 with x8, x9, λ x10 x11 . x10x4 leaving 3 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Apply H1 with x8, x9 leaving 2 subgoals.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
Let x4 of type ιιο be given.
Assume H1: x4 (pack_b_u_p x0 x1 x2 x3) (pack_b_u_p x0 x1 x2 x3).
The subproof is completed by applying H1.