Proofgold Signed Transaction

vin
PrCit../1d441.. PUddS../11fb4..

vout

PrCit../e1504.. 5.27 bars
TMaSc../96a0f.. ownership of d7b2c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPmy../8db3e.. ownership of cd813.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHfT../36f0e.. ownership of 9ec16.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMwN../38416.. ownership of 14b43.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJ8E../2641b.. ownership of 3ee80.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHnv../db398.. ownership of 64b0a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQ6F../8a002.. ownership of 9da85.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaZ9../95e72.. ownership of 3eb01.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZxr../d5dd2.. ownership of a4364.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdqU../c4b9f.. ownership of f65b9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEpu../238f2.. ownership of f0252.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUwS../f79cb.. ownership of 1eec9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMP22../0e0a8.. ownership of e4fb5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQvg../9bb07.. ownership of f394f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbVz../d2c09.. ownership of 2d7ca.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPAo../0234e.. ownership of d993a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVFD../b50e0.. ownership of fc764.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTqS../39abb.. ownership of d8316.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYCh../c65df.. ownership of 9522d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXQZ../dc486.. ownership of 0cac1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcCX../aaf85.. ownership of e6799.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJf9../5fa28.. ownership of 0abee.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRrC../a3056.. ownership of 15af9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXzc../c85df.. ownership of b5a5d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZMs../aa79b.. ownership of 05672.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKgM../eae53.. ownership of 9f645.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYun../c8e3b.. ownership of df5ed.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQR5../fb67f.. ownership of 1a4e0.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZ5r../a4a97.. ownership of fd0d9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFn4../b65e1.. ownership of 5787a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTef../c9afe.. ownership of d2f24.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcVS../7fce3.. ownership of 0f4c8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbnC../86d4b.. ownership of bb94c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKeT../8fafb.. ownership of 235e5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQPu../15496.. ownership of 469db.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcab../3b334.. ownership of c7d0f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVg5../791b3.. ownership of 8f227.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTwd../63f33.. ownership of d89f2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXxk../6afa2.. ownership of 43f74.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXYF../97a93.. ownership of e96e9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKVg../8a7e5.. ownership of 3cb84.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcfh../4dc2a.. ownership of 2fff7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMY7w../125aa.. ownership of 30da6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJom../566c9.. ownership of 3f854.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRk8../b07a3.. ownership of 610bf.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbCq../cc2f5.. ownership of c5dd5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMY9F../0f020.. ownership of 4c607.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYoM../1e11e.. ownership of 03d05.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZgR../3701a.. ownership of daa33.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNUb../75b6f.. ownership of c873e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVJU../f8417.. ownership of e8a0a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPTc../2367a.. ownership of 7349b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMb25../d4a84.. ownership of 2669c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVGC../fc1cf.. ownership of 07ad2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEtA../952dc.. ownership of d9e2e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEsX../d9069.. ownership of fac4b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMUQ../0fedc.. ownership of 86c65.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGXu../a3579.. ownership of b6349.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMG33../eb5f7.. ownership of 39d66.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZex../6c462.. ownership of 566d9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHhk../b6a00.. ownership of c0023.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbvL../b2e3c.. ownership of 303bf.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGo3../0746e.. ownership of b26f0.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMSsj../32fab.. ownership of bf1bd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZno../f3d62.. ownership of 3f720.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRYB../970a9.. ownership of 683b3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaXP../07415.. ownership of 43047.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEi4../7f2c6.. ownership of 0fd89.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFdG../e3f0e.. ownership of f647d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRXQ../cd960.. ownership of cd2e8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZUv../6f86b.. ownership of b017b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNfv../59d59.. ownership of 5736f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWEh../2acf2.. ownership of 4e557.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVBC../fae32.. ownership of 44091.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbY3../57428.. ownership of bb726.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMP9z../90697.. ownership of 0b224.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMK6Q../27844.. ownership of 4b7da.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNKz../74a6e.. ownership of 3392c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMceq../891c2.. ownership of 43d3d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMEqV../d06c8.. ownership of 2169d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGLx../c486c.. ownership of d9243.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRZQ../c1db2.. ownership of 7e53a.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJAN../4c59a.. ownership of 466b2.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQQR../9e08a.. ownership of b69ae.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMX8../a89de.. ownership of 7c98b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMcxh../a513f.. ownership of c82ad.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXNi../437b1.. ownership of f6fb6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHRw../9c4f6.. ownership of 6f757.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMa38../1e060.. ownership of b848e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYJh../349d6.. ownership of e8e6d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLYc../570c7.. ownership of 1bf92.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWxr../8b76d.. ownership of ed572.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWj7../60ec7.. ownership of 0a45b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVBD../12925.. ownership of 12724.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMaf../38214.. ownership of 66b3d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZrJ../c0935.. ownership of 10e8d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXap../ff5df.. ownership of 66cf5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNsc../305d7.. ownership of b9e6d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaGg../8f229.. ownership of 68754.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMVCK../c83a2.. ownership of 244f9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWb3../c1019.. ownership of 5d5e3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMaXT../56974.. ownership of d88f1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWMA../731e1.. ownership of c9952.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdjW../a8b55.. ownership of d5dbe.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPbi../f8dc1.. ownership of a1f0d.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLT1../95a05.. ownership of 0f550.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMN9w../43546.. ownership of 9d632.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKoV../9b0aa.. ownership of 110ad.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMRhC../56841.. ownership of 4613e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMdBF../0ffb2.. ownership of 97e3f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMa7Q../f1757.. ownership of 83d4c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZXJ../4ad93.. ownership of 9492e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPQa../1524d.. ownership of 335fd.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNiB../ab8f2.. ownership of f8517.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZTu../75a6a.. ownership of 5252e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKB3../9fa99.. ownership of 77fce.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHXb../eeee0.. ownership of 65f9c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMPfw../f346f.. ownership of 8f006.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUSRF../44d01.. doc published by Pr4zB..

