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