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.
Let x4 of type ιιο be given.
Let x5 of type ιιο be given.
Let x6 of type ιο be given.
Let x7 of type ιο be given.
Assume H0: pack_b_r_p x0 x2 x4 x6 = pack_b_r_p x1 x3 x5 x7.
Claim L1: x1 = ap (pack_b_r_p x0 x2 x4 x6) 0
Apply pack_b_r_p_0_eq with pack_b_r_p x0 x2 x4 x6, x1, x3, x5, x7.
The subproof is completed by applying H0.
Claim L2: x0 = x1
Apply L1 with λ x8 x9 . x0 = x9.
The subproof is completed by applying pack_b_r_p_0_eq2 with x0, x2, x4, x6.
Apply and4I with x0 = x1, ∀ x8 . x8x0∀ x9 . x9x0x2 x8 x9 = x3 x8 x9, ∀ x8 . x8x0∀ x9 . x9x0x4 x8 x9 = x5 x8 x9, ∀ x8 . x8x0x6 x8 = x7 x8 leaving 4 subgoals.
The subproof is completed by applying L2.
Let x8 of type ι be given.
Assume H3: x8x0.
Let x9 of type ι be given.
Assume H4: x9x0.
Apply pack_b_r_p_1_eq2 with x0, x2, x4, x6, x8, x9, λ x10 x11 . x11 = x3 x8 x9 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Claim L5: x8x1
Apply L2 with λ x10 x11 . x8x10.
The subproof is completed by applying H3.
Claim L6: x9x1
Apply L2 with λ x10 x11 . x9x10.
The subproof is completed by applying H4.
Apply H0 with λ x10 x11 . decode_b (ap x11 1) x8 x9 = x3 x8 x9.
Let x10 of type ιιο be given.
Apply pack_b_r_p_1_eq2 with x1, x3, x5, x7, x8, x9, λ x11 x12 . x10 x12 x11 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
Let x8 of type ι be given.
Assume H3: x8x0.
Let x9 of type ι be given.
Assume H4: x9x0.
Apply pack_b_r_p_2_eq2 with x0, x2, x4, x6, x8, x9, λ x10 x11 : ο . x11 = x5 x8 x9 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Claim L5: x8x1
Apply L2 with λ x10 x11 . x8x10.
The subproof is completed by applying H3.
Claim L6: x9x1
Apply L2 with λ x10 x11 . x9x10.
The subproof is completed by applying H4.
Apply H0 with λ x10 x11 . decode_r (ap x11 2) x8 x9 = x5 x8 x9.
Let x10 of type οοο be given.
Apply pack_b_r_p_2_eq2 with x1, x3, x5, x7, x8, x9, λ x11 x12 : ο . x10 x12 x11 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying L6.
Let x8 of type ι be given.
Assume H3: x8x0.
Apply pack_b_r_p_3_eq2 with x0, x2, x4, x6, x8, λ x9 x10 : ο . x10 = x7 x8 leaving 2 subgoals.
The subproof is completed by applying H3.
Claim L4: x8x1
Apply L2 with λ x9 x10 . x8x9.
The subproof is completed by applying H3.
Apply H0 with λ x9 x10 . decode_p (ap x10 3) x8 = x7 x8.
Let x9 of type οοο be given.
Apply pack_b_r_p_3_eq2 with x1, x3, x5, x7, x8, λ x10 x11 : ο . x9 x11 x10.
The subproof is completed by applying L4.