:: deftheorem Def13 defines AckermannSequence ACKERMAN:def 13 :
for b₁ being Function-yielding primitive-recursive satisfying_primrec_conditions 1 -ary ManySortedSet of NAT holds
( b₁ = AckermannSequence iff ( b₁ . 0 = 1 succ 1 & ( for m being Nat holds b₁ . (m + 1) = primrec ((0 const (Ackermann (m,1))),((b₁ . m) * <:<*(2 proj 2)*>:>),1) ) ) );