A5:
for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F_{5}(S,A,x,n) is non-empty MSAlgebra over F_{4}(S,x,n)
by A3;

defpred S_{3}[ object , object , Nat] means ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st

( S = $1 & A = $2 );

consider f, g, h being ManySortedSet of NAT such that

A6: ( f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() )
and

A7: 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 = g . n & x = h . n holds

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) )
from CIRCCMB2:sch 12();

A8: 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 = g . n & x = h . n & S_{2}[S,A,x,n] holds

S_{2}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1]
;

A9: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

( S = f . 0 & A = g . 0 & x = h . 0 & S_{2}[S,A,x, 0 ] )
by A6;

A10: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n & S_{2}[S,A,h . n,n] )
from CIRCCMB2:sch 13(A9, A7, A8, A5);

defpred S_{4}[ object , object , object , Nat] means S_{3}[$1,$2,$4];

A11: 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 = g . n & x = h . n & S_{4}[S,A,x,n] holds

S_{4}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1]

( S = f . 0 & A = g . 0 & x = h . 0 & S_{4}[S,A,x, 0 ] )
by A6;

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n & S_{4}[S,A,h . n,n] )
from CIRCCMB2:sch 13(A13, A7, A11, A5);

then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that

A14: S = f . F_{8}()
and

A15: A = g . F_{8}()
and

A16: S_{3}[S,A,F_{8}()]
;

consider f1, h1 being ManySortedSet of NAT such that

A17: F_{2}() = f1 . F_{8}()
and

A18: f1 . 0 = F_{1}()
and

A19: h1 . 0 = F_{6}()
and

A20: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n holds

( f1 . (n + 1) = F_{4}(S,x,n) & h1 . (n + 1) = F_{7}(x,n) )
by A2;

A21: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n & S_{1}[S,x,n] holds

S_{1}[F_{4}(S,x,n),F_{7}(x,n),n + 1]
;

defpred S_{5}[ Nat] means h1 . $1 = h . $1;

A22: ex S being non empty ManySortedSign ex x being set st

( S = f1 . 0 & x = h1 . 0 & S_{1}[S,x, 0 ] )
by A18;

A23: for n being Nat ex S being non empty ManySortedSign st

( S = f1 . n & S_{1}[S,h1 . n,n] )
from CIRCCMB2:sch 2(A22, A20, A21);

_{5}[ 0 ]
by A6, A19;

A28: for i being Nat holds S_{5}[i]
from NAT_1:sch 2(A27, A24);

defpred S_{6}[ Nat] means f1 . $1 = f . $1;

for i being object st i in NAT holds

h1 . i = h . i by A28;

then A29: h1 = h by PBOOLE:3;

_{6}[ 0 ]
by A6, A18;

A34: for i being Nat holds S_{6}[i]
from NAT_1:sch 2(A33, A30);

then for i being object st i in NAT holds

f1 . i = f . i ;

then f1 = f by PBOOLE:3;

then reconsider A = A as strict gate`2=den Boolean Circuit of F_{2}() by A17, A14, A16;

take A ; :: thesis: ex f, g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() & ( 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 = g . n & x = h . n holds

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )

take f ; :: thesis: ex g, h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() & ( 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 = g . n & x = h . n holds

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )

take g ; :: thesis: ex h being ManySortedSet of NAT st

( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() & ( 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 = g . n & x = h . n holds

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )

take h ; :: thesis: ( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() & ( 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 = g . n & x = h . n holds

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )

thus ( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{6}() & ( 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 = g . n & x = h . n holds

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )
by A6, A7, A17, A34, A15; :: thesis: verum

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

defpred S

( S = $1 & A = $2 );

consider f, g, h being ManySortedSet of NAT such that

A6: ( f . 0 = F

A7: 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 = g . n & x = h . n holds

( f . (n + 1) = F

A8: 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 = g . n & x = h . n & S

S

A9: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

( S = f . 0 & A = g . 0 & x = h . 0 & S

A10: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n & S

defpred S

A11: 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 = g . n & x = h . n & S

S

proof

A13:
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
let n be Nat; :: thesis: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n & S_{4}[S,A,x,n] holds

S_{4}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1]

let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n & S_{4}[S,A,x,n] holds

S_{4}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1]

let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f . n & A = g . n & x = h . n & S_{4}[S,A,x,n] holds

S_{4}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1]

let x be set ; :: thesis: ( S = f . n & A = g . n & x = h . n & S_{4}[S,A,x,n] implies S_{4}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1] )

assume that

S = f . n and

A = g . n and

x = h . n and

A12: S_{3}[S,A,n]
; :: thesis: S_{4}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1]

reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A12;

reconsider A = A as strict gate`2=den Boolean Circuit of S by A12;

