Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ο be given.
Apply unknownprop_6419f8fc1ff70ca950cf4e79a0f0cff9b9f9b876ea55c76aec20f2ed9adc5971 with 7eb85.. x0 x1, 0dfb2.. x0 x1, x0, 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1) = x0 leaving 5 subgoals.
Apply unknownprop_f108c6778b2486326f32d399bd20304abef55d1e47d936156e37eb3983681f51 with x0, x1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_b1db2370d04eeb6178d052b730fcb6295924aa036f14aa30a1494605521002e1 with x0, x1.
The subproof is completed by applying unknownprop_4a256b444b1c01564b66b1b28907359637ea99a833a2704a9682d62018db7ca5 with x0, x1.
Assume H1: and (ordinal (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1))) (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1))).
Apply H1 with (∀ x2 . prim1 x2 (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) ⟶ ∀ x3 : ι → ο . not (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x2 x3)) ⟶ 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1) = x0.
Assume H2: ordinal (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H3: 47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H4: ∀ x2 . prim1 x2 (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) ⟶ ∀ x3 : ι → ο . not (47618.. (7eb85.. x0 x1) (0dfb2.. x0 x1) x2 x3).
Apply H3 with 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1) = x0.
Assume H5: cae4c.. (7eb85.. x0 x1) (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Assume H6: bc2b0.. (0dfb2.. x0 x1) (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) (ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1)).
Apply ordinal_trichotomy_or with 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1), x0, 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1) = x0 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Assume H7: or (prim1 (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) x0) (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1) = x0).
Apply H7 with 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1) = x0 leaving 2 subgoals.
Assume H8: prim1 (7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1)) x0.
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with 7b9f3.. (7eb85.. x0 x1) (0dfb2.. x0 x1), x0, ce2d5.. (7eb85.. x0 x1) (0dfb2.. x0 x1), x1, 7b9f3.. (7eb85.. ... ...) ... = ... leaving 4 subgoals.
...
...
...
...
...
...
■