deffunc H1( non empty ManySortedSign , non-empty MSAlgebra over $1, set , set ) -> MSAlgebra over $1 +* F5($3,$4) = $2 +* (MSAlg (F6($3,$4),F5($3,$4)));
deffunc H2( non empty ManySortedSign , set , set ) -> ManySortedSign = $1 +* F5($2,$3);
defpred S3[ 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 = F7() . $4 & ( for s being State of A holds Following (s,(F10(0) + ($4 * F10(1)))) is stable ) );
deffunc H3( set ) -> set = F7() . $1;
consider f, g being ManySortedSet of NAT such that
A10: ( F2() = f . F10(2) & F4() = g . F10(2) ) and
A11: f . 0 = F1() and
A12: g . 0 = F3() and
F7() . 0 = F8() 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 F5(x,n) st S = f . n & A1 = g . n & x = F7() . n & A2 = F6(x,n) holds
( f . (n + 1) = S +* F5(x,n) & g . (n + 1) = A1 +* A2 & F7() . (n + 1) = F9(x,n) ) by A4;
deffunc H4( 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 = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) )
proof
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 = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(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 = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) )
let A be non-empty MSAlgebra over S; :: thesis: for x being set st S = f . n & A = g . n & x = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) )
let x be set ; :: thesis: ( S = f . n & A = g . n & x = F7() . n implies ( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) ) )
reconsider A2 = F6(x,n) as strict gate`2=den Boolean Circuit of F5(x,n) by A1;
A2 = MSAlg (F6(x,n),F5(x,n)) by Def1;
hence ( S = f . n & A = g . n & x = F7() . n implies ( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) ) ) by A13; :: thesis: verum
end;
A15: 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 = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
proof
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 = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(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 = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(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 = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
let x be set ; :: thesis: ( S = f . n & A = g . n & x = F7() . n & S3[S,A,x,n] implies S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1] )
assume that
A16: S = f . n and
A = g . n and
x = F7() . n ; :: thesis: ( not S3[S,A,x,n] or S3[H2(S,x,n),H1(S,A,x,n),F9(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 = F7() . n and
A20: for s being State of A9 holds Following (s,(F10(0) + (n * F10(1)))) is stable ; :: thesis: S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
thus S3[S +* F5(x,n),A +* (MSAlg (F6(x,n),F5(x,n))),F9(x,n),n + 1] :: thesis: verum
proof
reconsider A2 = F6(x,n) as strict gate`2=den Boolean Circuit of F5(x,n) by A1;
take S9 +* F5(x,n) ; :: thesis: ex A being strict gate`2=den Boolean Circuit of S9 +* F5(x,n) st
( S +* F5(x,n) = S9 +* F5(x,n) & A +* (MSAlg (F6(x,n),F5(x,n))) = A & F9(x,n) = F7() . (n + 1) & ( for s being State of A holds Following (s,(F10(0) + ((n + 1) * F10(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 H1(S,A,x,n) is non-empty MSAlgebra over H2(S,x,n) ;
A22: ( f . 0 = F1() & g . 0 = F3() ) by A11, A12;
for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = F7() . n holds
( f . (n + 1) = H2(S,x,n) & F7() . (n + 1) = F9(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 = H4(n) & x = F7() . n holds
( H4(n + 1) = S +* F5(x,n) & F7() . (n + 1) = F9(x,n) & x in InputVertices F5(x,n) & F9(x,n) in InnerVertices F5(x,n) ) by A9;
A9 +* A2 = A +* (MSAlg (F6(x,n),F5(x,n))) by A17, A18, Def1;
then reconsider AA = A +* (MSAlg (F6(x,n),F5(x,n))) as strict gate`2=den Boolean Circuit of S9 +* F5(x,n) ;
take AA ; :: thesis: ( S +* F5(x,n) = S9 +* F5(x,n) & A +* (MSAlg (F6(x,n),F5(x,n))) = AA & F9(x,n) = F7() . (n + 1) & ( for s being State of AA holds Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable ) )
A24: F10(0) + ((n + 1) * F10(1)) = (F10(0) + (n * F10(1))) + F10(1) ;
thus ( S9 +* F5(x,n) = S +* F5(x,n) & A +* (MSAlg (F6(x,n),F5(x,n))) = AA ) by A17; :: thesis: ( F9(x,n) = F7() . (n + 1) & ( for s being State of AA holds Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable ) )
thus F9(x,n) = H3(n + 1) by A9, A19; :: thesis: for s being State of AA holds Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable
let s be State of AA; :: thesis: Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable
A25: InnerVertices F1() is Relation by A5;
A26: for n being Nat
for x being set st x = F7() . n holds
(InputVertices F5(x,n)) \ {x} is without_pairs by A8;
A27: for n being Nat
for x being set holds InnerVertices F5(x,n) is Relation by A7;
A28: InputVertices F1() is without_pairs by A5;
A29: ( H4( 0 ) = F1() & F7() . 0 in InnerVertices F1() ) by A6, A11;
for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = H4(n) & S2 = H4(n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F5((F7() . n),n)) \ {(F7() . 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 F5(H3(n),n)) \ {H3(n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) ;
then A30: InputVertices S9 misses InnerVertices F5(x,n) by A7, A16, A17, FACIRC_1:5;
( A2 = MSAlg (F6(x,n),F5(x,n)) & ( for s being State of A2 holds Following (s,F10(1)) is stable ) ) by A3, A19, Def1;
hence Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable by A17, A18, A20, A30, A24, Th20, CIRCCOMB:60; :: thesis: verum
end;
end;
A31: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds H1(S,A,x,n) is non-empty MSAlgebra over H2(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 = F7() . 0 & S3[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 & S3[S,A,F7() . 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 . F10(2) & A = g . F10(2) & S3[S,A,F7() . F10(2),F10(2)] ) ;
hence for s being State of F4() holds Following (s,(F10(0) + (F10(2) * F10(1)))) is stable by A10; :: thesis: verum