reconsider S1 = F_{4}(S,x,n) as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A1;

F_{5}(S,A,x,n) is strict gate`2=den Boolean Circuit of S1
by A4;

hence S_{4}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{7}(x,n),n + 1]
; :: thesis: verum

end;for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n & S

S

let S be non empty ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n & S

S

let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f . n & A = g . n & x = h . n & S

S

let x be set ; :: thesis: ( S = f . n & A = g . n & x = h . n & S

assume that

S = f . n and

A = g . n and

x = h . n and

A12: S

reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A12;

reconsider A = A as strict gate`2=den Boolean Circuit of S by A12;

reconsider S1 = F

F

hence S

( S = f . 0 & A = g . 0 & x = h . 0 & S

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n & S

then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that

A14: S = f . F

A15: A = g . F

A16: S

consider f1, h1 being ManySortedSet of NAT such that

A17: F

A18: f1 . 0 = F

A19: h1 . 0 = F

A20: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n holds

( f1 . (n + 1) = F

A21: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n & S

S

defpred S

A22: ex S being non empty ManySortedSign ex x being set st

( S = f1 . 0 & x = h1 . 0 & S

A23: for n being Nat ex S being non empty ManySortedSign st

( S = f1 . n & S

A24: now :: thesis: for n being Nat st S_{5}[n] holds

S_{5}[n + 1]

A27:
SS

let n be Nat; :: thesis: ( S_{5}[n] implies S_{5}[n + 1] )

assume A25: S_{5}[n]
; :: thesis: S_{5}[n + 1]

ex S being non empty ManySortedSign st S = f1 . n by A23;

then A26: h1 . (n + 1) = F_{7}((h1 . n),n)
by A20;

ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n ) by A10;

hence S_{5}[n + 1]
by A7, A25, A26; :: thesis: verum

end;assume A25: S

ex S being non empty ManySortedSign st S = f1 . n by A23;

then A26: h1 . (n + 1) = F

ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n ) by A10;

hence S

A28: for i being Nat holds S

defpred S

for i being object st i in NAT holds

h1 . i = h . i by A28;

then A29: h1 = h by PBOOLE:3;

A30: now :: thesis: for n being Nat st S_{6}[n] holds

S_{6}[n + 1]

A33:
SS

let n be Nat; :: thesis: ( S_{6}[n] implies S_{6}[n + 1] )

consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that

A31: S = f . n and

A32: A = g . n by A10;

assume S_{6}[n]
; :: thesis: S_{6}[n + 1]

then f1 . (n + 1) = F_{4}(S,(h1 . n),n)
by A20, A31

.= f . (n + 1) by A7, A29, A31, A32 ;

hence S_{6}[n + 1]
; :: thesis: verum

end;consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that

A31: S = f . n and

A32: A = g . n by A10;

assume S

then f1 . (n + 1) = F

.= f . (n + 1) by A7, A29, A31, A32 ;

hence S

A34: for i being Nat holds S

then for i being object st i in NAT holds

f1 . i = f . i ;

then f1 = f by PBOOLE:3;

then reconsider A = A as strict gate`2=den Boolean Circuit of F

take A ; :: thesis: ex f, g, h being ManySortedSet of NAT st

( F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n holds

( f . (n + 1) = F

take f ; :: thesis: ex g, h being ManySortedSet of NAT st

( F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n holds

( f . (n + 1) = F

take g ; :: thesis: ex h being ManySortedSet of NAT st

( F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n holds

( f . (n + 1) = F

take h ; :: thesis: ( F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n holds

( f . (n + 1) = F

thus ( F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set st S = f . n & A = g . n & x = h . n holds

( f . (n + 1) = F