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.
Assume H0: ∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x3 x7 x8 = x5 x7 x8.
Assume H1: ∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 x7 x8 = x6 x7 x8.
Apply iffI with explicit_Field x0 x1 x2 x3 x4, explicit_Field x0 x1 x2 x5 x6 leaving 2 subgoals.
Apply unknownprop_020ff441acf63956db89023138d2e3bf192b2578e8bfb819c9422a66b469b129 with x0, x1, x2, x3, x4, x5, x6 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_020ff441acf63956db89023138d2e3bf192b2578e8bfb819c9422a66b469b129 with x0, x1, x2, x5, x6, x3, x4 leaving 2 subgoals.
Let x7 of type ι be given.
Assume H2: prim1 x7 x0.
Let x8 of type ι be given.
Assume H3: prim1 x8 x0.
Let x9 of type ιιο be given.
Apply H0 with x7, x8, λ x10 x11 . x9 x11 x10 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x7 of type ι be given.
Assume H2: prim1 x7 x0.
Let x8 of type ι be given.
Assume H3: prim1 x8 x0.
Let x9 of type ιιο be given.
Apply H1 with x7, x8, λ x10 x11 . x9 x11 x10 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.