Copyright (c) 1995 Association of Mizar Users
environ
vocabulary BOOLE, RELAT_1, FUNCT_1, FINSEQ_1, CIRCCOMB, FINSEQ_2, MSUALG_1,
PARTFUN1, MSAFREE2, FUNCT_4, MARGREL1, MIDSP_3, BINARITH, ZF_LANG, AMI_1,
ZF_REFLE, CIRCUIT1, QC_LANG1, CARD_3, LATTICES, MCART_1, FINSET_1,
CIRCUIT2, CLASSES1, FACIRC_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
MCART_1, RELAT_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1,
FINSEQ_2, FUNCT_4, MARGREL1, BINARITH, CARD_3, CLASSES1, PARTFUN1,
MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, MIDSP_3;
constructors MCART_1, BINARITH, CLASSES1, CIRCUIT1, CIRCUIT2, CIRCCOMB,
ENUMSET1;
clusters NUMBERS, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, RELSET_1, FINSEQ_2,
PRVECT_1, MSUALG_1, PRE_CIRC, CIRCCOMB, FINSEQ_1, XREAL_0, ARYTM_3,
ORDINAL1, ZFMISC_1, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_1, MSAFREE2, CIRCUIT2, CIRCCOMB, XBOOLE_0;
theorems TARSKI, AXIOMS, NAT_1, ENUMSET1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4, ORDINAL1, FINSEQ_1, FINSEQ_2, MSUALG_1, MSAFREE2, CIRCUIT1,
CIRCUIT2, CIRCCOMB, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1, RECDEF_1, FUNCT_2;
begin :: Pairs, Set Without Pairs, and Nonpair-yielding Functions
definition let IT be set;
attr IT is pair means:
Def1:
ex x,y being set st IT = [x,y];
end;
definition
cluster pair -> non empty set;
coherence
proof let z be set; given x,y being set such that
A1: z = [x,y];
thus thesis by A1;
end;
end;
definition
let x,y be set;
cluster [x,y] -> pair;
coherence proof take x,y; thus thesis; end;
end;
definition
cluster pair set;
existence proof take [0,1]; take 0,1; thus thesis; end;
cluster non pair set;
existence
proof take {}; let x,y be set;
thus thesis;
end;
end;
definition
cluster -> non pair Nat;
coherence
proof let n be Nat; given x,y being set such that
A1: n = [x,y];
A2: n = {{x,y},{x}} & 0 = {} by A1,TARSKI:def 5;
n > 0 & n = {k where k is Nat: k < n} by A1,AXIOMS:30,NAT_1:18;
then 0 in n; hence contradiction by A2,TARSKI:def 2;
end;
end;
definition let IT be set;
attr IT is with_pair means:
Def2:
ex x being pair set st x in IT;
antonym IT is without_pairs;
end;
definition
cluster empty -> without_pairs set;
coherence
proof let x be set; assume
A1: x is empty;
let a be pair set; thus thesis by A1;
end;
let x be non pair set;
cluster {x} -> without_pairs;
coherence
proof let a be pair set; assume a in {x};
hence contradiction by TARSKI:def 1;
end;
let y be non pair set;
cluster {x,y} -> without_pairs;
coherence
proof let a be pair set; assume a in {x,y};
hence contradiction by TARSKI:def 2;
end;
let z be non pair set;
cluster {x,y,z} -> without_pairs;
coherence
proof let a be pair set; assume a in {x,y,z};
hence contradiction by ENUMSET1:13;
end;
end;
definition
cluster without_pairs (non empty set);
existence
proof consider x being non pair set;
take {x}; thus thesis;
end;
end;
definition
let X, Y be without_pairs set;
cluster X \/ Y -> without_pairs;
coherence
proof let a be pair set; assume a in X \/ Y;
then a in X or a in Y by XBOOLE_0:def 2;
hence contradiction by Def2;
end;
end;
definition
let X be without_pairs set, Y be set;
cluster X \ Y -> without_pairs;
coherence
proof let a be pair set; assume a in X \ Y;
then a in X by XBOOLE_0:def 4;
hence contradiction by Def2;
end;
cluster X /\ Y -> without_pairs;
coherence
proof let a be pair set; assume a in X /\ Y;
then a in X by XBOOLE_0:def 3;
hence contradiction by Def2;
end;
cluster Y /\ X -> without_pairs;
coherence
proof let a be pair set; assume a in Y /\ X;
then a in X by XBOOLE_0:def 3;
hence contradiction by Def2;
end;
end;
definition
let x be pair set;
cluster {x} -> Relation-like;
coherence
proof let a be set; assume a in {x}; then a = x by TARSKI:def 1;
hence ex x,y being set st a = [x,y] by Def1;
end;
let y be pair set;
cluster {x,y} -> Relation-like;
coherence
proof let a be set; assume a in {x,y}; then a = x or a = y by TARSKI:def 2
;
hence ex x,y being set st a = [x,y] by Def1;
end;
let z be pair set;
cluster {x,y,z} -> Relation-like;
coherence
proof let a be set; assume a in {x,y,z};
then a = x or a = y or a = z by ENUMSET1:13;
hence ex x,y being set st a = [x,y] by Def1;
end;
end;
definition
cluster without_pairs Relation-like -> empty set;
coherence
proof let x be set; assume
A1: not ex a being pair set st a in x;
assume
A2: for a being set st a in x holds ex y,z being set st a = [y,z];
assume x is non empty;
then reconsider X = x as non empty set;
consider a being Element of X;
ex y,z being set st a = [y,z] by A2; hence contradiction by A1;
end;
end;
definition let IT be Function;
attr IT is nonpair-yielding means
for x being set st x in dom IT holds IT.x is non pair;
end;
definition
let x be non pair set;
cluster <*x*> -> nonpair-yielding;
coherence
proof let a be set; assume a in dom <*x*>;
then <*x*>.a in rng <*x*> by FUNCT_1:def 5;
then <*x*>.a in {x} by FINSEQ_1:56; hence thesis by TARSKI:def 1;
end;
let y be non pair set;
cluster <*x,y*> -> nonpair-yielding;
coherence
proof let a be set; assume a in dom <*x,y*>;
then <*x,y*>.a in rng <*x,y*> by FUNCT_1:def 5;
then <*x,y*>.a in {x,y} by FINSEQ_2:147; hence thesis by TARSKI:def 2;
end;
let z be non pair set;
cluster <*x,y,z*> -> nonpair-yielding;
coherence
proof let a be set; assume a in dom <*x,y,z*>;
then <*x,y,z*>.a in rng <*x,y,z*> by FUNCT_1:def 5;
then <*x,y,z*>.a in {x,y,z} by FINSEQ_2:148; hence thesis by ENUMSET1:13
;
end;
end;
theorem Th1:
for f being Function st f is nonpair-yielding holds rng f is without_pairs
proof let f be Function; assume
A1: for x being set st x in dom f holds f.x is non pair;
let y be pair set; assume y in rng f;
then consider x being set such that
A2: x in dom f & y = f.x by FUNCT_1:def 5;
thus thesis by A1,A2;
end;
definition let n be Nat;
cluster one-to-one nonpair-yielding FinSeqLen of n;
existence
proof reconsider p = id Seg n as FinSequence by FINSEQ_2:52;
len p = len idseq n by FINSEQ_2:def 1 .= n by FINSEQ_2:55;
then reconsider p as FinSeqLen of n by CIRCCOMB:def 12;
take p; thus p is one-to-one by FUNCT_1:52;
let x be set; assume A1: x in dom p;
then A2: x in Seg n by RELAT_1:71;
reconsider i = x as Nat by A1;
p.x = i by A2,FUNCT_1:34;
hence thesis;
end;
end;
definition
cluster one-to-one nonpair-yielding FinSequence;
existence
proof
consider n being Nat, p being one-to-one nonpair-yielding FinSeqLen of n;
take p; thus thesis;
end;
end;
definition
let f be nonpair-yielding Function;
cluster rng f -> without_pairs;
coherence by Th1;
end;
theorem Th2:
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
InnerVertices S1 is Relation & InnerVertices S2 is Relation
holds InnerVertices (S1+*S2) is Relation
proof let S1, S2 be non empty ManySortedSign; assume A1: S1 tolerates S2;
assume
InnerVertices S1 is Relation & InnerVertices S2 is Relation;
then reconsider R1 = InnerVertices S1, R2 = InnerVertices S2 as Relation;
R1 \/ R2 is Relation;
hence thesis by A1,CIRCCOMB:15;
end;
theorem Th3:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InnerVertices S1 is Relation & InnerVertices S2 is Relation
holds InnerVertices (S1+*S2) is Relation
proof let S1, S2 be unsplit gate`1=arity non empty ManySortedSign;
S1 tolerates S2 by CIRCCOMB:55;
hence thesis by Th2;
end;
theorem Th4:
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
InnerVertices S2 misses InputVertices S1
holds InputVertices S1 c= InputVertices (S1+*S2) &
InputVertices (S1+*S2) =
(InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1)
proof let S1,S2 be non empty ManySortedSign;
set S = S1+*S2;
set R = the ResultSort of S;
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
assume that
A1: S1 tolerates S2 and
A2: InnerVertices S2 misses InputVertices S1;
A3: InputVertices S = (the carrier of S) \ rng R &
InputVertices S1 = (the carrier of S1) \ rng R1 &
InputVertices S2 = (the carrier of S2) \ rng R2 by MSAFREE2:def 2;
A4: InnerVertices S1 = rng R1 & InnerVertices S2 = rng R2 &
InnerVertices S = rng R by MSAFREE2:def 3;
A5: the carrier of S = (the carrier of S1) \/ the carrier of S2 &
R = R1+*R2 by CIRCCOMB:def 2;
A6: rng R = (rng R1) \/ rng R2 by A1,A4,CIRCCOMB:15;
hereby let x be set; assume x in InputVertices S1;
then x in the carrier of S1 & not x in rng R1 & not x in rng R2
by A2,A3,A4,XBOOLE_0:3,def 4;
then x in the carrier of S & not x in rng R by A5,A6,XBOOLE_0:def 2;
hence x in InputVertices S by A3,XBOOLE_0:def 4;
end;
A7: InputVertices S c= (InputVertices S1) \/
InputVertices S2 by A1,CIRCCOMB:15
;
hereby let x be set; assume x in InputVertices (S1+*S2);
then x in (InputVertices S1) \/ InputVertices S2 & not x in rng R
by A3,A7,XBOOLE_0:def 4;
then x in InputVertices S1 or x in InputVertices S2 & not x in
InnerVertices S1
by A4,A6,XBOOLE_0:def 2;
then x in InputVertices S1 or x in InputVertices S2 \ InnerVertices S1
by XBOOLE_0:def 4;
hence x in (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1)
by XBOOLE_0:def 2;
end;
let x be set; assume
x in (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1);
then x in InputVertices S1 or x in InputVertices S2 \ rng R1 by A4,XBOOLE_0
:def 2
;
then x in InputVertices S1 & not x in rng R2 or
x in InputVertices S2 & not x in rng R1 by A2,A4,XBOOLE_0:3,def 4
;
then (x in the carrier of S1 or x in the carrier of S2) & not x in rng R1
&
not x in rng R2 by A3,XBOOLE_0:def 4;
then x in the carrier of S & not x in rng R by A5,A6,XBOOLE_0:def 2;
hence x in InputVertices (S1+*S2) by A3,XBOOLE_0:def 4;
end;
theorem Th5:
for X,R being set st X is without_pairs & R is Relation holds X misses R
proof let X,R be set; assume
A1: for x being pair set holds not x in X;
assume
A2: R is Relation;
now let x be set; assume x in X;
then not ex z1,z2 being set st x = [z1,z2] by A1;
hence not x in R by A2,RELAT_1:def 1;
end; hence thesis by XBOOLE_0:3;
end;
theorem Th6:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InputVertices S1 is without_pairs & InnerVertices S2 is Relation
holds InputVertices S1 c= InputVertices (S1+*S2) &
InputVertices (S1+*S2) =
(InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1)
proof let S1,S2 be unsplit gate`1=arity non empty ManySortedSign; assume
InputVertices S1 is without_pairs & InnerVertices S2 is Relation;
then S1 tolerates S2 & InnerVertices S2 misses InputVertices S1
by Th5,CIRCCOMB:55;
hence thesis by Th4;
end;
theorem Th7:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation
holds InputVertices (S1+*S2) = (InputVertices S1) \/ (InputVertices S2)
proof let S1,S2 be unsplit gate`1=arity non empty ManySortedSign; assume
A1: InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation;
then A2: InputVertices (S1+*S2) =
(InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1) by Th6;
InnerVertices S1 misses InputVertices S2 by A1,Th5;
hence thesis by A2,XBOOLE_1:83;
end;
theorem Th8:
for S1,S2 being non empty ManySortedSign st S1 tolerates S2 &
InputVertices S1 is without_pairs & InputVertices S2 is without_pairs
holds InputVertices (S1+*S2) is without_pairs
proof let S1, S2 be non empty ManySortedSign; assume S1 tolerates S2;
then A1: InputVertices (S1+*S2) c= (InputVertices S1) \/ InputVertices S2
by CIRCCOMB:15;
assume
A2: for x being pair set holds not x in InputVertices S1;
assume
A3: for x being pair set holds not x in InputVertices S2;
let x be pair set; assume x in InputVertices (S1+*S2);
then x in InputVertices S1 or x in InputVertices S2 by A1,XBOOLE_0:def 2;
hence contradiction by A2,A3;
end;
theorem Th9:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign st
InputVertices S1 is without_pairs & InputVertices S2 is without_pairs
holds InputVertices (S1+*S2) is without_pairs
proof let S1, S2 be unsplit gate`1=arity non empty ManySortedSign;
S1 tolerates S2 by CIRCCOMB:55;
hence thesis by Th8;
end;
begin :: Boolean Operations
scheme 2AryBooleEx {F(set,set) -> Element of BOOLEAN}:
ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st
for x,y being Element of BOOLEAN holds f.<*x,y*> = F(x,y)
proof
deffunc G(Tuple of 2, BOOLEAN) = F($1.1,$1.2);
consider f being Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 2, BOOLEAN holds f.a = G(a) from LambdaD;
hereby take f; let x,y be Element of BOOLEAN;
reconsider a = <*x,y*> as Tuple of 2, BOOLEAN by FINSEQ_2:121;
thus f.<*x,y*> = F(a.1,a.2) by A1
.= F(x,a.2) by FINSEQ_1:61
.= F(x,y) by FINSEQ_1:61;
end;
end;
scheme 2AryBooleUniq {F(set,set) -> Element of BOOLEAN}:
for f1,f2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
(for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y)) &
(for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
holds f1 = f2
proof
deffunc G(Tuple of 2, BOOLEAN) = F($1.1,$1.2);
let f1,f2 be Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A1: for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y) and
A2: for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y);
now let a be Tuple of 2, BOOLEAN;
consider x,y being Element of BOOLEAN such that
A3: a = <*x,y*> by FINSEQ_2:120;
thus f1.a = F(x,y) by A1,A3 .= f2.a by A2,A3;
end;
hence f1 = f2 by FUNCT_2:113;
end;
scheme 2AryBooleDef {F(set,set) -> Element of BOOLEAN}:
(ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st
for x,y being Element of BOOLEAN holds f.<*x,y*> = F(x,y)) &
for f1,f2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
(for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y)) &
(for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
holds f1 = f2
proof
deffunc G(Tuple of 2, BOOLEAN) = F($1.1,$1.2);
consider f being Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 2, BOOLEAN holds f.a = G(a) from LambdaD;
hereby take f; let x,y be Element of BOOLEAN;
reconsider a = <*x,y*> as Tuple of 2, BOOLEAN by FINSEQ_2:121;
thus f.<*x,y*> = F(a.1,a.2) by A1
.= F(x,a.2) by FINSEQ_1:61
.= F(x,y) by FINSEQ_1:61;
end;
let f1,f2 be Function of 2-tuples_on BOOLEAN, BOOLEAN such that
A2: for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y) and
A3: for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y);
now let a be Tuple of 2, BOOLEAN;
consider x,y being Element of BOOLEAN such that
A4: a = <*x,y*> by FINSEQ_2:120;
thus f1.a = F(x,y) by A2,A4 .= f2.a by A3,A4;
end;
hence f1 = f2 by FUNCT_2:113;
end;
scheme 3AryBooleEx {F(set,set,set) -> Element of BOOLEAN}:
ex f being Function of 3-tuples_on BOOLEAN, BOOLEAN st
for x,y,z being Element of BOOLEAN holds f.<*x,y,z*> = F(x,y,z)
proof
deffunc G(Tuple of 3, BOOLEAN) = F($1.1,$1.2,$1.3);
consider f being Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 3, BOOLEAN holds f.a = G(a) from LambdaD;
hereby take f; let x,y,z be Element of BOOLEAN;
reconsider a = <*x,y,z*> as Tuple of 3, BOOLEAN by FINSEQ_2:124;
thus f.<*x,y,z*> = F(a.1,a.2,a.3) by A1
.= F(x,a.2,a.3) by FINSEQ_1:62
.= F(x,y,a.3) by FINSEQ_1:62
.= F(x,y,z) by FINSEQ_1:62;
end;
end;
scheme 3AryBooleUniq {F(set,set,set) -> Element of BOOLEAN}:
for f1,f2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
(for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z)) &
(for x,y,z being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z))
holds f1 = f2
proof
deffunc G(Tuple of 3, BOOLEAN) = F($1.1,$1.2,$1.3);
let f1,f2 be Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A1: for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z) and
A2: for x,y,z being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z);
now let a be Tuple of 3, BOOLEAN;
consider x,y,z being Element of BOOLEAN such that
A3: a = <*x,y,z*> by FINSEQ_2:123;
thus f1.a = F(x,y,z) by A1,A3 .= f2.a by A2,A3;
end;
hence f1 = f2 by FUNCT_2:113;
end;
scheme 3AryBooleDef {F(set,set,set) -> Element of BOOLEAN}:
(ex f being Function of 3-tuples_on BOOLEAN, BOOLEAN st
for x,y,z being Element of BOOLEAN holds f.<*x,y,z*> = F(x,y,z)) &
for f1,f2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
(for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z)) &
(for x,y,z being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z))
holds f1 = f2
proof
deffunc G(Tuple of 3, BOOLEAN) = F($1.1,$1.2,$1.3);
consider f being Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A1: for a being Tuple of 3, BOOLEAN holds f.a = G(a) from LambdaD;
hereby take f; let x,y,z be Element of BOOLEAN;
reconsider a = <*x,y,z*> as Tuple of 3, BOOLEAN by FINSEQ_2:124;
thus f.<*x,y,z*> = F(a.1,a.2,a.3) by A1
.= F(x,a.2,a.3) by FINSEQ_1:62
.= F(x,y,a.3) by FINSEQ_1:62
.= F(x,y,z) by FINSEQ_1:62;
end;
let f1,f2 be Function of 3-tuples_on BOOLEAN, BOOLEAN such that
A2: for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z) and
A3: for x,y,z being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z);
now let a be Tuple of 3, BOOLEAN;
consider x,y,z being Element of BOOLEAN such that
A4: a = <*x,y,z*> by FINSEQ_2:123;
thus f1.a = F(x,y,z) by A2,A4 .= f2.a by A3,A4;
end;
hence f1 = f2 by FUNCT_2:113;
end;
definition
func 'xor' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def4:
for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'xor' y;
correctness
proof
deffunc F(Element of BOOLEAN,Element of BOOLEAN) = $1 'xor' $2;
(ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st
for x,y being Element of BOOLEAN holds f.<*x,y*> = F(x,y)) &
for f1,f2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
(for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y)) &
(for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
holds f1 = f2 from 2AryBooleDef;
hence thesis;
end;
func 'or' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def5:
for x,y being Element of BOOLEAN holds it.<*x,y*> = x 'or' y;
correctness
proof
deffunc F(Element of BOOLEAN,Element of BOOLEAN) = $1 'or' $2;
(ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st
for x,y being Element of BOOLEAN holds f.<*x,y*> = F(x,y)) &
for f1,f2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
(for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y)) &
(for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
holds f1 = f2 from 2AryBooleDef;
hence thesis;
end;
func '&' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means:
Def6:
for x,y being Element of BOOLEAN holds it.<*x,y*> = x '&' y;
correctness
proof
deffunc F(Element of BOOLEAN,Element of BOOLEAN) = $1 '&' $2;
(ex f being Function of 2-tuples_on BOOLEAN, BOOLEAN st
for x,y being Element of BOOLEAN holds f.<*x,y*> = F(x,y)) &
for f1,f2 being Function of 2-tuples_on BOOLEAN, BOOLEAN st
(for x,y being Element of BOOLEAN holds f1.<*x,y*> = F(x,y)) &
(for x,y being Element of BOOLEAN holds f2.<*x,y*> = F(x,y))
holds f1 = f2 from 2AryBooleDef;
hence thesis;
end;
end;
definition
func or3 -> Function of 3-tuples_on BOOLEAN, BOOLEAN means:
Def7:
for x,y,z being Element of BOOLEAN holds it.<*x,y,z*> = x 'or' y 'or' z;
correctness
proof
deffunc F(Element of BOOLEAN,Element of BOOLEAN,Element of BOOLEAN) =
$1 'or' $2 'or' $3;
(ex f being Function of 3-tuples_on BOOLEAN, BOOLEAN st
for x,y,z being Element of BOOLEAN holds f.<*x,y,z*> = F(x,y,z)) &
for f1,f2 being Function of 3-tuples_on BOOLEAN, BOOLEAN st
(for x,y,z being Element of BOOLEAN holds f1.<*x,y,z*> = F(x,y,z)) &
(for x,y,z being Element of BOOLEAN holds f2.<*x,y,z*> = F(x,y,z))
holds f1 = f2 from 3AryBooleDef;
hence thesis;
end;
end;
definition
let x be set;
redefine func <*x*> -> FinSeqLen of 1;
coherence proof thus len <*x*> = 1 by FINSEQ_1:57; end;
let y be set;
func <*x,y*> -> FinSeqLen of 2;
coherence proof thus len <*x,y*> = 2 by FINSEQ_1:61; end;
let z be set;
func <*x,y,z*> -> FinSeqLen of 3;
coherence proof thus len <*x,y,z*> = 3 by FINSEQ_1:62; end;
end;
definition let n,m be Nat;
let p be FinSeqLen of n;
let q be FinSeqLen of m;
redefine func p^q -> FinSeqLen of n+m;
coherence
proof
thus len (p^q) = len p + len q by FINSEQ_1:35
.= n+len q by CIRCCOMB:def 12
.= n+m by CIRCCOMB:def 12;
end;
end;
begin :: Computation and Stabilizable
Lm1:
now let S be non void non empty ManySortedSign;
let o be Gate of S;
the OperSymbols of S is non empty by MSUALG_1:def 5;
hence o in the OperSymbols of S;
end;
theorem Th10:
for S being Circuit-like non void (non empty ManySortedSign)
for A being non-empty Circuit of S
for s being State of A, g being Gate of S holds
(Following s).the_result_sort_of g = Den(g, A).(s*the_arity_of g)
proof let S be Circuit-like non void (non empty ManySortedSign);
let A be non-empty Circuit of S;
let s be State of A, g be Gate of S;
set v = the_result_sort_of g;
A1: g in the OperSymbols of S by Lm1;
A2: g depends_on_in s = s*the_arity_of g by CIRCUIT1:def 3;
dom the ResultSort of S = the OperSymbols of S by FUNCT_2:def 1;
then (the ResultSort of S).g in rng the ResultSort of S by A1,FUNCT_1:def 5
;
then (the ResultSort of S).g in InnerVertices S by MSAFREE2:def 3;
then A3: v in InnerVertices S by MSUALG_1:def 7;
then action_at v = g by MSAFREE2:def 7;
hence thesis by A2,A3,CIRCUIT2:def 5;
end;
definition
let S be non void Circuit-like (non empty ManySortedSign);
let A be non-empty Circuit of S;
let s be State of A;
let n be Nat;
func Following(s,n) -> State of A means
:Def8:
ex f being Function of NAT, product the Sorts of A st
it = f.n & f.0 = s &
for n being Nat holds f.(n+1) = Following f.n;
correctness
proof
set D = product the Sorts of A;
deffunc R(Nat,Element of D) = Following $2;
(ex y being Element of D st ex f being Function of NAT,D st
y = f.n & f.0 = s &
for n being Nat holds f.(n+1) = R(n,f.n)) &
for y1,y2 being Element of D st
(ex f being Function of NAT,D st
y1 = f.n & f.0 = s &
for n being Nat holds f.(n+1) = R(n,f.n)) &
(ex f being Function of NAT,D st
y2 = f.n & f.0 = s &
for n being Nat holds f.(n+1) = R(n,f.n)) holds y1 = y2
from LambdaDefRecD;
hence thesis;
end;
end;
theorem Th11:
for S being Circuit-like non void (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A holds
Following(s,0) = s
proof let S be Circuit-like non void (non empty ManySortedSign);
let A be non-empty Circuit of S, s be State of A;
ex f being Function of NAT, product the Sorts of A st
Following(s,0) = f.0 & f.0 = s &
for n being Nat holds f.(n+1) = Following f.n by Def8;
hence thesis;
end;
theorem Th12:
for S being Circuit-like non void (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A
for n being Nat holds Following(s,n+1) = Following Following(s,n)
proof let S be Circuit-like non void (non empty ManySortedSign);
let A be non-empty Circuit of S, s be State of A;
let n be Nat;
consider f being Function of NAT, product the Sorts of A such that
A1: Following(s,n) = f.n & f.0 = s &
for n being Nat holds f.(n+1) = Following f.n by Def8;
thus Following(s,n+1) = f.(n+1) by A1,Def8
.= Following Following(s,n) by A1;
end;
theorem Th13:
for S being Circuit-like non void (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A
for n,m being Nat holds Following(s,n+m) = Following(Following(s,n),m)
proof let S be Circuit-like non void (non empty ManySortedSign);
let A be non-empty Circuit of S, s be State of A;
let n be Nat;
defpred P[Nat] means Following(s,n+$1) = Following(Following(s,n),$1);
A1: P[0] by Th11;
A2: for m being Nat st P[m] holds P[m+1]
proof let m be Nat; assume
A3: Following(s,n+m) = Following(Following(s,n),m);
thus Following(s,n+(m+1)) = Following(s,n+m+1) by XCMPLX_1:1
.= Following Following(s,n+m) by Th12
.= Following(Following(s,n),m+1) by A3,Th12;
end;
thus for i being Nat holds P[i] from Ind(A1,A2);
end;
theorem Th14:
for S being non void Circuit-like (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A holds
Following(s,1) = Following s
proof let S be non void Circuit-like (non empty ManySortedSign);
let A be non-empty Circuit of S, s be State of A; 0+1 = 1;
hence Following(s,1) = Following Following(s,0) by Th12
.= Following s by Th11;
end;
theorem Th15:
for S being non void Circuit-like (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A holds
Following(s,2) = Following Following s
proof let S be non void Circuit-like (non empty ManySortedSign);
let A be non-empty Circuit of S, s be State of A; 2 = 1+1;
hence Following(s,2) = Following Following(s,0+1) by Th12
.= Following Following s by Th14;
end;
theorem Th16:
for S being Circuit-like non void (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A
for n being Nat holds Following(s,n+1) = Following(Following s, n)
proof let S be Circuit-like non void (non empty ManySortedSign);
let A be non-empty Circuit of S, s be State of A;
let n be Nat;
Following(s,n+1) = Following(Following(s,1), n) by Th13;
hence thesis by Th14;
end;
definition
let S be non void Circuit-like (non empty ManySortedSign);
let A be non-empty Circuit of S;
let s be State of A;
let x be set;
pred s is_stable_at x means:
Def9:
for n being Nat holds (Following(s,n)).x = s.x;
end;
theorem
for S being non void Circuit-like (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A
for x being set st s is_stable_at x
for n being Nat holds Following(s,n) is_stable_at x
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;
let x be set such that
A1: for n being Nat holds (Following(s,n)).x = s.x;
let n, m be Nat;
thus (Following(Following(s,n),m)).x = (Following(s,n+m)).x by Th13
.= s.x by A1
.= (Following(s,n)).x by A1;
end;
theorem
for S being non void Circuit-like (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A
for x being set st x in InputVertices S holds s is_stable_at x
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;
let x be set; assume
A1: x in InputVertices S;
defpred P[Nat] means (Following(s,$1)).x = s.x;
A2: P[0] by Th11;
A3: now let n be Nat; assume
A4: P[n];
(Following(s,n+1)).x = (Following Following(s,n)).x by Th12
.= s.x by A1,A4,CIRCUIT2:def 5;
hence P[n+1];
end;
thus for n being Nat holds P[n] from Ind(A2,A3);
end;
theorem Th19:
for S being non void Circuit-like (non empty ManySortedSign)
for A being non-empty Circuit of S, s being State of A
for g being Gate of S st
for x being set st x in rng the_arity_of g holds s is_stable_at x
holds Following s is_stable_at the_result_sort_of g
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;
let g be Gate of S; set p = the_arity_of g;
assume
A1: for x being set st x in rng p holds s is_stable_at x;
let n be Nat;
rng p c= the carrier of S & dom s = the carrier of S &
dom Following(s, n) = the carrier of S by CIRCUIT1:4,FINSEQ_1:def 4;
then A2: dom ((Following(s, n))*p) = dom p & dom (s*p) = dom p by RELAT_1:46;
now let a be set; assume
a in dom p;
then A3: ((Following(s, n))*p).a = (Following(s, n)).(p.a) & (s*p).a = s.(p.
a) &
p.a in rng p by FUNCT_1:23,def 5;
then s is_stable_at p.a by A1;
hence ((Following(s, n))*p).a = (s*p).a by A3,Def9;
end;
then A4: (Following(s, n))*p = s*p by A2,FUNCT_1:9;
thus (Following(Following s, n)).the_result_sort_of g
= (Following(s, n+1)).the_result_sort_of g by Th16
.= (Following Following(s, n)).the_result_sort_of g by Th12
.= (Den(g,A)).((Following(s, n))*p) by Th10
.= (Following s).the_result_sort_of g by A4,Th10;
end;
begin :: Combined Circuits
theorem Th20:
for S1,S2 being non empty ManySortedSign, v being Vertex of S1 holds
v in the carrier of S1+*S2 & v in the carrier of S2+*S1
proof let S1,S2 be non empty ManySortedSign; let v be Vertex of S1;
the carrier of (S1+*S2) = (the carrier of S1) \/ the carrier of S2 &
the carrier of (S2+*S1) = (the carrier of S2) \/ the carrier of S1
by CIRCCOMB:def 2;
hence v in the carrier of S1+*S2 & v in
the carrier of S2+*S1 by XBOOLE_0:def 2;
end;
theorem Th21:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
for x being set st x in InnerVertices S1 holds
x in InnerVertices (S1+*S2) & x in InnerVertices (S2+*S1)
proof let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
S1 tolerates S2 by CIRCCOMB:55;
then InnerVertices (S1+*S2) = InnerVertices S1 \/ InnerVertices S2 &
InnerVertices (S2+*S1) = InnerVertices S2 \/ InnerVertices S1
by CIRCCOMB:15;
hence thesis by XBOOLE_0:def 2;
end;
theorem
for S1,S2 being non empty ManySortedSign
for x being set st x in InnerVertices S2 holds x in InnerVertices (S1+*S2)
proof let S1,S2 be non empty ManySortedSign;
set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
A1: InnerVertices (S1+*S2) = rng the ResultSort of S1+*S2 by MSAFREE2:def 3
.= rng (R1+*R2) by CIRCCOMB:def 2;
InnerVertices S2 = rng R2 by MSAFREE2:def 3;
then InnerVertices S2 c= InnerVertices (S1+*S2) by A1,FUNCT_4:19;
hence thesis;
end;
theorem Th23:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds
S1+*S2 = S2+*S1
proof let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
S1 tolerates S2 by CIRCCOMB:55;
hence S1+*S2 = S2+*S1 by CIRCCOMB:9;
end;
theorem Th24:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
for A1 being Boolean gate`2=den Circuit of S1
for A2 being Boolean gate`2=den Circuit of S2 holds A1+*A2 = A2+*A1
proof
let S1,S2 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
A1 tolerates A2 by CIRCCOMB:68;
hence A1+*A2 = A2+*A1 by CIRCCOMB:26;
end;
theorem Th25:
for S1,S2,S3 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
for A1 being Boolean Circuit of S1, A2 being Boolean Circuit of S2
for A3 being Boolean Circuit of S3 holds (A1+*A2)+*A3 = A1+*(A2+*A3)
proof let S1,S2,S3 be
unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign;
let A1 be Boolean Circuit of S1;
let A2 be Boolean Circuit of S2;
let A3 be Boolean Circuit of S3;
the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates
the Sorts of A3 &
the Sorts of A3 tolerates the Sorts of A1 by CIRCCOMB:67;
hence A1+*A2+*A3 = A1+*(A2+*A3) by CIRCCOMB:27;
end;
theorem Th26:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
for A1 being Boolean gate`2=den non-empty Circuit of S1
for A2 being Boolean gate`2=den non-empty Circuit of S2
for s being State of A1+*A2 holds
s|the carrier of S1 is State of A1 & s|the carrier of S2 is State of A2
proof
let S1,S2 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
let s be State of A1+*A2;
the Sorts of A1 tolerates the Sorts of A2 by CIRCCOMB:67;
hence thesis by CIRCCOMB:33;
end;
theorem Th27:
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds
InnerVertices (S1+*S2) = (InnerVertices S1) \/ InnerVertices S2
proof
let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
S1 tolerates S2 by CIRCCOMB:55;
hence thesis by CIRCCOMB:15;
end;
theorem Th28:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
st InnerVertices S2 misses InputVertices S1
for A1 being Boolean gate`2=den Circuit of S1
for A2 being Boolean gate`2=den Circuit of S2
for s being State of A1+*A2, s1 being State of A1
st s1 = s|the carrier of S1
holds (Following s)|the carrier of S1 = Following s1
proof
let S1,S2 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign such that
A1: InnerVertices S2 misses InputVertices S1;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
let s be State of A1+*A2, s1 be State of A1 such that
A2: s1 = s|the carrier of S1;
reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
A1 tolerates A2 by CIRCCOMB:68;
then dom Following s1 = the carrier of S1 &
Following s = (Following s2)+*Following s1 by A1,A2,CIRCCOMB:40,CIRCUIT1:4;
hence (Following s)|the carrier of S1 = Following s1 by FUNCT_4:24;
end;
theorem Th29:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
st InnerVertices S1 misses InputVertices S2
for A1 being Boolean gate`2=den Circuit of S1
for A2 being Boolean gate`2=den Circuit of S2
for s being State of A1+*A2, 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 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
let s be State of A1+*A2, s2 be State of A2 such that
A2: s2 = s|the carrier of S2;
reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
A1 tolerates A2 by CIRCCOMB:68;
then dom Following s2 = the carrier of S2 &
Following s = (Following s1)+*Following s2 by A1,A2,CIRCCOMB:39,CIRCUIT1:4;
hence (Following s)|the carrier of S2 = Following s2 by FUNCT_4:24;
end;
theorem Th30:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
st InnerVertices S2 misses InputVertices S1
for A1 being Boolean gate`2=den Circuit of S1
for A2 being Boolean gate`2=den Circuit of S2
for s being State of A1+*A2, s1 being State of A1
st s1 = s|the carrier of S1
for n being Nat holds Following(s,n)|the carrier of S1 = Following(s1,n)
proof
let S1,S2 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign such that
A1: InnerVertices S2 misses InputVertices S1;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
let s be State of A1+*A2, s1 be State of A1 such that
A2: s1 = s|the carrier of S1;
defpred P[Nat] means
Following(s,$1)|the carrier of S1 = Following(s1,$1);
Following(s,0) = s by Th11;
then A3: P[0] by A2,Th11;
A4: for n being Nat st P[n] holds P[n+1]
proof let n be Nat; assume
A5: Following(s,n)|the carrier of S1 = Following(s1,n);
thus Following(s,n+1)|the carrier of S1
= (Following Following(s,n))|the carrier of S1 by Th12
.= Following Following(s1,n) by A1,A5,Th28
.= Following(s1,n+1) by Th12;
end;
thus for n being Nat holds P[n] from Ind(A3,A4);
end;
theorem Th31:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
st InnerVertices S1 misses InputVertices S2
for A1 being Boolean gate`2=den Circuit of S1
for A2 being Boolean gate`2=den Circuit of S2
for s being State of A1+*A2, s2 being 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 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
let s be State of A1+*A2, s2 be State of A2 such that
A2: s2 = s|the carrier of S2;
defpred P[Nat] means
Following(s,$1)|the carrier of S2 = Following(s2,$1);
Following(s,0) = s by Th11;
then A3: P[0] by A2,Th11;
A4: for n being Nat st P[n] holds P[n+1]
proof let n be Nat; assume
A5: Following(s,n)|the carrier of S2 = Following(s2,n);
thus Following(s,n+1)|the carrier of S2
= (Following Following(s,n))|the carrier of S2 by Th12
.= Following Following(s2,n) by A1,A5,Th29
.= Following(s2,n+1) by Th12;
end;
thus for n being Nat holds P[n] from Ind(A3,A4);
end;
theorem Th32:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
st InnerVertices S2 misses InputVertices S1
for A1 being Boolean gate`2=den Circuit of S1
for A2 being Boolean gate`2=den Circuit of S2
for s being State of A1+*A2, s1 being State of A1
st s1 = s|the carrier of S1 holds
for v being set st v in the carrier of S1
for n being Nat holds (Following(s,n)).v = (Following(s1,n)).v
proof
let S1,S2 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign such that
A1: InnerVertices S2 misses InputVertices S1;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
let s be State of A1+*A2, s1 be State of A1 such that
A2: s1 = s|the carrier of S1;
let v be set; assume
A3: v in the carrier of S1;
let n be Nat;
A4: Following(s,n)|the carrier of S1 = Following(s1,n) by A1,A2,Th30;
the carrier of S1 = dom Following(s1,n) by CIRCUIT1:4;
hence thesis by A3,A4,FUNCT_1:70;
end;
theorem Th33:
for S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign
st InnerVertices S1 misses InputVertices S2
for A1 being Boolean gate`2=den Circuit of S1
for A2 being Boolean gate`2=den Circuit of S2
for s being State of A1+*A2, s2 being State of A2
st s2 = s|the carrier of S2 holds
for v being set st v in the carrier of S2
for n being Nat holds (Following(s,n)).v = (Following(s2,n)).v
proof
let S1,S2 be unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2;
let A1 be Boolean gate`2=den Circuit of S1;
let A2 be Boolean gate`2=den Circuit of S2;
let s be State of A1+*A2, s1 be State of A2 such that
A2: s1 = s|the carrier of S2;
let v be set; assume
A3: v in the carrier of S2;
let n be Nat;
A4: Following(s,n)|the carrier of S2 = Following(s1,n) by A1,A2,Th31;
the carrier of S2 = dom Following(s1,n) by CIRCUIT1:4;
hence thesis by A3,A4,FUNCT_1:70;
end;
definition
let S be gate`2=den non void (non empty ManySortedSign);
let g be Gate of S;
cluster g`2 -> Function-like Relation-like;
coherence
proof consider A being MSAlgebra over S such that
A1: A is gate`2=den by CIRCCOMB:def 11;
g in the OperSymbols of S by Lm1;
then g`2 = [g`1, (the Charact of A).g]`2 by A1,CIRCCOMB:def 10
.= (the Charact of A).g by MCART_1:7
.= Den(g, A) by MSUALG_1:def 11;
hence thesis;
end;
end;
theorem Th34:
for S being gate`2=den Circuit-like non void (non empty ManySortedSign)
for A being non-empty Circuit of S st A is gate`2=den
for s being State of A, g being Gate of S holds
(Following s).the_result_sort_of g = g`2.(s*the_arity_of g)
proof let S be gate`2=den Circuit-like non void (non empty ManySortedSign);
let A be non-empty Circuit of S such that
A1: for g being set st g in the OperSymbols of S holds
g = [g`1, (the Charact of A).g];
let s be State of A, g be Gate of S;
set v = the_result_sort_of g;
A2: g in the OperSymbols of S by Lm1;
A3: g depends_on_in s = s*the_arity_of g by CIRCUIT1:def 3;
A4: Den(g, A) = (the Charact of A).g by MSUALG_1:def 11
.= [g`1, (the Charact of A).g]`2 by MCART_1:7 .= g`2 by A1,A2;
dom the ResultSort of S = the OperSymbols of S by FUNCT_2:def 1;
then (the ResultSort of S).g in rng the ResultSort of S by A2,FUNCT_1:def 5
;
then (the ResultSort of S).g in InnerVertices S by MSAFREE2:def 3;
then A5: v in InnerVertices S by MSUALG_1:def 7;
then action_at v = g by MSAFREE2:def 7;
hence thesis by A3,A4,A5,CIRCUIT2:def 5;
end;
theorem Th35:
for S being gate`1=arity gate`2isBoolean unsplit
non void non empty ManySortedSign
for A being Boolean gate`2=den non-empty Circuit of S
for s being State of A, p being FinSequence, f being Function
st [p,f] in the OperSymbols of S holds (Following s).[p,f] = f.(s*p)
proof let S be gate`1=arity gate`2isBoolean unsplit
non void non empty ManySortedSign;
let A be Boolean gate`2=den non-empty Circuit of S;
let s be State of A, p be FinSequence, f be Function; assume
A1: [p,f] in the OperSymbols of S;
then reconsider g = [p,f] as Gate of S;
A2: the_arity_of g = (the Arity of S).g by MSUALG_1:def 6
.= [(the Arity of S).g, g`2]`1 by MCART_1:7
.= g`1 by A1,CIRCCOMB:def 8;
A3: g`1 = p & g`2 = f by MCART_1:7;
the_result_sort_of g = (the ResultSort of S).g by MSUALG_1:def 7 .= g
by A1,CIRCCOMB:52;
hence (Following s).[p,f] = f.(s*p) by A2,A3,Th34;
end;
theorem
for S being gate`1=arity gate`2isBoolean unsplit
non void non empty ManySortedSign
for A being Boolean gate`2=den non-empty Circuit of S
for s being State of A, p being FinSequence, f being Function
st [p,f] in the OperSymbols of S &
for x being set st x in rng p holds s is_stable_at x
holds Following s is_stable_at [p,f]
proof let S be gate`1=arity gate`2isBoolean unsplit
non void non empty ManySortedSign;
let A be Boolean gate`2=den non-empty Circuit of S;
let s be State of A, p be FinSequence, f be Function; assume
A1: [p,f] in the OperSymbols of S;
then reconsider g = [p,f] as Gate of S;
assume
A2: for x being set st x in rng p holds s is_stable_at x;
A3: the_arity_of g = (the Arity of S).g by MSUALG_1:def 6
.= [(the Arity of S).g, g`2]`1 by MCART_1:7
.= g`1 by A1,CIRCCOMB:def 8
.= p by MCART_1:7;
the_result_sort_of g = (the ResultSort of S).g by MSUALG_1:def 7
.= g by A1,CIRCCOMB:52;
hence thesis by A2,A3,Th19;
end;
theorem Th37:
for S being unsplit non empty ManySortedSign holds
InnerVertices S = the OperSymbols of S
proof let S be unsplit non empty ManySortedSign;
the ResultSort of S = id the OperSymbols of S by CIRCCOMB:def 7;
then rng the ResultSort of S = the OperSymbols of S by RELAT_1:71;
hence thesis by MSAFREE2:def 3;
end;
begin :: One Gate Circuit
theorem Th38:
for f being set, p being FinSequence holds
InnerVertices 1GateCircStr(p,f) is Relation
proof let f be set, p be FinSequence;
InnerVertices 1GateCircStr(p,f) = {[p,f]} by CIRCCOMB:49;
hence thesis;
end;
theorem
for f being set, p being nonpair-yielding FinSequence holds
InputVertices 1GateCircStr(p,f) is without_pairs
proof let f be set, p be nonpair-yielding FinSequence;
InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:49;
hence thesis;
end;
theorem Th40:
for f being set, x,y being set holds
InputVertices 1GateCircStr(<*x,y*>,f) = {x,y}
proof let f be set, x,y be set;
set p = <*x,y*>;
thus InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:49
.= {x,y} by FINSEQ_2:147;
end;
theorem Th41:
for f being set, x,y being non pair set holds
InputVertices 1GateCircStr(<*x,y*>,f) is without_pairs
proof let f be set, x,y be non pair set;
set p = <*x,y*>;
A1: InputVertices 1GateCircStr(p,f) = {x,y} by Th40;
let z be pair set; assume z in
InputVertices 1GateCircStr(p,f); hence thesis
by A1,TARSKI:def 2;
end;
theorem Th42:
for f being set, x,y,z being set holds
InputVertices 1GateCircStr(<*x,y,z*>,f) = {x,y,z}
proof let f be set, x,y,z be set;
set p = <*x,y,z*>;
thus InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:49
.= {x,y,z} by FINSEQ_2:148;
end;
theorem Th43:
for x,y,f being set holds
x in the carrier of 1GateCircStr(<*x,y*>,f) &
y in the carrier of 1GateCircStr(<*x,y*>,f) &
[<*x,y*>,f] in the carrier of 1GateCircStr(<*x,y*>,f)
proof let x,y,f be set; set p = <*x,y*>;
x in {x,y} & y in {x,y} by TARSKI:def 2;
then the carrier of 1GateCircStr(p,f) = rng p \/ {[p,f]} &
x in rng p & y in rng p & [p,f] in {[p,f]}
by CIRCCOMB:def 6,FINSEQ_2:147,TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th44:
for x,y,z,f being set holds
x in the carrier of 1GateCircStr(<*x,y,z*>,f) &
y in the carrier of 1GateCircStr(<*x,y,z*>,f) &
z in the carrier of 1GateCircStr(<*x,y,z*>,f)
proof let x,y,z,f be set; set p = <*x,y,z*>;
set A = the carrier of 1GateCircStr(p,f);
x in {x,y,z} & y in {x,y,z} & z in {x,y,z} by ENUMSET1:14;
then A = rng p \/ {[p,f]} & x in rng p & y in rng p & z in rng p
by CIRCCOMB:def 6,FINSEQ_2:148;
hence x in A & y in A & z in A by XBOOLE_0:def 2;
end;
theorem
for f,x being set, p being FinSequence holds
x in the carrier of 1GateCircStr(p,f,x) &
for y being set st y in rng p holds y in the carrier of 1GateCircStr(p,f,x)
proof let f,x be set; let p be FinSequence;
set A = the carrier of 1GateCircStr(p,f,x);
A = rng p \/ {x} & x in {x} by CIRCCOMB:def 5,TARSKI:def 1;
hence x in A & for y being set st y in rng p holds y in A by XBOOLE_0:def 2
;
end;
theorem
for f,x being set, p being FinSequence holds
1GateCircStr(p,f,x) is gate`1=arity Circuit-like
proof let f,x be set; let p be FinSequence;
set S = 1GateCircStr(p,f,x);
thus S is gate`1=arity
proof let g be set; assume g in the OperSymbols of S;
then g in {[p,f]} by CIRCCOMB:def 5;
then g = [p,f] & [p,f]`2 = f by MCART_1:7,TARSKI:def 1;
hence thesis by CIRCCOMB:def 5;
end;
thus S is Circuit-like
proof let S' be non void non empty ManySortedSign such that
A1: S' = S;
let o1, o2 be OperSymbol of S';
o1 = [p,f] & o2 = [p,f] by A1,CIRCCOMB:44;
hence thesis;
end;
end;
theorem Th47:
for p being FinSequence, f be set holds
[p,f] in InnerVertices 1GateCircStr(p,f)
proof let p be FinSequence, f be set;
InnerVertices 1GateCircStr(p,f) = {[p,f]} by CIRCCOMB:49;
hence [p,f] in InnerVertices 1GateCircStr(p,f) by TARSKI:def 1;
end;
definition
let x,y be set;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 1GateCircuit(x,y,f) ->
Boolean gate`2=den strict Circuit of 1GateCircStr(<*x,y*>, f) equals:
Def10:
1GateCircuit(<*x,y*>, f);
coherence by CIRCCOMB:69;
end;
reserve x,y,z,c for set,
f for Function of 2-tuples_on BOOLEAN, BOOLEAN;
theorem Th48:
for X being finite non empty set, f being Function of 2-tuples_on X, X
for s being State of 1GateCircuit(<*x,y*>,f) holds
(Following s).[<*x,y*>, f] = f.<*s.x, s.y*> &
(Following s).x = s.x & (Following s).y = s.y
proof let X be finite non empty set, f be Function of 2-tuples_on X, X;
let s be State of 1GateCircuit(<*x,y*>,f);
set p = <*x,y*>;
x in {x,y} & y in {x,y} & dom s = the carrier of 1GateCircStr(p , f)
by CIRCUIT1:4,TARSKI:def 2;
then x in rng p & y in rng p & dom s = rng p \/ {[p,f]}
by CIRCCOMB:def 6,FINSEQ_2:147;
then A1: x in dom s & y in dom s by XBOOLE_0:def 2;
thus (Following s).[<*x,y*>, f] = f.(s*<*x,y*>) by CIRCCOMB:64
.= f.<*s.x, s.y*> by A1,FINSEQ_2:145;
reconsider x, y as Vertex of 1GateCircStr(p,f) by Th43;
InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:49
.= {x,y} by FINSEQ_2:147;
then x in InputVertices 1GateCircStr(p,f) &
y in InputVertices 1GateCircStr(p,f) by TARSKI:def 2;
hence thesis by CIRCUIT2:def 5;
end;
theorem Th49:
for X being finite non empty set, f being Function of 2-tuples_on X, X
for s being State of 1GateCircuit(<*x,y*>,f) holds
Following s is stable
proof let X be finite non empty set, f be Function of 2-tuples_on X, X;
set S = 1GateCircStr(<*x,y*>,f);
let s be State of 1GateCircuit(<*x,y*>,f);
set s1 = Following s, s2 = Following s1;
set p = <*x,y*>;
A1: dom s1 = the carrier of S & dom s2 = the carrier of S by CIRCUIT1:4;
A2: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6
.= {x,y} \/ {[p,f]} by FINSEQ_2:147;
now let a be set; assume a in the carrier of S;
then a in {x,y} or a in {[p,f]} by A2,XBOOLE_0:def 2;
then A3: a = x or a = y or a = [p,f] by TARSKI:def 1,def 2;
s2.x = s1.x & s1.x = s.x & s2.y = s1.y & s1.y = s.y &
s2.[p,f] = f.<*s1.x, s1.y*> & s1.[p,f] = f.<*s.x, s.y*> by Th48;
hence s2.a = s1.a by A3;
end;
hence Following s = Following Following s by A1,FUNCT_1:9;
end;
theorem Th50:
for s being State of 1GateCircuit(x,y,f) holds
(Following s).[<*x,y*>, f] = f.<*s.x, s.y*> &
(Following s).x = s.x & (Following s).y = s.y
proof let s be State of 1GateCircuit(x,y,f);
1GateCircuit(x,y,f) = 1GateCircuit(<*x,y*>, f) by Def10;
hence thesis by Th48;
end;
theorem
for s being State of 1GateCircuit(x,y,f) holds Following s is stable
proof let s be State of 1GateCircuit(x,y,f);
1GateCircuit(x,y,f) = 1GateCircuit(<*x,y*>, f) by Def10;
hence thesis by Th49;
end;
definition
let x,y,z be set;
let f be Function of 3-tuples_on BOOLEAN, BOOLEAN;
func 1GateCircuit(x,y,z,f) ->
Boolean gate`2=den strict Circuit of 1GateCircStr(<*x,y,z*>, f) equals:
Def11:
1GateCircuit(<*x,y,z*>, f);
coherence by CIRCCOMB:69;
end;
theorem Th52:
for X being finite non empty set, f being Function of 3-tuples_on X, X
for s being State of 1GateCircuit(<*x,y,z*>,f) holds
(Following s).[<*x,y,z*>, f] = f.<*s.x, s.y, s.z*> &
(Following s).x = s.x & (Following s).y = s.y & (Following s).z = s.z
proof let X be finite non empty set, f be Function of 3-tuples_on X, X;
let s be State of 1GateCircuit(<*x,y,z*>,f);
set p = <*x,y,z*>;
x in {x,y,z} & y in {x,y,z} & z in {x,y,z} &
dom s = the carrier of 1GateCircStr(p , f) by CIRCUIT1:4,ENUMSET1:14;
then x in rng p & y in rng p & z in rng p & dom s = rng p \/ {[p,f]}
by CIRCCOMB:def 6,FINSEQ_2:148;
then A1: x in dom s & y in dom s & z in dom s by XBOOLE_0:def 2;
thus (Following s).[p, f] = f.(s*p) by CIRCCOMB:64
.= f.<*s.x, s.y, s.z*> by A1,FINSEQ_2:146;
reconsider x, y, z as Vertex of 1GateCircStr(p,f) by Th44;
InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:49
.= {x,y,z} by FINSEQ_2:148;
then x in InputVertices 1GateCircStr(p,f) &
y in InputVertices 1GateCircStr(p,f) &
z in InputVertices 1GateCircStr(p,f) by ENUMSET1:14;
hence thesis by CIRCUIT2:def 5;
end;
theorem Th53:
for X being finite non empty set, f being Function of 3-tuples_on X, X
for s being State of 1GateCircuit(<*x,y,z*>,f) holds
Following s is stable
proof let X be finite non empty set, f be Function of 3-tuples_on X, X;
set p = <*x,y,z*>;
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 & dom s2 = the carrier of S by CIRCUIT1:4;
A2: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6
.= {x,y,z} \/ {[p,f]} by FINSEQ_2:148;
now let a be set; assume a in the carrier of S;
then a in {x,y,z} or a in {[p,f]} by A2,XBOOLE_0:def 2;
then A3: a = x or a = y or a = z or a = [p,f] by ENUMSET1:13,TARSKI:def 1;
s2.x = s1.x & s1.x = s.x & s2.y = s1.y & s1.y = s.y &
s2.z = s1.z & s1.z = s.z & s2.[p,f] = f.<*s1.x, s1.y, s1.z*> &
s1.[p,f] = f.<*s.x, s.y, s.z*> by Th52;
hence s2.a = s1.a by A3;
end;
hence Following s = Following Following s by A1,FUNCT_1:9;
end;
theorem
for f being Function of 3-tuples_on BOOLEAN, BOOLEAN
for s being State of 1GateCircuit(x,y,z,f) holds
(Following s).[<*x,y,z*>, f] = f.<*s.x, s.y, s.z*> &
(Following s).x = s.x & (Following s).y = s.y & (Following s).z = s.z
proof let f be Function of 3-tuples_on BOOLEAN, BOOLEAN;
let s be State of 1GateCircuit(x,y,z,f);
1GateCircuit(x,y,z,f) = 1GateCircuit(<*x,y,z*>, f) by Def11;
hence thesis by Th52;
end;
theorem
for f being Function of 3-tuples_on BOOLEAN, BOOLEAN
for s being State of 1GateCircuit(x,y,z,f) holds Following s is stable
proof let f be Function of 3-tuples_on BOOLEAN, BOOLEAN;
let s be State of 1GateCircuit(x,y,z,f);
1GateCircuit(x,y,z,f) = 1GateCircuit(<*x,y,z*>, f) by Def11;
hence thesis by Th53;
end;
begin :: Two Gates Circuit
definition
let x,y,c be set;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 2GatesCircStr(x,y,c,f) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign equals:
Def12:
1GateCircStr(<*x,y*>, f) +* 1GateCircStr(<*[<*x,y*>, f], c*>, f);
correctness;
end;
definition let x,y,c be set;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 2GatesCircOutput(x,y,c,f) ->
Element of InnerVertices 2GatesCircStr(x,y,c,f) equals:
Def13:
[<*[<*x,y*>, f], c*>, f];
coherence
proof set p = <*[<*x,y*>, f], c*>;
set S1 = 1GateCircStr(<*x,y*>, f);
set S2 = 1GateCircStr(p, f);
[p,f] in InnerVertices S2 &
2GatesCircStr(x,y,c,f) = S1+*S2 by Def12,Th47; hence thesis by Th21;
end;
correctness;
end;
definition let x,y,c be set;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
cluster 2GatesCircOutput(x,y,c,f) -> pair;
coherence
proof 2GatesCircOutput(x,y,c,f) = [<*[<*x,y*>, f], c*>, f] by Def13;
hence thesis;
end;
end;
theorem Th56:
InnerVertices 2GatesCircStr(x,y,c,f)
= {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)}
proof set p = <*[<*x,y*>, f], c*>;
set S1 = 1GateCircStr(<*x,y*>, f), S2 = 1GateCircStr(p, f);
set S = 2GatesCircStr(x,y,c,f);
S = S1+*S2 & S1 tolerates S2 by Def12,CIRCCOMB:51;
hence InnerVertices S
= (InnerVertices S1) \/ (InnerVertices S2) by CIRCCOMB:15
.= {[<*x,y*>, f]} \/ (InnerVertices S2) by CIRCCOMB:49
.= {[<*x,y*>, f]} \/ {[p, f]} by CIRCCOMB:49
.= {[<*x,y*>, f], [p, f]} by ENUMSET1:41
.= {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Def13;
end;
theorem Th57:
c <> [<*x,y*>, f] implies
InputVertices 2GatesCircStr(x,y,c,f) = {x,y,c}
proof assume
A1: c <> [<*x,y*>, f];
set p = <*[<*x,y*>, f], c*>;
set S1 = 1GateCircStr(<*x,y*>, f);
set S2 = 1GateCircStr(p, f);
set S = 2GatesCircStr(x,y,c,f);
set R = the ResultSort of S;
S = S1+*S2 by Def12;
then A2: the carrier of S = (the carrier of S1) \/ the carrier of S2
by CIRCCOMB:def 2;
A3: InputVertices S = (the carrier of S) \ rng R by MSAFREE2:def 2;
A4: rng R = InnerVertices S by MSAFREE2:def 3
.= {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56
.= {[<*x,y*>, f], [p,f]} by Def13;
A5: rng <*x,y*> = {x,y} by FINSEQ_2:147;
then A6: the carrier of S1 = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;
A7: rng p = {[<*x,y*>, f], c} by FINSEQ_2:147;
then A8: the carrier of S2 = {[<*x,y*>, f], c} \/ {[p,f]} by CIRCCOMB:def 6;
thus InputVertices S c= {x,y,c}
proof let z be set; assume A9: z in InputVertices S;
then A10: z in the carrier of S & not z in rng R by A3,XBOOLE_0:def 4;
z in the carrier of S1 or z in the carrier of S2 by A2,A9,XBOOLE_0:def
2;
then z in {x,y} or z in {[<*x,y*>,f]} or z in {[<*x,y*>, f], c} or
z in {[p,f]} by A6,A8,XBOOLE_0:def 2;
then z = x or z = y or z = [<*x,y*>,f] or z = c or z = [p,f] by TARSKI:def 1,
def 2;
hence thesis by A4,A10,ENUMSET1:14,TARSKI:def 2;
end;
let z be set;
assume z in {x,y,c};
then A11: z = x or z = y or z = c by ENUMSET1:13;
then z in {x,y} & [<*x,y*>, f] in rng p or z in {c} by A7,TARSKI:def 1,def 2;
then the_rank_of z in the_rank_of [<*x,y*>, f] &
the_rank_of [<*x,y*>, f] in the_rank_of [p,f] or
z = c & c in rng p by A5,A7,CIRCCOMB:50,TARSKI:def 1,def 2;
then A12: the_rank_of z in the_rank_of [p,f] & z <> [<*x,y*>, f]
by A1,CIRCCOMB:50,ORDINAL1:19;
then z <> [p,f];
then A13: not z in rng R by A4,A12,TARSKI:def 2;
z in {x,y} or z in rng p by A7,A11,TARSKI:def 2;
then z in InputVertices S1 or z in InputVertices S2 by A5,CIRCCOMB:49;
then z in the carrier of S by A2,XBOOLE_0:def 2;
hence thesis by A3,A13,XBOOLE_0:def 4;
end;
definition
let x,y,c be set;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
A1: 2GatesCircStr(x,y,c,f)
= 1GateCircStr(<*x,y*>, f) +* 1GateCircStr(<*[<*x,y*>, f], c*>, f)
by Def12;
func 2GatesCircuit(x,y,c,f) ->
strict Boolean gate`2=den Circuit of 2GatesCircStr(x,y,c,f) equals:
Def14:
1GateCircuit(x,y, f) +* 1GateCircuit([<*x,y*>, f], c, f);
coherence by A1;
end;
theorem Th58:
InnerVertices 2GatesCircStr(x,y,c,f) is Relation
proof
InnerVertices 2GatesCircStr(x,y,c,f)
= {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
hence thesis;
end;
theorem Th59:
for x,y,c being non pair set holds
InputVertices 2GatesCircStr(x,y,c,f) is without_pairs
proof let x,y,c be non pair set;
c <> [<*x,y*>, f];
then InputVertices 2GatesCircStr(x,y,c,f) = {x,y,c} by Th57;
hence thesis;
end;
theorem Th60:
x in the carrier of 2GatesCircStr(x,y,c,f) &
y in the carrier of 2GatesCircStr(x,y,c,f) &
c in the carrier of 2GatesCircStr(x,y,c,f)
proof set S1 = 1GateCircStr(<*x,y*>, f);
set S2 = 1GateCircStr(<*[<*x,y*>, f], c*>, f);
x in the carrier of S1 & y in the carrier of S1 & c in the carrier of S2
&
2GatesCircStr(x,y,c,f) = S1 +* S2 by Def12,Th43;
hence thesis by Th20;
end;
theorem
[<*x,y*>,f] in the carrier of 2GatesCircStr(x,y,c,f) &
[<*[<*x,y*>,f], c*>, f] in the carrier of 2GatesCircStr(x,y,c,f)
proof set S1 = 1GateCircStr(<*x,y*>, f);
set S2 = 1GateCircStr(<*[<*x,y*>, f], c*>, f);
[<*x,y*>, f] in the carrier of S1 &
[<*[<*x,y*>,f], c*>, f] in the carrier of S2 &
2GatesCircStr(x,y,c,f) = S1 +* S2 by Def12,Th43;
hence thesis by Th20;
end;
definition let S be unsplit non void non empty ManySortedSign;
let A be Boolean Circuit of S;
let s be State of A;
let v be Vertex of S;
redefine func s.v -> Element of BOOLEAN;
coherence
proof s.v in (the Sorts of A).v by CIRCUIT1:5;
hence thesis by CIRCCOMB:def 15;
end;
end;
reserve s for State of 2GatesCircuit(x,y,c,f);
Lm2: c <> [<*x,y*>, f] implies
(Following s).2GatesCircOutput(x,y,c,f) = f.<*s.[<*x,y*>,f], s.c*> &
(Following s).[<*x,y*>,f] = f.<*s.x, s.y*> &
(Following s).x = s.x & (Following s).y = s.y & (Following s).c = s.c
proof set p = <*[<*x,y*>, f], c*>;
set xyf = [<*x,y*>,f];
set S1 = 1GateCircStr(<*x,y*>, f), A1 = 1GateCircuit(x,y, f);
set S2 = 1GateCircStr(p, f), A2 = 1GateCircuit(xyf,c, f);
set S = 2GatesCircStr(x,y,c,f);
A1: S = S1+*S2 & 2GatesCircuit(x,y,c,f) = A1+*A2 by Def12,Def14;
assume c <> [<*x,y*>, f];
then A2: InputVertices S = {x,y,c} by Th57;
A3: InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
A4: 2GatesCircOutput(x,y,c,f) = [p,f] by Def13;
A5: x in InputVertices S & y in InputVertices S & c in InputVertices S
by A2,ENUMSET1:14;
reconsider xyf as Element of InnerVertices S by A3,TARSKI:def 2;
rng p = {xyf,c} by FINSEQ_2:147;
then xyf in rng p & c in rng p by TARSKI:def 2;
then A6: xyf in InputVertices S2 & c in InputVertices S2 by CIRCCOMB:49;
reconsider s1 = s|the carrier of S1 as State of A1 by A1,Th26;
reconsider s2 = s|the carrier of S2 as State of A2 by A1,Th26;
A7: dom s2 = the carrier of S2 by CIRCUIT1:4;
A8: dom s1 = the carrier of S1 by CIRCUIT1:4;
reconsider vx = x, vy = y as Vertex of S1 by Th43;
reconsider xyf1 = xyf as Element of InnerVertices S1 by Th47;
reconsider xyf' = xyf, c' = c as Vertex of S2 by A6;
reconsider v2 = [p,f] as Element of InnerVertices S2 by Th47;
thus (Following s).2GatesCircOutput(x,y,c,f)
= (Following s2).v2 by A1,A4,CIRCCOMB:72
.= f.<*s2.xyf', s2.c'*> by Th50
.= f.<*s.[<*x,y*>,f], s2.c'*> by A7,FUNCT_1:70
.= f.<*s.[<*x,y*>,f], s.c*> by A7,FUNCT_1:70;
thus (Following s).[<*x,y*>,f]
= (Following s1).xyf1 by A1,CIRCCOMB:72
.= f.<*s1.vx, s1.vy*> by Th50
.= f.<*s.x, s1.vy*> by A8,FUNCT_1:70
.= f.<*s.x, s.y*> by A8,FUNCT_1:70;
thus thesis by A5,CIRCUIT2:def 5;
end;
theorem Th62:
c <> [<*x,y*>, f] implies
(Following(s,2)).2GatesCircOutput(x,y,c,f) = f.<*f.<*s.x, s.y*>, s.c*> &
(Following(s,2)).[<*x,y*>,f] = f.<*s.x, s.y*> &
(Following(s,2)).x = s.x & (Following(s,2)).y = s.y &
(Following(s,2)).c = s.c
proof set p = <*[<*x,y*>, f], c*>;
set xyf = [<*x,y*>,f];
set S1 = 1GateCircStr(<*x,y*>, f), A1 = 1GateCircuit(x,y, f);
set S2 = 1GateCircStr(p, f), A2 = 1GateCircuit(xyf,c, f);
set S = 2GatesCircStr(x,y,c,f);
A1: S = S1+*S2 & 2GatesCircuit(x,y,c,f) = A1+*A2 by Def12,Def14;
assume c <> [<*x,y*>, f];
then A2: InputVertices S = {x,y,c} by Th57;
A3: InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
A4: 2GatesCircOutput(x,y,c,f) = [p,f] by Def13;
A5: x in {x,y} & y in {x,y} & c in {c} & c in {[<*x,y*>,f], c} by TARSKI:def 1,
def 2;
A6: x in InputVertices S & y in InputVertices S & c in InputVertices S
by A2,ENUMSET1:14;
reconsider xx = x, yy = y, cc = c as Vertex of S by Th60;
A7: (Following s).xx = s.x & (Following s).yy = s.y &
(Following s).cc = s.c by A6,CIRCUIT2:def 5;
then A8: (Following Following s).xx = s.x & (Following Following s).yy = s.y &
(Following Following s).cc = s.c by A6,CIRCUIT2:def 5;
reconsider xyf as Element of InnerVertices S by A3,TARSKI:def 2;
rng p = {xyf,c} by FINSEQ_2:147;
then xyf in rng p & c in rng p by TARSKI:def 2;
then A9: xyf in InputVertices S2 & c in InputVertices S2 by CIRCCOMB:49;
reconsider s1 = s|the carrier of S1 as State of A1 by A1,Th26;
set fs = Following s;
reconsider fs2 = fs|the carrier of S2 as State of A2 by A1,Th26;
reconsider fs1 = fs|the carrier of S1 as State of A1 by A1,Th26;
A10: dom fs2 = the carrier of S2 by CIRCUIT1:4;
A11: dom fs1 = the carrier of S1 by CIRCUIT1:4;
reconsider vx = x, vy = y as Vertex of S1 by Th43;
A12: xyf in InnerVertices S1 by Th47;
reconsider xyf1 = xyf as Element of InnerVertices S1 by Th47;
A13: dom s1 = the carrier of S1 & InputVertices S1 = rng <*x,y*> &
rng <*x,y*> = {x,y} & InputVertices S1 c= the carrier of S1
by CIRCCOMB:49,CIRCUIT1:4,FINSEQ_2:147;
reconsider xyf' = xyf, c' = c as Vertex of S2 by A9;
reconsider v2 = [p,f] as Element of InnerVertices S2 by Th47;
A14: Following(s,1+1) = Following Following s by Th15;
hence (Following(s,2)).2GatesCircOutput(x,y,c,f)
= (Following fs2).v2 by A1,A4,CIRCCOMB:72
.= f.<*fs2.xyf', fs2.c'*> by Th50
.= f.<*(Following s).xyf, fs2.c*> by A10,FUNCT_1:70
.= f.<*(Following s).xyf, (Following s).c'*> by A10,FUNCT_1:70
.= f.<*(Following s).xyf, s.cc*> by A6,CIRCUIT2:def 5
.= f.<*(Following s1).xyf, s.cc*> by A1,A12,CIRCCOMB:72
.= f.<*f.<*s1.x, s1.y*>, s.cc*> by Th50
.= f.<*f.<*s.x,s1.y*>, s.cc*> by A5,A13,FUNCT_1:70
.= f.<*f.<*s.x,s.y*>, s.c*> by A5,A13,FUNCT_1:70;
thus (Following(s,2)).[<*x,y*>,f]
= (Following fs1).xyf1 by A1,A14,CIRCCOMB:72
.= f.<*fs1.vx, fs1.vy*> by Th50
.= f.<*s.x, fs1.vy*> by A7,A11,FUNCT_1:70
.= f.<*s.x, s.y*> by A7,A11,FUNCT_1:70;
thus thesis by A8,Th15;
end;
theorem Th63:
c <> [<*x,y*>, f] implies Following(s,2) is stable
proof assume
A1: c <> [<*x,y*>, f];
set S = 2GatesCircStr(x,y,c,f);
now
thus dom Following Following(s,2) = the carrier of S &
dom Following(s,2) = the carrier of S by CIRCUIT1:4;
let a be set; assume a in the carrier of S;
then reconsider v = a as Vertex of S;
A2: InputVertices S = {x,y,c} by A1,Th57;
A3: InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
A4: InputVertices S \/ InnerVertices S = the carrier of S by MSAFREE2:3;
A5: (Following(s,2)).[<*x,y*>,f] = f.<*s.x, s.y*> &
(Following(s,2)).2GatesCircOutput(x,y,c,f) = f.<*f.<*s.x, s.y*>, s.c*> &
(Following(s,2)).x = s.x & (Following(s,2)).y = s.y &
(Following(s,2)).c = s.c
by A1,Th62;
per cases by A4,XBOOLE_0:def 2;
suppose v in InputVertices S;
then v = x or v = y or v = c by A2,ENUMSET1:13;
hence (Following Following(s,2)).a = (Following(s,2)).a by A1,Lm2;
suppose v in InnerVertices S;
then v = [<*x,y*>, f] or v = 2GatesCircOutput(x,y,c,f) by A3,TARSKI:def
2;
hence (Following Following(s,2)).a = (Following(s,2)).a by A1,A5,Lm2;
end;
hence Following(s,2) = Following Following(s,2) by FUNCT_1:9;
end;
theorem Th64:
c <> [<*x,y*>, 'xor'] implies
for s being State of 2GatesCircuit(x,y,c,'xor')
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds
(Following(s,2)).2GatesCircOutput(x,y,c,'xor') = a1 'xor' a2 'xor' a3
proof set f = 'xor'; assume
A1: c <> [<*x,y*>, f];
let s be State of 2GatesCircuit(x,y,c,f);
let a1,a2,a3 be Element of BOOLEAN; assume
a1 = s.x & a2 = s.y & a3 = s.c;
hence (Following(s,2)).2GatesCircOutput(x,y,c,f)
= f.<*f.<*a1, a2*>, a3*> by A1,Th62
.= f.<*a1 'xor' a2, a3*> by Def4
.= a1 'xor' a2 'xor' a3 by Def4;
end;
theorem
c <> [<*x,y*>, 'or'] implies
for s being State of 2GatesCircuit(x,y,c,'or')
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds
(Following(s,2)).2GatesCircOutput(x,y,c,'or') = a1 'or' a2 'or' a3
proof set f = 'or'; assume
A1: c <> [<*x,y*>, f];
let s be State of 2GatesCircuit(x,y,c,f);
let a1,a2,a3 be Element of BOOLEAN; assume
a1 = s.x & a2 = s.y & a3 = s.c;
hence (Following(s,2)).2GatesCircOutput(x,y,c,f)
= f.<*f.<*a1, a2*>, a3*> by A1,Th62
.= f.<*a1 'or' a2, a3*> by Def5
.= a1 'or' a2 'or' a3 by Def5;
end;
theorem
c <> [<*x,y*>, '&'] implies
for s being State of 2GatesCircuit(x,y,c,'&')
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds
(Following(s,2)).2GatesCircOutput(x,y,c,'&') = a1 '&' a2 '&' a3
proof set f = '&'; assume
A1: c <> [<*x,y*>, f];
let s be State of 2GatesCircuit(x,y,c,f);
let a1,a2,a3 be Element of BOOLEAN; assume
a1 = s.x & a2 = s.y & a3 = s.c;
hence (Following(s,2)).2GatesCircOutput(x,y,c,f)
= f.<*f.<*a1, a2*>, a3*> by A1,Th62
.= f.<*a1 '&' a2, a3*> by Def6
.= a1 '&' a2 '&' a3 by Def6;
end;
begin :: Bit Adder Circuit
definition
let x,y,c be set;
func BitAdderOutput(x,y,c) ->
Element of InnerVertices 2GatesCircStr(x,y,c, 'xor') equals:
Def15:
2GatesCircOutput(x,y,c, 'xor');
coherence;
end;
definition
let x,y,c be set;
func BitAdderCirc(x,y,c) ->
strict Boolean gate`2=den Circuit of 2GatesCircStr(x,y,c, 'xor') equals:
Def16:
2GatesCircuit(x,y,c, 'xor');
coherence;
end;
definition
let x,y,c be set;
func MajorityIStr(x,y,c) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign equals:
Def17:
1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&') +*
1GateCircStr(<*c,x*>, '&');
correctness;
end;
definition
let x,y,c be set;
func MajorityStr(x,y,c) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign equals:
Def18:
MajorityIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3);
correctness;
end;
definition
let x,y,c be set;
A1: MajorityIStr(x,y,c) = 1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&') by Def17;
func MajorityICirc(x,y,c) ->
strict Boolean gate`2=den Circuit of MajorityIStr(x,y,c) equals:
Def19:
1GateCircuit(x,y, '&') +* 1GateCircuit(y,c, '&') +*
1GateCircuit(c,x, '&');
coherence by A1;
end;
theorem Th67:
InnerVertices MajorityStr(x,y,c) is Relation
proof
A1: MajorityStr(x,y,c) = MajorityIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3)
by Def18;
A2: MajorityIStr(x,y,c) = 1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&') by Def17;
A3: InnerVertices 1GateCircStr(<*x,y*>,'&') is Relation &
InnerVertices 1GateCircStr(<*c,x*>,'&') is Relation &
InnerVertices 1GateCircStr(<*y,c*>,'&') is Relation by Th38;
then InnerVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&'))
is Relation by Th3;
then InnerVertices 1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'],
[<*c,x*>, '&']*>, or3) is Relation &
InnerVertices MajorityIStr(x,y,c) is Relation by A2,A3,Th3,Th38;
hence thesis by A1,Th3;
end;
theorem Th68:
for x,y,c being non pair set holds
InputVertices MajorityStr(x,y,c) is without_pairs
proof let x,y,c be non pair set;
set M = MajorityStr(x,y,c), MI = MajorityIStr(x,y,c);
set S = 1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'],
[<*c,x*>, '&']*>, or3);
A1: M = MI +* S by Def18;
A2: MI = 1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&') by Def17;
A3: InputVertices 1GateCircStr(<*x,y*>,'&') is without_pairs &
InputVertices 1GateCircStr(<*c,x*>,'&') is without_pairs &
InputVertices 1GateCircStr(<*y,c*>,'&') is without_pairs by Th41;
then InputVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&'))
is without_pairs by Th9;
then A4: InputVertices MI is without_pairs by A2,A3,Th9;
InnerVertices S is Relation by Th38;
then A5: InputVertices M =
(InputVertices MI) \/
(InputVertices S \ InnerVertices MI) by A1,A4,Th6;
given xx being pair set such that
A6: xx in InputVertices M;
A7: InputVertices S = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by Th42;
A8: InnerVertices 1GateCircStr(<*x,y*>, '&') = {[<*x,y*>, '&']} &
InnerVertices 1GateCircStr(<*y,c*>, '&') = {[<*y,c*>, '&']} &
InnerVertices 1GateCircStr(<*c,x*>, '&') = {[<*c,x*>, '&']} by CIRCCOMB:49;
A9: 1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*y,c*>, '&') &
1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') &
1GateCircStr(<*y,c*>, '&') tolerates 1GateCircStr(<*c,x*>, '&')
by CIRCCOMB:51;
then A10: InnerVertices (1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>,
'&')) =
{[<*x,y*>, '&']} \/ {[<*y,c*>, '&']} by A8,CIRCCOMB:15;
1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&')
tolerates 1GateCircStr(<*c,x*>, '&') by A9,CIRCCOMB:7;
then InnerVertices MI = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/ {[<*c,x*>,
'&']}
by A2,A8,A10,CIRCCOMB:15
.= {[<*x,y*>,'&'], [<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:41
.= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by ENUMSET1:43;
then InputVertices S \ InnerVertices MI = {} by A7,XBOOLE_1:37;
hence thesis by A4,A5,A6,Def2;
end;
theorem
for s being State of MajorityICirc(x,y,c), a,b being Element of BOOLEAN
st a = s.x & b = s.y holds (Following s).[<*x,y*>, '&'] = a '&' b
proof set xy = <*x,y*>;
set S1 = 1GateCircStr(xy, '&'), A1 = 1GateCircuit(x,y, '&');
set S2 = 1GateCircStr(<*y,c*>, '&'), A2 = 1GateCircuit(y,c, '&');
set S3 = 1GateCircStr(<*c,x*>, '&'), A3 = 1GateCircuit(c,x, '&');
set S = MajorityIStr(x,y,c), A = MajorityICirc(x,y,c);
let s be State of A; let a,b be Element of BOOLEAN such that
A1: a = s.x & b = s.y;
reconsider v1 = [xy, '&'] as Element of InnerVertices S1 by Th47;
S = S1+*S2+*S3 by Def17;
then A2: S = S1+*(S2+*S3) by CIRCCOMB:10;
then reconsider v = v1 as Element of InnerVertices S by Th21;
A = A1+*A2+*A3 by Def19;
then A3: A = A1+*(A2+*A3) by Th25;
then reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
A4: dom s1 = the carrier of S1 by CIRCUIT1:4;
reconsider xx = x, yy = y as Vertex of S1 by Th43;
reconsider xx, yy as Vertex of S by A2,Th20;
thus (Following s).[xy, '&'] = (Following s1).v by A2,A3,CIRCCOMB:72
.= '&'.<*s1.xx,s1.yy*> by Th50
.= '&'.<*s.xx,s1.yy*> by A4,FUNCT_1:70
.= '&'.<*s.xx,s.yy*> by A4,FUNCT_1:70
.= a '&' b by A1,Def6;
end;
theorem
for s being State of MajorityICirc(x,y,c), a,b being Element of BOOLEAN
st a = s.y & b = s.c holds (Following s).[<*y,c*>, '&'] = a '&' b
proof set yc = <*y,c*>;
set S1 = 1GateCircStr(<*x,y*>, '&'), A1 = 1GateCircuit(x,y, '&');
set S2 = 1GateCircStr(yc, '&'), A2 = 1GateCircuit(y,c, '&');
set S3 = 1GateCircStr(<*c,x*>, '&'), A3 = 1GateCircuit(c,x, '&');
set S = MajorityIStr(x,y,c), A = MajorityICirc(x,y,c);
let s be State of A; let a,b be Element of BOOLEAN such that
A1: a = s.y & b = s.c;
reconsider v2 = [yc, '&'] as Element of InnerVertices S2 by Th47;
A2: S = S1+*S2+*S3 & S1+*S2 = S2+*S1 by Def17,Th23;
then A3: S = S2+*(S1+*S3) by CIRCCOMB:10;
then reconsider v = v2 as Element of InnerVertices S by Th21;
A = A1+*A2+*A3 & A1+*A2 = A2+*A1 by Def19,Th24;
then A4: A = A2+*(A1+*A3) by A2,Th25;
then reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
A5: dom s2 = the carrier of S2 by CIRCUIT1:4;
reconsider yy = y, cc = c as Vertex of S2 by Th43;
reconsider yy, cc as Vertex of S by A3,Th20;
thus (Following s).[yc, '&'] = (Following s2).v by A3,A4,CIRCCOMB:72
.= '&'.<*s2.yy,s2.cc*> by Th50
.= '&'.<*s.yy,s2.cc*> by A5,FUNCT_1:70
.= '&'.<*s.yy,s.cc*> by A5,FUNCT_1:70
.= a '&' b by A1,Def6;
end;
theorem
for s being State of MajorityICirc(x,y,c), a,b being Element of BOOLEAN
st a = s.c & b = s.x holds (Following s).[<*c,x*>, '&'] = a '&' b
proof set cx = <*c,x*>;
set S1 = 1GateCircStr(<*x,y*>, '&'), A1 = 1GateCircuit(x,y, '&');
set S2 = 1GateCircStr(<*y,c*>, '&'), A2 = 1GateCircuit(y,c, '&');
set S3 = 1GateCircStr(cx, '&'), A3 = 1GateCircuit(c,x, '&');
set S = MajorityIStr(x,y,c), A = MajorityICirc(x,y,c);
let s be State of A; let a,b be Element of BOOLEAN such that
A1: a = s.c & b = s.x;
reconsider v3 = [cx, '&'] as Element of InnerVertices S3 by Th47;
A2: S = S1+*S2+*S3 by Def17;
then reconsider v = v3 as Element of InnerVertices S by Th21;
A3: A = A1+*A2+*A3 by Def19;
then reconsider s3 = s|the carrier of S3 as State of A3 by Th26;
A4: dom s3 = the carrier of S3 by CIRCUIT1:4;
reconsider cc = c, xx = x as Vertex of S3 by Th43;
reconsider cc, xx as Vertex of S by A2,Th20;
thus (Following s).[cx, '&'] = (Following s3).v by A2,A3,CIRCCOMB:72
.= '&'.<*s3.cc,s3.xx*> by Th50
.= '&'.<*s.cc,s3.xx*> by A4,FUNCT_1:70
.= '&'.<*s.cc,s.xx*> by A4,FUNCT_1:70
.= a '&' b by A1,Def6;
end;
definition
let x,y,c be set;
A1: MajorityStr(x,y,c) = MajorityIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3)
by Def18;
func MajorityOutput(x,y,c) -> Element of InnerVertices MajorityStr(x,y,c)
equals:
Def20:
[<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3];
coherence
proof
[<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3] in
InnerVertices
1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3)
by Th47; hence thesis by A1,Th21;
end;
correctness;
end;
definition
let x,y,c be set;
A1: MajorityStr(x,y,c) = MajorityIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3)
by Def18;
func MajorityCirc(x,y,c) ->
strict Boolean gate`2=den Circuit of MajorityStr(x,y,c) equals
MajorityICirc(x,y,c) +*
1GateCircuit([<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&'], or3);
coherence by A1;
end;
theorem Th72:
x in the carrier of MajorityStr(x,y,c) &
y in the carrier of MajorityStr(x,y,c) &
c in the carrier of MajorityStr(x,y,c)
proof
A1: MajorityStr(x,y,c) = MajorityIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3)
by Def18;
A2: MajorityIStr(x,y,c) = 1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&') by Def17;
y in the carrier of 1GateCircStr(<*x,y*>, '&') by Th43;
then A3: y in the carrier of 1GateCircStr(<*x,y*>, '&')+*1GateCircStr(<*y,c*>,
'&')
by Th20;
x in the carrier of 1GateCircStr(<*c,x*>, '&') &
c in the carrier of 1GateCircStr(<*c,x*>, '&') by Th43;
then x in the carrier of MajorityIStr(x,y,c) &
y in the carrier of MajorityIStr(x,y,c) &
c in the carrier of MajorityIStr(x,y,c)
by A2,A3,Th20;
hence thesis by A1,Th20;
end;
theorem Th73:
[<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) &
[<*y,c*>,'&'] in InnerVertices MajorityStr(x,y,c) &
[<*c,x*>,'&'] in InnerVertices MajorityStr(x,y,c)
proof
A1: MajorityStr(x,y,c) = MajorityIStr(x,y,c) +*
1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3)
by Def18;
A2: MajorityIStr(x,y,c) = 1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&') by Def17;
[<*x,y*>,'&'] in InnerVertices 1GateCircStr(<*x,y*>, '&') &
[<*y,c*>,'&'] in InnerVertices 1GateCircStr(<*y,c*>, '&') by Th47;
then [<*c,x*>,'&'] in InnerVertices 1GateCircStr(<*c,x*>, '&') &
[<*x,y*>,'&'] in InnerVertices
(1GateCircStr(<*x,y*>, '&')+*1GateCircStr(<*y,c*>, '&')) &
[<*y,c*>,'&'] in InnerVertices
(1GateCircStr(<*x,y*>, '&')+*1GateCircStr(<*y,c*>, '&'))
by Th21,Th47;
then [<*x,y*>,'&'] in InnerVertices MajorityIStr(x,y,c) &
[<*y,c*>,'&'] in InnerVertices MajorityIStr(x,y,c) &
[<*c,x*>,'&'] in InnerVertices MajorityIStr(x,y,c) by A2,Th21;
hence thesis by A1,Th21;
end;
theorem Th74:
for x,y,c being non pair set holds
x in InputVertices MajorityStr(x,y,c) &
y in InputVertices MajorityStr(x,y,c) &
c in InputVertices MajorityStr(x,y,c)
proof let x,y,c be non pair set;
InputVertices MajorityStr(x,y,c) = (the carrier of MajorityStr(x,y,c)) \
rng the ResultSort of MajorityStr(x,y,c) by MSAFREE2:def 2;
then A1: InputVertices MajorityStr(x,y,c) =
(the carrier of MajorityStr(x,y,c)) \ InnerVertices MajorityStr(x,y,c)
by MSAFREE2:def 3;
A2: x in the carrier of MajorityStr(x,y,c) &
y in the carrier of MajorityStr(x,y,c) &
c in the carrier of MajorityStr(x,y,c) by Th72;
A3: InnerVertices MajorityStr(x,y,c) is Relation by Th67;
assume not thesis;
then x in InnerVertices MajorityStr(x,y,c) or
y in InnerVertices MajorityStr(x,y,c) or
c in InnerVertices MajorityStr(x,y,c) by A1,A2,XBOOLE_0:def 4;
then (ex a,b being set st x = [a,b]) or
(ex a,b being set st y = [a,b]) or
(ex a,b being set st c = [a,b]) by A3,RELAT_1:def 1;
hence contradiction;
end;
theorem Th75:
for x,y,c being non pair set holds
InputVertices MajorityStr(x,y,c) = {x,y,c} &
InnerVertices MajorityStr(x,y,c) =
{[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)}
proof let x,y,c be non pair set;
set x_y =[<*x,y*>,'&'], y_c = [<*y,c*>,'&'], c_x = [<*c,x*>,'&'];
set MI = MajorityIStr(x,y,c), S = 1GateCircStr(<*x_y, y_c, c_x*>, or3);
set M = MajorityStr(x,y,c);
A1: M = MI +* S by Def18;
A2: MI = 1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&') by Def17;
A3: InputVertices 1GateCircStr(<*x,y*>,'&') is without_pairs &
InputVertices 1GateCircStr(<*c,x*>,'&') is without_pairs &
InputVertices 1GateCircStr(<*y,c*>,'&') is without_pairs by Th41;
then A4: InputVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&'))
is without_pairs by Th9;
then A5: InputVertices MI is without_pairs by A2,A3,Th9;
A6: InputVertices 1GateCircStr(<*x,y*>,'&') = {x,y} &
InputVertices 1GateCircStr(<*c,x*>,'&') = {c,x} &
InputVertices 1GateCircStr(<*y,c*>,'&') = {y,c} by Th40;
InnerVertices S is Relation by Th38;
then A7: InputVertices M =
(InputVertices MI) \/
(InputVertices S \ InnerVertices MI) by A1,A5,Th6;
A8: InputVertices S = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by Th42;
A9: InnerVertices 1GateCircStr(<*x,y*>, '&') = {[<*x,y*>, '&']} &
InnerVertices 1GateCircStr(<*y,c*>, '&') = {[<*y,c*>, '&']} &
InnerVertices 1GateCircStr(<*c,x*>, '&') = {[<*c,x*>, '&']} by CIRCCOMB:49;
A10: 1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*y,c*>, '&') &
1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') &
1GateCircStr(<*y,c*>, '&') tolerates 1GateCircStr(<*c,x*>, '&')
by CIRCCOMB:51;
then A11: InnerVertices (1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>,
'&')) =
{[<*x,y*>, '&']} \/ {[<*y,c*>, '&']} by A9,CIRCCOMB:15;
1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&')
tolerates 1GateCircStr(<*c,x*>, '&') by A10,CIRCCOMB:7;
then A12: InnerVertices MI = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/ {[<*c,x*>,
'&']}
by A2,A9,A11,CIRCCOMB:15
.= {[<*x,y*>,'&'], [<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:41
.= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by ENUMSET1:43;
then InputVertices S \ InnerVertices MI = {} by A8,XBOOLE_1:37;
hence InputVertices M =
(InputVertices(1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&')))
\/ InputVertices 1GateCircStr(<*c,x*>,'&') by A2,A3,A4,A7,A9,A11,Th7
.= (InputVertices 1GateCircStr(<*x,y*>,'&')) \/
(InputVertices 1GateCircStr(<*y,c*>,'&')) \/
(InputVertices 1GateCircStr(<*c,x*>,'&')) by A3,A9,Th7
.= {x,y,y,c} \/ {c,x} by A6,ENUMSET1:45
.= {y,y,x,c} \/ {c,x} by ENUMSET1:110
.= {y,x,c} \/ {c,x} by ENUMSET1:71
.= {x,y,c} \/ {c,x} by ENUMSET1:99
.= {x,y,c} \/ ({c}\/{x}) by ENUMSET1:41
.= {x,y,c} \/ {c} \/ {x} by XBOOLE_1:4
.= {c,x,y} \/ {c} \/ {x} by ENUMSET1:100
.= {c,c,x,y} \/ {x} by ENUMSET1:44
.= {c,x,y} \/ {x} by ENUMSET1:71
.= {x,y,c} \/ {x} by ENUMSET1:100
.= {x,x,y,c} by ENUMSET1:44
.= {x,y,c} by ENUMSET1:71;
MI tolerates S by CIRCCOMB:55;
hence InnerVertices M = (InnerVertices MI) \/ (InnerVertices S)
by A1,CIRCCOMB:15
.= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/
{[<*x_y, y_c, c_x*>, or3]} by A12,CIRCCOMB:49
.= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/
{MajorityOutput(x,y,c)} by Def20;
end;
Lm3:
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c
holds
(Following s).[<*x,y*>,'&'] = a1 '&' a2 &
(Following s).[<*y,c*>,'&'] = a2 '&' a3 &
(Following s).[<*c,x*>,'&'] = a3 '&' a1
proof let x,y,c be non pair set;
let s be State of MajorityCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.x & a2 = s.y & a3 = s.c;
set S = MajorityStr(x,y,c);
A2: InnerVertices S = the OperSymbols of S by Th37;
A3: dom s = the carrier of S by CIRCUIT1:4;
A4: x in the carrier of S & y in the carrier of S & c in the carrier of S
by Th72;
[<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
hence (Following s).[<*x,y*>,'&']
= '&'.(s*<*x,y*>) by A2,Th35
.= '&'.<*a1,a2*> by A1,A3,A4,FINSEQ_2:145
.= a1 '&' a2 by Def6;
[<*y,c*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
hence (Following s).[<*y,c*>,'&']
= '&'.(s*<*y,c*>) by A2,Th35
.= '&'.<*a2,a3*> by A1,A3,A4,FINSEQ_2:145
.= a2 '&' a3 by Def6;
[<*c,x*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
hence (Following s).[<*c,x*>,'&']
= '&'.(s*<*c,x*>) by A2,Th35
.= '&'.<*a3,a1*> by A1,A3,A4,FINSEQ_2:145
.= a3 '&' a1 by Def6;
end;
theorem
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.y
holds (Following s).[<*x,y*>,'&'] = a1 '&' a2
proof let x,y,c be non pair set; let s be State of MajorityCirc(x,y,c);
reconsider a = c as Vertex of MajorityStr(x,y,c) by Th72;
s.a is Element of BOOLEAN;
hence thesis by Lm3;
end;
theorem
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a2,a3 being Element of BOOLEAN st a2 = s.y & a3 = s.c
holds (Following s).[<*y,c*>,'&'] = a2 '&' a3
proof let x,y,c be non pair set; let s be State of MajorityCirc(x,y,c);
reconsider a = x as Vertex of MajorityStr(x,y,c) by Th72;
s.a is Element of BOOLEAN;
hence thesis by Lm3;
end;
theorem
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a3 being Element of BOOLEAN st a1 = s.x & a3 = s.c
holds (Following s).[<*c,x*>,'&'] = a3 '&' a1
proof let x,y,c be non pair set; let s be State of MajorityCirc(x,y,c);
reconsider a = y as Vertex of MajorityStr(x,y,c) by Th72;
s.a is Element of BOOLEAN;
hence thesis by Lm3;
end;
theorem Th79:
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a2,a3 being Element of BOOLEAN st
a1 = s.[<*x,y*>,'&'] & a2 = s.[<*y,c*>,'&'] & a3 = s.[<*c,x*>,'&']
holds (Following s).MajorityOutput(x,y,c) = a1 'or' a2 'or' a3
proof let x,y,c be non pair set;
let s be State of MajorityCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.[<*x,y*>,'&'] & a2 = s.[<*y,c*>,'&'] & a3 = s.[<*c,x*>,'&'];
set x_y =[<*x,y*>,'&'], y_c = [<*y,c*>,'&'], c_x = [<*c,x*>,'&'];
set S = MajorityStr(x,y,c);
A2: InnerVertices S = the OperSymbols of S by Th37;
A3: dom s = the carrier of S by CIRCUIT1:4;
reconsider x_y, y_c, c_x as Element of InnerVertices S by Th73;
MajorityOutput(x,y,c) = [<*x_y, y_c, c_x*>, or3] by Def20;
hence (Following s).MajorityOutput(x,y,c)
= or3.(s*<*x_y, y_c, c_x*>) by A2,Th35
.= or3.<*a1,a2,a3*> by A1,A3,FINSEQ_2:146
.= a1 'or' a2 'or' a3 by Def7;
end;
Lm4:
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c
holds
(Following(s,2)).MajorityOutput(x,y,c) =
a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 &
(Following(s,2)).[<*x,y*>,'&'] = a1 '&' a2 &
(Following(s,2)).[<*y,c*>,'&'] = a2 '&' a3 &
(Following(s,2)).[<*c,x*>,'&'] = a3 '&' a1
proof let x,y,c be non pair set;
let s be State of MajorityCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.x & a2 = s.y & a3 = s.c;
set x_y =[<*x,y*>,'&'], y_c = [<*y,c*>,'&'], c_x = [<*c,x*>,'&'];
set S = MajorityStr(x,y,c);
reconsider x' = x, y' = y, c' = c as Vertex of S by Th72;
x in InputVertices S & y in InputVertices S & c in InputVertices S
by Th74;
then A2: (Following s).x' = s.x & (Following s).y' = s.y & (Following s).c' =
s.c
by CIRCUIT2:def 5;
A3: Following(s,2) = Following Following s by Th15;
(Following s).x_y = a1 '&' a2 & (Following s).y_c = a2 '&' a3 &
(Following s).c_x = a3 '&' a1 by A1,Lm3;
hence (Following(s,2)).MajorityOutput(x,y,c) =
a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by A3,Th79;
thus thesis by A1,A2,A3,Lm3;
end;
theorem
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a2 being Element of BOOLEAN st a1 = s.x & a2 = s.y
holds (Following(s,2)).[<*x,y*>,'&'] = a1 '&' a2
proof let x,y,c be non pair set; let s be State of MajorityCirc(x,y,c);
reconsider a = c as Vertex of MajorityStr(x,y,c) by Th72;
s.a is Element of BOOLEAN;
hence thesis by Lm4;
end;
theorem
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a2,a3 being Element of BOOLEAN st a2 = s.y & a3 = s.c
holds (Following(s,2)).[<*y,c*>,'&'] = a2 '&' a3
proof let x,y,c be non pair set; let s be State of MajorityCirc(x,y,c);
reconsider a = x as Vertex of MajorityStr(x,y,c) by Th72;
s.a is Element of BOOLEAN;
hence thesis by Lm4;
end;
theorem
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a3 being Element of BOOLEAN st a1 = s.x & a3 = s.c
holds (Following(s,2)).[<*c,x*>,'&'] = a3 '&' a1
proof let x,y,c be non pair set; let s be State of MajorityCirc(x,y,c);
reconsider a = y as Vertex of MajorityStr(x,y,c) by Th72;
s.a is Element of BOOLEAN;
hence thesis by Lm4;
end;
theorem
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c
holds
(Following(s,2)).MajorityOutput(x,y,c) =
a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by Lm4;
theorem Th84:
for x,y,c being non pair set for s being State of MajorityCirc(x,y,c)
holds Following(s,2) is stable
proof let x,y,c be non pair set; set S = MajorityStr(x,y,c);
let s be State of MajorityCirc(x,y,c);
A1: dom Following Following(s,2) = the carrier of S &
dom Following(s,2) = the carrier of S by CIRCUIT1:4;
reconsider xx = x, yy = y, cc = c as Vertex of S by Th72;
set a1 = s.xx, a2 = s.yy, a3 = s.cc;
set ffs = Following(s,2), fffs = Following ffs;
a1 = s.x & a2 = s.y & a3 = s.c;
then A2: ffs.MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 &
ffs.[<*x,y*>,'&'] = a1 '&' a2 &
ffs.[<*y,c*>,'&'] = a2 '&' a3 &
ffs.[<*c,x*>,'&'] = a3 '&' a1 by Lm4;
A3: ffs = Following Following s by Th15;
A4: x in InputVertices S & y in InputVertices S & c in InputVertices S
by Th74;
then (Following s).x = a1 & (Following s).y = a2 & (Following s).c = a3
by CIRCUIT2:def 5;
then A5: ffs.x = a1 & ffs.y = a2 & ffs.c = a3 by A3,A4,CIRCUIT2:def 5;
now let a be set; assume
A6: a in the carrier of S;
then reconsider v = a as Vertex of S;
A7: v in InputVertices S \/ InnerVertices S by A6,MSAFREE2:3;
thus ffs.a = (fffs).a
proof per cases by A7,XBOOLE_0:def 2;
suppose v in InputVertices S;
hence thesis by CIRCUIT2:def 5;
suppose v in InnerVertices S;
then v in {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/
{MajorityOutput(x,y,c)} by Th75;
then v in {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} or
v in {MajorityOutput(x,y,c)} by XBOOLE_0:def 2;
then v = [<*x,y*>,'&'] or v = [<*y,c*>,'&'] or v = [<*c,x*>,'&'] or
v = MajorityOutput(x,y,c) by ENUMSET1:13,TARSKI:def 1;
hence thesis by A2,A5,Lm3,Th79;
end;
end;
hence ffs = fffs by A1,FUNCT_1:9;
end;
definition
let x,y,c be set;
func BitAdderWithOverflowStr(x,y,c) ->
unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign
equals:
Def22:
2GatesCircStr(x,y,c, 'xor') +* MajorityStr(x,y,c);
coherence;
end;
theorem Th85:
for x,y,c being non pair set holds
InputVertices BitAdderWithOverflowStr(x,y,c) = {x,y,c}
proof let x,y,c be non pair set;
set S = BitAdderWithOverflowStr(x,y,c);
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
A1: S = S1 +* S2 by Def22;
A2: InputVertices S1 is without_pairs & InnerVertices S1 is Relation
by Th58,Th59;
A3: InputVertices S2 is without_pairs & InnerVertices S2 is Relation
by Th67,Th68;
c <> [<*x,y*>, 'xor'];
then InputVertices S1 = {x,y,c} & InputVertices S2 = {x,y,c} by Th57,Th75;
hence InputVertices S = {x,y,c} \/ {x,y,c} by A1,A2,A3,Th7
.= {x,y,c};
end;
theorem
for x,y,c being non pair set holds
InnerVertices BitAdderWithOverflowStr(x,y,c) =
{[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
{[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)}
proof let x,y,c be non pair set;
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
A1: BitAdderWithOverflowStr(x,y,c) = S1 +* S2 by Def22;
A2: {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
{[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)}
= {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} \/
({[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,c)})
by XBOOLE_1:4;
InnerVertices S1 = {[<*x,y*>, 'xor'], 2GatesCircOutput(x,y,c,'xor')} &
InnerVertices S2 = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/
{MajorityOutput(x,y,c)} by Th56,Th75;
hence thesis by A1,A2,Th27;
end;
theorem
for S being non empty ManySortedSign st S = BitAdderWithOverflowStr(x,y,c)
holds x in the carrier of S & y in the carrier of S & c in the carrier of S
proof set S1 = 2GatesCircStr(x,y,c, 'xor');
let S be non empty ManySortedSign;
assume S = BitAdderWithOverflowStr(x,y,c);
then x in the carrier of S1 & y in the carrier of S1 & c in the carrier of
S1 &
S = S1 +* MajorityStr(x,y,c) by Def22,Th60;
hence thesis by Th20;
end;
definition
let x,y,c be set;
A1: BitAdderWithOverflowStr(x,y,c)
= 2GatesCircStr(x,y,c, 'xor') +* MajorityStr(x,y,c) by Def22;
func BitAdderWithOverflowCirc(x,y,c) ->
strict Boolean gate`2=den Circuit of BitAdderWithOverflowStr(x,y,c) equals:
Def23:
BitAdderCirc(x,y,c) +* MajorityCirc(x,y,c);
coherence by A1;
end;
theorem
InnerVertices BitAdderWithOverflowStr(x,y,c) is Relation
proof
A1: BitAdderWithOverflowStr(x,y,c) =
2GatesCircStr(x,y,c, 'xor') +* MajorityStr(x,y,c) by Def22;
InnerVertices 2GatesCircStr(x,y,c, 'xor') is Relation &
InnerVertices MajorityStr(x,y,c) is Relation by Th58,Th67;
hence thesis by A1,Th3;
end;
theorem
for x,y,c being non pair set holds
InputVertices BitAdderWithOverflowStr(x,y,c) is without_pairs
proof let x,y,c be non pair set;
InputVertices BitAdderWithOverflowStr(x,y,c) = {x,y,c} by Th85;
hence thesis;
end;
theorem
BitAdderOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c) &
MajorityOutput(x,y,c) in InnerVertices BitAdderWithOverflowStr(x,y,c)
proof
BitAdderWithOverflowStr(x,y,c)
= 2GatesCircStr(x,y,c, 'xor') +* MajorityStr(x,y,c) by Def22;
hence thesis by Th21;
end;
theorem
for x,y,c being non pair set
for s being State of BitAdderWithOverflowCirc(x,y,c)
for a1,a2,a3 being Element of BOOLEAN st a1 = s.x & a2 = s.y & a3 = s.c holds
(Following(s,2)).BitAdderOutput(x,y,c) = a1 'xor' a2 'xor' a3 &
(Following(s,2)).MajorityOutput(x,y,c)
= a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1
proof let x,y,c be non pair set;
set f = 'xor';
set S = BitAdderWithOverflowStr(x,y,c);
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
set A = BitAdderWithOverflowCirc(x,y,c);
set A1 = BitAdderCirc(x,y,c), A2 = MajorityCirc(x,y,c);
let s be State of A;
let a1,a2,a3 be Element of BOOLEAN; assume
A1: a1 = s.x & a2 = s.y & a3 = s.c;
A2: x in the carrier of S1 & y in the carrier of S1 & c in the carrier of S1
by Th60;
A3: x in the carrier of S2 & y in the carrier of S2 & c in the carrier of S2
by Th72;
A4: A = A1 +* A2 & S = S1+*S2 by Def22,Def23;
then reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
reconsider s2 = s|the carrier of S2 as State of A2 by A4,Th26;
reconsider t = s as State of A1+*A2 by A4;
InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation
by Th58,Th59,Th67,Th68;
then A5: InnerVertices S1 misses InputVertices S2 &
InnerVertices S2 misses InputVertices S1 by Th5;
A6: BitAdderOutput(x,y,c) = 2GatesCircOutput(x,y,c, f) &
BitAdderCirc(x,y,c) = 2GatesCircuit(x,y,c, f) by Def15,Def16;
dom s1 = the carrier of S1 by CIRCUIT1:4;
then A7: a1 = s1.x & a2 = s1.y & a3 = s1.c by A1,A2,FUNCT_1:70;
c <> [<*x,y*>, f];
then (Following(t,2)).2GatesCircOutput(x,y,c, f)
= (Following(s1,2)).2GatesCircOutput(x,y,c, f) &
(Following(s1,2)).2GatesCircOutput(x,y,c,f) = a1 'xor' a2 'xor' a3
by A5,A6,A7,Th32,Th64;
hence (Following(s,2)).BitAdderOutput(x,y,c) = a1 'xor' a2 'xor' a3
by A4,Def15;
dom s2 = the carrier of S2 by CIRCUIT1:4;
then a1 = s2.x & a2 = s2.y & a3 = s2.c by A1,A3,FUNCT_1:70;
then (Following(t,2)).MajorityOutput(x,y,c)
= (Following(s2,2)).MajorityOutput(x,y,c) &
(Following(s2,2)).MajorityOutput(x,y,c)
= a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by A5,Lm4,Th33;
hence (Following(s,2)).MajorityOutput(x,y,c)
= a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by A4;
end;
theorem
for x,y,c being non pair set
for s being State of BitAdderWithOverflowCirc(x,y,c)
holds Following(s,2) is stable
proof let x,y,c be non pair set;
set f = 'xor';
set S = BitAdderWithOverflowStr(x,y,c);
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
set A = BitAdderWithOverflowCirc(x,y,c);
set A1 = BitAdderCirc(x,y,c), A2 = MajorityCirc(x,y,c);
let s be State of A;
A1: A = A1 +* A2 & S = S1+*S2 by Def22,Def23;
then reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
reconsider s2 = s|the carrier of S2 as State of A2 by A1,Th26;
reconsider t = s as State of A1+*A2 by A1;
InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation
by Th58,Th59,Th67,Th68;
then InnerVertices S1 misses InputVertices S2 &
InnerVertices S2 misses InputVertices S1 by Th5;
then A2: Following(s1,2) = Following(t,2)|the carrier of S1 &
Following(s1,3) = Following(t,3)|the carrier of S1 &
Following(s2,2) = Following(t,2)|the carrier of S2 &
Following(s2,3) = Following(t,3)|the carrier of S2 by Th30,Th31;
c <> [<*x,y*>, f] & A1 = 2GatesCircuit(x,y,c, f) by Def16;
then Following(s1,2) is stable by Th63;
then A3: Following(s1,2) = Following Following(s1,2) by CIRCUIT2:def 6
.= Following(s1,2+1) by Th12;
Following(s2,2) is stable by Th84;
then A4: Following(s2,2) = Following Following(s2,2) by CIRCUIT2:def 6
.= Following(s2,2+1) by Th12;
A5: Following(s,2+1) = Following Following(s,2) by Th12;
A6: dom Following(s,2) = the carrier of S &
dom Following(s,3) = the carrier of S &
dom Following(s1,2) = the carrier of S1 &
dom Following(s2,2) = the carrier of S2 by CIRCUIT1:4;
S = S1+*S2 by Def22;
then A7: the carrier of S = (the carrier of S1) \/ the carrier of S2
by CIRCCOMB:def 2;
now let a be set; assume a in the carrier of S;
then a in the carrier of S1 or a in the carrier of S2 by A7,XBOOLE_0:def
2;
then (Following(s,2)).a = (Following(s1,2)).a &
(Following(s,3)).a = (Following(s1,3)).a or
(Following(s,2)).a = (Following(s2,2)).a &
(Following(s,3)).a = (Following(s2,3)).a by A1,A2,A3,A4,A6,FUNCT_1:70;
hence (Following(s,2)).a = (Following Following(s,2)).a by A3,A4,Th12;
end;
hence Following(s,2) = Following Following(s,2) by A5,A6,FUNCT_1:9;
end;