Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . In x2 (mul_nat x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x1 ⟶ x2 = add_nat x4 (mul_nat x5 x0) ⟶ (∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x1 ⟶ x2 = add_nat x6 (mul_nat x7 x0) ⟶ and (x6 = x4) (x7 = x5)) ⟶ x3) ⟶ x3

type
prop

theory
HF

name
-

proof
PUZkx..

Megalodon
quot_rem_nat_impred

proofgold address
TMK5A..^{quot_rem_nat_impred}

creator
2364 PrGxv../b1ef6..

owner
2364 PrGxv../b1ef6..

term root
eb163..