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

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

defpred S_{3}[ object , 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

( $1 = S & $2 = A & $3 = F_{7}() . $4 & ( for s being State of A holds Following (s,(F_{10}(0) + ($4 * F_{10}(1)))) is stable ) );

deffunc H_{3}( set ) -> set = F_{7}() . $1;

consider f, g being ManySortedSet of NAT such that

A10: ( F_{2}() = f . F_{10}(2) & F_{4}() = g . F_{10}(2) )
and

A11: f . 0 = F_{1}()
and

A12: g . 0 = F_{3}()
and

F_{7}() . 0 = F_{8}()
and

A13: 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_{5}(x,n) st S = f . n & A1 = g . n & x = F_{7}() . n & A2 = F_{6}(x,n) holds

( f . (n + 1) = S +* F_{5}(x,n) & g . (n + 1) = A1 +* A2 & F_{7}() . (n + 1) = F_{9}(x,n) )
by A4;

deffunc H_{4}( set ) -> set = f . $1;

A14: 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 = F_{7}() . n holds

( f . (n + 1) = H_{2}(S,x,n) & g . (n + 1) = H_{1}(S,A,x,n) & F_{7}() . (n + 1) = F_{9}(x,n) )

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 = F_{7}() . n & S_{3}[S,A,x,n] holds

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

for A being non-empty MSAlgebra over S

for x being set

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

A32: 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 = F_{7}() . 0 & S_{3}[S,A,x, 0 ] )
by A2, A11, A12;

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_{3}[S,A,F_{7}() . n,n] )
from CIRCCMB2:sch 13(A32, A14, A15, A31);

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

( S = f . F_{10}(2) & A = g . F_{10}(2) & S_{3}[S,A,F_{7}() . F_{10}(2),F_{10}(2)] )
;

hence for s being State of F_{4}() holds Following (s,(F_{10}(0) + (F_{10}(2) * F_{10}(1)))) is stable
by A10; :: thesis: verum

deffunc H

defpred S

