deffunc H_{1}( non empty ManySortedSign , set , set ) -> ManySortedSign = $1 +* F_{4}($2,$3);

consider f1, h1 being ManySortedSet of NAT such that

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

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

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

A6: 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) = H_{1}(S,x,n) & h1 . (n + 1) = F_{7}(x,n) )
by A1;

defpred S_{3}[ object , object , Nat] means ( $3 <> 0 implies 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 ) );

deffunc H_{2}( non empty ManySortedSign , non-empty MSAlgebra over $1, set , set ) -> MSAlgebra over $1 +* F_{4}($3,$4) = $2 +* (MSAlg (F_{5}($3,$4),F_{4}($3,$4)));

A7: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds H_{2}(S,A,x,n) is non-empty MSAlgebra over H_{1}(S,x,n)
;

A8: 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}[H_{1}(S,x,n),F_{7}(x,n),n + 1]
;

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

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

A10: 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) = H_{1}(S,x,n) & g . (n + 1) = H_{2}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) )
from CIRCCMB2:sch 12();

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_{2}[S,A,x,n] holds

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

A12: 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 A9;

A13: 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(A12, A10, A11, A7);

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

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

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

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

( S = f1 . n & S_{1}[S,h1 . n,n] )
from CIRCCMB2:sch 2(A14, A6, A8);

_{4}[ 0 ]
by A9, A5;

A20: for i being Nat holds S_{4}[i]
from NAT_1:sch 2(A19, A16);

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

for i being object st i in NAT holds

h1 . i = h . i by A20;

then A21: h1 = h by PBOOLE:3;

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

A25: 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_{6}[S,A,x,n] holds

S_{6}[H_{1}(S,x,n),H_{2}(S,A,x,n),F_{7}(x,n),n + 1]

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

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_{6}[S,A,h . n,n] )
from CIRCCMB2:sch 13(A30, A10, A25, A7);

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

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

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

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

A34: S_{5}[ 0 ]
by A9, A4;

A35: for i being Nat holds S_{5}[i]
from NAT_1:sch 2(A34, A22);

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 A9, A3, A31, A32, A33;

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 A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & 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}() )
by A9, A3, A35, A32; :: thesis: for n being Nat

for S being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) )

let n be Nat; :: thesis: for S being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) )

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

for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) )

let A1 be non-empty MSAlgebra over S; :: thesis: for x being set

for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) )

let x be set ; :: thesis: for A2 being non-empty MSAlgebra over F_{4}(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) holds

( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) )

let A2 be non-empty MSAlgebra over F_{4}(x,n); :: thesis: ( S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) implies ( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) ) )

assume A36: ( S = f . n & A1 = g . n & x = h . n & A2 = F_{5}(x,n) )
; :: thesis: ( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) )

A2 = MSAlg (A2,F_{4}(x,n))
by Def1;

hence ( f . (n + 1) = S +* F_{4}(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F_{7}(x,n) )
by A10, A36; :: thesis: verum

consider f1, h1 being ManySortedSet of NAT such that

A3: F

A4: f1 . 0 = F

A5: h1 . 0 = F

A6: 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) = H

defpred S

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

deffunc H

A7: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds H

A8: for n being Nat

for S being non empty ManySortedSign

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

S

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

A9: ( f . 0 = F

A10: 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) = H

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

A12: 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

A13: 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

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

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

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

( S = f1 . n & S

A16: now :: thesis: for n being Nat st S_{4}[n] holds

S_{4}[n + 1]

A19:
SS

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

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

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

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

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

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

hence S_{4}[n + 1]
by A10, A17, A18; :: thesis: verum

end;assume A17: S

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

then A18: 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 A13;

hence S

A20: for i being Nat holds S

defpred S

for i being object st i in NAT holds

h1 . i = h . i by A20;

then A21: h1 = h by PBOOLE:3;

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

S_{5}[n + 1]

defpred SS

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

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

A23: S = f . n and

A24: A = g . n by A13;

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

then f1 . (n + 1) = S +* F_{4}((h1 . n),n)
by A6, A23

.= f . (n + 1) by A10, A21, A23, A24 ;

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

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

A23: S = f . n and

A24: A = g . n by A13;

assume S

then f1 . (n + 1) = S +* F

.= f . (n + 1) by A10, A21, A23, A24 ;

hence S

A25: 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

A30:
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_{6}[S,A,x,n] holds

S_{6}[H_{1}(S,x,n),H_{2}(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_{6}[S,A,x,n] holds

S_{6}[H_{1}(S,x,n),H_{2}(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_{6}[S,A,x,n] holds

S_{6}[H_{1}(S,x,n),H_{2}(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_{6}[S,A,x,n] implies S_{6}[H_{1}(S,x,n),H_{2}(S,A,x,n),F_{7}(x,n),n + 1] )

assume that

A26: ( S = f . n & A = g . n ) and

x = h . n and

A27: S_{3}[S,A,n]
and

n + 1 <> 0 ; :: thesis: 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 = H_{1}(S,x,n) & A = H_{2}(S,A,x,n) )

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

A26: ( S = f . n & A = g . n ) and

x = h . n and

A27: S

n + 1 <> 0 ; :: thesis: 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 = H

per cases
( n = 0 or n <> 0 )
;

end;

suppose A28:
n = 0
; :: thesis: 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 = H_{1}(S,x,n) & A = H_{2}(S,A,x,n) )

( S = H

reconsider A2 = F_{5}(x,0) as strict gate`2=den Boolean Circuit of F_{4}(x,0) by A2;

F_{3}() +* (MSAlg (F_{5}(x,0),F_{4}(x,0))) = F_{3}() +* A2
by Def1;

hence 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 = H_{1}(S,x,n) & A = H_{2}(S,A,x,n) )
by A9, A26, A28; :: thesis: verum

end;F

hence 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 = H

suppose A29:
n <> 0
; :: thesis: 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 = H_{1}(S,x,n) & A = H_{2}(S,A,x,n) )

( S = H

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

reconsider A = A as strict gate`2=den Boolean Circuit of S by A27, A29;

reconsider A9 = F_{5}(x,n) as strict gate`2=den Boolean Circuit of F_{4}(x,n) by A2;

A +* (MSAlg (F_{5}(x,n),F_{4}(x,n))) = A +* A9
by Def1;

hence 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 = H_{1}(S,x,n) & A = H_{2}(S,A,x,n) )
; :: thesis: verum

end;reconsider A = A as strict gate`2=den Boolean Circuit of S by A27, A29;

reconsider A9 = F

A +* (MSAlg (F

hence 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 = H

( 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

A31: S = f . F

A32: A = g . F

A33: S

A34: S

A35: 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 A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

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

( F

for S being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

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

( F

for S being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

take h ; :: thesis: ( F

for S being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

thus ( F

for S being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

let n be Nat; :: thesis: for S being non empty ManySortedSign

for A1 being non-empty MSAlgebra over S

for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

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

for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

let A1 be non-empty MSAlgebra over S; :: thesis: for x being set

for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

let x be set ; :: thesis: for A2 being non-empty MSAlgebra over F

( f . (n + 1) = S +* F

let A2 be non-empty MSAlgebra over F

assume A36: ( S = f . n & A1 = g . n & x = h . n & A2 = F

A2 = MSAlg (A2,F

hence ( f . (n + 1) = S +* F