scheme :: CIRCCMB2:sch 2
CIRCCMB29sch2{ F₁( object , object , object ) -> non empty ManySortedSign , F₂( object , object ) -> object , P₁[ object , object , object ], F₃() -> ManySortedSet of NAT , F₄() -> ManySortedSet of NAT } :

for n being Nat ex S being non empty ManySortedSign st
( S = F₃() . n & P₁[S,F₄() . n,n] )

provided

A1: ex S being non empty ManySortedSign ex x being set st
( S = F₃() . 0 & x = F₄() . 0 & P₁[S,x, 0 ] ) 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) ) and
A3: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F₃() . n & x = F₄() . n & P₁[S,x,n] holds
P₁[F₁(S,x,n),F₂(x,n),n + 1]