( $1 = S & $2 = A & $3 = F

deffunc H

consider f, g being ManySortedSet of NAT such that

A10: ( F

A11: f . 0 = F

A12: g . 0 = F

F

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

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

deffunc H

A14: 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 = F

( f . (n + 1) = H

proof

A15:
for n being Nat
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 = F_{7}() . n holds

( f . (n + 1) = H_{2}(S,x,n) & g . (n + 1) = H_{1}(S,A,x,n) & F_{7}() . (n + 1) = F_{9}(x,n) )

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 = F_{7}() . n holds

( f . (n + 1) = H_{2}(S,x,n) & g . (n + 1) = H_{1}(S,A,x,n) & F_{7}() . (n + 1) = F_{9}(x,n) )

let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f . n & A = g . n & x = F_{7}() . n holds

( f . (n + 1) = H_{2}(S,x,n) & g . (n + 1) = H_{1}(S,A,x,n) & F_{7}() . (n + 1) = F_{9}(x,n) )

let x be set ; :: thesis: ( S = f . n & A = g . n & x = F_{7}() . n implies ( f . (n + 1) = H_{2}(S,x,n) & g . (n + 1) = H_{1}(S,A,x,n) & F_{7}() . (n + 1) = F_{9}(x,n) ) )

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

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

hence ( S = f . n & A = g . n & x = F_{7}() . n implies ( f . (n + 1) = H_{2}(S,x,n) & g . (n + 1) = H_{1}(S,A,x,n) & F_{7}() . (n + 1) = F_{9}(x,n) ) )
by A13; :: thesis: verum

end;for A being non-empty MSAlgebra over S

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

( f . (n + 1) = H

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 = F

( f . (n + 1) = H

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

( f . (n + 1) = H

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

reconsider A2 = F

A2 = MSAlg (F

hence ( S = f . n & A = g . n & x = 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 = F

S

proof

A31:
for S being non empty ManySortedSign
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 = F_{7}() . n & S_{3}[S,A,x,n] holds

S_{3}[H_{2}(S,x,n),H_{1}(S,A,x,n),F_{9}(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 = F_{7}() . n & S_{3}[S,A,x,n] holds

S_{3}[H_{2}(S,x,n),H_{1}(S,A,x,n),F_{9}(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 = F_{7}() . n & S_{3}[S,A,x,n] holds

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

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

assume that

A16: S = f . n and

A = g . n and

x = F_{7}() . n
; :: thesis: ( not S_{3}[S,A,x,n] or S_{3}[H_{2}(S,x,n),H_{1}(S,A,x,n),F_{9}(x,n),n + 1] )

given S9 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , A9 being strict gate`2=den Boolean Circuit of S9 such that A17: S = S9 and

A18: A = A9 and

A19: x = F_{7}() . n
and

A20: for s being State of A9 holds Following (s,(F_{10}(0) + (n * F_{10}(1)))) is stable
; :: thesis: S_{3}[H_{2}(S,x,n),H_{1}(S,A,x,n),F_{9}(x,n),n + 1]

thus S_{3}[S +* F_{5}(x,n),A +* (MSAlg (F_{6}(x,n),F_{5}(x,n))),F_{9}(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 = F

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 = F

S

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

S

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

assume that

A16: S = f . n and

A = g . n and

x = F

given S9 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , A9 being strict gate`2=den Boolean Circuit of S9 such that A17: S = S9 and

A18: A = A9 and

A19: x = F

A20: for s being State of A9 holds Following (s,(F

thus S

proof

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

take S9 +* F_{5}(x,n)
; :: thesis: ex A being strict gate`2=den Boolean Circuit of S9 +* F_{5}(x,n) st

( S +* F_{5}(x,n) = S9 +* F_{5}(x,n) & A +* (MSAlg (F_{6}(x,n),F_{5}(x,n))) = A & F_{9}(x,n) = F_{7}() . (n + 1) & ( for s being State of A holds Following (s,(F_{10}(0) + ((n + 1) * F_{10}(1)))) is stable ) )

A21: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

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

A22: ( f . 0 = F_{1}() & g . 0 = F_{3}() )
by A11, A12;

for n being Nat

for S being non empty ManySortedSign

for x being set st S = f . n & x = F_{7}() . n holds

( f . (n + 1) = H_{2}(S,x,n) & F_{7}() . (n + 1) = F_{9}(x,n) )
from CIRCCMB2:sch 15(A22, A14, A21);

then A23: for n being Nat

for S being non empty ManySortedSign

for x being set st S = H_{4}(n) & x = F_{7}() . n holds

( H_{4}(n + 1) = S +* F_{5}(x,n) & F_{7}() . (n + 1) = F_{9}(x,n) & x in InputVertices F_{5}(x,n) & F_{9}(x,n) in InnerVertices F_{5}(x,n) )
by A9;

A9 +* A2 = A +* (MSAlg (F_{6}(x,n),F_{5}(x,n)))
by A17, A18, Def1;

then reconsider AA = A +* (MSAlg (F_{6}(x,n),F_{5}(x,n))) as strict gate`2=den Boolean Circuit of S9 +* F_{5}(x,n) ;

take AA ; :: thesis: ( S +* F_{5}(x,n) = S9 +* F_{5}(x,n) & A +* (MSAlg (F_{6}(x,n),F_{5}(x,n))) = AA & F_{9}(x,n) = F_{7}() . (n + 1) & ( for s being State of AA holds Following (s,(F_{10}(0) + ((n + 1) * F_{10}(1)))) is stable ) )

A24: F_{10}(0) + ((n + 1) * F_{10}(1)) = (F_{10}(0) + (n * F_{10}(1))) + F_{10}(1)
;

thus ( S9 +* F_{5}(x,n) = S +* F_{5}(x,n) & A +* (MSAlg (F_{6}(x,n),F_{5}(x,n))) = AA )
by A17; :: thesis: ( F_{9}(x,n) = F_{7}() . (n + 1) & ( for s being State of AA holds Following (s,(F_{10}(0) + ((n + 1) * F_{10}(1)))) is stable ) )

thus F_{9}(x,n) = H_{3}(n + 1)
by A9, A19; :: thesis: for s being State of AA holds Following (s,(F_{10}(0) + ((n + 1) * F_{10}(1)))) is stable

let s be State of AA; :: thesis: Following (s,(F_{10}(0) + ((n + 1) * F_{10}(1)))) is stable

A25: InnerVertices F_{1}() is Relation
by A5;

A26: for n being Nat

for x being set st x = F_{7}() . n holds

(InputVertices F_{5}(x,n)) \ {x} is without_pairs
by A8;

A27: for n being Nat

for x being set holds InnerVertices F_{5}(x,n) is Relation
by A7;

A28: InputVertices F_{1}() is without_pairs
by A5;

A29: ( H_{4}( 0 ) = F_{1}() & F_{7}() . 0 in InnerVertices F_{1}() )
by A6, A11;

for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st

( S1 = H_{4}(n) & S2 = H_{4}(n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F_{5}((F_{7}() . n),n)) \ {(F_{7}() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
from CIRCCMB2:sch 10(A25, A28, A29, A27, A26, A23);

then ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st

( S1 = f . n & S2 = f . (n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F_{5}(H_{3}(n),n)) \ {H_{3}(n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
;

then A30: InputVertices S9 misses InnerVertices F_{5}(x,n)
by A7, A16, A17, FACIRC_1:5;

( A2 = MSAlg (F_{6}(x,n),F_{5}(x,n)) & ( for s being State of A2 holds Following (s,F_{10}(1)) is stable ) )
by A3, A19, Def1;

hence Following (s,(F_{10}(0) + ((n + 1) * F_{10}(1)))) is stable
by A17, A18, A20, A30, A24, Th20, CIRCCOMB:60; :: thesis: verum

end;take S9 +* F

( S +* F

A21: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds H

A22: ( f . 0 = F

for n being Nat

for S being non empty ManySortedSign

for x being set st S = f . n & x = F

( f . (n + 1) = H

then A23: for n being Nat

for S being non empty ManySortedSign

for x being set st S = H

( H

A9 +* A2 = A +* (MSAlg (F

then reconsider AA = A +* (MSAlg (F

take AA ; :: thesis: ( S +* F

A24: F

thus ( S9 +* F

thus F

let s be State of AA; :: thesis: Following (s,(F

A25: InnerVertices F

A26: for n being Nat

for x being set st x = F

(InputVertices F

A27: for n being Nat

for x being set holds InnerVertices F

A28: InputVertices F

A29: ( H

for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st

( S1 = H

then ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st

( S1 = f . n & S2 = f . (n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F

then A30: InputVertices S9 misses InnerVertices F

( A2 = MSAlg (F

hence Following (s,(F

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds H

A32: 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 = F

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 ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . F

hence for s being State of F