Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: Field x0.
Apply H0 with ∀ x1 . x1K_field_0 x0 x0∀ x2 . x2K_field_0 x0 x0K_field_1_b x0 x0 x1 x2K_field_0 x0 x0.
Apply unknownprop_e08b2452b1a2fc464ffe03692b94bd4650b3a041709d65cf5d5d9c41083a3cb8 with x0, λ x1 x2 . struct_b_b_e_e x2unpack_b_b_e_e_o x0 (λ x3 . λ x4 x5 : ι → ι → ι . λ x6 x7 . explicit_Field x3 x6 x7 x4 x5)∀ x3 . x3K_field_0 x0 x0∀ x4 . x4K_field_0 x0 x0K_field_1_b x0 x0 x3 x4K_field_0 x0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: struct_b_b_e_e (pack_b_b_e_e (K_field_0 x0 x0) (K_field_1_b x0 x0) (K_field_2_b x0 x0) (K_field_3 x0 x0) (K_field_4 x0 x0)).
Assume H2: unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3).
Apply pack_struct_b_b_e_e_E1 with K_field_0 x0 x0, K_field_1_b x0 x0, K_field_2_b x0 x0, K_field_3 x0 x0, K_field_4 x0 x0.
The subproof is completed by applying H1.