Definition ChurchNum_p := λ x0 : (ι → ι) → ι → ι . ∀ x1 : ((ι → ι) → ι → ι) → ο . x1 (λ x2 : ι → ι . λ x3 . x3) ⟶ (∀ x2 : (ι → ι) → ι → ι . x1 x2 ⟶ x1 (λ x3 : ι → ι . λ x4 . x3 (x2 x3 x4))) ⟶ x1 x0
Theorem 5252e.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x1) (proof)
Theorem 335fd.. : ∀ x0 : (ι → ι) → ι → ι . ChurchNum_p x0 ⟶ ChurchNum_p (λ x1 : ι → ι . λ x2 . x1 (x0 x1 x2)) (proof)
Theorem 83d4c.. : ChurchNum_p (λ x0 : ι → ι . x0) (proof)
Theorem 4613e.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 x1)) (proof)
Theorem 9d632.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 x1))) (proof)
Theorem a1f0d.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 x1)))) (proof)
Theorem c9952.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 x1))))) (proof)
Theorem 5d5e3.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 x1)))))) (proof)
Theorem 68754.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))) (proof)
Theorem 66cf5.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))) (proof)
Theorem 66b3d.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))) (proof)
Theorem 0a45b.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))) (proof)
Theorem 1bf92.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))) (proof)
Theorem b848e.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))) (proof)
Theorem f6fb6.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))))) (proof)
Theorem 7c98b.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))) (proof)
Theorem 466b2.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))))))) (proof)
Theorem d9243.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))) (proof)
Theorem 43d3d.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))))))))) (proof)
Theorem 4b7da.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))) (proof)
Theorem bb726.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))))))))))) (proof)
Theorem 4e557.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))) (proof)
Theorem b017b.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))))))))))))) (proof)
Theorem f647d.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))))) (proof)
Theorem 43047.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))))))))))))))))))) (proof)
Theorem 3f720.. : ChurchNum_p (λ x0 : ι → ι . λ x1 . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))))))))))))))))))) (proof)
Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Known nat_0^nat_0 : nat_p 0
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem b26f0.. : ∀ x0 : (ι → ι) → ι → ι . ChurchNum_p x0 ⟶ nat_p (x0 ordsucc 0) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem c0023.. : ∀ x0 : ((ι → ι) → ι → ι) → ο . x0 (λ x1 : ι → ι . λ x2 . x2) ⟶ (∀ x1 : (ι → ι) → ι → ι . ChurchNum_p x1 ⟶ x0 x1 ⟶ x0 (λ x2 : ι → ι . λ x3 . x2 (x1 x2 x3))) ⟶ ∀ x1 : (ι → ι) → ι → ι . ChurchNum_p x1 ⟶ x0 x1 (proof)
Param add_nat^add_nat : ι → ι → ι
Known add_nat_0L^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0
Known add_nat_SL^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Theorem 39d66.. : ∀ x0 : (ι → ι) → ι → ι . ChurchNum_p x0 ⟶ ∀ x1 : (ι → ι) → ι → ι . ChurchNum_p x1 ⟶ x0 ordsucc (x1 ordsucc 0) = add_nat (x0 ordsucc 0) (x1 ordsucc 0) (proof)
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Theorem 86c65.. : nat_p u18 (proof)
Definition u19 := ordsucc u18
Theorem d9e2e.. : nat_p u19 (proof)
Definition u20 := ordsucc u19
Theorem 2669c.. : nat_p u20 (proof)
Definition u21 := ordsucc u20
Theorem e8a0a.. : nat_p u21 (proof)
Definition u22 := ordsucc u21
Theorem daa33.. : nat_p u22 (proof)
Definition u23 := ordsucc u22
Theorem b73b8.. : nat_p u23 (proof)
Definition u24 := ordsucc u23
Theorem 73189.. : nat_p u24 (proof)
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Theorem 4c607.. : 0 ∈ u24 (proof)
Known d8085.. : ∀ x0 x1 . nat_p x1 ⟶ x0 ∈ ordsucc (add_nat x0 x1)
Theorem 610bf.. : u1 ∈ u24 (proof)
Theorem 30da6.. : u2 ∈ u24 (proof)
Theorem 3cb84.. : u3 ∈ u24 (proof)
Theorem 43f74.. : u4 ∈ u24 (proof)
Theorem 8f227.. : u5 ∈ u24 (proof)
Known nat_17^nat_17 : nat_p 17
Theorem 469db.. : u6 ∈ u24 (proof)
Known nat_16^nat_16 : nat_p 16
Theorem bb94c.. : u7 ∈ u24 (proof)
Known nat_15^nat_15 : nat_p 15
Theorem d2f24.. : u8 ∈ u24 (proof)
Known nat_14^nat_14 : nat_p 14
Theorem fd0d9.. : u9 ∈ u24 (proof)
Known nat_13^nat_13 : nat_p 13
Theorem df5ed.. : u10 ∈ u24 (proof)
Known nat_12^nat_12 : nat_p 12
Theorem 05672.. : u11 ∈ u24 (proof)
Known nat_11^nat_11 : nat_p 11
Theorem 15af9.. : u12 ∈ u24 (proof)
Known nat_10^nat_10 : nat_p 10
Theorem e6799.. : u13 ∈ u24 (proof)
Known nat_9^nat_9 : nat_p 9
Theorem 9522d.. : u14 ∈ u24 (proof)
Known nat_8^nat_8 : nat_p 8
Theorem fc764.. : u15 ∈ u24 (proof)
Known nat_7^nat_7 : nat_p 7
Theorem 2d7ca.. : u16 ∈ u24 (proof)
Known nat_6^nat_6 : nat_p 6
Theorem e4fb5.. : u17 ∈ u24 (proof)
Known nat_5^nat_5 : nat_p 5
Theorem f0252.. : u18 ∈ u24 (proof)
Known nat_4^nat_4 : nat_p 4
Theorem a4364.. : u19 ∈ u24 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem 9da85.. : u20 ∈ u24 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem 3ee80.. : u21 ∈ u24 (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 9ec16.. : u22 ∈ u24 (proof)
Theorem d7b2c.. : u23 ∈ u24 (proof)