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_r_r_e x0 x2 x4 x6 = pack_r_r_e x1 x3 x5 x7.
Claim L1: x1 = ap (pack_r_r_e x0 x2 x4 x6) 0
Apply pack_r_r_e_0_eq with pack_r_r_e 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_r_r_e_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, x6 = x7 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_r_r_e_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_r (ap x11 1) x8 x9 = x3 x8 x9.
Let x10 of type οοο be given.
Apply pack_r_r_e_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_r_r_e_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_r_r_e_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.
Apply pack_r_r_e_3_eq2 with x0, x2, x4, x6, λ x8 x9 . x9 = x7.
Apply H0 with λ x8 x9 . ap x9 3 = x7.
Let x8 of type ιιο be given.
The subproof is completed by applying pack_r_r_e_3_eq2 with x1, x3, x5, x7, λ x9 x10 . x8 x10 x9.