scheme :: CIRCCMB2:sch 3
CIRCCMB29sch3{ F₁() -> non empty ManySortedSign , F₂( object , object , object ) -> non empty ManySortedSign , F₃( object , object ) -> object , F₄() -> ManySortedSet of NAT , F₅() -> ManySortedSet of NAT } :

for n being Nat
for x being set st x = F₅() . n holds
F₅() . (n + 1) = F₃(x,n)

provided

A1: F₄() . 0 = F₁() and
A2: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F₄() . n & x = F₅() . n holds
( F₄() . (n + 1) = F₂(S,x,n) & F₅() . (n + 1) = F₃(x,n) )