Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι be given.
Assume H0: ∀ x1 . nat_p (x0 x1).
Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with λ x1 . ∀ x2 : ο . (x1 = 0 ⟶ x2) ⟶ (∀ x3 . In x3 x1 ⟶ (∀ x4 . In x4 x1 ⟶ Subq (x0 x4) (x0 x3)) ⟶ x2) ⟶ x2 leaving 2 subgoals.
Let x1 of type ο be given.
Assume H1: 0 = 0 ⟶ x1.
Assume H2: ∀ x2 . In x2 0 ⟶ (∀ x3 . In x3 0 ⟶ Subq (x0 x3) (x0 x2)) ⟶ x1.
Apply H1.
Let x2 of type ι → ι → ο be given.
Assume H3: x2 0 0.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H1: nat_p x1.
Assume H2: ∀ x2 : ο . (x1 = 0 ⟶ x2) ⟶ (∀ x3 . In x3 x1 ⟶ (∀ x4 . In x4 x1 ⟶ Subq (x0 x4) (x0 x3)) ⟶ x2) ⟶ x2.
Let x2 of type ο be given.
Assume H3: ordsucc x1 = 0 ⟶ x2.
Assume H4: ∀ x3 . In x3 (ordsucc x1) ⟶ (∀ x4 . In x4 (ordsucc x1) ⟶ Subq (x0 x4) (x0 x3)) ⟶ x2.
Apply H2 with x2 leaving 2 subgoals.
Assume H5: x1 = 0.
Claim L6: In 0 (ordsucc x1)
Apply H5 with λ x3 x4 . In 0 (ordsucc x4).
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.
Apply H4 with 0 leaving 2 subgoals.
The subproof is completed by applying L6.
Apply H5 with λ x3 x4 . ∀ x5 . In x5 (ordsucc x4) ⟶ Subq (x0 x5) (x0 0).
Let x3 of type ι be given.
Assume H7: In x3 1.
Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with x3, λ x4 . Subq (x0 x4) (x0 0) leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with x0 0.
Let x3 of type ι be given.
Assume H5: In x3 x1.
Assume H6: ∀ x4 . In x4 x1 ⟶ Subq (x0 x4) (x0 x3).
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ordinal (x0 x1)
...
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with Subq (x0 x3) (x0 x1), Subq (x0 x1) (x0 x3), x2 leaving 3 subgoals.
Apply unknownprop_0f4c846b295f2eb5f79f47ff4ccb007f1db387ecfe4e8f437b57d42e2567ceb0 with x0 x3, x0 x1 leaving 2 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L10.
Assume H11: Subq (x0 x3) (x0 x1).
Apply H4 with x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x1.
Let x4 of type ι be given.
Assume H12: In x4 (ordsucc x1).
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with x1, x4, Subq (x0 x4) (x0 x1) leaving 3 subgoals.
The subproof is completed by applying H12.
Assume H13: In x4 x1.
Apply unknownprop_16d2e0ac4e61f9d6f4710f68fd29bc0751fdb2a43ae4ee41dc39565d6502f8a7 with x0 x4, x0 x3, x0 x1 leaving 2 subgoals.
Apply H6 with x4.
The subproof is completed by applying H13.
The subproof is completed by applying H11.
Assume H13: x4 = x1.
Apply H13 with λ x5 x6 . Subq (x0 x6) (x0 x1).
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with x0 x1.
Assume H11: Subq (x0 x1) (x0 x3).
Apply H4 with x3 leaving 2 subgoals.
Apply unknownprop_9d1f2833af10907d78259d2045ff2d1e1026643f459cca4199c4ae7f89385ba4 with x1, x3.
The subproof is completed by applying H5.
Let x4 of type ι be given.
Assume H12: In x4 (ordsucc x1).
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with x1, x4, Subq (x0 x4) (x0 x3) leaving 3 subgoals.
The subproof is completed by applying H12.
Assume H13: In x4 x1.
Apply H6 with x4.
The subproof is completed by applying H13.
Assume H13: x4 = x1.
Apply H13 with λ x5 x6 . Subq (x0 x6) (x0 x3).
The subproof is completed by applying H11.
■