Proofgold Address

Param ordsucc^ordsucc : ι → ι
Param nat_p^nat_p : ι → ο
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Known nat_10^nat_10 : nat_p 10
Theorem 3ed90.. : 0 ∈ 11 (proof)
Known nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known d4e95.. : 0 ∈ 10
Theorem c92a5.. : 1 ∈ 11 (proof)
Known b7a5e.. : 1 ∈ 10
Theorem f5815.. : 2 ∈ 11 (proof)
Known 3c603.. : 2 ∈ 10
Theorem 157cb.. : 3 ∈ 11 (proof)
Known 01826.. : 3 ∈ 10
Theorem 52414.. : 4 ∈ 11 (proof)
Known 35ffd.. : 4 ∈ 10
Theorem 4f9f7.. : 5 ∈ 11 (proof)
Known a1b2a.. : 5 ∈ 10
Theorem db527.. : 6 ∈ 11 (proof)
Known 1beb5.. : 6 ∈ 10
Theorem 45b9a.. : 7 ∈ 11 (proof)
Known 16542.. : 7 ∈ 10
Theorem 15f81.. : 8 ∈ 11 (proof)
Known 56b84.. : 8 ∈ 10
Theorem 2c8c5.. : 9 ∈ 11 (proof)
Known fa1e6.. : 9 ∈ 10
Theorem 9be62.. : 10 ∈ 11 (proof)
Known nat_11^nat_11 : nat_p 11
Theorem 46814.. : 0 ∈ 12 (proof)
Theorem 2b77d.. : 1 ∈ 12 (proof)
Theorem 7c2ac.. : 2 ∈ 12 (proof)
Theorem 2f583.. : 3 ∈ 12 (proof)
Theorem e4fc0.. : 4 ∈ 12 (proof)
Theorem 04716.. : 5 ∈ 12 (proof)
Theorem fbe39.. : 6 ∈ 12 (proof)
Theorem 35d73.. : 7 ∈ 12 (proof)
Theorem 5196c.. : 8 ∈ 12 (proof)
Theorem 4fa36.. : 9 ∈ 12 (proof)
Theorem 42552.. : 10 ∈ 12 (proof)
Theorem fee2e.. : 11 ∈ 12 (proof)
Known nat_12^nat_12 : nat_p 12
Theorem cc8e9.. : 0 ∈ 13 (proof)
Theorem ab386.. : 1 ∈ 13 (proof)
Theorem a582b.. : 2 ∈ 13 (proof)
Theorem c03b3.. : 3 ∈ 13 (proof)
Theorem 39abb.. : 4 ∈ 13 (proof)
Theorem 88508.. : 5 ∈ 13 (proof)
Theorem 827a1.. : 6 ∈ 13 (proof)
Theorem 4039c.. : 7 ∈ 13 (proof)
Theorem 17545.. : 8 ∈ 13 (proof)
Theorem e5d7b.. : 9 ∈ 13 (proof)
Theorem 74a33.. : 10 ∈ 13 (proof)
Theorem 925e4.. : 11 ∈ 13 (proof)
Theorem f6a92.. : 12 ∈ 13 (proof)