:: Combining of Multi Cell Circuits
:: by Grzegorz Bancerek , Shin'nosuke Yamaguchi and Yasunari Shidama
::
:: Received March 22, 2002
:: Copyright (c) 2002-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NAT_1, FUNCT_1, FINSEQ_2, MARGREL1, CIRCCOMB, LATTICES, FINSET_1,
XBOOLE_0, MSUALG_1, FSM_1, CIRCUIT1, RELAT_1, CIRCUIT2, STRUCT_0,
MSAFREE2, GLIB_000, ARYTM_3, CARD_1, XXREAL_0, PBOOLE, NUMBERS, MCART_1,
FUNCT_4, PARTFUN1, FACIRC_1, TARSKI, ORDINAL1;
notations TARSKI, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XFAMILY, XXREAL_0,
NAT_1, XTUPLE_0, MCART_1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FINSEQ_2, FUNCT_4, PBOOLE, MARGREL1, STRUCT_0, MSUALG_1, MSAFREE2,
CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1;
constructors LIMFUNC1, CIRCUIT1, CIRCUIT2, FACIRC_1, NAT_1, RELSET_1,
XTUPLE_0, XFAMILY;
registrations RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, CARD_3, STRUCT_0, CIRCCOMB,
FACIRC_1, NAT_1, MARGREL1, CARD_1, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
definitions CIRCUIT2;
equalities MSAFREE2;
expansions CIRCUIT2;
theorems TARSKI, FUNCT_1, RELAT_1, ZFMISC_1, NAT_1, MCART_1, PBOOLE, CIRCCOMB,
FACIRC_1, FUNCT_4, FRECHET, CIRCUIT1, CIRCUIT2, XBOOLE_0, XBOOLE_1,
XXREAL_0, ORDINAL1;
schemes NAT_1, PBOOLE;
begin :: One gate circuits
registration
let n be Nat;
let f be Function of n-tuples_on BOOLEAN, BOOLEAN;
let p be FinSeqLen of n;
cluster 1GateCircuit(p,f) -> Boolean;
coherence by CIRCCOMB:61;
end;
theorem Th1:
for X being finite non empty set, n being Nat for p being
FinSeqLen of n for f being Function of n-tuples_on X, X for o being OperSymbol
of 1GateCircStr(p,f) for s being State of 1GateCircuit(p,f) holds o
depends_on_in s = s*p
proof
let X be finite non empty set;
let n be Nat;
let p be FinSeqLen of n;
let f be Function of n-tuples_on X, X;
let o be OperSymbol of 1GateCircStr(p,f);
let s be State of 1GateCircuit(p,f);
o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def 3
.= s*p by CIRCCOMB:41;
hence thesis;
end;
theorem
for X being finite non empty set, n being Nat for p being FinSeqLen of
n for f being Function of n-tuples_on X, X for s being State of 1GateCircuit(p,
f) holds Following s is stable
proof
let X be finite non empty set, n be Nat;
let p be FinSeqLen of n;
let f be Function of n-tuples_on X, X;
set S = 1GateCircStr(p,f);
let s be State of 1GateCircuit(p,f);
set s1 = Following s, s2 = Following s1;
A1: dom s1 = the carrier of S by CIRCUIT1:3;
A2: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6;
A3: InputVertices S = rng p by CIRCCOMB:42;
A4: InnerVertices S = {[p,f]} by CIRCCOMB:42;
A5: now
let a be object;
assume a in the carrier of S;
then reconsider v = a as Vertex of S;
dom s = the carrier of S by CIRCUIT1:3;
then
A6: dom (s*p) = dom p by A2,RELAT_1:27,XBOOLE_1:7;
A7: dom (s1*p) = dom p by A1,A2,RELAT_1:27,XBOOLE_1:7;
A8: now
let i be object;
assume
A9: i in dom p;
then
A10: p.i in rng p by FUNCT_1:3;
(s1*p).i = s1.(p.i) & (s*p).i = s.(p.i) by A7,A6,A9,FUNCT_1:12;
hence (s1*p).i = (s*p).i by A3,A10,CIRCUIT2:def 5;
end;
v in rng p or v in {[p,f]} by A2,XBOOLE_0:def 3;
then
s2.v = s1.v or v = [p,f] & (v = [p,f] implies action_at v = v) & s2.v
= (Den(action_at v, 1GateCircuit(p,f))). (action_at v depends_on_in s1) & s1.v
= (Den(action_at v, 1GateCircuit(p,f))). (action_at v depends_on_in s) & (
action_at v = [p,f] implies action_at v depends_on_in s = s*p & action_at v
depends_on_in s1 = s1*p) by A3,A4,Th1,CIRCCOMB:41,CIRCUIT2:def 5
,TARSKI:def 1;
hence s2.a = s1.a by A7,A6,A8,FUNCT_1:2;
end;
dom s2 = the carrier of S by CIRCUIT1:3;
hence Following s = Following Following s by A1,A5,FUNCT_1:2;
end;
theorem Th3:
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A st s is stable
for n being natural Number holds Following(s, n) = s
proof
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A such that
A1: s is stable;
let n be natural Number;
A0: n is Nat by TARSKI:1;
defpred P[Nat] means Following(s,$1) = s;
A2: for n being Nat st P[n] holds P[n+1] by A1,FACIRC_1:12;
A3: P[ 0 ] by FACIRC_1:11;
for n being Nat holds P[n] from NAT_1:sch 2(A3,A2);
hence thesis by A0;
end;
theorem Th4:
for S being non void Circuit-like non empty ManySortedSign for
A being non-empty Circuit of S for s being State of A,
n1, n2 being natural Number st Following(s, n1) is stable & n1 <= n2
holds Following(s, n2) = Following(s, n1)
proof
let S be non void Circuit-like non empty ManySortedSign;
let A be non-empty Circuit of S;
let s be State of A, n1, n2 be natural Number such that
A1: Following(s, n1) is stable and
A2: n1 <= n2;
consider k being Nat such that
A3: n2 = n1+k by A2,NAT_1:10;
reconsider k as Nat;
n1 is Nat & n2 is Nat by TARSKI:1;
then Following(s, n2) = Following(Following(s, n1), k) by A3,FACIRC_1:13;
hence thesis by A1,Th3;
end;
begin :: Defining Many Cell Circuit Structures
scheme
CIRCCMB29sch1 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object)-> non empty ManySortedSign,
o(object,object) -> object}:
ex f,h being ManySortedSet of
NAT st f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
n+1) = o(x,n) proof
deffunc f(object,object) = [S($2`1,$2`2,$1), o($2`2,$1)];
consider F being Function such that
A1: dom F = NAT & F.0 = [S0(),o0()] and
A2: for n being Nat holds F.(n+1) = f(n,F.n) from NAT_1:sch 11;
deffunc h(object) = (F.$1)`2;
deffunc f(object) = (F.$1)`1;
consider f being ManySortedSet of NAT such that
A3: for n being object st n in NAT holds f.n = f(n) from PBOOLE:sch 4;
consider h being ManySortedSet of NAT such that
A4: for n being object st n in NAT holds h.n = h(n) from PBOOLE:sch 4;
take f,h;
(F.0)`1 = S0() & (F.0)`2 = o0() by A1;
hence f.0 = S0() & h.0 = o0() by A3,A4;
let n be Nat, S be non empty ManySortedSign, x be set;
set x = F.n;
A5: n in NAT by ORDINAL1:def 12;
then
A6: h.n = x`2 by A4;
assume S = f.n;
then S = x`1 by A3,A5;
then F.(n+1) = [S(S,h.n,n), o(h.n,n)] by A2,A6;
then (F.(n+1))`1 = S(S,h.n,n) & (F.(n+1))`2 = o(h.n,n);
hence thesis by A3,A4;
end;
scheme ::CircSch1
CIRCCMB29sch2 {S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, P[object,object,object],
f,h() -> ManySortedSet of NAT}:
for n being Nat ex S being
non empty ManySortedSign st S = f().n & P[S,h().n,n]
provided
A1: ex S being non empty ManySortedSign, x being set st S = f().0 & x =
h().0 & P[S, x, 0] and
A2: for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n) and
A3: for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n & P[S,x,n] holds P[S(S,x,n), o(x,n), n+1]
proof
defpred Q[Nat] means ex S being non empty ManySortedSign st S = f().$1 & P[S
,h().$1,$1];
A4: for n being Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
given S being non empty ManySortedSign such that
A5: S = f().n and
A6: P[S,h().n,n];
take S(S,h().n,n);
h().(n+1) = o(h().n, n) by A2,A5;
hence thesis by A2,A3,A5,A6;
end;
A7: Q[ 0 ] by A1;
thus for n being Nat holds Q[n] from NAT_1:sch 2(A7,A4);
end;
defpred Pl[object,object,object] means not contradiction;
scheme :: CircSchR0
CIRCCMB29sch3 {S0() -> non empty ManySortedSign,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, f,h() -> ManySortedSet of NAT}: for n being
Nat, x being set st x = h().n holds h().(n+1) = o(x,n)
provided
A1: f().0 = S0() and
A2: for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n)
proof
A3: ex S being non empty ManySortedSign, x being set st S = f().0 & x = h().
0 & Pl[S, x, 0] by A1;
let n be Nat, x be set;
A4: for n being Nat, S being non empty ManySortedSign, x being set st S = f(
).n & x = h().n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A5: for n being Nat, S being non empty ManySortedSign, x being set st S = f(
).n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n) by A2;
for n being Nat ex S being non empty ManySortedSign st S = f().n & Pl[S,
h().n,n] from CIRCCMB29sch2(A3,A5,A4);
then
A6: ex S being non empty ManySortedSign st S = f().n;
assume x = h().n;
hence thesis by A2,A6;
end;
scheme :: CircStrExSch
CIRCCMB29sch4 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, n() -> Nat}:
ex S being non
empty ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) proof
consider f,h being ManySortedSet of NAT such that
A1: f.0 = S0() & h.0 = o0() and
A2: for n being Nat, S being non empty ManySortedSign, x being set st S
= f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch1;
A3: for n being Nat, S being non empty ManySortedSign, x being set st S = f.
n & x = h.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A4: ex S being non empty ManySortedSign, x being set st S = f.0 & x = h.0 &
Pl[S, x, 0] by A1;
for n being Nat ex S being non empty ManySortedSign st S = f.n & Pl[S,h.
n,n] from CIRCCMB29sch2(A4,A2,A3);
then consider S being non empty ManySortedSign such that
A5: S = f.n();
take S,f,h;
thus thesis by A1,A2,A5;
end;
scheme :: CircStrUniqSch
CIRCCMB29sch5 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, n() -> Nat}:
for S1,S2 being non empty ManySortedSign
st (ex f,h being ManySortedSet of NAT st S1 = f.n() &
f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x
being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & (
ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 = S0() & h.0 = o0() & for
n being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2 proof
let S1,S2 be non empty ManySortedSign;
given f1,h1 being ManySortedSet of NAT such that
A1: S1 = f1.n() and
A2: f1.0 = S0() and
A3: h1.0 = o0() and
A4: for n being Nat, S being non empty ManySortedSign, x being set st S
= f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n);
A5: for n being Nat, S being non empty ManySortedSign, x being set st S =
f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n) by A4;
A6: for n being Nat, S being non empty ManySortedSign, x being set st S =
f1.n & x = h1.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A7: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
& Pl[S,x,0] by A2;
A8: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
h1.n,n] from CIRCCMB29sch2(A7,A5,A6);
given f2,h2 being ManySortedSet of NAT such that
A9: S2 = f2.n() and
A10: f2.0 = S0() and
A11: h2.0 = o0() and
A12: for n being Nat, S being non empty ManySortedSign, x being set st S
= f2.n & x = h2.n holds f2.(n+1) = S(S,x,n) & h2.(n+1) = o(x,n);
A13: for n being Nat, S being non empty ManySortedSign, x being set st S =
f2.n & x = h2.n holds f2.(n+1) = S(S,x,n) & h2.(n+1) = o(x,n) by A12;
defpred A[Nat] means h1.$1 = h2.$1;
A14: for n being Nat, S being non empty ManySortedSign, x being set st S =
f2.n & x = h2.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A15: ex S being non empty ManySortedSign, x being set st S = f2.0 & x = h2.0
& Pl[S,x,0] by A10;
A16: for n being Nat ex S being non empty ManySortedSign st S = f2.n & Pl[S,
h2.n,n] from CIRCCMB29sch2(A15,A13,A14);
A17: now
let n be Nat;
assume
A18: A[n];
ex S being non empty ManySortedSign st S = f1.n & Pl[S,h1.n,n] by A8;
then
A19: h1.(n+1) = o(h1.n,n) by A4;
ex S being non empty ManySortedSign st S = f2.n & Pl[S,h2.n,n] by A16;
hence A[n+1] by A12,A18,A19;
end;
defpred B[Nat] means f1.$1 = f2.$1;
A20: A[ 0 ] by A3,A11;
for i being Nat holds A[i] from NAT_1:sch 2(A20,A17);
then for i being object st i in NAT holds h1.i = h2.i;
then
A21: h1 = h2 by PBOOLE:3;
A22: now
let n be Nat;
assume
A23: B[n];
consider S being non empty ManySortedSign such that
A24: S = f1.n and
Pl[S,h1.n,n] by A8;
f1.(n+1) = S(S,h1.n,n) by A4,A24
.= f2.(n+1) by A12,A21,A23,A24;
hence B[n+1];
end;
A25: B[ 0 ] by A2,A10;
for i being Nat holds B[i] from NAT_1:sch 2(A25,A22);
hence thesis by A1,A9;
end;
scheme :: CircStrDefSch
CIRCCMB29sch6 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object, n() -> Nat}: (ex S being non
empty ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & for S1,S2
being non empty ManySortedSign st (ex f,h being ManySortedSet of NAT st S1 = f.
n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
n+1) = o(x,n)) & (ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2
proof
thus ex S being non empty ManySortedSign, f,h being ManySortedSet of NAT st
S = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
n+1) = o(x,n) from CIRCCMB29sch4;
thus for S1,S2 being non empty ManySortedSign st (ex f,h being ManySortedSet
of NAT st S1 = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non
empty ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n)
& h.(n+1) = o(x,n)) & (ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 =
S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being
set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1
= S2 from CIRCCMB29sch5;
end;
scheme :: attrCircStrExSch
CIRCCMB29sch7 {S0() -> non empty ManySortedSign,
S(object,object,object) -> non empty
ManySortedSign, o0()-> object, o(object,object) -> object, n() -> Nat}:
ex S being unsplit
gate`1=arity gate`2isBoolean non void non empty non empty strict ManySortedSign
, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0() & h.0 = o0() & for n
being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)
provided
A1: S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict and
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, x being set, n being Nat holds S(S,x,n) is unsplit
gate`1=arity gate`2isBoolean non void non empty strict
proof
defpred P[non empty ManySortedSign, object] means
$1 is unsplit gate`1=arity
gate`2isBoolean non void strict;
defpred Pl[non empty ManySortedSign, object,object] means P[$1,$2];
consider S being non empty ManySortedSign, f,h being ManySortedSet of NAT
such that
A3: S = f.n() & f.0 = S0() & h.0 = o0() and
A4: for n being Nat, S being non empty ManySortedSign, x being set st S
= f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch4;
A5: for n being Nat, S being non empty ManySortedSign, x being set st S = f.
n & x = h.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1] by A2;
A6: ex S being non empty ManySortedSign, x being set st S = f.0 & x = h.0 &
Pl[S,x,0] by A1,A3;
for n being Nat ex S being non empty ManySortedSign st S = f.n & Pl[S,h.
n,n ] from CIRCCMB29sch2(A6,A4,A5);
then ex S being non empty ManySortedSign st S = f.n() & P[S,n()];
then reconsider
S as unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign by A3;
take S,f,h;
thus thesis by A3,A4;
end;
scheme :: ManyCellCircStrExSch
CIRCCMB29sch8 {S0() -> non empty ManySortedSign, S(object,object) -> unsplit
gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
o0()-> object, o(object,object) -> object, n() -> Nat}:
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign, f,h being ManySortedSet of
NAT st S = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S +* S(x,n) &
h.(n+1) = o(x,n)
provided
A1: S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict
proof
deffunc Sl(non empty ManySortedSign,set,set) = $1+*S($2,$3);
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, x being set, n being Nat holds Sl(S,x,n) is unsplit
gate`1=arity gate`2isBoolean non void non empty strict;
thus ex S being unsplit gate`1=arity gate`2isBoolean non void non empty non
empty strict ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0
= S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x
being set st S = f.n & x = h.n holds f.(n+1) = Sl(S,x,n) & h.(n+1) = o(x,n)
from CIRCCMB29sch7(A1,A2);
end;
scheme :: attrCircStrUniqSch
CIRCCMB29sch9 {S0() -> non empty ManySortedSign, o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
o(object,object) -> object,
n() -> Nat}:
for S1,S2 being
unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty
ManySortedSign st (ex f,h being ManySortedSet of NAT st S1 = f.n() & f.0 = S0()
& h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & (ex f,h
being ManySortedSet of NAT st S2 = f.n() & f.0 = S0() & h.0 = o0() & for n
being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2 proof
for S1,S2 being non empty ManySortedSign st (ex f,h being ManySortedSet
of NAT st S1 = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non
empty ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n)
& h.(n+1) = o(x,n)) & (ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 =
S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being
set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1
= S2 from CIRCCMB29sch5;
hence thesis;
end;
begin
theorem Th5:
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 holds
InputVertices (S1+*S2) = ((InputVertices S1)\(InnerVertices S2)) \/ ((
InputVertices S2)\(InnerVertices S1))
proof
let S1,S2 be non empty ManySortedSign;
A1: ((the carrier of S1) \ ((rng the ResultSort of S1)\/(rng the ResultSort
of S2))) =(InputVertices S1) \ (InnerVertices S2) by XBOOLE_1:41;
assume S1 tolerates S2;
then
A2: the ResultSort of S1 tolerates the ResultSort of S2 by CIRCCOMB:def 1;
InputVertices (S1+*S2) = (the carrier of S1+*S2) \ rng ((the ResultSort
of S1) +* (the ResultSort of S2)) by CIRCCOMB:def 2
.= (the carrier of S1)\/(the carrier of S2) \ rng ((the ResultSort of S1
) +* (the ResultSort of S2)) by CIRCCOMB:def 2
.= (the carrier of S1)\/(the carrier of S2) \ ((rng the ResultSort of S1
)\/rng the ResultSort of S2) by A2,FRECHET:35
.= ((the carrier of S1) \ ((rng the ResultSort of S1)\/(rng the
ResultSort of S2)))\/ ((the carrier of S2) \ ((rng the ResultSort of S1)\/(rng
the ResultSort of S2))) by XBOOLE_1:42;
hence thesis by A1,XBOOLE_1:41;
end;
theorem Th6:
for X being without_pairs set, Y being Relation holds X \ Y = X
proof
let X being without_pairs set;
let Y being Relation;
X /\ Y = {};
then X misses Y by XBOOLE_0:def 7;
hence thesis by XBOOLE_1:83;
end;
theorem
for X being Relation, Y, Z being set st Z c= Y & Y \ Z is
without_pairs holds X \ Y = X \ Z
proof
let X be Relation;
let Y,Z be set;
assume
A1: Z c= Y;
assume Y \ Z is without_pairs;
then not(ex x being object st x in X /\ (Y \ Z));
then X /\ (Y \ Z) = {} by XBOOLE_0:7;
then X misses Y \ Z by XBOOLE_0:def 7;
then
A2: X \ (Y \ Z) = X by XBOOLE_1:83;
X \ Y = X \ ( (Y \ Z)\/Z ) by A1,XBOOLE_1:45
.= X \ Z by A2,XBOOLE_1:41;
hence thesis;
end;
theorem Th8:
for X,Z being set, Y being Relation st Z c= Y & X \ Z is
without_pairs holds X \ Y = X \ Z
proof
let X,Z being set;
let Y being Relation;
assume
A1: Z c= Y;
assume X \ Z is without_pairs;
then not(ex x being object st x in (Y \ Z) /\ (X \ Z));
then (Y \ Z) /\ (X \ Z) = {} by XBOOLE_0:7;
then Y \ Z misses X \ Z by XBOOLE_0:def 7;
then
A2: (X \ Z) \ (Y \ Z) = (X \ Z) by XBOOLE_1:83;
X \ Y = X \ ((Y \ Z) \/ Z) by A1,XBOOLE_1:45
.= X \ Z by A2,XBOOLE_1:41;
hence thesis;
end;
scheme :: InputOfManyCellCircStr
CIRCCMB29sch10 {S0() -> unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign, f(object) -> object, h() -> ManySortedSet of NAT,
S(object,object) ->
unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
o(object,object) -> object}: for n being Nat
ex S1,S2 being unsplit gate`1=arity
gate`2isBoolean non void non empty ManySortedSign st S1 = f(n) & S2 = f(n+1) &
InputVertices S2 = (InputVertices S1)\/((InputVertices S(h().n,n)) \ {h().n}) &
InnerVertices S1 is Relation & InputVertices S1 is without_pairs
provided
A1: InnerVertices S0() is Relation and
A2: InputVertices S0() is without_pairs and
A3: f(0) = S0() & h().0 in InnerVertices S0() and
A4: for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
A5: for n being Nat, x being set st x = h().n holds (InputVertices S(x,n
)) \ {x} is without_pairs and
A6: for n being Nat, S being non empty ManySortedSign, x being set st S
= f(n) & x = h().n holds f(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n)
proof
A7: InnerVertices S(h().0, 0) is Relation by A4;
defpred P[Nat] means ex S1,S2 being unsplit gate`1=arity gate`2isBoolean non
void non empty ManySortedSign st S1 = f($1) & S2 = f($1+1) & InputVertices S2 =
(InputVertices S1)\/((InputVertices S(h().$1,$1)) \ {h().$1}) & h().($1+1) in
InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is
Relation;
A8: for i being Nat st P[i] holds P[i+1]
proof
let i being Nat;
given S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign such that
S1 = f(i) and
A9: S2 = f(i+1) and
InputVertices S2 = (InputVertices S1)\/((InputVertices S(h().(i),i)) \
{h().(i)}) and
A10: h().(i+1) in InnerVertices S2 and
A11: InputVertices S2 is without_pairs and
A12: InnerVertices S2 is Relation;
A13: {h().(i+1)} c= InnerVertices S2 by A10,ZFMISC_1:31;
take S2, S3 = S2+*S(h().(i+1),i+1);
thus S2 = f(i+1) & S3 = f(i+1+1) by A6,A9;
A14: InputVertices S(h().(i+1),i+1) \ {h().(i+1)} is without_pairs by A5;
reconsider X1 = InputVertices S2, X2 = (InputVertices S(h().(i+1),i+1)) \
{h().(i+1)} as without_pairs set by A5,A11;
A15: InnerVertices S(h().(i+1),i+1) is Relation by A4;
thus InputVertices S3 = ((InputVertices S2)\(InnerVertices S(h().(i+1
),i+1))) \/ ((InputVertices S(h().(i+1),i+1))\(InnerVertices S2)) by Th5,
CIRCCOMB:47
.= InputVertices S2 \/ ((InputVertices S(h().(i+1),i+1))\(
InnerVertices S2)) by A11,A15,Th6
.= (InputVertices S2)\/((InputVertices S(h().(i+1),i+1)) \ {h().(i+1)}
) by A12,A14,A13,Th8;
then
A16: InputVertices S3 = X1 \/ X2;
A17: h().(i+1+1) = o(h().(i+1),i+1) & o(h().(i+1),i+1) in InnerVertices S(
h().(i+ 1), i+1) by A6,A9;
reconsider X1 = InnerVertices S2, X2 = InnerVertices S(h().(i+1), i+1) as
Relation by A4,A12;
S2 tolerates S(h().(i+1),i+1) by CIRCCOMB:47;
then InnerVertices S3 = X1 \/ X2 by CIRCCOMB:11;
hence thesis by A17,A16,XBOOLE_0:def 3;
end;
let n be Nat;
A18: S0() tolerates S(h().0,0) by CIRCCOMB:47;
A19: InputVertices (S0() +* S(h().0,0)) = ((InputVertices S0())\(
InnerVertices S(h().0,0))) \/ ((InputVertices S(h().0,0))\(InnerVertices S0()))
by Th5,CIRCCOMB:47
.= InputVertices S0() \/ ((InputVertices S(h().0,0))\(InnerVertices S0()
)) by A2,A7,Th6;
A20: P[ 0 ]
proof
reconsider A = InputVertices S(h().0,0) \ {h().0}, B = InputVertices S0()
as without_pairs set by A2,A5;
take S0 = S0(), S1 = S0()+* S(h().0,0);
thus S0 = f(0) & S1 = f(0+1) by A3,A6;
reconsider R1 = InnerVertices S0(), R2 = InnerVertices S(h().0,0) as
Relation by A1,A4;
for x being object st x in {h().0} holds x in InnerVertices S0() by A3,
TARSKI:def 1;
then {h().0} c= InnerVertices S0() by TARSKI:def 3;
then
A21: InputVertices S1= B\/A by A1,A19,Th8;
h().(0+1) = o(h().(0),0) & o(h().(0),0) in R2 by A3,A6;
then h().(0+1) in R1 \/ R2 by XBOOLE_0:def 3;
hence thesis by A18,A21,CIRCCOMB:11;
end;
A22: for i being Nat holds P[i] from NAT_1:sch 2(A20,A8);
then consider
S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign such that
A23: S1 = f(n) and
A24: S2 = f(n+1) & InputVertices S2 = (InputVertices S1)\/((
InputVertices S(h().( n),n) ) \ {h().(n)}) and
h().(n+1) in InnerVertices S2 and
InputVertices S2 is without_pairs and
InnerVertices S2 is Relation;
take S1,S2;
thus S1 = f(n) & S2 = f(n+1) & InputVertices S2 = (InputVertices S1)\/((
InputVertices S(h().(n),n)) \ {h().(n)}) by A23,A24;
per cases by NAT_1:6;
suppose
n = 0;
hence thesis by A1,A2,A3,A23;
end;
suppose
ex i being Nat st n = i+1;
then consider i being Nat such that
A25: n = i+1;
reconsider i as Nat;
ex T1,T2 being unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign st T1 = f(i) & T2 = f(i+1) & InputVertices T2 = (
InputVertices T1)\/((InputVertices S(h().(i),i)) \ {h().(i)}) & h().(i+1) in
InnerVertices T2 & InputVertices T2 is without_pairs & InnerVertices T2 is
Relation by A22;
hence thesis by A23,A25;
end;
end;
scheme :: InputOfManyCellCircStr
CIRCCMB29sch11 {Sn(set) -> unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign, h() -> ManySortedSet of NAT,
S(object,object) -> unsplit
gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
o(object,object) -> object}:
for n being Nat holds InputVertices Sn(n+1) = (InputVertices Sn(n))\/((
InputVertices S(h().(n),n)) \ {h().(n)}) & InnerVertices Sn(n) is Relation &
InputVertices Sn(n) is without_pairs
provided
A1: InnerVertices Sn(0) is Relation and
A2: InputVertices Sn(0) is without_pairs and
A3: h().(0) in InnerVertices Sn(0) and
A4: for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
A5: for n being Nat, x being set st x = h().(n) holds (InputVertices S(x
,n)) \ {x} is without_pairs and
A6: for n being Nat, S being non empty ManySortedSign, x being set st S
= Sn(n) & x = h().(n) holds Sn(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n)
proof
deffunc SN(set) = Sn($1);
A7: for n being Nat, S being non empty ManySortedSign, x being set st S = SN
(n) & x = h().n holds SN(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n) by A6;
let n be Nat;
A8: for n being Nat, x being set st x = h().n holds (InputVertices S(x,n)) \
{x} is without_pairs by A5;
A9: SN(0) = SN(0) & h().0 in InnerVertices SN(0) by A3;
A10: for n being Nat, x being set holds InnerVertices S(x,n) is Relation by A4;
for n being Nat ex S1,S2 being unsplit gate`1=arity gate`2isBoolean non
void non empty ManySortedSign st S1 = SN(n) & S2 = SN(n+1) & InputVertices S2 =
(InputVertices S1)\/((InputVertices S(h().n,n)) \ {h().n}) & InnerVertices S1
is Relation & InputVertices S1 is without_pairs from CIRCCMB29sch10(A1,A2,A9,
A10, A8,A7);
then ex S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign st S1 = Sn(n) & S2 = Sn(n+1) & InputVertices S2 = (InputVertices
S1)\/((InputVertices S(h().(n),n)) \ {h().(n)}) & InnerVertices S1 is Relation
& InputVertices S1 is without_pairs;
hence thesis;
end;
begin :: Defining Many Cell Circuits
scheme
CIRCCMB29sch12 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object}:
ex f,g,h being ManySortedSet of
NAT st f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non
empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+
1) = o(x,n) proof
deffunc F(set,set) = [[S($2`11,$2`2,$1), A($2`11,$2`12,$2`2,$1)], o($2`2,$1)
];
consider F being Function such that
A1: dom F = NAT & F.0 = [[S0(),A0()],o0()] and
A2: for n being Nat holds F.(n+1) = F(n,F.n) from NAT_1:sch 11;
A3: (F.0)`2 = o0() by A1;
deffunc h(object) = (F.$1)`2;
deffunc g(object) = (F.$1)`12;
deffunc f(object) = (F.$1)`11;
consider f being ManySortedSet of NAT such that
A4: for n being object st n in NAT holds f.n = f(n) from PBOOLE:sch 4;
consider h being ManySortedSet of NAT such that
A5: for n being object st n in NAT holds h.n = h(n) from PBOOLE:sch 4;
consider g being ManySortedSet of NAT such that
A6: for n being object st n in NAT holds g.n = g(n) from PBOOLE:sch 4;
take f,g,h;
(F.0)`11 = S0() & (F.0)`12 = A0() by A1,MCART_1:85;
hence f.0 = S0() & g.0 = A0() & h.0 = o0() by A4,A6,A5,A3;
let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S
, x be set;
set x = F.n;
A7: n in NAT by ORDINAL1:def 12;
then
A8: h.n = x`2 by A5;
assume that
A9: S = f.n and
A10: A = g.n;
A11: A = x`12 by A6,A7,A10;
S = x`11 by A4,A7,A9;
then
A12: F.(n+1) = [[S(S,h.n,n), A(S,A,h.n,n)], o(h.n,n)] by A2,A11,A8;
then
A13: (F.(n+1))`2 = o(h.n,n);
(F.(n+1))`11 = S(S,h.n,n) & (F.(n+1))`12 = A(S,A,h.n,n) by A12,MCART_1:85;
hence thesis by A4,A6,A5,A13;
end;
scheme :: CircSch3
CIRCCMB29sch13 {S(set,set,set) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object,
P[object,object,object,object],
f,g,h() -> ManySortedSet of NAT}:
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f().n & A = g().n & P[S,A,h().n,n]
provided
A1: ex S being non empty ManySortedSign, A being non-empty MSAlgebra
over S, x being set st S = f().0 & A = g().0 & x = h().0 & P[S, A, x, 0] and
A2: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) and
A3: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f().n & A = g().n & x = h().n & P[S,A,x
,n] holds P[S(S,x,n), A(S,A,x,n), o(x,n), n+1] and
A4: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
defpred Q[Nat] means ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S, x being set st S = f().$1 & A = g().$1 & x = h().$1 & P[S,A,x
,$1];
A5: for n being Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
given S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set such that
A6: S = f().n & A = g().n & x = h().n and
A7: P[S,A,x,n];
take S9 = S(S,x,n);
reconsider A9 = A(S,A,x,n) as non-empty MSAlgebra over S9 by A4;
take A9, y = h().(n+1);
y = o(x,n) by A2,A6;
hence thesis by A2,A3,A6,A7;
end;
let n be Nat;
A8: Q[ 0 ] by A1;
for n being Nat holds Q[n] from NAT_1:sch 2(A8,A5);
then consider
S being non empty ManySortedSign, A being non-empty MSAlgebra over
S, x being set such that
A9: S = f().n & A = g().n & x = h().n & P[S,A,x,n];
take S,A;
thus thesis by A9;
end;
defpred R[object,object,object,object] means not contradiction;
scheme :: CircSchU2
CIRCCMB29sch14 {S(set,set,set) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object,
f1,f2, g1,g2, h1,h2() -> ManySortedSet of NAT}:
f1() = f2() & g1() = g2() & h1() = h2()
provided
A1: ex S being non empty ManySortedSign, A being non-empty MSAlgebra
over S st S = f1().0 & A = g1().0 and
A2: f1().0 = f2().0 & g1().0 = g2().0 & h1().0 = h2().0 and
A3: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f1().n & A = g1().n & x = h1().n holds
f1().(n+1) = S(S,x,n) & g1().(n+1) = A(S,A,x,n) & h1().(n+1) = o(x,n) and
A4: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f2().n & A = g2().n & x = h2().n holds
f2().(n+1) = S(S,x,n) & g2().(n+1) = A(S,A,x,n) & h2().(n+1) = o(x,n) and
A5: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A6: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f1().n & A = g1().n & x = h1().n holds
f1().(n+1) = S(S,x,n) & g1().(n+1) = A(S,A,x,n) & h1().(n+1) = o(x,n) by A3;
set f1 = f1(), g1 = g1(), h1 = h1();
A7: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f1.n & A = g1.n & x = h1.n & R[S,A,x,n]
holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A8: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
,n) by A5;
A9: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
x being set st S = f1.0 & A = g1.0 & x = h1.0 & R[S, A, x, 0] by A1;
A10: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f1.n & A = g1.n & R[S,A,h1.n,n] from CIRCCMB29sch13(A9,
A6,A7,A8);
set f2 = f2(), g2 = g2(), h2 = h2();
A11: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f2.n & A = g2.n & x = h2.n & R[S,A,x,n]
holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
defpred P[Nat] means h1.$1 = h2.$1;
A12: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f2().n & A = g2().n & x = h2().n holds
f2().(n+1) = S(S,x,n) & g2().(n+1) = A(S,A,x,n) & h2().(n+1) = o(x,n) by A4;
A13: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f2.0 & A = g2.0 & x = h2.0 & R[S, A, x, 0] by A1,A2;
A14: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f2.n & A = g2.n & R[S,A,h2.n,n] from CIRCCMB29sch13(A13
,A12,A11,A8);
A15: now
let n be Nat;
assume
A16: P[n];
ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
S st S = f1.n & A = g1.n by A10;
then
A17: h1.(n+1) = o(h1.n,n) by A3;
ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
S st S = f2.n & A = g2.n by A14;
hence P[n+1] by A4,A16,A17;
end;
A18: P[ 0 ] by A2;
for i being Nat holds P[i] from NAT_1:sch 2(A18,A15);
then
A19: for i being object st i in NAT holds h1.i = h2.i;
defpred P[Nat] means f1.$1 = f2.$1 & g1.$1 = g2.$1;
A20: h1 = h2 by A19,PBOOLE:3;
A21: now
let n be Nat;
assume
A22: P[n];
consider S being non empty ManySortedSign, A being non-empty MSAlgebra
over S such that
A23: S = f1.n & A = g1.n by A10;
A24: g1.(n+1) = A(S,A,h1.n,n) by A3,A23
.= g2.(n+1) by A4,A20,A22,A23;
f1.(n+1) = S(S,h1.n,n) by A3,A23
.= f2.(n+1) by A4,A20,A22,A23;
hence P[n+1] by A24;
end;
A25: P[ 0 ] by A2;
for i being Nat holds P[i] from NAT_1:sch 2(A25,A21);
then ( for i being object st i in NAT holds f1.i = f2.i)&
for i being object st i
in NAT holds g1.i = g2.i;
hence thesis by A19,PBOOLE:3;
end;
scheme :: CircSchR2
CIRCCMB29sch15 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object, o(object,object) -> object,
f,g,h() -> ManySortedSet of NAT}: for n being
Nat, S being non empty ManySortedSign, x being set st S = f().n & x = h().n
holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n)
provided
A1: f().0 = S0() & g().0 = A0() and
A2: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) and
A3: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A4: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
x being set st S = f().0 & A = g().0 & x = h().0 & R[S,A,x,0] by A1;
let n be Nat, S be non empty ManySortedSign, x be set;
A5: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f().n & A = g().n & x = h().n & R[S,A,x
,n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A6: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
,n) by A3;
A7: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) by A2;
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f().n & A = g().n & R[S,A,h().n,n] from CIRCCMB29sch13(
A4,A7,A5, A6);
then
A8: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f().n & A = g().n;
assume S = f().n & x = h().n;
hence thesis by A2,A8;
end;
scheme :: CircuitExSch1
CIRCCMB29sch16 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object, o(object,object) -> object,
n() -> Nat}: ex S being non empty
ManySortedSign, A being non-empty MSAlgebra over S, f,g,h being ManySortedSet
of NAT st S = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n
being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+
1) = A(S,A,x,n) & h.(n+1) = o(x,n)
provided
A1: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
,n) by A1;
consider f,g,h being ManySortedSet of NAT such that
A3: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A4: for n being Nat, S being non empty ManySortedSign, 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) =
S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A5: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A6: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A3;
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A6,A4,
A5,A2);
then consider
S being non empty ManySortedSign, A being non-empty MSAlgebra over
S such that
A7: S = f.n() & A = g.n();
take S,A,f,g,h;
thus thesis by A3,A4,A7;
end;
scheme :: CircuitExSch2
CIRCCMB29sch17 {S0,Sn() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object, n() -> Nat}: ex A being non-empty
MSAlgebra over Sn(), f,g,h being ManySortedSet of NAT st Sn() = f.n() & A = g.n
() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o
(x,n)
provided
A1: ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) and
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A3: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
,n) by A2;
consider f,g,h being ManySortedSet of NAT such that
A4: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A5: for n being Nat, S being non empty ManySortedSign, 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) =
S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A6: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A7: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A8: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A4;
A9: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A8,A5
,A7,A3);
A10: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A4;
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A10,A5
,A6,A3);
then consider
S being non empty ManySortedSign, A being non-empty MSAlgebra over
S such that
A11: S = f.n() and
A12: A = g.n();
consider f1,h1 being ManySortedSet of NAT such that
A13: Sn() = f1.n() and
A14: f1.0 = S0() and
A15: h1.0 = o0() and
A16: for n being Nat, S being non empty ManySortedSign, x being set st S
= f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n) by A1;
A17: for n being Nat, S being non empty ManySortedSign, x being set st S =
f1.n & x = h1.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
defpred P[Nat] means h1.$1 = h.$1;
A18: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
& Pl[S,x,0] by A14;
A19: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
h1.n,n] from CIRCCMB29sch2(A18,A16,A17);
A20: now
let n be Nat;
assume
A21: P[n];
ex S being non empty ManySortedSign st S = f1.n by A19;
then
A22: h1.(n+1) = o(h1.n,n) by A16;
ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
S st S = f.n & A = g.n by A9;
hence P[n+1] by A5,A21,A22;
end;
A23: P[ 0 ] by A4,A15;
A24: for i being Nat holds P[i] from NAT_1:sch 2(A23,A20);
defpred P[Nat] means f1.$1 = f.$1;
for i being object st i in NAT holds h1.i = h.i by A24;
then
A25: h1 = h by PBOOLE:3;
A26: now
let n be Nat;
consider S being non empty ManySortedSign, A being non-empty MSAlgebra
over S such that
A27: S = f.n and
A28: A = g.n by A9;
assume P[n];
then f1.(n+1) = S(S,h1.n,n) by A16,A27
.= f.(n+1) by A5,A25,A27,A28;
hence P[n+1];
end;
A29: P[ 0 ] by A4,A14;
A30: for i being Nat holds P[i] from NAT_1:sch 2(A29,A26);
then for i being object st i in NAT holds f1.i = f.i;
then f1 = f by PBOOLE:3;
then reconsider A as non-empty MSAlgebra over Sn() by A13,A11;
take A,f,g,h;
thus thesis by A4,A5,A13,A30,A12;
end;
scheme :: CircuitUniqSch
CIRCCMB29sch18 {S0,Sn() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object, n() -> Nat}:
for A1,A2 being
non-empty MSAlgebra over Sn() st (ex f,g,h being ManySortedSet of NAT st Sn() =
f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S
being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x
,n) & h.(n+1) = o(x,n)) & (ex f,g,h being ManySortedSet of NAT st Sn() = f.n()
& A2 = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being
non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h
.(n+1) = o(x,n)) holds A1 = A2
provided
A1: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
,n) by A1;
let A1,A2 be non-empty MSAlgebra over Sn();
given f1,g1,h1 being ManySortedSet of NAT such that
Sn() = f1.n() and
A3: A1 = g1.n() and
A4: f1.0 = S0() & g1.0 = A0() and
A5: h1.0 = o0() and
A6: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f1.n & A = g1.n & x = h1.n holds f1.(n+
1) = S(S,x,n) & g1.(n+1) = A(S,A,x,n) & h1.(n+1) = o(x,n);
A7: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f1.0 & A = g1.0 by A4;
given f2,g2,h2 being ManySortedSet of NAT such that
Sn() = f2.n() and
A8: A2 = g2.n() and
A9: f2.0 = S0() & g2.0 = A0() & h2.0 = o0() and
A10: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f2.n & A = g2.n & x = h2.n holds f2.(n+
1) = S(S,x,n) & g2.(n+1) = A(S,A,x,n) & h2.(n+1) = o(x,n);
A11: f1.0 = f2.0 & g1.0 = g2.0 & h1.0 = h2.0 by A4,A5,A9;
f1 = f2 & g1 = g2 & h1 = h2 from CIRCCMB29sch14(A7,A11,A6,A10, A2);
hence thesis by A3,A8;
end;
scheme
CIRCCMB29sch19 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(), S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object, o0()-> object,
o(object,object) -> object, n() -> Nat}:
ex A being Boolean gate`2=den strict
Circuit of Sn(), f,g,h being ManySortedSet of NAT st Sn() = f.n() & A = g.n() &
f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o
(x,n)
provided
A1: for S being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, x being set, n being Nat holds S(S,x,n) is unsplit
gate`1=arity gate`2isBoolean non void strict and
A2: ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) and
A3: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n) and
A4: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S for x
being set, n being Nat st S1 = S(S,x,n) holds A(S,A,x,n) is Boolean gate`2=den
strict Circuit of S1
proof
A5: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
,n) by A3;
defpred P[object,object,Nat] means
ex S being unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign, A being Boolean gate`2=den strict
Circuit of S st S = $1 & A = $2;
consider f,g,h being ManySortedSet of NAT such that
A6: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A7: for n being Nat, S being non empty ManySortedSign, 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) =
S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A8: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A9: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A6;
A10: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A9,A7
,A8,A5);
defpred R[object,object,object,Nat] means P[$1,$2,$4];
A11: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1]
proof
let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over
S;
let x be set;
assume that
S = f.n and
A = g.n and
x = h.n and
A12: P[S,A,n];
reconsider S as unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign by A12;
reconsider A as Boolean gate`2=den strict Circuit of S by A12;
reconsider S1 = S(S,x,n) as unsplit gate`1=arity gate`2isBoolean non void
non empty strict non empty ManySortedSign by A1;
A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1 by A4;
hence thesis;
end;
A13: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A6;
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A13,A7
,A11,A5);
then consider
S being non empty ManySortedSign, A being non-empty MSAlgebra over
S such that
A14: S = f.n() and
A15: A = g.n() and
A16: P[S,A,n()];
consider f1,h1 being ManySortedSet of NAT such that
A17: Sn() = f1.n() and
A18: f1.0 = S0() and
A19: h1.0 = o0() and
A20: for n being Nat, S being non empty ManySortedSign, x being set st S
= f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n) by A2;
A21: for n being Nat, S being non empty ManySortedSign, x being set st S =
f1.n & x = h1.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
defpred P[Nat] means h1.$1 = h.$1;
A22: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
& Pl[S,x,0] by A18;
A23: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
h1.n,n] from CIRCCMB29sch2(A22,A20,A21);
A24: now
let n be Nat;
assume
A25: P[n];
ex S being non empty ManySortedSign st S = f1.n by A23;
then
A26: h1.(n+1) = o(h1.n,n) by A20;
ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
S st S = f.n & A = g.n by A10;
hence P[n+1] by A7,A25,A26;
end;
A27: P[ 0 ] by A6,A19;
A28: for i being Nat holds P[i] from NAT_1:sch 2(A27,A24);
defpred P[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;
A30: now
let n be Nat;
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 P[n];
then f1.(n+1) = S(S,h1.n,n) by A20,A31
.= f.(n+1) by A7,A29,A31,A32;
hence P[n+1];
end;
A33: P[ 0 ] by A6,A18;
A34: for i being Nat holds P[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 as Boolean gate`2=den strict Circuit of Sn() by A17,A14,A16
;
take A,f,g,h;
thus thesis by A6,A7,A17,A34,A15;
end;
definition
let S be non empty ManySortedSign;
let A be object such that
A1: A is non-empty MSAlgebra over S;
func MSAlg(A,S) -> non-empty MSAlgebra over S means
:Def1:
it = A;
existence by A1;
uniqueness;
end;
scheme :: ManyCellCircuitExSch
CIRCCMB29sch20 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(),
S(object,object) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign, A(object,object) -> object, o0()-> object,
o(object,object) -> object, n() -> Nat}:
ex A being Boolean gate`2=den strict Circuit of Sn(), f,g,h being ManySortedSet
of NAT st Sn() = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for
n being Nat, S being non empty ManySortedSign, A1 being non-empty MSAlgebra
over S for x being set, A2 being non-empty MSAlgebra over S(x,n) st S = f.n &
A1 = g.n & x = h.n & A2 = A(x,n) holds f.(n+1) = S +* S(x,n) & g.(n+1) = A1 +*
A2 & h.(n+1) = o(x,n)
provided
A1: ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x,n) and
A2: for x being set, n being Nat holds A(x,n) is Boolean gate`2=den
strict Circuit of S(x,n)
proof
deffunc Sl(non empty ManySortedSign,set,set) = $1+*S($2,$3);
consider f1,h1 being ManySortedSet of NAT such that
A3: Sn() = f1.n() and
A4: f1.0 = S0() and
A5: h1.0 = o0() and
A6: for n being Nat, S being non empty ManySortedSign, x being set st S
= f1.n & x = h1.n holds f1.(n+1) = Sl(S,x,n) & h1.(n+1) = o(x,n) by A1;
defpred P[object,object,Nat] means $3 <> 0 implies
ex S being unsplit gate`1=arity
gate`2isBoolean non void strict non empty ManySortedSign, A being Boolean
gate`2=den strict Circuit of S st S = $1 & A = $2;
deffunc Al(non empty ManySortedSign,non-empty MSAlgebra over $1, set,set) =
$2+*MSAlg(A($3,$4),S($3,$4));
A7: for S being non empty ManySortedSign, A being non-empty MSAlgebra over
S for x being set, n being Nat holds Al(S,A,x,n) is non-empty MSAlgebra over Sl
(S,x,n);
A8: for n being Nat, S being non empty ManySortedSign, x being set st S =
f1.n & x = h1.n & Pl[S,x,n] holds Pl[Sl(S,x,n), o(x,n), n+1];
consider f,g,h being ManySortedSet of NAT such that
A9: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A10: for n being Nat, S being non empty ManySortedSign, 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) =
Sl(S,x,n) & g.(n+1) = Al(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A11: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
holds R[Sl(S,x,n), Al(S,A,x,n), o(x, n), n+1];
A12: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A9;
A13: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A12,
A10
,A11,A7);
defpred P[Nat] means h1.$1 = h.$1;
A14: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
& Pl[S,x,0] by A4;
A15: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
h1.n,n] from CIRCCMB29sch2(A14,A6,A8);
A16: now
let n be Nat;
assume
A17: P[n];
ex S being non empty ManySortedSign st S = f1.n by A15;
then
A18: h1.(n+1) = o(h1.n,n) by A6;
ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
S st S = f.n & A = g.n by A13;
hence P[n+1] by A10,A17,A18;
end;
A19: P[ 0 ] by A9,A5;
A20: for i being Nat holds P[i] from NAT_1:sch 2(A19,A16);
defpred P[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;
A22: now
let n be Nat;
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 P[n];
then f1.(n+1) = S+*S(h1.n,n) by A6,A23
.= f.(n+1) by A10,A21,A23,A24;
hence P[n+1];
end;
defpred R[object,object,object,Nat] means P[$1,$2,$4];
A25: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
holds R[Sl(S,x,n), Al(S,A,x,n), o(x, n), n+1]
proof
let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over
S;
let x be set;
assume that
A26: S = f.n & A = g.n and
x = h.n and
A27: P[S,A,n] and
n+1 <> 0;
per cases;
suppose
A28: n = 0;
reconsider A2 = A(x,0) as Boolean gate`2=den strict Circuit of S(x,0) by
A2;
A0()+*MSAlg(A(x,0),S(x,0)) = A0()+*A2 by Def1;
hence thesis by A9,A26,A28;
end;
suppose
A29: n <> 0;
then reconsider
S as unsplit gate`1=arity gate`2isBoolean non void non empty
strict non empty ManySortedSign by A27;
reconsider A as Boolean gate`2=den strict Circuit of S by A27,A29;
reconsider A9 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n) by
A2;
A+*MSAlg(A(x,n),S(x,n)) = A+*A9 by Def1;
hence thesis;
end;
end;
A30: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A9;
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A30,
A10
,A25,A7);
then consider
S being non empty ManySortedSign, A being non-empty MSAlgebra over
S such that
A31: S = f.n() and
A32: A = g.n() and
A33: P[S,A,n()];
A34: P[ 0 ] by A9,A4;
A35: for i being Nat holds P[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 as Boolean gate`2=den strict Circuit of Sn() by A9,A3,A31
,A32,A33;
take A,f,g,h;
thus Sn() = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() by A9,A3
,A35,A32;
let n being Nat, S being non empty ManySortedSign, A1 being non-empty
MSAlgebra over S;
let x being set, A2 being non-empty MSAlgebra over S(x,n);
assume
A36: S = f.n & A1 = g.n & x = h.n & A2 = A(x,n);
A2 = MSAlg(A2, S(x,n)) by Def1;
hence thesis by A10,A36;
end;
scheme :: attrCircuitUniqSch
CIRCCMB29sch21 {S0() -> non empty ManySortedSign, Sn() -> unsplit
gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A0() ->
non-empty MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object, n() -> Nat}:
for A1,A2 being Boolean gate`2=den strict Circuit of Sn() st
(ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h
.0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) & (ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A2 = g.n() & f.0 = S0() & g.0 = A0() & h
.0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) holds A1 = A2
provided
A1: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
,n) by A1;
for A1,A2 being non-empty MSAlgebra over Sn() st (ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h
.0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) & (ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A2 = g.n() & f.0 = S0() & g.0 = A0() & h
.0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) holds A1 = A2
from CIRCCMB29sch18(A2);
hence thesis;
end;
begin :: Correctness of Many Cell Circuit
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for C1 being non-empty
Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
of S st C1 tolerates C2 & C = C1+*C2 for s2 being State of C2 for s being State
of C st s2 = s|the carrier of S2 holds Following s2 = (Following s)|the carrier
of S2
proof
let S1,S2,S be non void Circuit-likenon empty ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2 & S = S1+*S2;
let C1 be non-empty Circuit of S1;
let C2 be non-empty Circuit of S2;
let C be non-empty Circuit of S such that
A2: C1 tolerates C2 and
A3: C = C1+*C2;
let s2 be State of C2;
let s be State of C such that
A4: s2 = s|the carrier of S2;
the Sorts of C1 tolerates the Sorts of C2 by A2,CIRCCOMB:def 3;
then reconsider s1 = s|the carrier of S1 as State of C1 by A3,CIRCCOMB:26;
dom Following s2 = the carrier of S2 & Following s = (Following s1)+*(
Following s2) by A1,A2,A3,A4,CIRCCOMB:32,CIRCUIT1:3;
hence thesis by FUNCT_4:23;
end;
theorem Th10:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for C1
being non-empty Circuit of S1, C2 being non-empty Circuit of S2 for C being
non-empty Circuit of S st C1 tolerates C2 & C = C1+*C2 for s1 being State of C1
for s being State of C st s1 = s|the carrier of S1 holds Following s1 = (
Following s)|the carrier of S1
proof
let S1,S2,S be non void Circuit-likenon empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
let C1 be non-empty Circuit of S1;
let C2 be non-empty Circuit of S2;
let C be non-empty Circuit of S such that
A2: C1 tolerates C2 and
A3: C = C1+*C2;
let s1 be State of C1;
let s be State of C such that
A4: s1 = s|the carrier of S1;
the Sorts of C1 tolerates the Sorts of C2 by A2,CIRCCOMB:def 3;
then reconsider s2 = s|the carrier of S2 as State of C2 by A3,CIRCCOMB:26;
dom Following s1 = the carrier of S1 & Following s = (Following s2)+*(
Following s1) by A1,A2,A3,A4,CIRCCOMB:33,CIRCUIT1:3;
hence thesis by FUNCT_4:23;
end;
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for C1 being non-empty
Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
of S st C1 tolerates C2 & C = C1+*C2 for s1 being State of C1 for s2 being
State of C2 for s being State of C st s1 = s|the carrier of S1 & s2 = s|the
carrier of S2 & s1 is stable & s2 is stable holds s is stable
proof
let S1,S2,S be non void Circuit-likenon empty ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2 and
A2: S = S1+*S2;
let C1 be non-empty Circuit of S1;
let C2 be non-empty Circuit of S2;
let C be non-empty Circuit of S such that
A3: C1 tolerates C2 & C = C1+*C2;
let s1 be State of C1;
let s2 be State of C2;
let s be State of C such that
A4: s1 = s|the carrier of S1 & s2 = s|the carrier of S2 and
A5: s1 is stable and
A6: s2 is stable;
dom s = the carrier of S & the carrier of S = (the carrier of S1) \/ the
carrier of S2 by A2,CIRCCOMB:def 2,CIRCUIT1:3;
then s = s1+*s2 by A4,FUNCT_4:70;
then s = (Following s1) +* s2 by A5
.= (Following s1) +* (Following s2) by A6
.= Following s by A1,A2,A3,A4,CIRCCOMB:32;
hence s = Following s;
end;
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for C1 being non-empty
Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
of S st C1 tolerates C2 & C = C1+*C2 for s1 being State of C1 for s2 being
State of C2 for s being State of C st s1 = s|the carrier of S1 & s2 = s|the
carrier of S2 & s1 is stable & s2 is stable holds s is stable
proof
let S1,S2,S be non void Circuit-likenon empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1+*S2;
let C1 be non-empty Circuit of S1;
let C2 be non-empty Circuit of S2;
let C be non-empty Circuit of S such that
A3: C1 tolerates C2 & C = C1+*C2;
let s1 be State of C1;
let s2 be State of C2;
let s be State of C such that
A4: s1 = s|the carrier of S1 & s2 = s|the carrier of S2 and
A5: s1 is stable and
A6: s2 is stable;
dom s = the carrier of S & the carrier of S = (the carrier of S1) \/ the
carrier of S2 by A2,CIRCCOMB:def 2,CIRCUIT1:3;
then s = s2+*s1 by A4,FUNCT_4:70;
then s = (Following s2) +* s1 by A6
.= (Following s2) +* (Following s1) by A5
.= Following s by A1,A2,A3,A4,CIRCCOMB:33;
hence s = Following s;
end;
theorem Th13:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A,
s1 be State of A1 st s1 = s|the carrier of S1
for n being natural Number holds
Following(s, n)|the carrier of S1 = Following(s1, n)
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A2: A1 tolerates A2 & A = A1+*A2;
let s be State of A, s1 be State of A1 such that
A3: s1 = s|the carrier of S1;
let n be natural Number;
A0: n is Nat by TARSKI:1;
defpred P[Nat] means Following(s, $1)|the carrier of S1 = Following(s1, $1);
A4: now
let n be Nat;
A5: Following(s, n+1) = Following Following(s, n) & Following Following(s1
, n) = Following(s1, n+1) by FACIRC_1:12;
assume P[n];
hence P[n+1] by A1,A2,A5,Th10;
end;
Following(s, 0)|the carrier of S1 = s1 by A3,FACIRC_1:11
.= Following(s1, 0) by FACIRC_1:11;
then
A6: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A6,A4);
hence thesis by A0;
end;
theorem Th14:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S2 misses InnerVertices S1 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A,
s2 be State of A2 st s2 = s|the carrier of S2 for n being Nat holds Following(s
, n)|the carrier of S2 = Following(s2, n)
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S2 misses InnerVertices S1 and
A2: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A3: A1 tolerates A2 and
A4: A = A1+*A2;
S1 tolerates S2 by A3,CIRCCOMB:def 3;
then
A5: S = S2+*S1 by A2,CIRCCOMB:5;
A = A2+*A1 by A3,A4,CIRCCOMB:22;
hence thesis by A1,A3,A5,Th13,CIRCCOMB:19;
end;
theorem Th15:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A
for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is stable for s2
being State of A2 st s2 = s|the carrier of S2 holds (Following s)|the carrier
of S2 = Following s2
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1+*S2;
A3: the carrier of S = (the carrier of S1)\/the carrier of S2 by A2,
CIRCCOMB:def 2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A4: A1 tolerates A2 and
A5: A = A1+*A2;
let s be State of A;
let s1 be State of A1 such that
A6: s1 = s|the carrier of S1 and
A7: s1 is stable;
let s2 be State of A2 such that
A8: s2 = s|the carrier of S2;
A9: now
let a be object;
assume a in the carrier of S2;
then reconsider v = a as Vertex of S2;
reconsider vv = v as Vertex of S by A3,XBOOLE_0:def 3;
A10: v in InputVertices S2 & not v in InnerVertices S1 implies v in (
InputVertices S2)\InnerVertices S1 by XBOOLE_0:def 5;
A11: S1 tolerates S2 by A4,CIRCCOMB:def 3;
A12: now
assume that
A13: v in InputVertices S2 and
A14: v in InnerVertices S1;
reconsider v1 = v as Vertex of S1 by A14;
thus (Following s).vv = (Following s1).vv by A2,A4,A5,A6,A14,CIRCCOMB:31
.= s1.v by A7
.= s.v1 by A6,FUNCT_1:49
.= s2.v by A8,FUNCT_1:49
.= (Following s2).vv by A13,CIRCUIT2:def 5;
end;
the carrier of S2 = InnerVertices S2 \/ InputVertices S2 & (
InputVertices S1 )\InnerVertices S2 = InputVertices S1 by A1,XBOOLE_1:45,83;
then v in InnerVertices S2 or v in InputVertices S2 & (v in InnerVertices
S1 or not v in InnerVertices S1) & InputVertices S = (InputVertices S1)\/((
InputVertices S2)\InnerVertices S1) by A2,A11,Th5,XBOOLE_0:def 3;
then
A15: vv in InnerVertices S2 or v in InputVertices S or v in InputVertices
S2 & v in InnerVertices S1 by A10,XBOOLE_0:def 3;
thus ((Following s)|the carrier of S2).a = (Following s).v by FUNCT_1:49
.= (Following s2).a by A2,A4,A5,A8,A12,A15,CIRCCOMB:31;
end;
dom Following s = the carrier of S by CIRCUIT1:3;
then dom Following s2 = the carrier of S2 & dom ((Following s)|the carrier
of S2) = the carrier of S2 by A3,CIRCUIT1:3,RELAT_1:62,XBOOLE_1:7;
hence thesis by A9,FUNCT_1:2;
end;
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of
S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s
being State of A for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is
stable for s2 being State of A2 st s2 = s|the carrier of S2 & s2 is stable
holds s is stable
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
S1 tolerates S2 by A2,CIRCCOMB:def 3;
then
A4: InnerVertices S = (InnerVertices S1) \/ InnerVertices S2 by A1,CIRCCOMB:11;
let s be State of A;
let s1 be State of A1 such that
A5: s1 = s|the carrier of S1 and
A6: s1 = Following s1;
let s2 be State of A2 such that
A7: s2 = s|the carrier of S2 and
A8: s2 = Following s2;
A9: the carrier of S = (the carrier of S1) \/ the carrier of S2 by A1,
CIRCCOMB:def 2;
A10: now
let x be object;
assume x in the carrier of S;
then reconsider v = x as Vertex of S;
the carrier of S = (InputVertices S) \/ InnerVertices S by XBOOLE_1:45;
then v in InputVertices S or v in InnerVertices S by XBOOLE_0:def 3;
then
v in InputVertices S & v in the carrier of S1 or v in InputVertices S
& v in the carrier of S2 or v in InnerVertices S1 or v in InnerVertices S2 by
A4,A9,XBOOLE_0:def 3;
then (Following s).v = s1.v & v in the carrier of S1 or (Following s).v =
s2.v & v in the carrier of S2 by A1,A2,A3,A5,A6,A7,A8,CIRCCOMB:31;
hence s.x = (Following s).x by A5,A7,FUNCT_1:49;
end;
dom Following s = the carrier of S & dom s = the carrier of S by CIRCUIT1:3;
hence s = Following s by A10,FUNCT_1:2;
end;
theorem Th17:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
A = A1+*A2 for s being State of A st s is stable holds (for s1 being State of
A1 st s1 = s|the carrier of S1 holds s1 is stable) & (for s2 being State of A2
st s2 = s|the carrier of S2 holds s2 is stable)
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2;
A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by A1,
CIRCCOMB:def 2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A3: A1 tolerates A2 & A = A1+*A2;
let s be State of A such that
A4: s = Following s;
hereby
let s1 be State of A1 such that
A5: s1 = s|the carrier of S1;
A6: now
let x be object;
assume x in the carrier of S1;
then reconsider v = x as Vertex of S1;
reconsider v9 = v as Vertex of S by A2,XBOOLE_0:def 3;
the carrier of S1 = (InputVertices S1) \/ InnerVertices S1 by XBOOLE_1:45
;
then v in InputVertices S1 or v9 in InnerVertices S1 by XBOOLE_0:def 3;
then s1.v = (Following s1).v or s.v9 = (Following s1).v by A1,A3,A4,A5,
CIRCCOMB:31,CIRCUIT2:def 5;
hence s1.x = (Following s1).x by A5,FUNCT_1:49;
end;
dom s1 = the carrier of S1 & dom Following s1 = the carrier of S1 by
CIRCUIT1:3;
then s1 = Following s1 by A6,FUNCT_1:2;
hence s1 is stable;
end;
let s2 be State of A2 such that
A7: s2 = s|the carrier of S2;
A8: now
let x be object;
assume x in the carrier of S2;
then reconsider v = x as Vertex of S2;
reconsider v9 = v as Vertex of S by A2,XBOOLE_0:def 3;
the carrier of S2 = (InputVertices S2) \/ InnerVertices S2 by XBOOLE_1:45;
then v in InputVertices S2 or v9 in InnerVertices S2 by XBOOLE_0:def 3;
then s2.v = (Following s2).v or s.v9 = (Following s2).v by A1,A3,A4,A7,
CIRCCOMB:31,CIRCUIT2:def 5;
hence s2.x = (Following s2).x by A7,FUNCT_1:49;
end;
dom s2 = the carrier of S2 & dom Following s2 = the carrier of S2 by
CIRCUIT1:3;
hence s2 = Following s2 by A8,FUNCT_1:2;
end;
theorem Th18:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s1 being State of A1
, s2 being State of A2, s being State of A st s1 = s|the carrier of S1 & s2 = s
|the carrier of S2 & s1 is stable for n being Nat holds Following(s, n)|the
carrier of S2 = Following(s2, n)
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
let s1 be State of A1, s2 be State of A2, s be State of A such that
A4: s1 = s|the carrier of S1 and
A5: s2 = s|the carrier of S2 and
A6: s1 is stable;
defpred P[Nat] means Following(s,$1)|the carrier of S2 = Following(s2,$1);
A7: now
let n be Nat;
A8: Following(s, n+1) = Following Following(s, n) & Following Following(
s2, n) = Following(s2, n+1) by FACIRC_1:12;
the Sorts of A1 tolerates the Sorts of A2 by A2,CIRCCOMB:def 3;
then reconsider
Fs1 = Following(s, n)|the carrier of S1 as State of A1 by A3,CIRCCOMB:26;
Following(s1, n) = Fs1 by A1,A2,A3,A4,Th13;
then
A9: Fs1 is stable by A6,Th3;
assume P[n];
hence P[n+1] by A1,A2,A3,A8,A9,Th15;
end;
Following(s, 0)|the carrier of S2 = s2 by A5,FACIRC_1:11
.= Following(s2, 0) by FACIRC_1:11;
then
A10: P[ 0 ];
thus for n being Nat holds P[n] from NAT_1:sch 2(A10,A7);
end;
theorem Th19:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for n1,n2 being Nat for
s being State of A for s1 being State of A1, s2 being State of A2 st s1 = s|the
carrier of S1 & Following(s1, n1) is stable & s2 = Following(s, n1)|the carrier
of S2 & Following(s2, n2) is stable holds Following(s, n1+n2) is stable
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A3: A1 tolerates A2 and
A4: A = A1+*A2;
let n1,n2 be Nat;
let s be State of A, s9 be State of A1, s99 be State of A2 such that
A5: s9 = s|the carrier of S1 & Following(s9, n1) is stable and
A6: s99 = Following(s, n1)|the carrier of S2 & Following(s99, n2) is stable;
A7: the Sorts of A1 tolerates the Sorts of A2 by A3,CIRCCOMB:def 3;
then reconsider
s1 = Following(s, n1)|the carrier of S1, s0 = s|the carrier of S1
as State of A1 by A4,CIRCCOMB:26;
A8: Following(Following(s, n1), n2) = Following(s, n1+n2) by FACIRC_1:13;
then
A9: Following(s, n1+n2)|the carrier of S1 = Following(s1, n2) by A1,A2,A3,A4
,Th13;
reconsider s2 = Following(s, n1)|the carrier of S2 as State of A2 by A4,A7,
CIRCCOMB:26;
A10: dom Following(s, n1+n2) = the carrier of S by CIRCUIT1:3;
A11: the carrier of S = (the carrier of S1)\/the carrier of S2 by A2,
CIRCCOMB:def 2;
A12: s1 = Following(s0, n1) by A1,A2,A3,A4,Th13;
then
A13: Following(s, n1+n2)|the carrier of S2 = Following(s2, n2) by A1,A2,A3,A4
,A5,A8,Th18;
then Following Following(s, n1+n2) = (Following Following(s2, n2))+*
Following Following(s1, n2) by A1,A2,A3,A4,A9,CIRCCOMB:33
.= Following(s2, n2)+*Following Following(s1, n2) by A6
.= Following(s2, n2)+*Following(s1, n2+1) by FACIRC_1:12
.= Following(s2, n2)+*s1 by A5,A12,Th3
.= Following(s2, n2)+*Following(s1, n2) by A5,A12,Th3
.= Following(s, n1+n2) by A11,A10,A9,A13,FUNCT_4:70;
hence thesis;
end;
theorem Th20:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for n1,n2 being Nat st (
for s being State of A1 holds Following(s, n1) is stable) & (for s being State
of A2 holds Following(s, n2) is stable) for s being State of A holds Following(
s, n1+n2) is stable
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
let n1,n2 be Nat such that
A4: ( for s being State of A1 holds Following(s, n1) is stable)& for s
being State of A2 holds Following(s, n2) is stable;
let s be State of A;
A5: the Sorts of A1 tolerates the Sorts of A2 by A2,CIRCCOMB:def 3;
then reconsider s1 = s|the carrier of S1 as State of A1 by A3,CIRCCOMB:26;
reconsider s2 = Following(s,n1)|the carrier of S2 as State of A2 by A3,A5,
CIRCCOMB:26;
Following(s1,n1) is stable & Following(s2,n2) is stable by A4;
hence thesis by A1,A2,A3,Th19;
end;
theorem Th21:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2
misses InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2
being non-empty Circuit of S2 for A being non-empty Circuit of S st A1
tolerates A2 & A = A1+*A2 for s being State of A for s1 being State of A1 st s1
= s|the carrier of S1 for s2 being State of A2 st s2 = s|the carrier of S2
for n being natural Number holds
Following(s, n) = Following(s1, n)+*Following(s2, n)
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: InputVertices S2 misses InnerVertices S1 and
A3: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A4: A1 tolerates A2 and
A5: A = A1+*A2;
let s be State of A;
let s1 be State of A1 such that
A6: s1 = s|the carrier of S1;
let s2 be State of A2 such that
A7: s2 = s|the carrier of S2;
let n be natural Number;
A8: Following(s, n)|the carrier of S1 = Following(s1, n) by A1,A3,A4,A5,A6,Th13
;
A9: dom Following(s, n) = the carrier of S & the carrier of S = (the
carrier of S1) \/ the carrier of S2 by A3,CIRCCOMB:def 2,CIRCUIT1:3;
S1 tolerates S2 by A4,CIRCCOMB:def 3;
then
A10: S1+*S2 = S2+*S1 by CIRCCOMB:5;
A1+*A2 = A2+*A1 by A4,CIRCCOMB:22;
then Following(s, n)|the carrier of S2 = Following(s2, n) by A2,A3,A4,A5,A7
,A10,Th13,CIRCCOMB:19;
hence thesis by A8,A9,FUNCT_4:70;
end;
theorem Th22:
for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2
misses InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2
being non-empty Circuit of S2 for A being non-empty Circuit of S st A1
tolerates A2 & A = A1+*A2 for n1,n2 being Nat, s being State of A for s1 being
State of A1 st s1 = s|the carrier of S1 for s2 being State of A2 st s2 = s|the
carrier of S2 & Following(s1, n1) is stable & Following(s2, n2) is stable holds
Following(s, max(n1,n2)) is stable
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: InputVertices S2 misses InnerVertices S1 and
A3: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A4: A1 tolerates A2 and
A5: A = A1+*A2;
let n1,n2 be Nat;
let s be State of A;
set n = max(n1,n2);
let s0 be State of A1 such that
A6: s0 = s|the carrier of S1;
A7: Following(s, n)|the carrier of S1 = Following(s0, n) by A1,A3,A4,A5,A6,Th13
;
S1 tolerates S2 by A4,CIRCCOMB:def 3;
then
A8: S1+*S2 = S2+*S1 by CIRCCOMB:5;
let s3 be State of A2 such that
A9: s3 = s|the carrier of S2 and
A10: Following(s0, n1) is stable and
A11: Following(s3, n2) is stable;
A1+*A2 = A2+*A1 by A4,CIRCCOMB:22;
then
A12: Following(s, n)|the carrier of S2 = Following(s3, n) by A2,A3,A4,A5,A9,A8
,Th13,CIRCCOMB:19;
A13: Following(s3, n) is stable by A11,Th4,XXREAL_0:25;
A14: Following(s0, n) is stable by A10,Th4,XXREAL_0:25;
thus Following(s, max(n1,n2)) = Following(s0, n)+*Following(s3, n) by A1,A2
,A3,A4,A5,A6,A9,Th21
.= (Following Following(s0, n))+*Following(s3, n) by A14
.= (Following Following(s0, n))+*Following Following(s3, n) by A13
.= Following Following(s, n) by A2,A3,A4,A5,A7,A12,CIRCCOMB:32;
end;
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
A = A1+*A2 for n being Nat, s being State of A for s1 being State of A1 st s1 =
s|the carrier of S1 for s2 being State of A2 st s2 = s|the carrier of S2 & (
Following(s1, n) is not stable or Following(s2, n) is not stable) holds
Following(s, n) is not stable
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: InputVertices S2 misses InnerVertices S1 and
A3: S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A4: A1 tolerates A2 & A = A1+*A2;
let n be Nat;
let s be State of A;
let s0 be State of A1;
assume s0 = s|the carrier of S1;
then
A5: Following(s, n)|the carrier of S1 = Following(s0, n) by A1,A3,A4,Th13;
let s3 be State of A2 such that
A6: s3 = s|the carrier of S2 and
A7: Following(s0, n) is not stable or Following(s3, n) is not stable;
Following(s, n)|the carrier of S2 = Following(s3, n) by A2,A3,A4,A6,Th14;
hence thesis by A3,A4,A7,A5,Th17;
end;
theorem
for S1,S2,S being non void Circuit-like non empty ManySortedSign st
InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
A = A1+*A2 for n1,n2 being Nat st (for s being State of A1 holds Following(s,
n1) is stable) & (for s being State of A2 holds Following(s, n2) is stable) for
s being State of A holds Following(s, max(n1,n2)) is stable
proof
let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
InnerVertices S1 & S = S1+*S2;
let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
let n1,n2 be Nat such that
A4: ( for s being State of A1 holds Following(s, n1) is stable)& for s
being State of A2 holds Following(s, n2) is stable;
let s be State of A;
A5: the Sorts of A1 tolerates the Sorts of A2 by A2,CIRCCOMB:def 3;
then reconsider s0 = s|the carrier of S1 as State of A1 by A3,CIRCCOMB:26;
reconsider s3 = s|the carrier of S2 as State of A2 by A3,A5,CIRCCOMB:26;
Following(s0, n1) is stable & Following(s3, n2) is stable by A4;
hence thesis by A1,A2,A3,Th22;
end;
scheme
CIRCCMB29sch22 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(), An() -> Boolean gate`2=den strict Circuit of Sn(),
S(object,object) -> unsplit
gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign,
A(object,object) -> object, h() -> ManySortedSet of NAT,
o0()-> object, o(object,object) -> object, n(Nat)-> Nat}:
for s being State of An() holds Following(s, n(0)+n(2)*n(1)) is stable
provided
A1: for x being set, n being Nat holds A(x,n) is Boolean gate`2=den
strict Circuit of S(x,n) and
A2: for s being State of A0() holds Following(s, n(0)) is stable and
A3: for n being Nat, x being set for A being non-empty Circuit of S(x,n)
st x = h().(n) & A = A(x,n) for s being State of A holds Following(s, n(1)) is
stable and
A4: ex f,g being ManySortedSet of NAT st Sn() = f.n(2) & An() = g.n(2) &
f.0 = S0() & g.0 = A0() & h().0 = o0() & for n being Nat, S being non empty
ManySortedSign, A1 being non-empty MSAlgebra over S for x being set, A2 being
non-empty MSAlgebra over S(x,n) st S = f.n & A1 = g.n & x = h().n & A2 = A(x,n)
holds f.(n+1) = S +* S(x,n) & g.(n+1) = A1 +* A2 & h().(n+1) = o(x,n) and
A5: InnerVertices S0() is Relation & InputVertices S0() is without_pairs and
A6: h().0 = o0() & o0() in InnerVertices S0() and
A7: for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
A8: for n being Nat, x being set st x = h().(n) holds (InputVertices S(x
,n)) \ {x} is without_pairs and
A9: for n being Nat, x being set st x = h().(n) holds h().(n+1) = o(x,n)
& x in InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n)
proof
deffunc Al(non empty ManySortedSign,non-empty MSAlgebra over $1, set,set) =
$2+*MSAlg(A($3,$4),S($3,$4));
deffunc Sl(non empty ManySortedSign,set,set) = $1+*S($2,$3);
defpred Q[object,object,object,Nat] means ex S being unsplit gate`1=arity
gate`2isBoolean non void strict non empty ManySortedSign, A being Boolean
gate`2=den strict Circuit of S st $1 = S & $2 = A & $3 = h().$4 & for s being
State of A holds Following(s, n(0)+$4*n(1)) is stable;
deffunc h(set) = h().$1;
consider f,g being ManySortedSet of NAT such that
A10: Sn() = f.n(2) & An() = g.n(2) and
A11: f.0 = S0() and
A12: g.0 = A0() and
h().0 = o0() and
A13: for n being Nat, S being non empty ManySortedSign, A1 being
non-empty MSAlgebra over S for x being set, A2 being non-empty MSAlgebra over S
(x,n) st S = f.n & A1 = g.n & x = h().n & A2 = A(x,n) holds f.(n+1) = S +* S(x,
n) & g.(n+1) = A1 +* A2 & h().(n+1) = o(x,n) by A4;
deffunc f(set) = f.$1;
A14: for n being Nat, S being non empty ManySortedSign, 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)
= Sl(S,x,n) & g.(n+1) = Al(S,A,x,n) & h().(n+1) = o(x,n)
proof
let n be Nat, S be non empty ManySortedSign;
let A be non-empty MSAlgebra over S, x be set;
reconsider A2 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n)
by A1;
A2 = MSAlg(A(x,n),S(x,n)) by Def1;
hence thesis by A13;
end;
A15: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h().n & Q[S,A,x,n]
holds Q[Sl(S,x,n), Al(S,A,x,n), o(x,n), n+1]
proof
let n be Nat, S be non empty ManySortedSign;
let A being non-empty MSAlgebra over S, x being set such that
A16: S = f.n and
A = g.n and
x = h().n;
given S9 being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, A9 being Boolean gate`2=den strict Circuit of S9 such
that
A17: S = S9 and
A18: A = A9 and
A19: x = h().(n) and
A20: for s being State of A9 holds Following(s, n(0)+n*n(1)) is stable;
thus Q[S+*S(x,n), A+*MSAlg(A(x,n),S(x,n)), o(x,n), n+1]
proof
reconsider A2 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n) by
A1;
take S9+*S(x,n);
A21: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds Al(S,A,x,n) is non-empty MSAlgebra
over Sl(S,x,n);
A22: f.0 = S0() & g.0 = A0() by A11,A12;
for n being Nat, S being non empty ManySortedSign, x being set st S
= f.n & x = h().n holds f.(n+1) = Sl(S,x,n) & h().(n+1) = o(x,n) from
CIRCCMB29sch15(A22,A14,A21);
then
A23: for n being Nat, S being non empty ManySortedSign, x being set st S
= f(n) & x = h().n holds f(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n) by A9;
A9+*A2 = A+*MSAlg(A(x,n),S(x,n)) by A17,A18,Def1;
then reconsider
AA = A+*MSAlg(A(x,n),S(x,n)) as Boolean gate`2=den strict
Circuit of S9+*S(x,n);
take AA;
A24: n(0)+(n+1)*n(1) = n(0)+n*n(1)+n(1);
thus S9+*S(x,n) = S+*S(x,n) & A+*MSAlg(A(x,n),S(x,n)) = AA by A17;
thus o(x,n) = h(n+1) by A9,A19;
let s be State of AA;
A25: InnerVertices S0() is Relation by A5;
A26: for n being Nat, x being set st x = h().n holds (InputVertices S(x,
n)) \ {x} is without_pairs by A8;
A27: for n being Nat, x being set holds InnerVertices S(x,n) is Relation
by A7;
A28: InputVertices S0() is without_pairs by A5;
A29: f(0) = S0() & h().0 in InnerVertices S0() by A6,A11;
for n being Nat ex S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign st S1 = f(n) & S2 = f(n+1) & InputVertices S2
= (InputVertices S1)\/((InputVertices S(h().n,n)) \ {h().n}) & InnerVertices S1
is Relation & InputVertices S1 is without_pairs from CIRCCMB29sch10(A25,A28,A29
,A27,A26,A23);
then ex S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign st S1 = f.(n) & S2 = f.(n+1) & InputVertices S2 = (
InputVertices S1)\/((InputVertices S(h(n),n)) \ {h(n)}) & InnerVertices S1 is
Relation & InputVertices S1 is without_pairs;
then
A30: InputVertices S9 misses InnerVertices S(x,n) by A7,A16,A17,FACIRC_1:5;
A2 = MSAlg(A(x,n),S(x,n)) & for s being State of A2 holds Following
(s, n(1)) is stable by A3,A19,Def1;
hence Following(s, n(0)+(n+1)*n(1)) is stable by A17,A18,A20,A30,A24,Th20
,CIRCCOMB:60;
end;
end;
A31: for S being non empty ManySortedSign, A being non-empty MSAlgebra over
S for x being set, n being Nat holds Al(S,A,x,n) is non-empty MSAlgebra over Sl
(S,x,n);
A32: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
, x being set st S = f.0 & A = g.0 & x = h().0 & Q[S, A, x, 0] by A2,A11,A12;
for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & Q[S,A,h().n,n] from CIRCCMB29sch13(A32,
A14,A15,A31);
then
ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
st S = f.n(2) & A = g.n(2) & Q[S,A,h().n(2),n(2)];
hence thesis by A10;
end;