Proofgold Asset

Definition ChurchNum2 := λ x0 : ι → ι . λ x1 . x0 (x0 x1)
Definition ChurchNum_ii_2 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 x1)
Definition ChurchNum_ii_3 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 x1))
Definition ChurchNum_ii_4 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 x1)))
Definition ChurchNum_ii_5 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 x1))))
Definition ChurchNum_ii_6 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 x1)))))
Definition ChurchNum_ii_7 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 (x0 x1))))))
Definition ChurchNum_ii_8 := λ x0 : (ι → ι) → ι → ι . λ x1 : ι → ι . x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 x1)))))))
Theorem 1b77a.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum2 x0 x2) (proof)
Theorem 7df32.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_2 ChurchNum2 x0 x2) (proof)
Theorem 9ba2f.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_3 ChurchNum2 x0 x2) (proof)
Theorem 8c01a.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_4 ChurchNum2 x0 x2) (proof)
Theorem 80fa6.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_5 ChurchNum2 x0 x2) (proof)
Theorem b8288.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_6 ChurchNum2 x0 x2) (proof)
Theorem 90a58.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_7 ChurchNum2 x0 x2) (proof)
Theorem 7f821.. : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (x0 x2)) ⟶ ∀ x2 x3 . x1 x3 x2 ⟶ x1 x3 (ChurchNum_ii_8 ChurchNum2 x0 x2) (proof)
Theorem a5a30.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum2 x0 x2) (proof)
Theorem 52b00.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_2 ChurchNum2 x0 x2) (proof)
Theorem 078b0.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_3 ChurchNum2 x0 x2) (proof)
Theorem 3ae46.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_4 ChurchNum2 x0 x2) (proof)
Theorem 9821b.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_5 ChurchNum2 x0 x2) (proof)
Theorem f3785.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_6 ChurchNum2 x0 x2) (proof)
Theorem c3586.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_7 ChurchNum2 x0 x2) (proof)
Theorem 29be5.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . (∀ x2 . x1 x2 ⟶ x1 (x0 x2)) ⟶ ∀ x2 . x1 x2 ⟶ x1 (ChurchNum_ii_8 ChurchNum2 x0 x2) (proof)
Theorem 39a30.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum2 x0 x3) = ChurchNum2 x0 (x2 x3) (proof)
Theorem fb78a.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_2 ChurchNum2 x0 x3) = ChurchNum_ii_2 ChurchNum2 x0 (x2 x3) (proof)
Theorem 69b84.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_3 ChurchNum2 x0 x3) = ChurchNum_ii_3 ChurchNum2 x0 (x2 x3) (proof)
Theorem 218e1.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_4 ChurchNum2 x0 x3) = ChurchNum_ii_4 ChurchNum2 x0 (x2 x3) (proof)
Theorem 93d19.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_5 ChurchNum2 x0 x3) = ChurchNum_ii_5 ChurchNum2 x0 (x2 x3) (proof)
Theorem 73d5c.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_6 ChurchNum2 x0 x3) = ChurchNum_ii_6 ChurchNum2 x0 (x2 x3) (proof)
Theorem ff06e.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_7 ChurchNum2 x0 x3) = ChurchNum_ii_7 ChurchNum2 x0 (x2 x3) (proof)
Theorem e3c69.. : ∀ x0 : ι → ι . ∀ x1 : ι → ο . ∀ x2 : ι → ι . (∀ x3 . x1 x3 ⟶ x1 (x0 x3)) ⟶ (∀ x3 . x1 x3 ⟶ x2 (x0 x3) = x0 (x2 x3)) ⟶ ∀ x3 . x1 x3 ⟶ x2 (ChurchNum_ii_8 ChurchNum2 x0 x3) = ChurchNum_ii_8 ChurchNum2 x0 (x2 x3) (proof)
Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known nat_0^nat_0 : nat_p 0
Theorem 5a366.. : nat_p 64 (proof)
Theorem 5eca6.. : nat_p 128 (proof)
Theorem 28496.. : nat_p 256 (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Param mul_nat^mul_nat : ι → ι → ι
Definition exp_nat^exp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem 856b4..^exp_nat_0 : ∀ x0 . exp_nat x0 0 = 1 (proof)
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Theorem caaf4..^exp_nat_S : ∀ x0 x1 . nat_p x1 ⟶ exp_nat x0 (ordsucc x1) = mul_nat x0 (exp_nat x0 x1) (proof)
Theorem e29a8.. : exp_nat 2 0 = 1 (proof)
Param add_nat^add_nat : ι → ι → ι
Known add_nat_1_1_2^{add_nat_1_1_2} : add_nat 1 1 = 2
Known mul_add_nat_distrR^{mul_add_nat_distrR} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat (add_nat x0 x1) x2 = add_nat (mul_nat x0 x2) (mul_nat x1 x2)
Known nat_1^nat_1 : nat_p 1
Known 4f402..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_nat x0 x1)
Known nat_2^nat_2 : nat_p 2
Known f11bb.. : ∀ x0 . nat_p x0 ⟶ mul_nat 1 x0 = x0
Theorem afaae.. : ∀ x0 . nat_p x0 ⟶ exp_nat 2 (ordsucc x0) = add_nat (exp_nat 2 x0) (exp_nat 2 x0) (proof)
Known 3e9f7..^exp_nat_1 : ∀ x0 . exp_nat x0 1 = x0
Theorem 16f52.. : exp_nat 2 1 = 2 (proof)
Known a8f07.. : exp_nat 2 2 = 4
Theorem 5e733.. : exp_nat 2 2 = ChurchNum_ii_2 ChurchNum2 ordsucc 0 (proof)
Known adab1.. : exp_nat 2 3 = 8
Theorem db234.. : exp_nat 2 3 = ChurchNum_ii_3 ChurchNum2 ordsucc 0 (proof)
Known db1de.. : exp_nat 2 4 = 16
Theorem bcc97.. : exp_nat 2 4 = ChurchNum_ii_4 ChurchNum2 ordsucc 0 (proof)
Known e089c.. : exp_nat 2 5 = 32
Theorem 85ed8.. : exp_nat 2 5 = ChurchNum_ii_5 ChurchNum2 ordsucc 0 (proof)
Known nat_5^nat_5 : nat_p 5
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem b3a97.. : exp_nat 2 6 = ChurchNum_ii_6 ChurchNum2 ordsucc 0 (proof)
Theorem 337ce.. : exp_nat 2 6 = 64 (proof)
Known nat_6^nat_6 : nat_p 6
Theorem cc1c2.. : exp_nat 2 7 = ChurchNum_ii_7 ChurchNum2 ordsucc 0 (proof)
Theorem ab619.. : exp_nat 2 7 = 128 (proof)
Known nat_7^nat_7 : nat_p 7
Theorem bbc1b.. : exp_nat 2 8 = ChurchNum_ii_8 ChurchNum2 ordsucc 0 (proof)
Theorem 55cf1.. : exp_nat 2 8 = 256 (proof)