:: Full Adder Circuit. Part { I }
:: by Grzegorz Bancerek and Yatsuka Nakamura
::
:: Received August 10, 1995
:: Copyright (c) 1995-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, CARD_1, NAT_1, SUBSET_1, ARYTM_3, RELAT_1,
FUNCT_1, FINSEQ_1, CIRCCOMB, FINSEQ_2, MSUALG_1, PARTFUN1, MSAFREE2,
FUNCT_4, TARSKI, STRUCT_0, MARGREL1, XBOOLEAN, CIRCUIT1, FSM_1, CIRCUIT2,
CARD_3, GLIB_000, LATTICES, MCART_1, FINSET_1, CLASSES1, FACIRC_1,
ORDINAL1;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, MCART_1, RELAT_1, CARD_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,
XXREAL_0, NAT_1;
constructors ENUMSET1, XXREAL_0, NAT_1, CLASSES1, BINARITH, CIRCUIT1,
CIRCUIT2, CIRCCOMB, RELSET_1, BINOP_1, WELLORD2, DOMAIN_1, XTUPLE_0,
NUMBERS, VALUED_0, XFAMILY;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XXREAL_0, FINSEQ_1,
FINSEQ_2, CARD_3, STRUCT_0, MSUALG_1, CIRCCOMB, NAT_1, XCMPLX_0,
MSAFREE2, MARGREL1, FINSET_1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_1, MSAFREE2, CIRCUIT2, CIRCCOMB, XBOOLE_0, XTUPLE_0;
equalities TARSKI, MSAFREE2, MARGREL1, ORDINAL1, CARD_1;
expansions CIRCUIT2, CIRCCOMB, XBOOLE_0;
theorems TARSKI, ENUMSET1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, ORDINAL1,
FINSEQ_1, FINSEQ_2, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB,
XBOOLE_0, XBOOLE_1, CLASSES1, CARD_1, XTUPLE_0, NAT_1;
schemes NAT_1, RECDEF_1, FUNCT_2;
begin :: Pairs, Set Without Pairs, and Nonpair-yielding Functions
registration
cluster pair -> non empty for set;
coherence
proof
let z be set;
given x,y being object such that
A1: z = [x,y];
thus thesis by A1;
end;
end;
registration
cluster non pair for object;
existence
proof
take {};
let x,y be object;
thus thesis;
end;
end;
registration
cluster -> non pair for Nat;
coherence
proof
let n be Nat;
given x,y being object such that
A1: n = [x,y];
n <> 0 by A1;
then 0 < n;
then 0 in Segm n by NAT_1:44;
hence contradiction by A1,TARSKI:def 2;
end;
end;
definition
::$CD
let IT be set;
attr IT is with_pair means
: Def1:
ex x being pair object st x in IT;
end;
notation
let IT be set;
antonym IT is without_pairs for IT is with_pair;
end;
registration
cluster empty -> without_pairs for set;
coherence;
let x be non pair object;
cluster {x} -> without_pairs;
coherence
by TARSKI:def 1;
let y be non pair object;
cluster {x,y} -> without_pairs;
coherence
by TARSKI:def 2;
let z be non pair object;
cluster {x,y,z} -> without_pairs;
coherence
by ENUMSET1:def 1;
end;
registration
cluster without_pairs for non empty set;
existence
proof
set x = the non pair set;
take {x};
thus thesis;
end;
end;
registration
let X, Y be without_pairs set;
cluster X \/ Y -> without_pairs;
coherence
proof
let a be pair object;
assume a in X \/ Y;
then a in X or a in Y by XBOOLE_0:def 3;
hence contradiction by Def1;
end;
end;
registration
let X be without_pairs set, Y be set;
cluster X \ Y -> without_pairs;
coherence
by Def1;
cluster X /\ Y -> without_pairs;
coherence
proof
let a be pair object;
assume a in X /\ Y;
then a in X by XBOOLE_0:def 4;
hence contradiction by Def1;
end;
cluster Y /\ X -> without_pairs;
coherence;
end;
registration
let x be pair object;
cluster {x} -> Relation-like;
coherence
proof
let a be object;
assume a in {x};
then a = x by TARSKI:def 1;
then ex y,z being object st a = [y,z] by XTUPLE_0:def 1;
hence thesis;
end;
let y be pair object;
cluster {x,y} -> Relation-like;
coherence
proof
let a be object;
assume a in {x,y};
then a = x or a = y by TARSKI:def 2;
then ex y,z being object st a = [y,z] by XTUPLE_0:def 1;
hence thesis;
end;
let z be pair object;
cluster {x,y,z} -> Relation-like;
coherence
proof
let a be object;
assume a in {x,y,z};
then a = x or a = y or a = z by ENUMSET1:def 1;
then ex y,z being object st a = [y,z] by XTUPLE_0:def 1;
hence thesis;
end;
end;
registration
cluster without_pairs Relation-like -> empty for set;
coherence
proof
let x be set;
assume
A1: not ex a being pair object st a in x;
assume
A2: for a being object st a in x holds ex y,z being object st a = [y,z];
assume x is non empty;
then reconsider X = x as non empty set;
set a = the Element of X;
ex y,z being object 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;
registration
let x be non pair object;
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 3;
then <*x*>.a in {x} by FINSEQ_1:39;
hence thesis by TARSKI:def 1;
end;
let y be non pair object;
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 3;
then <*x,y*>.a in {x,y} by FINSEQ_2:127;
hence thesis by TARSKI:def 2;
end;
let z be non pair object;
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 3;
then <*x,y,z*>.a in {x,y,z} by FINSEQ_2:128;
hence thesis by ENUMSET1:def 1;
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 object;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence thesis by A1;
end;
registration
let n be Nat;
cluster one-to-one nonpair-yielding for FinSeqLen of n;
existence
proof
reconsider p = id Seg n as FinSequence by FINSEQ_2:48;
len p = len idseq n by FINSEQ_2:def 1
.= n by CARD_1:def 7;
then reconsider p as FinSeqLen of n by CARD_1:def 7;
take p;
thus p is one-to-one;
let x be set;
assume
A1: x in dom p;
x in Seg n by A1;
hence thesis by FUNCT_1:17;
end;
end;
registration
cluster one-to-one nonpair-yielding for FinSequence;
existence
proof
set n = the Nat,p = the one-to-one nonpair-yielding FinSeqLen of n;
take p;
thus thesis;
end;
end;
registration
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:11;
end;
theorem
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 by Th2,CIRCCOMB:47;
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: InnerVertices S = rng R;
InnerVertices S1 = rng R1 & InnerVertices S2 = rng R2;
then
A4: rng R = (rng R1) \/ rng R2 by A1,A3,CIRCCOMB:11;
A5: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
hereby
let x be object;
assume
A6: x in InputVertices S1;
then ( not x in rng R1)& not x in rng R2 by A2,XBOOLE_0:3,def 5;
then
A7: not x in rng R by A4,XBOOLE_0:def 3;
x in the carrier of S by A5,A6,XBOOLE_0:def 3;
hence x in InputVertices S by A7,XBOOLE_0:def 5;
end;
A8: InputVertices S c= (InputVertices S1) \/ InputVertices S2 by A1,CIRCCOMB:11
;
hereby
let x be object;
assume
A9: x in InputVertices (S1+*S2);
then not x in rng R by XBOOLE_0:def 5;
then x in InputVertices S1 or x in InputVertices S2 & not x in
InnerVertices S1 by A4,A8,A9,XBOOLE_0:def 3;
then x in InputVertices S1 or x in InputVertices S2 \ InnerVertices S1 by
XBOOLE_0:def 5;
hence x in (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1) by
XBOOLE_0:def 3;
end;
let x be object;
assume x in (InputVertices S1) \/ (InputVertices S2 \ InnerVertices S1);
then
A10: x in InputVertices S1 or x in InputVertices S2 \ rng R1 by XBOOLE_0:def 3;
then
A11: x in the carrier of S by A5,XBOOLE_0:def 3;
x in InputVertices S1 & not x in rng R2 or x in InputVertices S2 & not
x in rng R1 by A2,A10,XBOOLE_0:3,def 5;
then
A12: not x in rng R2 by XBOOLE_0:def 5;
not x in rng R1 by A10,XBOOLE_0:def 5;
then not x in rng R by A4,A12,XBOOLE_0:def 3;
hence thesis by A11,XBOOLE_0:def 5;
end;
theorem Th5:
for X,R being set st X is without_pairs & R is Relation holds X misses R;
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
CIRCCOMB:47;
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 InputVertices S1 is without_pairs & InnerVertices S1 is Relation &
InputVertices S2 is without_pairs & InnerVertices S2 is Relation;
then InputVertices (S1+*S2) = (InputVertices S1) \/ (InputVertices S2 \
InnerVertices S1) & InnerVertices S1 misses InputVertices S2 by Th6;
hence thesis by 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:11;
assume
A2: for x being pair object holds not x in InputVertices S1;
assume
A3: for x being pair object holds not x in InputVertices S2;
let x be pair object;
assume x in InputVertices (S1+*S2);
then x in InputVertices S1 or x in InputVertices S2 by A1,XBOOLE_0:def 3;
hence contradiction by A2,A3;
end;
theorem
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 by Th8,CIRCCOMB:47;
begin :: Boolean Operations
definition
let i be Nat, D be non empty set;
mode Tuple of i,D is Element of i-tuples_on D;
end;
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 FUNCT_2:sch 4;
hereby
take f;
let x,y be Element of BOOLEAN;
reconsider a = <*x,y*> as Tuple of 2, BOOLEAN by FINSEQ_2:101;
thus f.<*x,y*> = F(a.1,a.2) by A1
.= F(x,a.2) by FINSEQ_1:44
.= F(x,y) by FINSEQ_1:44;
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
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:100;
thus f1.a = F(x,y) by A1,A3
.= f2.a by A2,A3;
end;
hence thesis by FUNCT_2:63;
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 FUNCT_2:sch 4;
hereby
take f;
let x,y be Element of BOOLEAN;
reconsider a = <*x,y*> as Tuple of 2, BOOLEAN by FINSEQ_2:101;
thus f.<*x,y*> = F(a.1,a.2) by A1
.= F(x,a.2) by FINSEQ_1:44
.= F(x,y) by FINSEQ_1:44;
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:100;
thus f1.a = F(x,y) by A2,A4
.= f2.a by A3,A4;
end;
hence thesis by FUNCT_2:63;
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 FUNCT_2:sch 4;
hereby
take f;
let x,y,z be Element of BOOLEAN;
reconsider a = <*x,y,z*> as Tuple of 3, BOOLEAN by FINSEQ_2:104;
thus f.<*x,y,z*> = F(a.1,a.2,a.3) by A1
.= F(x,a.2,a.3) by FINSEQ_1:45
.= F(x,y,a.3) by FINSEQ_1:45
.= F(x,y,z) by FINSEQ_1:45;
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
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:103;
thus f1.a = F(x,y,z) by A1,A3
.= f2.a by A2,A3;
end;
hence thesis by FUNCT_2:63;
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 FUNCT_2:sch 4;
hereby
take f;
let x,y,z be Element of BOOLEAN;
reconsider a = <*x,y,z*> as Tuple of 3, BOOLEAN by FINSEQ_2:104;
thus f.<*x,y,z*> = F(a.1,a.2,a.3) by A1
.= F(x,a.2,a.3) by FINSEQ_1:45
.= F(x,y,a.3) by FINSEQ_1:45
.= F(x,y,z) by FINSEQ_1:45;
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:103;
thus f1.a = F(x,y,z) by A2,A4
.= f2.a by A3,A4;
end;
hence thesis by FUNCT_2:63;
end;
definition
func 'xor' -> Function of 2-tuples_on BOOLEAN, BOOLEAN means
: Def3:
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
: Def4:
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
: Def5:
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
: Def6:
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;
begin :: Computation and Stabilizable
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;
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then (the ResultSort of S).g in rng the ResultSort of S by FUNCT_1:def 3;
then
A1: v in InnerVertices S by MSUALG_1:def 2;
then g depends_on_in s = s*the_arity_of g & action_at v = g by CIRCUIT1:def 3
,MSAFREE2:def 7;
hence thesis by A1,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 natural Number;
func Following(s,n) -> State of A means
:Def7:
ex f being sequence of 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
reconsider n as Nat by TARSKI:1;
set D = product the Sorts of A;
deffunc R(natural Number,Element of D) = Following $2;
(ex y being Element of D st ex f being sequence of 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 sequence of D st y1 = f.n & f.0 = s & for n being Nat
holds f.(n+1) = R(n,f.n)) & (ex f being sequence of D st y2 = f.n & f.0 = s
& for n being Nat holds f.(n+1) = R(n,f.n)) holds y1 = y2 from RECDEF_1:sch 14;
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 sequence of 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 Def7;
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 sequence of product the Sorts of A such that
A1: Following(s,n) = f.n and
A2: f.0 = s and
A3: for n being Nat holds f.(n+1) = Following f.n by Def7;
thus Following(s,n+1) = f.(n+1) by A2,A3,Def7
.= Following Following(s,n) by A1,A3;
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: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume
A2: Following(s,n+m) = Following(Following(s,n),m);
thus Following(s,n+(m+1)) = Following(s,n+m+1)
.= Following Following(s,n+m) by Th12
.= Following(Following(s,n),m+1) by A2,Th12;
end;
A3: P[0] by Th11;
thus for i being Nat holds P[i] from NAT_1:sch 2(A3,A1);
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 object;
pred s is_stable_at x means
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;
defpred P[Nat] means (Following(s,$1)).x = s.x;
assume
A1: x in InputVertices S;
A2: now
let n be Nat;
assume
A3: P[n];
(Following(s,n+1)).x = (Following Following(s,n)).x by Th12
.= s.x by A1,A3,CIRCUIT2:def 5;
hence P[n+1];
end;
A4: P[0] by Th11;
thus for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
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;
A2: now
let a be object;
assume
A3: a in dom p;
then p.a in rng p by FUNCT_1:def 3;
then
A4: s is_stable_at p.a by A1;
((Following(s, n))*p).a = (Following(s, n)).(p.a) & (s*p).a = s.(p . a
) by A3,FUNCT_1:13;
hence ((Following(s, n))*p).a = (s*p).a by A4;
end;
A5: rng p c= the carrier of S by FINSEQ_1:def 4;
dom Following(s, n) = the carrier of S by CIRCUIT1:3;
then
A6: dom ((Following(s, n))*p) = dom p by A5,RELAT_1:27;
dom s = the carrier of S by CIRCUIT1:3;
then dom (s*p) = dom p by A5,RELAT_1:27;
then
A7: (Following(s, n))*p = s*p by A6,A2,FUNCT_1:2;
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 A7,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 thesis by XBOOLE_0:def 3;
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:47;
then InnerVertices (S1+*S2) = InnerVertices S1 \/ InnerVertices S2 &
InnerVertices (S2+*S1) = InnerVertices S2 \/ InnerVertices S1 by CIRCCOMB:11;
hence thesis by XBOOLE_0:def 3;
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;
InnerVertices (S1+*S2) = rng (R1+*R2) by CIRCCOMB:def 2;
then InnerVertices S2 c= InnerVertices (S1+*S2) by FUNCT_4:18;
hence thesis;
end;
theorem
for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds S1
+*S2 = S2+*S1 by CIRCCOMB:5,47;
theorem
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 by CIRCCOMB:22,60;
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;
A1: the Sorts of A3 tolerates the Sorts of A1 by CIRCCOMB:59;
the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates
the Sorts of A3 by CIRCCOMB:59;
hence thesis by A1,CIRCCOMB:23;
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:59;
hence thesis by CIRCCOMB:26;
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:47;
hence thesis by CIRCCOMB:11;
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;
dom Following s1 = the carrier of S1 & Following s = (Following s2)+*
Following s1 by A1,A2,CIRCCOMB:33,60,CIRCUIT1:3;
hence thesis by FUNCT_4:23;
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;
dom Following s2 = the carrier of S2 & Following s = (Following s1)+*
Following s2 by A1,A2,CIRCCOMB:32,60,CIRCUIT1:3;
hence thesis by FUNCT_4:23;
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);
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: 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,A4,Th28
.= Following(s1,n+1) by Th12;
end;
Following(s,0) = s by Th11;
then
A5: P[0] by A2,Th11;
thus for n being Nat holds P[n] from NAT_1:sch 2(A5,A3);
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);
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: 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,A4,Th29
.= Following(s2,n+1) by Th12;
end;
Following(s,0) = s by Th11;
then
A5: P[0] by A2,Th11;
thus for n being Nat holds P[n] from NAT_1:sch 2(A5,A3);
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: the carrier of S1 = dom Following(s1,n) by CIRCUIT1:3;
Following(s,n)|the carrier of S1 = Following(s1,n) by A1,A2,Th30;
hence thesis by A3,A4,FUNCT_1:47;
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: the carrier of S2 = dom Following(s1,n) by CIRCUIT1:3;
Following(s,n)|the carrier of S2 = Following(s1,n) by A1,A2,Th31;
hence thesis by A3,A4,FUNCT_1:47;
end;
registration
let S be gate`2=den non void non empty ManySortedSign;
let g be Gate of S;
cluster g`2 -> Function-like Relation-like for set;
coherence
proof
consider A being MSAlgebra over S such that
A1: A is gate`2=den by CIRCCOMB:def 11;
g`2 = [g`1, (the Charact of A).g]`2 by A1
.= (the Charact of A).g
.= Den(g, A) by MSUALG_1:def 6;
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 carrier' of S holds g = [g`1, (the
Charact of A).g];
let s be State of A, g be Gate of S;
A2: Den(g, A) = (the Charact of A).g by MSUALG_1:def 6
.= [g`1, (the Charact of A).g]`2
.= g`2 by A1;
set v = the_result_sort_of g;
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then (the ResultSort of S).g in rng the ResultSort of S by FUNCT_1:def 3;
then
A3: v in InnerVertices S by MSUALG_1:def 2;
then g depends_on_in s = s*the_arity_of g & action_at v = g by CIRCUIT1:def 3
,MSAFREE2:def 7;
hence thesis by A2,A3,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
carrier' 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 [p,f] in the carrier' of S;
then reconsider g = [p,f] as Gate of S;
A1: g`1 = p & g`2 = f;
A2: the_result_sort_of g = (the ResultSort of S).g by MSUALG_1:def 2
.= g by CIRCCOMB:44;
the_arity_of g = (the Arity of S).g by MSUALG_1:def 1
.= [(the Arity of S).g, g`2]`1
.= g`1 by CIRCCOMB:def 8;
hence thesis by A1,A2,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
carrier' 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 [p,f] in the carrier' of S;
then reconsider g = [p,f] as Gate of S;
A1: the_arity_of g = (the Arity of S).g by MSUALG_1:def 1
.= [(the Arity of S).g, g`2]`1
.= g`1 by CIRCCOMB:def 8
.= p;
A2: the_result_sort_of g = (the ResultSort of S).g by MSUALG_1:def 2
.= g by CIRCCOMB:44;
assume for x being set st x in rng p holds s is_stable_at x;
hence thesis by A1,A2,Th19;
end;
theorem Th37:
for S being unsplit non empty ManySortedSign holds InnerVertices
S = the carrier' of S
proof
let S be unsplit non empty ManySortedSign;
the ResultSort of S = id the carrier' of S by CIRCCOMB:def 7;
hence thesis;
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:42;
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:42;
hence thesis;
end;
theorem Th40:
for f,x,y being object holds InputVertices 1GateCircStr(
<*x,y*>,f) = {x,y}
proof
let f, x,y be object;
set p = <*x,y*>;
thus InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
.= {x,y} by FINSEQ_2:127;
end;
theorem Th41:
for f being set, x,y being non pair object holds InputVertices
1GateCircStr(<*x,y*>,f) is without_pairs
proof
let f be set, x,y be non pair object;
set p = <*x,y*>;
let z be pair object;
assume
A1: z in InputVertices 1GateCircStr(p,f);
InputVertices 1GateCircStr(p,f) = {x,y} by Th40;
hence thesis by A1,TARSKI:def 2;
end;
theorem Th42:
for f,x,y,z being object holds InputVertices
1GateCircStr(<*x,y,z*>,f) = {x,y,z}
proof
let f, x,y,z be object;
set p = <*x,y,z*>;
thus InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
.= {x,y,z} by FINSEQ_2:128;
end;
theorem Th43:
for x,y,f being object 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 object;
set p = <*x,y*>;
x in {x,y} by TARSKI:def 2;
then
A1: x in rng p by FINSEQ_2:127;
y in {x,y} by TARSKI:def 2;
then
A2: y in rng p by FINSEQ_2:127;
the carrier of 1GateCircStr(p,f) = rng p \/ {[p,f]} & [p,f] in {[p,f]}
by CIRCCOMB:def 6,TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:def 3;
end;
theorem Th44:
for x,y,z,f being object 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 object;
set p = <*x,y,z*>;
set A = the carrier of 1GateCircStr(p,f);
y in {x,y,z} by ENUMSET1:def 1;
then
A1: y in rng p by FINSEQ_2:128;
z in {x,y,z} by ENUMSET1:def 1;
then
A2: z in rng p by FINSEQ_2:128;
x in {x,y,z} by ENUMSET1:def 1;
then A = rng p \/ {[p,f]} & x in rng p by CIRCCOMB:def 6,FINSEQ_2:128;
hence thesis by A1,A2,XBOOLE_0:def 3;
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 thesis by XBOOLE_0:def 3;
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 carrier' of S;
then g in {[p,f]} by CIRCCOMB:def 5;
then
A1: g = [p,f] by TARSKI:def 1;
thus thesis by A1,CIRCCOMB:def 5;
end;
thus S is Circuit-like
proof
let S9 be non void non empty ManySortedSign such that
A2: S9 = S;
let o1, o2 be OperSymbol of S9;
o1 = [p,f] by A2,CIRCCOMB:37;
hence thesis by A2,CIRCCOMB:37;
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:42;
hence thesis by TARSKI:def 1;
end;
definition
let x,y be object;
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
1GateCircuit(<*x,y*> qua FinSeqLen of 2, f);
coherence by CIRCCOMB:61;
end;
reserve x,y,z,c for object,
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*>;
dom s = the carrier of 1GateCircStr(p, f) by CIRCUIT1:3;
then
A1: dom s = rng p \/ {[p,f]} by CIRCCOMB:def 6;
y in {x,y} by TARSKI:def 2;
then y in rng p by FINSEQ_2:127;
then
A2: y in dom s by A1,XBOOLE_0:def 3;
x in {x,y} by TARSKI:def 2;
then x in rng p by FINSEQ_2:127;
then
A3: x in dom s by A1,XBOOLE_0:def 3;
thus (Following s).[<*x,y*>, f] = f.(s*<*x,y*>) by CIRCCOMB:56
.= f.<*s.x, s.y*> by A3,A2,FINSEQ_2:125;
reconsider x, y as Vertex of 1GateCircStr(p,f) by Th43;
InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
.= {x,y} by FINSEQ_2:127;
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: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6
.= {x,y} \/ {[p,f]} by FINSEQ_2:127;
A2: now
let a be object;
A3: s2.[p,f] = f.<*s1.x, s1.y*> by Th48;
assume a in the carrier of S;
then a in {x,y} or a in {[p,f]} by A1,XBOOLE_0:def 3;
then
A4: a = x or a = y or a = [p,f] by TARSKI:def 1,def 2;
s1.x = s.x & s1.y = s.y by Th48;
hence s2.a = s1.a by A4,A3,Th48;
end;
dom s1 = the carrier of S & dom s2 = the carrier of S by CIRCUIT1:3;
hence Following s = Following Following s by A2,FUNCT_1:2;
end;
theorem
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 by Th48;
theorem
for s being State of 1GateCircuit(x,y,f) holds Following s is stable by Th49;
definition
let x,y,z be object;
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
1GateCircuit(<*x,y,z*>, f);
coherence by CIRCCOMB:61;
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*>;
dom s = the carrier of 1GateCircStr(p, f) by CIRCUIT1:3;
then
A1: dom s = rng p \/ {[p,f]} by CIRCCOMB:def 6;
y in {x,y,z} by ENUMSET1:def 1;
then y in rng p by FINSEQ_2:128;
then
A2: y in dom s by A1,XBOOLE_0:def 3;
x in {x,y,z} by ENUMSET1:def 1;
then x in rng p by FINSEQ_2:128;
then
A3: x in dom s by A1,XBOOLE_0:def 3;
z in {x,y,z} by ENUMSET1:def 1;
then z in rng p by FINSEQ_2:128;
then
A4: z in dom s by A1,XBOOLE_0:def 3;
thus (Following s).[p, f] = f.(s*p) by CIRCCOMB:56
.= f.<*s.x, s.y, s.z*> by A3,A2,A4,FINSEQ_2:126;
reconsider x, y, z as Vertex of 1GateCircStr(p,f) by Th44;
A5: InputVertices 1GateCircStr(p,f) = rng p by CIRCCOMB:42
.= {x,y,z} by FINSEQ_2:128;
then
A6: z in InputVertices 1GateCircStr(p,f) by ENUMSET1:def 1;
x in InputVertices 1GateCircStr(p,f) & y in InputVertices 1GateCircStr(
p,f) by A5,ENUMSET1:def 1;
hence thesis by A6,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: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6
.= {x,y,z} \/ {[p,f]} by FINSEQ_2:128;
A2: now
let a be object;
A3: s1.z = s.z & s2.[p,f] = f.<*s1.x, s1.y, s1.z*> by Th52;
assume a in the carrier of S;
then a in {x,y,z} or a in {[p,f]} by A1,XBOOLE_0:def 3;
then
A4: a = x or a = y or a = z or a = [p,f] by ENUMSET1:def 1,TARSKI:def 1;
s1.x = s.x & s1.y = s.y by Th52;
hence s2.a = s1.a by A4,A3,Th52;
end;
dom s1 = the carrier of S & dom s2 = the carrier of S by CIRCUIT1:3;
hence Following s = Following Following s by A2,FUNCT_1:2;
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
by Th52;
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 by Th53;
begin :: Two Gates Circuit
definition
let x,y,c be object;
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
1GateCircStr(<*x,y*>, f) +* 1GateCircStr
(<*[<*x,y*>, f], c*>, f);
correctness;
end;
definition
let x,y,c be object;
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
[<*[<*x,y*>, f], c*>, f];
coherence
proof
set p = <*[<*x,y*>, f], c*>;
set S2 = 1GateCircStr(p, f);
[p,f] in InnerVertices S2 by Th47;
hence thesis by Th21;
end;
correctness;
end;
registration
let x,y,c be object;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
cluster 2GatesCircOutput(x,y,c,f) -> pair;
coherence;
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);
S1 tolerates S2 by CIRCCOMB:43;
hence InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by
CIRCCOMB:11
.= {[<*x,y*>, f]} \/ (InnerVertices S2) by CIRCCOMB:42
.= {[<*x,y*>, f]} \/ {[p, f]} by CIRCCOMB:42
.= {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by ENUMSET1:1;
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 S = 2GatesCircStr(x,y,c,f);
set S1 = 1GateCircStr(<*x,y*>, f);
set p = <*[<*x,y*>, f], c*>;
set S2 = 1GateCircStr(p, f);
set R = the ResultSort of S;
A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
A3: rng <*x,y*> = {x,y} by FINSEQ_2:127;
then
A4: the carrier of S1 = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;
A5: rng R = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56
.= {[<*x,y*>, f], [p,f]};
A6: rng p = {[<*x,y*>, f], c} by FINSEQ_2:127;
then
A7: 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 object;
assume
A8: z in InputVertices S;
then z in the carrier of S1 or z in the carrier of S2 by A2,XBOOLE_0:def 3;
then
z in {x,y} or z in {[<*x,y*>,f]} or z in {[<*x,y*>, f], c} or z in {[
p,f]} by A4,A7,XBOOLE_0:def 3;
then
A9: z = x or z = y or z = [<*x,y*>,f] or z = c or z = [p,f] by TARSKI:def 1
,def 2;
not z in rng R by A8,XBOOLE_0:def 5;
hence thesis by A5,A9,ENUMSET1:def 1,TARSKI:def 2;
end;
let z be object;
reconsider zz=z as set by TARSKI:1;
assume z in {x,y,c};
then
A10: z = x or z = y or z = c by ENUMSET1:def 1;
then z in {x,y} or z in rng p by A6,TARSKI:def 2;
then z in InputVertices S1 or z in InputVertices S2 by A3,CIRCCOMB:42;
then
A11: z in the carrier of S by A2,XBOOLE_0:def 3;
z in {x,y} & [<*x,y*>, f] in rng p or z in {c} by A6,A10,TARSKI:def 1,def 2;
then
A12: the_rank_of zz 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 A3,A6,CLASSES1:82,TARSKI:def 1
,def 2;
then the_rank_of zz in the_rank_of [p,f] by CLASSES1:82,ORDINAL1:10;
then
A13: z <> [p,f];
z <> [<*x,y*>, f] by A1,A12;
then not z in rng R by A5,A13,TARSKI:def 2;
hence thesis by A11,XBOOLE_0:def 5;
end;
definition
let x,y,c be object;
let f be Function of 2-tuples_on BOOLEAN, BOOLEAN;
func 2GatesCircuit(x,y,c,f) -> strict Boolean gate`2=den Circuit of
2GatesCircStr(x,y,c,f) equals
1GateCircuit(x,y, f) +* 1GateCircuit([<*x,y*>, f], c, f);
coherence;
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 object
holds InputVertices 2GatesCircStr(x,y,c,f) is without_pairs
proof
let x,y,c be non pair object;
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);
A1: c in the carrier of S2 by Th43;
x in the carrier of S1 & y in the carrier of S1 by Th43;
hence thesis by A1,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 by 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:4;
hence thesis by CIRCCOMB:def 14;
end;
end;
reserve s for State of 2GatesCircuit(x,y,c,f);
Lm1: 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 S1 = 1GateCircStr(<*x,y*>, f), A1 = 1GateCircuit(x,y, f);
reconsider vx = x, vy = y as Vertex of S1 by Th43;
reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
set p = <*[<*x,y*>, f], c*>;
set xyf = [<*x,y*>,f];
set S2 = 1GateCircStr(p, f), A2 = 1GateCircuit(xyf,c, f);
set S = 2GatesCircStr(x,y,c,f);
A1: dom s1 = the carrier of S1 by CIRCUIT1:3;
reconsider v2 = [p,f] as Element of InnerVertices S2 by Th47;
InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
then reconsider xyf as Element of InnerVertices S by TARSKI:def 2;
A2: rng p = {xyf,c} by FINSEQ_2:127;
then c in rng p by TARSKI:def 2;
then
A3: c in InputVertices S2 by CIRCCOMB:42;
xyf in rng p by A2,TARSKI:def 2;
then xyf in InputVertices S2 by CIRCCOMB:42;
then reconsider xyf9 = xyf, c9 = c as Vertex of S2 by A3;
reconsider xyf1 = xyf as Element of InnerVertices S1 by Th47;
reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
A4: dom s2 = the carrier of S2 by CIRCUIT1:3;
assume c <> [<*x,y*>, f];
then
A5: InputVertices S = {x,y,c} by Th57;
then
A6: c in InputVertices S by ENUMSET1:def 1;
thus (Following s).2GatesCircOutput(x,y,c,f) = (Following s2).v2 by
CIRCCOMB:64
.= f.<*s2.xyf9, s2.c9*> by Th48
.= f.<*s.[<*x,y*>,f], s2.c9*> by A4,FUNCT_1:47
.= f.<*s.[<*x,y*>,f], s.c*> by A4,FUNCT_1:47;
thus (Following s).[<*x,y*>,f] = (Following s1).xyf1 by CIRCCOMB:64
.= f.<*s1.vx, s1.vy*> by Th48
.= f.<*s.x, s1.vy*> by A1,FUNCT_1:47
.= f.<*s.x, s.y*> by A1,FUNCT_1:47;
x in InputVertices S & y in InputVertices S by A5,ENUMSET1:def 1;
hence thesis by A6,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 S = 2GatesCircStr(x,y,c,f);
A1: rng <*x,y*> = {x,y} by FINSEQ_2:127;
reconsider xx = x, yy = y, cc = c as Vertex of S by Th60;
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);
A2: x in {x,y} by TARSKI:def 2;
assume c <> [<*x,y*>, f];
then
A3: InputVertices S = {x,y,c} by Th57;
then
A4: x in InputVertices S by ENUMSET1:def 1;
then
A5: (Following s).xx = s.x by CIRCUIT2:def 5;
InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
then reconsider xyf as Element of InnerVertices S by TARSKI:def 2;
A6: rng p = {xyf,c} by FINSEQ_2:127;
then c in rng p by TARSKI:def 2;
then
A7: c in InputVertices S2 by CIRCCOMB:42;
xyf in rng p by A6,TARSKI:def 2;
then xyf in InputVertices S2 by CIRCCOMB:42;
then reconsider xyf9 = xyf, c9 = c as Vertex of S2 by A7;
reconsider vx = x, vy = y as Vertex of S1 by Th43;
set fs = Following s;
reconsider fs1 = fs|the carrier of S1 as State of A1 by Th26;
A8: y in {x,y} by TARSKI:def 2;
reconsider fs2 = fs|the carrier of S2 as State of A2 by Th26;
reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
A9: dom fs2 = the carrier of S2 by CIRCUIT1:3;
A10: c in InputVertices S by A3,ENUMSET1:def 1;
then (Following s).cc = s.c by CIRCUIT2:def 5;
then
A11: (Following Following s).cc = s.c by A10,CIRCUIT2:def 5;
reconsider xyf1 = xyf as Element of InnerVertices S1 by Th47;
A12: dom fs1 = the carrier of S1 by CIRCUIT1:3;
reconsider v2 = [p,f] as Element of InnerVertices S2 by Th47;
A13: xyf in InnerVertices S1 by Th47;
A14: dom s1 = the carrier of S1 & InputVertices S1 = rng <*x,y*> by CIRCCOMB:42
,CIRCUIT1:3;
A15: Following(s,1+1) = Following Following s by Th15;
hence (Following(s,2)).2GatesCircOutput(x,y,c,f) = (Following fs2).v2 by
CIRCCOMB:64
.= f.<*fs2.xyf9, fs2.c9*> by Th48
.= f.<*(Following s).xyf, fs2.c*> by A9,FUNCT_1:47
.= f.<*(Following s).xyf, (Following s).c9*> by A9,FUNCT_1:47
.= f.<*(Following s).xyf, s.cc*> by A10,CIRCUIT2:def 5
.= f.<*(Following s1).xyf, s.cc*> by A13,CIRCCOMB:64
.= f.<*f.<*s1.x, s1.y*>, s.cc*> by Th48
.= f.<*f.<*s.x,s1.y*>, s.cc*> by A2,A14,A1,FUNCT_1:47
.= f.<*f.<*s.x,s.y*>, s.c*> by A8,A14,A1,FUNCT_1:47;
A16: y in InputVertices S by A3,ENUMSET1:def 1;
then
A17: (Following s).yy = s.y by CIRCUIT2:def 5;
then
A18: (Following Following s).yy = s.y by A16,CIRCUIT2:def 5;
thus (Following(s,2)).[<*x,y*>,f] = (Following fs1).xyf1 by A15,CIRCCOMB:64
.= f.<*fs1.vx, fs1.vy*> by Th48
.= f.<*s.x, fs1.vy*> by A5,A12,FUNCT_1:47
.= f.<*s.x, s.y*> by A17,A12,FUNCT_1:47;
(Following Following s).xx = s.x by A4,A5,CIRCUIT2:def 5;
hence thesis by A18,A11,Th15;
end;
theorem Th63:
c <> [<*x,y*>, f] implies Following(s,2) is stable
proof
set S = 2GatesCircStr(x,y,c,f);
assume
A1: c <> [<*x,y*>, f];
now
thus dom Following Following(s,2) = the carrier of S & dom Following(s,2)
= the carrier of S by CIRCUIT1:3;
let a be object;
A2: InputVertices S \/ InnerVertices S = the carrier of S by XBOOLE_1:45;
assume a in the carrier of S;
then reconsider v = a as Vertex of S;
A3: InnerVertices S = {[<*x,y*>, f], 2GatesCircOutput(x,y,c,f)} by Th56;
A4: (Following(s,2)).c = s.c by A1,Th62;
A5: (Following(s,2)).x = s.x & (Following(s,2)).y = s.y by A1,Th62;
A6: (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*> by A1,Th62;
A7: InputVertices S = {x,y,c} by A1,Th57;
per cases by A2,XBOOLE_0:def 3;
suppose
v in InputVertices S;
then v = x or v = y or v = c by A7,ENUMSET1:def 1;
hence (Following Following(s,2)).a = (Following(s,2)).a by A1,Lm1;
end;
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,A6,A5,A4
,Lm1;
end;
end;
hence Following(s,2) = Following Following(s,2) by FUNCT_1:2;
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 Def3
.= a1 'xor' a2 'xor' a3 by Def3;
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 Def4
.= a1 'or' a2 'or' a3 by Def4;
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 Def5
.= a1 '&' a2 '&' a3 by Def5;
end;
begin :: Bit Adder Circuit
definition
let x,y,c be object;
func BitAdderOutput(x,y,c) -> Element of InnerVertices 2GatesCircStr(x,y,c,
'xor') equals
2GatesCircOutput(x,y,c, 'xor');
coherence;
end;
definition
let x,y,c be object;
func BitAdderCirc(x,y,c) -> strict Boolean gate`2=den Circuit of
2GatesCircStr(x,y,c, 'xor') equals
2GatesCircuit(x,y,c, 'xor');
coherence;
end;
definition
let x,y,c be object;
func MajorityIStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign equals
1GateCircStr(<*x,y*>, '&') +*
1GateCircStr(<*y,c*>, '&') +* 1GateCircStr(<*c,x*>, '&');
correctness;
end;
definition
let x,y,c be object;
func MajorityStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void
strict non empty ManySortedSign equals
MajorityIStr(x,y,c) +* 1GateCircStr(<*[
<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3);
correctness;
end;
definition
let x,y,c be object;
func MajorityICirc(x,y,c) -> strict Boolean gate`2=den Circuit of
MajorityIStr(x,y,c) equals
1GateCircuit(x,y, '&') +* 1GateCircuit(y,c, '&') +*
1GateCircuit(c,x, '&');
coherence;
end;
theorem Th67:
InnerVertices MajorityStr(x,y,c) is Relation
proof
A1: InnerVertices 1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>,
'&']*>, or3) is Relation by Th38;
InnerVertices 1GateCircStr(<*x,y*>,'&') is Relation & InnerVertices
1GateCircStr(<*y,c*>,'&') is Relation by Th38;
then
A2: InnerVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&')) is
Relation by Th2,CIRCCOMB:47;
InnerVertices 1GateCircStr(<*c,x*>,'&') is Relation by Th38;
then InnerVertices MajorityIStr(x,y,c) is Relation by A2,Th2,CIRCCOMB:47;
hence thesis by A1,Th2,CIRCCOMB:47;
end;
theorem Th68:
for x,y,c being non pair object holds InputVertices MajorityStr(x,y
,c) is without_pairs
proof
let x,y,c be non pair object;
set M = MajorityStr(x,y,c), MI = MajorityIStr(x,y,c);
set S = 1GateCircStr(<*[<*x,y*>, '&'], [<*y,c*>, '&'], [<*c,x*>, '&']*>, or3
);
given xx being pair object such that
A1: xx in InputVertices M;
A2: 1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*y,c*>, '&') by
CIRCCOMB:43;
1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') &
1GateCircStr(<*y,c*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') by CIRCCOMB:43;
then
A3: 1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&') tolerates
1GateCircStr(<*c,x*>, '&') by A2,CIRCCOMB:3;
InnerVertices 1GateCircStr(<*x,y*>, '&') = {[<*x,y*>, '&']} &
InnerVertices 1GateCircStr(<*y,c*>, '&') = {[<*y,c*>, '&']} by CIRCCOMB:42;
then InnerVertices 1GateCircStr(<*c,x*>, '&') = {[<*c,x*>, '&']} &
InnerVertices (1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&')) = {[<*
x,y*>, '&']} \/ {[<*y,c*>, '&']} by A2,CIRCCOMB:11,42;
then
A4: InnerVertices MI = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/ {[<*c,x*>, '&'
]} by A3,CIRCCOMB:11
.= {[<*x,y*>,'&'], [<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:1
.= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by ENUMSET1:3;
InputVertices S = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by Th42;
then
A5: InputVertices S \ InnerVertices MI = {} by A4,XBOOLE_1:37;
InputVertices 1GateCircStr(<*x,y*>,'&') is without_pairs & InputVertices
1GateCircStr(<*y,c*>,'&') is without_pairs by Th41;
then
A6: InputVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&')) is
without_pairs by Th8,CIRCCOMB:47;
InputVertices 1GateCircStr(<*c,x*>,'&') is without_pairs by Th41;
then
A7: InputVertices MI is without_pairs by A6,Th8,CIRCCOMB:47;
InnerVertices S is Relation by Th38;
then
InputVertices M = (InputVertices MI) \/ (InputVertices S \ InnerVertices
MI) by A7,Th6;
hence thesis by A7,A1,A5;
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, '&');
reconsider xx = x, yy = y as Vertex of S1 by Th43;
reconsider v1 = [xy, '&'] as Element of InnerVertices S1 by Th47;
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;
A2: A = A1+*(A2+*A3) by Th25;
then reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
A3: S = S1+*(S2+*S3) by CIRCCOMB:6;
then reconsider v = v1 as Element of InnerVertices S by Th21;
reconsider xx, yy as Vertex of S by A3,Th20;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
thus (Following s).[xy, '&'] = (Following s1).v by A3,A2,CIRCCOMB:64
.= '&'.<*s1.xx,s1.yy*> by Th48
.= '&'.<*s.xx,s1.yy*> by A4,FUNCT_1:47
.= '&'.<*s.xx,s.yy*> by A4,FUNCT_1:47
.= a '&' b by A1,Def5;
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 S2 = 1GateCircStr(yc, '&'), A2 = 1GateCircuit(y,c, '&');
reconsider yy = y, cc = c as Vertex of S2 by Th43;
reconsider v2 = [yc, '&'] as Element of InnerVertices S2 by Th47;
set S1 = 1GateCircStr(<*x,y*>, '&'), A1 = 1GateCircuit(x,y, '&');
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;
A2: S1+*S2 = S2+*S1 by CIRCCOMB:5,47;
then
A3: S = S2+*(S1+*S3) by CIRCCOMB:6;
then reconsider v = v2 as Element of InnerVertices S by Th21;
A1+*A2 = A2+*A1 by CIRCCOMB:22,60;
then
A4: A = A2+*(A1+*A3) by A2,Th25;
then reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
reconsider yy, cc as Vertex of S by A3,Th20;
A5: dom s2 = the carrier of S2 by CIRCUIT1:3;
thus (Following s).[yc, '&'] = (Following s2).v by A3,A4,CIRCCOMB:64
.= '&'.<*s2.yy,s2.cc*> by Th48
.= '&'.<*s.yy,s2.cc*> by A5,FUNCT_1:47
.= '&'.<*s.yy,s.cc*> by A5,FUNCT_1:47
.= a '&' b by A1,Def5;
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 S3 = 1GateCircStr(cx, '&'), A3 = 1GateCircuit(c,x, '&');
reconsider cc = c, xx = x as Vertex of S3 by Th43;
reconsider v3 = [cx, '&'] as Element of InnerVertices S3 by Th47;
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 cc, xx as Vertex of S by Th20;
reconsider s3 = s|the carrier of S3 as State of A3 by Th26;
reconsider v = v3 as Element of InnerVertices S by Th21;
A2: dom s3 = the carrier of S3 by CIRCUIT1:3;
thus (Following s).[cx, '&'] = (Following s3).v by CIRCCOMB:64
.= '&'.<*s3.cc,s3.xx*> by Th48
.= '&'.<*s.cc,s3.xx*> by A2,FUNCT_1:47
.= '&'.<*s.cc,s.xx*> by A2,FUNCT_1:47
.= a '&' b by A1,Def5;
end;
definition
let x,y,c be object;
func MajorityOutput(x,y,c) -> Element of InnerVertices MajorityStr(x,y,c)
equals
[<*[<*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 Th21;
end;
correctness;
end;
definition
let x,y,c be object;
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;
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
c in the carrier of 1GateCircStr(<*c,x*>, '&') by Th43;
then
A1: c in the carrier of MajorityIStr(x,y,c) by Th20;
y in the carrier of 1GateCircStr(<*x,y*>, '&') by Th43;
then y in the carrier of 1GateCircStr(<*x,y*>, '&')+*1GateCircStr(<*y,c*> ,
'&') by Th20;
then
A2: y in the carrier of MajorityIStr(x,y,c) by Th20;
x in the carrier of 1GateCircStr(<*c,x*>, '&') by Th43;
then x in the carrier of MajorityIStr(x,y,c) by Th20;
hence thesis by A2,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
[<*x,y*>,'&'] in InnerVertices 1GateCircStr(<*x,y*>, '&') by Th47;
then
[<*x,y*>,'&'] in InnerVertices (1GateCircStr(<*x,y*>, '&')+*1GateCircStr
(<*y,c*>, '&')) by Th21;
then
A1: [<*x,y*>,'&'] in InnerVertices MajorityIStr(x,y,c) by Th21;
[<*y,c*>,'&'] in InnerVertices 1GateCircStr(<*y,c*>, '&') by Th47;
then
[<*y,c*>,'&'] in InnerVertices (1GateCircStr(<*x,y*>, '&')+*1GateCircStr
(<*y,c*>, '&')) by Th21;
then
A2: [<*y,c*>,'&'] in InnerVertices MajorityIStr(x,y,c) by Th21;
[<*c,x*>,'&'] in InnerVertices 1GateCircStr(<*c,x*>, '&') by Th47;
then [<*c,x*>,'&'] in InnerVertices MajorityIStr(x,y,c) by Th21;
hence thesis by A1,A2,Th21;
end;
theorem Th74:
for x,y,c being non pair object 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 object;
assume
A1: not thesis;
A2: c in the carrier of MajorityStr(x,y,c) by Th72;
A3: InnerVertices MajorityStr(x,y,c) is Relation by Th67;
x in the carrier of MajorityStr(x,y,c) & y in the carrier of MajorityStr
(x,y,c) by Th72;
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 A2,A1,XBOOLE_0:def 5;
then
(ex a,b being object st x = [a,b]) or
(ex a,b being object st y = [a,b]) or ex
a,b being object st c = [a,b] by A3,RELAT_1:def 1;
hence contradiction;
end;
theorem Th75:
for x,y,c being non pair object 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 object;
set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
set MI = MajorityIStr(x,y,c), S = 1GateCircStr(<*xy, yc, cx*>, or3);
set M = MajorityStr(x,y,c);
A1: 1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*y,c*>, '&') by
CIRCCOMB:43;
A2: InnerVertices S is Relation by Th38;
A3: InputVertices 1GateCircStr(<*y,c*>,'&') = {y,c} by Th40;
A4: InnerVertices 1GateCircStr(<*x,y*>, '&') = {[<*x,y*>, '&']} &
InnerVertices 1GateCircStr(<*y,c*>, '&') = {[<*y,c*>, '&']} by CIRCCOMB:42;
then
A5: InnerVertices 1GateCircStr(<*c,x*>, '&') = {[<*c,x*>, '&']} &
InnerVertices (1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&')) = {[<*
x,y*>, '&']} \/ {[<*y,c*>, '&']} by A1,CIRCCOMB:11,42;
1GateCircStr(<*x,y*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') &
1GateCircStr(<*y,c*>, '&') tolerates 1GateCircStr(<*c,x*>, '&') by CIRCCOMB:43;
then 1GateCircStr(<*x,y*>, '&') +* 1GateCircStr(<*y,c*>, '&') tolerates
1GateCircStr(<*c,x*>, '&') by A1,CIRCCOMB:3;
then
A6: InnerVertices MI = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} \/ {[<*c,x*>, '&'
]} by A5,CIRCCOMB:11
.= {[<*x,y*>,'&'], [<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:1
.= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by ENUMSET1:3;
InputVertices S = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} by Th42;
then
A7: InputVertices S \ InnerVertices MI = {} by A6,XBOOLE_1:37;
A8: InputVertices 1GateCircStr(<*x,y*>,'&') = {x,y} & InputVertices
1GateCircStr (<*c,x*>,'&') = {c,x} by Th40;
A9: InputVertices 1GateCircStr(<*c,x*>,'&') is without_pairs by Th41;
A10: InputVertices 1GateCircStr(<*x,y*>,'&') is without_pairs & InputVertices
1GateCircStr(<*y,c*>,'&') is without_pairs by Th41;
then
A11: InputVertices (1GateCircStr(<*x,y*>,'&')+*1GateCircStr(<*y,c*>,'&')) is
without_pairs by Th8,CIRCCOMB:47;
then InputVertices MI is without_pairs by A9,Th8,CIRCCOMB:47;
then
InputVertices M = (InputVertices MI) \/ (InputVertices S \ InnerVertices
MI) by A2,Th6;
hence InputVertices M = (InputVertices(1GateCircStr(<*x,y*>,'&')+*
1GateCircStr(<*y,c*>,'&'))) \/ InputVertices 1GateCircStr(<*c,x*>,'&') by A9
,A11,A5,A7,Th7
.= (InputVertices 1GateCircStr(<*x,y*>,'&')) \/ (InputVertices
1GateCircStr(<*y,c*>,'&')) \/ (InputVertices 1GateCircStr(<*c,x*>,'&')) by A10
,A4,Th7
.= {x,y,y,c} \/ {c,x} by A8,A3,ENUMSET1:5
.= {y,y,x,c} \/ {c,x} by ENUMSET1:67
.= {y,x,c} \/ {c,x} by ENUMSET1:31
.= {x,y,c} \/ {c,x} by ENUMSET1:58
.= {x,y,c} \/ ({c}\/{x}) by ENUMSET1:1
.= {x,y,c} \/ {c} \/ {x} by XBOOLE_1:4
.= {c,x,y} \/ {c} \/ {x} by ENUMSET1:59
.= {c,c,x,y} \/ {x} by ENUMSET1:4
.= {c,x,y} \/ {x} by ENUMSET1:31
.= {x,y,c} \/ {x} by ENUMSET1:59
.= {x,x,y,c} by ENUMSET1:4
.= {x,y,c} by ENUMSET1:31;
MI tolerates S by CIRCCOMB:47;
hence InnerVertices M = (InnerVertices MI) \/ (InnerVertices S) by
CIRCCOMB:11
.= {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {MajorityOutput(x,y,
c)} by A6,CIRCCOMB:42;
end;
Lm2: for x,y,c being non pair object
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 object;
let s be State of MajorityCirc(x,y,c);
let a1,a2,a3 be Element of BOOLEAN such that
A1: a1 = s.x and
A2: a2 = s.y and
A3: a3 = s.c;
set S = MajorityStr(x,y,c);
A4: dom s = the carrier of S by CIRCUIT1:3;
A5: y in the carrier of S by Th72;
A6: x in the carrier of S by Th72;
A7: InnerVertices S = the carrier' of S by Th37;
[<*x,y*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
hence (Following s).[<*x,y*>,'&'] = '&'.(s*<*x,y*>) by A7,Th35
.= '&'.<*a1,a2*> by A1,A2,A4,A6,A5,FINSEQ_2:125
.= a1 '&' a2 by Def5;
A8: c in the carrier of S by Th72;
[<*y,c*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
hence (Following s).[<*y,c*>,'&'] = '&'.(s*<*y,c*>) by A7,Th35
.= '&'.<*a2,a3*> by A2,A3,A4,A5,A8,FINSEQ_2:125
.= a2 '&' a3 by Def5;
[<*c,x*>,'&'] in InnerVertices MajorityStr(x,y,c) by Th73;
hence (Following s).[<*c,x*>,'&'] = '&'.(s*<*c,x*>) by A7,Th35
.= '&'.<*a3,a1*> by A1,A3,A4,A6,A8,FINSEQ_2:125
.= a3 '&' a1 by Def5;
end;
theorem
for x,y,c being non pair object 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 object;
reconsider a = c as Vertex of MajorityStr(x,y,c) by Th72;
let s be State of MajorityCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm2;
end;
theorem
for x,y,c being non pair object 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 object;
reconsider a = x as Vertex of MajorityStr(x,y,c) by Th72;
let s be State of MajorityCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm2;
end;
theorem
for x,y,c being non pair object 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 object;
reconsider a = y as Vertex of MajorityStr(x,y,c) by Th72;
let s be State of MajorityCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm2;
end;
theorem Th79:
for x,y,c being non pair object 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 object;
set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
set S = MajorityStr(x,y,c);
reconsider xy, yc, cx as Element of InnerVertices S by Th73;
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*>,'&'];
A2: dom s = the carrier of S by CIRCUIT1:3;
InnerVertices S = the carrier' of S by Th37;
hence (Following s).MajorityOutput(x,y,c) = or3.(s*<*xy, yc, cx*>) by Th35
.= or3.<*a1,a2,a3*> by A1,A2,FINSEQ_2:126
.= a1 'or' a2 'or' a3 by Def6;
end;
Lm3: for x,y,c being non pair object
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 object;
set S = MajorityStr(x,y,c);
reconsider x9 = x, y9 = y, c9 = c as Vertex of S by Th72;
let s be State of MajorityCirc(x,y,c);
set xy =[<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'];
A1: Following(s,2) = Following Following s by Th15;
let a1,a2,a3 be Element of BOOLEAN such that
A2: a1 = s.x & a2 = s.y & a3 = s.c;
A3: (Following s).cx = a3 '&' a1 by A2,Lm2;
(Following s).xy = a1 '&' a2 & (Following s).yc = a2 '&' a3 by A2,Lm2;
hence (Following(s,2)).MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or'
a3 '&' a1 by A1,A3,Th79;
y in InputVertices S by Th74;
then
A4: (Following s).y9 = s.y by CIRCUIT2:def 5;
c in InputVertices S by Th74;
then
A5: (Following s).c9 = s.c by CIRCUIT2:def 5;
x in InputVertices S by Th74;
then (Following s).x9 = s.x by CIRCUIT2:def 5;
hence thesis by A2,A4,A5,A1,Lm2;
end;
theorem
for x,y,c being non pair object 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 object;
reconsider a = c as Vertex of MajorityStr(x,y,c) by Th72;
let s be State of MajorityCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm3;
end;
theorem
for x,y,c being non pair object 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 object;
reconsider a = x as Vertex of MajorityStr(x,y,c) by Th72;
let s be State of MajorityCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm3;
end;
theorem
for x,y,c being non pair object 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 object;
reconsider a = y as Vertex of MajorityStr(x,y,c) by Th72;
let s be State of MajorityCirc(x,y,c);
s.a is Element of BOOLEAN;
hence thesis by Lm3;
end;
theorem
for x,y,c being non pair object 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 Lm3;
theorem Th84:
for x,y,c being non pair object for s being State of MajorityCirc(x
,y,c) holds Following(s,2) is stable
proof
let x,y,c be non pair object;
set S = MajorityStr(x,y,c);
reconsider xx = x, yy = y, cc = c as Vertex of S by Th72;
let s be State of MajorityCirc(x,y,c);
set a1 = s.xx, a2 = s.yy, a3 = s.cc;
set ffs = Following(s,2), fffs = Following ffs;
A1: ffs = Following Following s by Th15;
A2: y in InputVertices S by Th74;
then (Following s).y = a2 by CIRCUIT2:def 5;
then
A3: ffs.y = a2 by A1,A2,CIRCUIT2:def 5;
a2 = s.y;
then
A4: ffs.[<*c,x*>,'&'] = a3 '&' a1 by Lm3;
A5: x in InputVertices S by Th74;
then (Following s).x = a1 by CIRCUIT2:def 5;
then
A6: ffs.x = a1 by A1,A5,CIRCUIT2:def 5;
a1 = s.x;
then
A7: ffs.[<*y,c*>,'&'] = a2 '&' a3 by Lm3;
A8: c in InputVertices S by Th74;
then (Following s).c = a3 by CIRCUIT2:def 5;
then
A9: ffs.c = a3 by A1,A8,CIRCUIT2:def 5;
a3 = s.c;
then
A10: ffs.[<*x,y*>,'&'] = a1 '&' a2 by Lm3;
A11: ffs.MajorityOutput(x,y,c) = a1 '&' a2 'or' a2 '&' a3 'or' a3 '&' a1 by Lm3
;
A12: now
let a be object;
assume
A13: a in the carrier of S;
then reconsider v = a as Vertex of S;
A14: v in InputVertices S \/ InnerVertices S by A13,XBOOLE_1:45;
thus ffs.a = (fffs).a
proof
per cases by A14,XBOOLE_0:def 3;
suppose
v in InputVertices S;
hence thesis by CIRCUIT2:def 5;
end;
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 3;
then v = [<*x,y*>,'&'] or v = [<*y,c*>,'&'] or v = [<*c,x*>,'&'] or v
= MajorityOutput(x,y,c) by ENUMSET1:def 1,TARSKI:def 1;
hence thesis by A11,A10,A7,A4,A6,A3,A9,Lm2,Th79;
end;
end;
end;
dom Following Following(s,2) = the carrier of S & dom Following(s,2) =
the carrier of S by CIRCUIT1:3;
hence ffs = fffs by A12,FUNCT_1:2;
end;
definition
let x,y,c be object;
func BitAdderWithOverflowStr(x,y,c) -> unsplit gate`1=arity gate`2isBoolean
non void strict non empty ManySortedSign equals
2GatesCircStr(x,y,c, 'xor') +*
MajorityStr(x,y,c);
coherence;
end;
theorem Th85:
for x,y,c being non pair object holds InputVertices
BitAdderWithOverflowStr(x,y,c) = {x,y,c}
proof
let x,y,c be non pair object;
set S = BitAdderWithOverflowStr(x,y,c);
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
A1: InputVertices S1 = {x,y,c} & InputVertices S2 = {x,y,c} by Th57,Th75;
InnerVertices S1 is Relation & InnerVertices S2 is Relation by Th58,Th67;
hence InputVertices S = {x,y,c} \/ {x,y,c} by A1,Th7
.= {x,y,c};
end;
theorem
for x,y,c being non pair object 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 object;
set S1 = 2GatesCircStr(x,y,c, 'xor'), S2 = MajorityStr(x,y,c);
A1: InnerVertices S2 = {[<*x,y*>,'&'], [<*y,c*>,'&'], [<*c,x*>,'&']} \/ {
MajorityOutput(x,y,c)} by Th75;
{[<*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)}) & InnerVertices S1 = {[<*x,y*>, 'xor'],
2GatesCircOutput(x,y,c,'xor')} by Th56,XBOOLE_1:4;
hence thesis by A1,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
A1: S = BitAdderWithOverflowStr(x,y,c);
A2: c in the carrier of S1 by Th60;
x in the carrier of S1 & y in the carrier of S1 by Th60;
hence thesis by A1,A2,Th20;
end;
definition
let x,y,c be object;
func BitAdderWithOverflowCirc(x,y,c) -> strict Boolean gate`2=den Circuit of
BitAdderWithOverflowStr(x,y,c) equals
BitAdderCirc(x,y,c) +* MajorityCirc(x,y,c
);
coherence;
end;
theorem
InnerVertices BitAdderWithOverflowStr(x,y,c) is Relation
proof
InnerVertices 2GatesCircStr(x,y,c, 'xor') is Relation & InnerVertices
MajorityStr(x,y,c) is Relation by Th58,Th67;
hence thesis by Th2,CIRCCOMB:47;
end;
theorem
for x,y,c being non pair object holds InputVertices
BitAdderWithOverflowStr(x,y,c) is without_pairs
proof
let x,y,c be non pair object;
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) by Th21
;
theorem
for x,y,c being non pair object 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 object;
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;
reconsider t = s as State of A1+*A2;
reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
set f = 'xor';
let a1,a2,a3 be Element of BOOLEAN;
assume that
A1: a1 = s.x and
A2: a2 = s.y and
A3: a3 = s.c;
A4: dom s1 = the carrier of S1 by CIRCUIT1:3;
y in the carrier of S1 by Th60;
then
A5: a2 = s1.y by A2,A4,FUNCT_1:47;
InputVertices S1 is without_pairs by Th59;
then InnerVertices S2 misses InputVertices S1 by Th5,Th67;
then
A6: (Following(t,2)).2GatesCircOutput(x,y,c, f) = (Following(s1,2)).
2GatesCircOutput(x,y,c, f) by Th32;
c in the carrier of S1 by Th60;
then
A7: a3 = s1.c by A3,A4,FUNCT_1:47;
reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
A8: dom s2 = the carrier of S2 by CIRCUIT1:3;
x in the carrier of S1 by Th60;
then a1 = s1.x by A1,A4,FUNCT_1:47;
hence (Following(s,2)).BitAdderOutput(x,y,c) = a1 'xor' a2 'xor' a3 by A5,A7
,A6,Th64;
InputVertices S2 is without_pairs by Th68;
then InnerVertices S1 misses InputVertices S2 by Th5,Th58;
then
A9: (Following(t,2)).MajorityOutput(x,y,c) = (Following(s2,2)).
MajorityOutput(x,y,c) by Th33;
c in the carrier of S2 by Th72;
then
A10: a3 = s2.c by A3,A8,FUNCT_1:47;
y in the carrier of S2 by Th72;
then
A11: a2 = s2.y by A2,A8,FUNCT_1:47;
x in the carrier of S2 by Th72;
then a1 = s2.x by A1,A8,FUNCT_1:47;
hence thesis by A11,A10,A9,Lm3;
end;
theorem
for x,y,c being non pair object for s being State of
BitAdderWithOverflowCirc(x,y,c) holds Following(s,2) is stable
proof
let x,y,c be non pair object;
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;
reconsider s2 = s|the carrier of S2 as State of A2 by Th26;
reconsider t = s as State of A1+*A2;
reconsider s1 = s|the carrier of S1 as State of A1 by Th26;
set S = BitAdderWithOverflowStr(x,y,c);
A1: dom Following(s,3) = the carrier of S by CIRCUIT1:3;
A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by
CIRCCOMB:def 2;
InputVertices S1 is without_pairs by Th59;
then InnerVertices S2 misses InputVertices S1 by Th5,Th67;
then
A3: Following(s1,2) = Following(t,2)|the carrier of S1 & Following(s1,3) =
Following(t,3)|the carrier of S1 by Th30;
Following(s1,2) is stable by Th63;
then
A4: Following(s1,2) = Following Following(s1,2)
.= Following(s1,2+1) by Th12;
InputVertices S2 is without_pairs by Th68;
then InnerVertices S1 misses InputVertices S2 by Th5,Th58;
then
A5: Following(s2,2) = Following(t,2)|the carrier of S2 & Following(s2,3) =
Following(t,3)|the carrier of S2 by Th31;
Following(s2,2) is stable by Th84;
then
A6: Following(s2,2) = Following Following(s2,2)
.= Following(s2,2+1) by Th12;
A7: dom Following(s1,2) = the carrier of S1 & dom Following(s2,2) = the
carrier of S2 by CIRCUIT1:3;
A8: now
let a be object;
assume a in the carrier of S;
then a in the carrier of S1 or a in the carrier of S2 by A2,XBOOLE_0:def 3;
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 A3,A5,A4,A6,A7,FUNCT_1:47;
hence (Following(s,2)).a = (Following Following(s,2)).a by A4,A6,Th12;
end;
Following(s,2+1) = Following Following(s,2) & dom Following(s,2) = the
carrier of S by Th12,CIRCUIT1:3;
hence Following(s,2) = Following Following(s,2) by A1,A8,FUNCT_1:2;
end;