scheme :: CIRCCMB2:sch 13
CIRCCMB29sch13{ F₁( set , set , set ) -> non empty ManySortedSign , F₂( object , object , object , object ) -> object , F₃( object , object ) -> object , P₁[ object , object , object , object ], F₄() -> ManySortedSet of NAT , F₅() -> ManySortedSet of NAT , F₆() -> ManySortedSet of NAT } :

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F₄() . n & A = F₅() . n & P₁[S,A,F₆() . n,n] )

provided

A1: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F₄() . 0 & A = F₅() . 0 & x = F₆() . 0 & P₁[S,A,x, 0 ] ) and
A2: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F₄() . n & A = F₅() . n & x = F₆() . n holds
( F₄() . (n + 1) = F₁(S,x,n) & F₅() . (n + 1) = F₂(S,A,x,n) & F₆() . (n + 1) = F₃(x,n) ) and
A3: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F₄() . n & A = F₅() . n & x = F₆() . n & P₁[S,A,x,n] holds
P₁[F₁(S,x,n),F₂(S,A,x,n),F₃(x,n),n + 1] and
A4: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F₂(S,A,x,n) is non-empty MSAlgebra over F₁(S,x,n)