[ "nat_pred ( ↓? )" "nat_pred_succ" * ]
[ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]
[ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" *"nat_tri" ]
}
]
[ { "positive integers" * } {
[ "nat_pred ( ↓? )" "nat_pred_succ" * ]
[ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]
[ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" *"nat_tri" ]
}
]
[ { "positive integers" * } {