Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι be given.
Assume H1: ordinal x1.
Claim L2: ...
...
Claim L3: ...
...
Apply unknownprop_b2d3cb96a6a882d02e5e57dcfc02559b580d1f8621959f82afe70dc68a4b010f with x0, x1, λ x2 x3 . x3 = 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply unknownprop_86c2165c77c44d5e1d081afbaeff7f801039b19e7625930f5477e7454e71d8b9 with x0, λ x2 x3 . 02a50.. (0ac37.. (94f9e.. x3 (λ x4 . bc82c.. x4 x1)) (94f9e.. (23e07.. x1) (λ x4 . bc82c.. x0 x4))) (0ac37.. (94f9e.. (5246e.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (5246e.. x1) (λ x4 . bc82c.. x0 x4))) = 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_86c2165c77c44d5e1d081afbaeff7f801039b19e7625930f5477e7454e71d8b9 with x1, λ x2 x3 . 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. x3 (λ x4 . bc82c.. x0 x4))) (0ac37.. (94f9e.. (5246e.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (5246e.. x1) (λ x4 . bc82c.. x0 x4))) = 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_005438d764083bea1294b44c961d5f19c2cd9cd771adb2fa1c8f63bc715a63a9 with x0, λ x2 x3 . 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) (0ac37.. (94f9e.. x3 (λ x4 . bc82c.. x4 x1)) (94f9e.. (5246e.. x1) (λ x4 . bc82c.. x0 x4))) = 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_005438d764083bea1294b44c961d5f19c2cd9cd771adb2fa1c8f63bc715a63a9 with x1, λ x2 x3 . 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) (0ac37.. (94f9e.. 4a7ef.. (λ x4 . bc82c.. x4 x1)) (94f9e.. x3 (λ x4 . bc82c.. x0 x4))) = 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_cad282ef0fdd0498b9d72e39ef4bede1603c0487cbba81dcc7e691931f33d73a with λ x2 . bc82c.. x2 x1, λ x2 x3 . 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x4 . bc82c.. x4 x1)) (94f9e.. (56ded.. x1) (λ x4 . bc82c.. x0 x4))) (0ac37.. x3 (94f9e.. 4a7ef.. (λ x4 . ...))) = ....
...
■