Proofgold Address

Definition 70c47.. := λ x0 . and (nat_p x0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = mul_nat 2 x2) ⟶ x1) ⟶ x1)
Definition 5ad3b.. := nat_primrec 0 (λ x0 x1 . If_i (70c47.. x0) x1 (ordsucc x1))
Definition 79006.. := λ x0 . If_i (70c47.. x0) (5ad3b.. x0) (ordsucc (mul_nat 3 x0))
Definition 1b30d.. := λ x0 . λ x1 : ι → ι . λ x2 . nat_primrec x2 (λ x3 . x1) x0
Conjecture aa000.. : ∀ x0 . nat_p x0 ⟶ not (x0 = 0) ⟶ ∀ x1 : ο . (∀ x2 . and (nat_p x2) (1b30d.. x2 79006.. x0 = 1) ⟶ x1) ⟶ x1