:: FACIRC_1 semantic presentation

begin

registration
cluster pair  ->  non empty for set ;
coherence
 for b1 being set st b1 is pair holds
not b1 is empty
proof
let z be set ; ::_thesis: ( z is pair implies not z is empty )
given x, y being set  such that A1: z = [x,y] ; :: according to XTUPLE_0:def_1 ::_thesis: not z is empty
thus  not z is empty by A1; ::_thesis: verum
end;
end;

registration
cluster non pair for set ;
existence
 not for b1 being set holds b1 is pair
proof
take  {} ; ::_thesis: not {} is pair
let x, y be set ; :: according to XTUPLE_0:def_1 ::_thesis: not {} = [x,y]
thus  not {} = [x,y] ; ::_thesis: verum
end;
end;

registration
clusterV13()  ->  non pair for set ;
coherence
 for b1 being Nat holds not b1 is pair
proof
let n be Nat; ::_thesis: not n is pair
given x, y being set  such that A1: n = [x,y] ; :: according to XTUPLE_0:def_1 ::_thesis: contradiction
 n =  {  k where k is Element of NAT : k < n  }  by AXIOMS:4;
then  0 in n by A1;
hence  contradiction by A1, TARSKI:def_2; ::_thesis: verum
end;
end;

definition
canceled;
let IT be set ;
attrIT is with_pair  means :Def2: :: FACIRC_1:def 2
 ex x being pair set st x in IT;
end;

:: deftheorem  FACIRC_1:def_1_:_
canceled;

:: deftheorem Def2 defines with_pair FACIRC_1:def_2_:_
 for IT being set holds
( IT is with_pair iff ex x being pair set st x in IT );

notation
let IT be set ;
antonym  without_pairs IT for  with_pair ;
end;

registration
cluster empty  ->  without_pairs for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is without_pairs
proof
let x be set ; ::_thesis: ( x is empty implies x is without_pairs )
assume A1: x is empty ; ::_thesis: x is without_pairs
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in x
thus  not a in x by A1; ::_thesis: verum
end;
let x be non pair set ;
cluster{x} ->  without_pairs ;
coherence
 not {x} is with_pair
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in {x}
assume  a in {x} ; ::_thesis: contradiction
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
let y be non pair set ;
cluster{x,y} ->  without_pairs ;
coherence
 not {x,y} is with_pair
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in {x,y}
assume  a in {x,y} ; ::_thesis: contradiction
hence  contradiction by TARSKI:def_2; ::_thesis: verum
end;
let z be non pair set ;
cluster{x,y,z} ->  without_pairs ;
coherence
 not {x,y,z} is with_pair
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in {x,y,z}
assume  a in {x,y,z} ; ::_thesis: contradiction
hence  contradiction by ENUMSET1:def_1; ::_thesis: verum
end;
end;

registration
cluster non empty without_pairs for set ;
existence
 ex b1 being non empty set st b1 is without_pairs
proof
set x = the non pair set ;
take  { the non pair set } ; ::_thesis: { the non pair set } is without_pairs
thus  { the non pair set } is without_pairs ; ::_thesis: verum
end;
end;

registration
let X, Y be without_pairs set ;
clusterX \/ Y ->  without_pairs ;
coherence
 not X \/ Y is with_pair
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in X \/ Y
assume  a in X \/ Y ; ::_thesis: contradiction
then  ( a in X or a in Y ) by XBOOLE_0:def_3;
hence  contradiction by Def2; ::_thesis: verum
end;
end;

registration
let X be without_pairs set ;
let Y be set ;
clusterX \ Y ->  without_pairs ;
coherence
 not X \ Y is with_pair
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in X \ Y
assume  a in X \ Y ; ::_thesis: contradiction
hence  contradiction by Def2; ::_thesis: verum
end;
clusterX /\ Y ->  without_pairs ;
coherence
 not X /\ Y is with_pair
proof
let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in X /\ Y
assume  a in X /\ Y ; ::_thesis: contradiction
then  a in X by XBOOLE_0:def_4;
hence  contradiction by Def2; ::_thesis: verum
end;
clusterY /\ X ->  without_pairs ;
coherence
 not Y /\ X is with_pair ;
end;

registration
let x be pair set ;
cluster{x} ->  Relation-like ;
coherence
 {x} is Relation-like
proof
let a be set ; :: according to RELAT_1:def_1 ::_thesis: ( not a in {x} or ex b1, b2 being set st a = [b1,b2] )
assume  a in {x} ; ::_thesis: ex b1, b2 being set st a = [b1,b2]
then  a = x by TARSKI:def_1;
hence  ex b1, b2 being set st a = [b1,b2] by XTUPLE_0:def_1; ::_thesis: verum
end;
let y be pair set ;
cluster{x,y} ->  Relation-like ;
coherence
 {x,y} is Relation-like
proof
let a be set ; :: according to RELAT_1:def_1 ::_thesis: ( not a in {x,y} or ex b1, b2 being set st a = [b1,b2] )
assume  a in {x,y} ; ::_thesis: ex b1, b2 being set st a = [b1,b2]
then  ( a = x or a = y ) by TARSKI:def_2;
hence  ex b1, b2 being set st a = [b1,b2] by XTUPLE_0:def_1; ::_thesis: verum
end;
let z be pair set ;
cluster{x,y,z} ->  Relation-like ;
coherence
 {x,y,z} is Relation-like
proof
let a be set ; :: according to RELAT_1:def_1 ::_thesis: ( not a in {x,y,z} or ex b1, b2 being set st a = [b1,b2] )
assume  a in {x,y,z} ; ::_thesis: ex b1, b2 being set st a = [b1,b2]
then  ( a = x or a = y or a = z ) by ENUMSET1:def_1;
hence  ex b1, b2 being set st a = [b1,b2] by XTUPLE_0:def_1; ::_thesis: verum
end;
end;

registration
cluster Relation-like without_pairs  ->  empty for set ;
coherence
 for b1 being set st b1 is without_pairs & b1 is Relation-like holds
b1 is empty
proof
let x be set ; ::_thesis: ( x is without_pairs & x is Relation-like implies x is empty )
assume A1: for a being pair set holds not a in x ; :: according to FACIRC_1:def_2 ::_thesis: ( not x is Relation-like or x is empty )
assume A2: for a being set st a in x holds
ex y, z being set st a = [y,z] ; :: according to RELAT_1:def_1 ::_thesis: x is empty
assume  not x is empty ; ::_thesis: contradiction
then reconsider X = x as non empty set ;
set a = the Element of X;
 ex y, z being set st the Element of X = [y,z] by A2;
hence  contradiction by A1; ::_thesis: verum
end;
end;

definition
let IT be Function;
attrIT is nonpair-yielding  means :: FACIRC_1:def 3
 for x being set st x in dom IT holds
not IT . x is pair ;
end;

:: deftheorem  defines nonpair-yielding FACIRC_1:def_3_:_
 for IT being Function holds
( IT is nonpair-yielding iff for x being set st x in dom IT holds
not IT . x is pair );

registration
let x be non pair set ;
cluster<*x*> ->  nonpair-yielding ;
coherence
 <*x*> is nonpair-yielding
proof
let a be set ; :: according to FACIRC_1:def_3 ::_thesis: ( a in dom <*x*> implies not <*x*> . a is pair )
assume  a in dom <*x*> ; ::_thesis: not <*x*> . a is pair
then  <*x*> . a in rng <*x*> by FUNCT_1:def_3;
then  <*x*> . a in {x} by FINSEQ_1:39;
hence  not <*x*> . a is pair by TARSKI:def_1; ::_thesis: verum
end;
let y be non pair set ;
cluster<*x,y*> ->  nonpair-yielding ;
coherence
 <*x,y*> is nonpair-yielding
proof
let a be set ; :: according to FACIRC_1:def_3 ::_thesis: ( a in dom <*x,y*> implies not <*x,y*> . a is pair )
assume  a in dom <*x,y*> ; ::_thesis: not <*x,y*> . a is pair
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  not <*x,y*> . a is pair by TARSKI:def_2; ::_thesis: verum
end;
let z be non pair set ;
cluster<*x,y,z*> ->  nonpair-yielding ;
coherence
 <*x,y,z*> is nonpair-yielding
proof
let a be set ; :: according to FACIRC_1:def_3 ::_thesis: ( a in dom <*x,y,z*> implies not <*x,y,z*> . a is pair )
assume  a in dom <*x,y,z*> ; ::_thesis: not <*x,y,z*> . a is pair
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  not <*x,y,z*> . a is pair by ENUMSET1:def_1; ::_thesis: verum
end;
end;

theorem Th1: :: FACIRC_1:1
for f being Function st f is nonpair-yielding holds
rng f is without_pairs
proof
let f be Function; ::_thesis: ( f is nonpair-yielding implies rng f is without_pairs )
assume A1: for x being set st x in dom f holds
not f . x is pair ; :: according to FACIRC_1:def_3 ::_thesis: rng f is without_pairs
let y be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not y in rng f
assume  y in rng f ; ::_thesis: contradiction
then  ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def_3;
hence  contradiction by A1; ::_thesis: verum
end;

registration
let n be Nat;
cluster Relation-like NAT -defined Function-like one-to-one finite V46(n) FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;
existence
 ex b1 being FinSeqLen of n st
( b1 is one-to-one & b1 is nonpair-yielding )
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 = p as FinSeqLen of n by CARD_1:def_7;
take  p ; ::_thesis: ( p is one-to-one & p is nonpair-yielding )
thus  p is one-to-one ; ::_thesis: p is nonpair-yielding
let x be set ; :: according to FACIRC_1:def_3 ::_thesis: ( x in dom p implies not p . x is pair )
assume A1: x in dom p ; ::_thesis: not p . x is pair
 x in Seg n by A1, RELAT_1:45;
hence  not p . x is pair by FUNCT_1:17; ::_thesis: verum
end;
end;

registration
cluster Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;
existence
 ex b1 being FinSequence st
( b1 is one-to-one & b1 is nonpair-yielding )
proof
set n = the Nat;
set p = the one-to-one nonpair-yielding FinSeqLen of the Nat;
take  the one-to-one nonpair-yielding FinSeqLen of the Nat ; ::_thesis: ( the one-to-one nonpair-yielding FinSeqLen of the Nat is one-to-one & the one-to-one nonpair-yielding FinSeqLen of the Nat is nonpair-yielding )
thus  ( the one-to-one nonpair-yielding FinSeqLen of the Nat is one-to-one & the one-to-one nonpair-yielding FinSeqLen of the Nat is nonpair-yielding ) ; ::_thesis: verum
end;
end;

registration
let f be nonpair-yielding Function;
cluster proj2 f ->  without_pairs ;
coherence
 not rng f is with_pair by Th1;
end;

theorem Th2: :: FACIRC_1:2
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 ; ::_thesis: ( S1 tolerates S2 & InnerVertices S1 is Relation & InnerVertices S2 is Relation implies InnerVertices (S1 +* S2) is Relation )
assume A1: S1 tolerates S2 ; ::_thesis: ( not InnerVertices S1 is Relation or not InnerVertices S2 is Relation or InnerVertices (S1 +* S2) is Relation )
assume  ( InnerVertices S1 is Relation & InnerVertices S2 is Relation ) ; ::_thesis: InnerVertices (S1 +* S2) is Relation
then reconsider R1 = InnerVertices S1, R2 = InnerVertices S2 as Relation ;
 R1 \/ R2 is Relation ;
hence  InnerVertices (S1 +* S2) is Relation by A1, CIRCCOMB:11; ::_thesis: verum
end;

theorem :: FACIRC_1:3
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InnerVertices S1 is Relation & InnerVertices S2 is Relation holds
InnerVertices (S1 +* S2) is Relation by Th2, CIRCCOMB:47;

theorem Th4: :: FACIRC_1:4
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 ; ::_thesis: ( S1 tolerates S2 & InnerVertices S2 misses InputVertices S1 implies ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ) )
set S = S1 +* S2;
set R = the ResultSort of (S1 +* S2);
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 ; ::_thesis: ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
A3: InnerVertices (S1 +* S2) = rng the ResultSort of (S1 +* S2) ;
 ( InnerVertices S1 = rng the ResultSort of S1 & InnerVertices S2 = rng the ResultSort of S2 ) ;
then A4: rng the ResultSort of (S1 +* S2) = (rng the ResultSort of S1) \/ (rng the ResultSort of S2) by A1, A3, CIRCCOMB:11;
A5: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def_2;
hereby  :: according to TARSKI:def_3 ::_thesis: InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1))
let x be set ; ::_thesis: ( x in InputVertices S1 implies x in InputVertices (S1 +* S2) )
assume A6: x in InputVertices S1 ; ::_thesis: x in InputVertices (S1 +* S2)
then  ( not x in rng the ResultSort of S1 & not x in rng the ResultSort of S2 ) by A2, XBOOLE_0:3, XBOOLE_0:def_5;
then A7: not x in rng the ResultSort of (S1 +* S2) by A4, XBOOLE_0:def_3;
 x in the carrier of (S1 +* S2) by A5, A6, XBOOLE_0:def_3;
hence  x in InputVertices (S1 +* S2) by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
A8: InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) by A1, CIRCCOMB:11;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) c= InputVertices (S1 +* S2)
let x be set ; ::_thesis: ( x in InputVertices (S1 +* S2) implies x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
assume A9: x in InputVertices (S1 +* S2) ; ::_thesis: x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1))
then  not x in rng the ResultSort of (S1 +* S2) 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; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) or x in InputVertices (S1 +* S2) )
assume  x in (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ; ::_thesis: x in InputVertices (S1 +* S2)
then A10: ( x in InputVertices S1 or x in (InputVertices S2) \ (rng the ResultSort of S1) ) by XBOOLE_0:def_3;
then A11: x in the carrier of (S1 +* S2) by A5, XBOOLE_0:def_3;
 ( ( x in InputVertices S1 & not x in rng the ResultSort of S2 ) or ( x in InputVertices S2 & not x in rng the ResultSort of S1 ) ) by A2, A10, XBOOLE_0:3, XBOOLE_0:def_5;
then A12: not x in rng the ResultSort of S2 by XBOOLE_0:def_5;
 not x in rng the ResultSort of S1 by A10, XBOOLE_0:def_5;
then  not x in rng the ResultSort of (S1 +* S2) by A4, A12, XBOOLE_0:def_3;
hence  x in InputVertices (S1 +* S2) by A11, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th5: :: FACIRC_1:5
for X, R being set st X is without_pairs & R is Relation holds
X misses R
proof
let X, R be set ; ::_thesis: ( X is without_pairs & R is Relation implies X misses R )
assume A1: for x being pair set holds not x in X ; :: according to FACIRC_1:def_2 ::_thesis: ( not R is Relation or X misses R )
assume A2: R is Relation ; ::_thesis: X misses R
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
not_x_in_R
let x be set ; ::_thesis: ( x in X implies not x in R )
assume  x in X ; ::_thesis: not x in R
then  for z1, z2 being set holds not x = [z1,z2] by A1;
hence  not x in R by A2, RELAT_1:def_1; ::_thesis: verum
end;
hence  X misses R by XBOOLE_0:3; ::_thesis: verum
end;

theorem Th6: :: FACIRC_1:6
for S1, S2 being non empty unsplit gate`1=arity 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 non empty unsplit gate`1=arity ManySortedSign ; ::_thesis: ( InputVertices S1 is without_pairs & InnerVertices S2 is Relation implies ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ) )
assume  ( InputVertices S1 is without_pairs & InnerVertices S2 is Relation ) ; ::_thesis: ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
then  ( S1 tolerates S2 & InnerVertices S2 misses InputVertices S1 ) by Th5, CIRCCOMB:47;
hence  ( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) ) by Th4; ::_thesis: verum
end;

theorem Th7: :: FACIRC_1:7
for S1, S2 being non empty unsplit gate`1=arity 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 non empty unsplit gate`1=arity ManySortedSign ; ::_thesis: ( InputVertices S1 is without_pairs & InnerVertices S1 is Relation & InputVertices S2 is without_pairs & InnerVertices S2 is Relation implies InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2) )
assume  ( InputVertices S1 is without_pairs & InnerVertices S1 is Relation & InputVertices S2 is without_pairs & InnerVertices S2 is Relation ) ; ::_thesis: InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2)
then  ( InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) & InnerVertices S1 misses InputVertices S2 ) by Th5, Th6;
hence  InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2) by XBOOLE_1:83; ::_thesis: verum
end;

theorem Th8: :: FACIRC_1:8
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 ; ::_thesis: ( S1 tolerates S2 & InputVertices S1 is without_pairs & InputVertices S2 is without_pairs implies InputVertices (S1 +* S2) is without_pairs )
assume  S1 tolerates S2 ; ::_thesis: ( not InputVertices S1 is without_pairs or not InputVertices S2 is without_pairs or InputVertices (S1 +* S2) is without_pairs )
then A1: InputVertices (S1 +* S2) c= (InputVertices S1) \/ (InputVertices S2) by CIRCCOMB:11;
assume A2: for x being pair set holds not x in InputVertices S1 ; :: according to FACIRC_1:def_2 ::_thesis: ( not InputVertices S2 is without_pairs or InputVertices (S1 +* S2) is without_pairs )
assume A3: for x being pair set holds not x in InputVertices S2 ; :: according to FACIRC_1:def_2 ::_thesis: InputVertices (S1 +* S2) is without_pairs
let x be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not x in InputVertices (S1 +* S2)
assume  x in InputVertices (S1 +* S2) ; ::_thesis: contradiction
then  ( x in InputVertices S1 or x in InputVertices S2 ) by A1, XBOOLE_0:def_3;
hence  contradiction by A2, A3; ::_thesis: verum
end;

theorem :: FACIRC_1:9
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InputVertices S1 is without_pairs & InputVertices S2 is without_pairs holds
InputVertices (S1 +* S2) is without_pairs by Th8, CIRCCOMB:47;

begin

definition
let i be Nat;
let D be non empty set ;
mode Tuple of i,D is Element of i -tuples_on D;
end;

scheme :: FACIRC_1:sch 1
2AryBooleEx{ F1( 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*> = F1(x,y)
proof
deffunc H1( Tuple of 2,BOOLEAN) ->  Element of BOOLEAN = F1(($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 = H1(a) from FUNCT_2:sch_4();
hereby  ::_thesis: verum
take f = f; ::_thesis: for x, y being Element of BOOLEAN holds f . <*x,y*> = F1(x,y)
let x, y be Element of BOOLEAN ; ::_thesis: f . <*x,y*> = F1(x,y)
reconsider a = <*x,y*> as Tuple of 2,BOOLEAN by FINSEQ_2:101;
thus f . <*x,y*> = F1((a . 1),(a . 2)) by A1
.= F1(x,(a . 2)) by FINSEQ_1:44
.= F1(x,y) by FINSEQ_1:44 ; ::_thesis: verum
end;
end;

scheme :: FACIRC_1:sch 2
2AryBooleUniq{ F1( 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*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) holds
f1 = f2
proof
let f1, f2 be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: ( ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) implies f1 = f2 )
assume that
A1: for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) and
A2: for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_Tuple_of_2,BOOLEAN_holds_f1_._a_=_f2_._a
let a be Tuple of 2,BOOLEAN; ::_thesis: f1 . a = f2 . a
consider x, y being Element of BOOLEAN  such that
A3: a = <*x,y*> by FINSEQ_2:100;
thus f1 . a = F1(x,y) by A1, A3
.= f2 . a by A2, A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: FACIRC_1:sch 3
2AryBooleDef{ F1( 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*> = F1(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*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) holds
f1 = f2 ) )
proof
deffunc H1( Tuple of 2,BOOLEAN) ->  Element of BOOLEAN = F1(($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 = H1(a) from FUNCT_2:sch_4();
hereby  ::_thesis: for f1, f2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) holds
f1 = f2
take f = f; ::_thesis: for x, y being Element of BOOLEAN holds f . <*x,y*> = F1(x,y)
let x, y be Element of BOOLEAN ; ::_thesis: f . <*x,y*> = F1(x,y)
reconsider a = <*x,y*> as Tuple of 2,BOOLEAN by FINSEQ_2:101;
thus f . <*x,y*> = F1((a . 1),(a . 2)) by A1
.= F1(x,(a . 2)) by FINSEQ_1:44
.= F1(x,y) by FINSEQ_1:44 ; ::_thesis: verum
end;
let f1, f2 be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: ( ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) implies f1 = f2 )
assume that
A2: for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) and
A3: for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_Tuple_of_2,BOOLEAN_holds_f1_._a_=_f2_._a
let a be Tuple of 2,BOOLEAN; ::_thesis: f1 . a = f2 . a
consider x, y being Element of BOOLEAN  such that
A4: a = <*x,y*> by FINSEQ_2:100;
thus f1 . a = F1(x,y) by A2, A4
.= f2 . a by A3, A4 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: FACIRC_1:sch 4
3AryBooleEx{ F1( 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*> = F1(x,y,z)
proof
deffunc H1( Tuple of 3,BOOLEAN) ->  Element of BOOLEAN = F1(($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 = H1(a) from FUNCT_2:sch_4();
hereby  ::_thesis: verum
take f = f; ::_thesis: for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F1(x,y,z)
let x, y, z be Element of BOOLEAN ; ::_thesis: f . <*x,y,z*> = F1(x,y,z)
reconsider a = <*x,y,z*> as Tuple of 3,BOOLEAN by FINSEQ_2:104;
thus f . <*x,y,z*> = F1((a . 1),(a . 2),(a . 3)) by A1
.= F1(x,(a . 2),(a . 3)) by FINSEQ_1:45
.= F1(x,y,(a . 3)) by FINSEQ_1:45
.= F1(x,y,z) by FINSEQ_1:45 ; ::_thesis: verum
end;
end;

scheme :: FACIRC_1:sch 5
3AryBooleUniq{ F1( 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*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) holds
f1 = f2
proof
let f1, f2 be Function of (3 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: ( ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) implies f1 = f2 )
assume that
A1: for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) and
A2: for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_Tuple_of_3,BOOLEAN_holds_f1_._a_=_f2_._a
let a be Tuple of 3,BOOLEAN; ::_thesis: f1 . a = f2 . a
consider x, y, z being Element of BOOLEAN  such that
A3: a = <*x,y,z*> by FINSEQ_2:103;
thus f1 . a = F1(x,y,z) by A1, A3
.= f2 . a by A2, A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: FACIRC_1:sch 6
3AryBooleDef{ F1( 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*> = F1(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*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) holds
f1 = f2 ) )
proof
deffunc H1( Tuple of 3,BOOLEAN) ->  Element of BOOLEAN = F1(($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 = H1(a) from FUNCT_2:sch_4();
hereby  ::_thesis: 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*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) holds
f1 = f2
take f = f; ::_thesis: for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F1(x,y,z)
let x, y, z be Element of BOOLEAN ; ::_thesis: f . <*x,y,z*> = F1(x,y,z)
reconsider a = <*x,y,z*> as Tuple of 3,BOOLEAN by FINSEQ_2:104;
thus f . <*x,y,z*> = F1((a . 1),(a . 2),(a . 3)) by A1
.= F1(x,(a . 2),(a . 3)) by FINSEQ_1:45
.= F1(x,y,(a . 3)) by FINSEQ_1:45
.= F1(x,y,z) by FINSEQ_1:45 ; ::_thesis: verum
end;
let f1, f2 be Function of (3 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: ( ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) implies f1 = f2 )
assume that
A2: for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) and
A3: for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_Tuple_of_3,BOOLEAN_holds_f1_._a_=_f2_._a
let a be Tuple of 3,BOOLEAN; ::_thesis: f1 . a = f2 . a
consider x, y, z being Element of BOOLEAN  such that
A4: a = <*x,y,z*> by FINSEQ_2:103;
thus f1 . a = F1(x,y,z) by A2, A4
.= f2 . a by A3, A4 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

definition
func 'xor'  ->  Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def4: :: FACIRC_1:def 4
 for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'xor' y;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds
b1 = b2;
proof
deffunc H1( Element of BOOLEAN , 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*> = H1(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*> = H1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = H1(x,y) ) holds
f1 = f2 ) ) from FACIRC_1:sch_3();
hence  ( ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y & ( for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
func 'or'  ->  Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def5: :: FACIRC_1:def 5
 for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'or' y;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds
b1 = b2;
proof
deffunc H1( Element of BOOLEAN , 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*> = H1(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*> = H1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = H1(x,y) ) holds
f1 = f2 ) ) from FACIRC_1:sch_3();
hence  ( ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y & ( for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
func '&'  ->  Function of (2 -tuples_on BOOLEAN),BOOLEAN means :Def6: :: FACIRC_1:def 6
 for x, y being Element of BOOLEAN holds it . <*x,y*> = x '&' y;
correctness
existence
ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y;
uniqueness
for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2;
proof
deffunc H1( Element of BOOLEAN , 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*> = H1(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*> = H1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = H1(x,y) ) holds
f1 = f2 ) ) from FACIRC_1:sch_3();
hence  ( ex b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y & ( for b1, b2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines 'xor' FACIRC_1:def_4_:_
 for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = 'xor' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y );

:: deftheorem Def5 defines 'or' FACIRC_1:def_5_:_
 for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = 'or' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y );

:: deftheorem Def6 defines '&' FACIRC_1:def_6_:_
 for b1 being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = '&' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y );

definition
func or3  ->  Function of (3 -tuples_on BOOLEAN),BOOLEAN means :Def7: :: FACIRC_1:def 7
 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x 'or' y) 'or' z;
correctness
existence
ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z;
uniqueness
for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'or' y) 'or' z ) holds
b1 = b2;
proof
deffunc H1( Element of BOOLEAN , 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*> = H1(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*> = H1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = H1(x,y,z) ) holds
f1 = f2 ) ) from FACIRC_1:sch_6();
hence  ( ex b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z & ( for b1, b2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'or' y) 'or' z ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines or3 FACIRC_1:def_7_:_
 for b1 being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds
( b1 = or3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z );

begin

theorem Th10: :: FACIRC_1:10
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for 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 non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))
let A be non-empty Circuit of S; ::_thesis: for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))
let s be State of A; ::_thesis: for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))
let g be Gate of S; ::_thesis: (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g))
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: the_result_sort_of g in InnerVertices S by MSUALG_1:def_2;
then  ( g depends_on_in s = s * (the_arity_of g) & action_at (the_result_sort_of g) = g ) by CIRCUIT1:def_3, MSAFREE2:def_7;
hence  (Following s) . (the_result_sort_of g) = (Den (g,A)) . (s * (the_arity_of g)) by A1, CIRCUIT2:def_5; ::_thesis: verum
end;

definition
let S be non empty non void Circuit-like 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: :: FACIRC_1:def 8
 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
existence
ex b1 being State of A ex f being Function of NAT,(product the Sorts of A) st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) );
uniqueness
for b1, b2 being State of A st ex f being Function of NAT,(product the Sorts of A) st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ex f being Function of NAT,(product the Sorts of A) st
( b2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) holds
b1 = b2;
proof
set D = product the Sorts of A;
deffunc H1( Nat, Element of product the Sorts of A) ->  Element of product the Sorts of A = Following $2;
 ( ex y being Element of product the Sorts of A ex f being Function of NAT,(product the Sorts of A) st
( y = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) & ( for y1, y2 being Element of product the Sorts of A st ex f being Function of NAT,(product the Sorts of A) st
( y1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) & ex f being Function of NAT,(product the Sorts of A) st
( y2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) holds
y1 = y2 ) ) from RECDEF_1:sch_14();
hence  ( ex b1 being State of A ex f being Function of NAT,(product the Sorts of A) st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ( for b1, b2 being State of A st ex f being Function of NAT,(product the Sorts of A) st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ex f being Function of NAT,(product the Sorts of A) st
( b2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Following FACIRC_1:def_8_:_
 for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat
for b5 being State of A holds
( b5 = Following (s,n) iff ex f being Function of NAT,(product the Sorts of A) st
( b5 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) );

theorem Th11: :: FACIRC_1:11
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following (s,0) = s
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A holds Following (s,0) = s
let A be non-empty Circuit of S; ::_thesis: for s being State of A holds Following (s,0) = s
let s be State of A; ::_thesis: Following (s,0) = s
 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  Following (s,0) = s ; ::_thesis: verum
end;

theorem Th12: :: FACIRC_1:12
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
let A be non-empty Circuit of S; ::_thesis: for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
let s be State of A; ::_thesis: for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
let n be Nat; ::_thesis: Following (s,(n + 1)) = Following (Following (s,n))
consider f being Function of NAT,(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 Def8;
thus  Following (s,(n + 1)) = f . (n + 1) by A2, A3, Def8
.= Following (Following (s,n)) by A1, A3 ; ::_thesis: verum
end;

theorem Th13: :: FACIRC_1:13
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A
for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)
let A be non-empty Circuit of S; ::_thesis: for s being State of A
for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)
let s be State of A; ::_thesis: for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)
let n be Nat; ::_thesis: for m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)
defpred S1[ Nat] means  Following (s,(n + $1)) = Following ((Following (s,n)),$1);
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: Following (s,(n + m)) = Following ((Following (s,n)),m) ; ::_thesis: S1[m + 1]
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 ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th11;
thus  for i being Nat holds S1[i] from NAT_1:sch_2(A3, A1); ::_thesis: verum
end;

theorem Th14: :: FACIRC_1:14
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following (s,1) = Following s
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A holds Following (s,1) = Following s
let A be non-empty Circuit of S; ::_thesis: for s being State of A holds Following (s,1) = Following s
let s be State of A; ::_thesis: Following (s,1) = Following s
 0 + 1 = 1 ;
hence  Following (s,1) = Following (Following (s,0)) by Th12
.= Following s by Th11 ;
::_thesis: verum
end;

theorem Th15: :: FACIRC_1:15
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following (s,2) = Following (Following s)
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A holds Following (s,2) = Following (Following s)
let A be non-empty Circuit of S; ::_thesis: for s being State of A holds Following (s,2) = Following (Following s)
let s be State of A; ::_thesis: Following (s,2) = Following (Following s)
 2 = 1 + 1 ;
hence  Following (s,2) = Following (Following (s,(0 + 1))) by Th12
.= Following (Following s) by Th14 ;
::_thesis: verum
end;

theorem Th16: :: FACIRC_1:16
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
let A be non-empty Circuit of S; ::_thesis: for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
let s be State of A; ::_thesis: for n being Nat holds Following (s,(n + 1)) = Following ((Following s),n)
let n be Nat; ::_thesis: Following (s,(n + 1)) = Following ((Following s),n)
 Following (s,(n + 1)) = Following ((Following (s,1)),n) by Th13;
hence  Following (s,(n + 1)) = Following ((Following s),n) by Th14; ::_thesis: verum
end;

definition
let S be non empty non void Circuit-like ManySortedSign ;
let A be non-empty Circuit of S;
let s be State of A;
let x be set ;
preds is_stable_at x means :Def9: :: FACIRC_1:def 9
 for n being Nat holds (Following (s,n)) . x = s . x;
end;

:: deftheorem Def9 defines is_stable_at FACIRC_1:def_9_:_
 for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set holds
( s is_stable_at x iff for n being Nat holds (Following (s,n)) . x = s . x );

theorem :: FACIRC_1:17
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set st s is_stable_at x holds
for n being Nat holds Following (s,n) is_stable_at x
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A
for x being set st s is_stable_at x holds
for n being Nat holds Following (s,n) is_stable_at x
let A be non-empty Circuit of S; ::_thesis: for s being State of A
for x being set st s is_stable_at x holds
for n being Nat holds Following (s,n) is_stable_at x
let s be State of A; ::_thesis: for x being set st s is_stable_at x holds
for n being Nat holds Following (s,n) is_stable_at x
let x be set ; ::_thesis: ( s is_stable_at x implies for n being Nat holds Following (s,n) is_stable_at x )
assume A1: for n being Nat holds (Following (s,n)) . x = s . x ; :: according to FACIRC_1:def_9 ::_thesis: for n being Nat holds Following (s,n) is_stable_at x
let n, m be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following ((Following (s,n)),m)) . x = (Following (s,n)) . x
thus (Following ((Following (s,n)),m)) . x = (Following (s,(n + m))) . x by Th13
.= s . x by A1
.= (Following (s,n)) . x by A1 ; ::_thesis: verum
end;

theorem :: FACIRC_1:18
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for 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 empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A
for x being set st x in InputVertices S holds
s is_stable_at x
let A be non-empty Circuit of S; ::_thesis: for s being State of A
for x being set st x in InputVertices S holds
s is_stable_at x
let s be State of A; ::_thesis: for x being set st x in InputVertices S holds
s is_stable_at x
let x be set ; ::_thesis: ( x in InputVertices S implies s is_stable_at x )
defpred S1[ Nat] means (Following (s,$1)) . x = s . x;
assume A1: x in InputVertices S ; ::_thesis: s is_stable_at x
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
(Following (s,(n + 1))) . x = (Following (Following (s,n))) . x by Th12
.= s . x by A1, A3, CIRCUIT2:def_5 ;
hence  S1[n + 1] ; ::_thesis: verum
end;
A4: S1[ 0 ] by Th11;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A4, A2); :: according to FACIRC_1:def_9 ::_thesis: verum
end;

theorem Th19: :: FACIRC_1:19
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for 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 empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for 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
let A be non-empty Circuit of S; ::_thesis: for 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
let s be State of A; ::_thesis: 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
let g be Gate of S; ::_thesis: ( ( for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ) implies Following s is_stable_at the_result_sort_of g )
set p = the_arity_of g;
assume A1: for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ; ::_thesis: Following s is_stable_at the_result_sort_of g
let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following ((Following s),n)) . (the_result_sort_of g) = (Following s) . (the_result_sort_of g)
A2: now__::_thesis:_for_a_being_set_st_a_in_dom_(the_arity_of_g)_holds_
((Following_(s,n))_*_(the_arity_of_g))_._a_=_(s_*_(the_arity_of_g))_._a
let a be set ; ::_thesis: ( a in dom (the_arity_of g) implies ((Following (s,n)) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a )
assume A3: a in dom (the_arity_of g) ; ::_thesis: ((Following (s,n)) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a
then  (the_arity_of g) . a in rng (the_arity_of g) by FUNCT_1:def_3;
then A4: s is_stable_at (the_arity_of g) . a by A1;
 ( ((Following (s,n)) * (the_arity_of g)) . a = (Following (s,n)) . ((the_arity_of g) . a) & (s * (the_arity_of g)) . a = s . ((the_arity_of g) . a) ) by A3, FUNCT_1:13;
hence  ((Following (s,n)) * (the_arity_of g)) . a = (s * (the_arity_of g)) . a by A4, Def9; ::_thesis: verum
end;
A5: rng (the_arity_of g) 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)) * (the_arity_of g)) = dom (the_arity_of g) by A5, RELAT_1:27;
 dom s = the carrier of S by CIRCUIT1:3;
then  dom (s * (the_arity_of g)) = dom (the_arity_of g) by A5, RELAT_1:27;
then A7: (Following (s,n)) * (the_arity_of g) = s * (the_arity_of g) 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)) * (the_arity_of g)) by Th10
.= (Following s) . (the_result_sort_of g) by A7, Th10 ; ::_thesis: verum
end;

begin

theorem Th20: :: FACIRC_1:20
for S1, S2 being non empty ManySortedSign
for 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 ; ::_thesis: for v being Vertex of S1 holds
( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) )
let v be Vertex of S1; ::_thesis: ( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* 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_3; ::_thesis: verum
end;

theorem Th21: :: FACIRC_1:21
for S1, S2 being non empty unsplit gate`1=arity 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 non empty unsplit gate`1=arity ManySortedSign ; ::_thesis: for x being set st x in InnerVertices S1 holds
( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) )
 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  for x being set st x in InnerVertices S1 holds
( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: FACIRC_1:22
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 ; ::_thesis: for x being set st x in InnerVertices S2 holds
x in InnerVertices (S1 +* S2)
set R1 = the ResultSort of S1;
set R2 = the ResultSort of S2;
 InnerVertices (S1 +* S2) = rng ( the ResultSort of S1 +* the ResultSort of S2) by CIRCCOMB:def_2;
then  InnerVertices S2 c= InnerVertices (S1 +* S2) by FUNCT_4:18;
hence  for x being set st x in InnerVertices S2 holds
x in InnerVertices (S1 +* S2) ; ::_thesis: verum
end;

theorem :: FACIRC_1:23
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds S1 +* S2 = S2 +* S1 by CIRCCOMB:5, CIRCCOMB:47;

theorem :: FACIRC_1:24
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2 holds A1 +* A2 = A2 +* A1 by CIRCCOMB:22, CIRCCOMB:60;

theorem Th25: :: FACIRC_1:25
for S1, S2, S3 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being Boolean Circuit of S1
for 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 non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: for A1 being Boolean Circuit of S1
for A2 being Boolean Circuit of S2
for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A1 be Boolean Circuit of S1; ::_thesis: for A2 being Boolean Circuit of S2
for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A2 be Boolean Circuit of S2; ::_thesis: for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
let A3 be Boolean Circuit of S3; ::_thesis: (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
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  (A1 +* A2) +* A3 = A1 +* (A2 +* A3) by A1, CIRCCOMB:23; ::_thesis: verum
end;

theorem Th26: :: FACIRC_1:26
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being non-empty gate`2=den Boolean Circuit of S1
for A2 being non-empty gate`2=den Boolean 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 non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: for A1 being non-empty gate`2=den Boolean Circuit of S1
for A2 being non-empty gate`2=den Boolean 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 )
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: for A2 being non-empty gate`2=den Boolean 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 )
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: 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 )
let s be State of (A1 +* A2); ::_thesis: ( s | the carrier of S1 is State of A1 & s | the carrier of S2 is State of A2 )
 the Sorts of A1 tolerates the Sorts of A2 by CIRCCOMB:59;
hence  ( s | the carrier of S1 is State of A1 & s | the carrier of S2 is State of A2 ) by CIRCCOMB:26; ::_thesis: verum
end;

theorem Th27: :: FACIRC_1:27
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2)
proof
let S1, S2 be non empty unsplit gate`1=arity ManySortedSign ; ::_thesis: InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2)
 S1 tolerates S2 by CIRCCOMB:47;
hence  InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2) by CIRCCOMB:11; ::_thesis: verum
end;

theorem Th28: :: FACIRC_1:28
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for 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 non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: ( InnerVertices S2 misses InputVertices S1 implies for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
(Following s) | the carrier of S1 = Following s1 )
assume A1: InnerVertices S2 misses InputVertices S1 ; ::_thesis: for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
(Following s) | the carrier of S1 = Following s1
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
(Following s) | the carrier of S1 = Following s1
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
(Following s) | the carrier of S1 = Following s1
let s be State of (A1 +* A2); ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
(Following s) | the carrier of S1 = Following s1
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 implies (Following s) | the carrier of S1 = Following s1 )
assume A2: s1 = s | the carrier of S1 ; ::_thesis: (Following s) | the carrier of S1 = Following 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, CIRCCOMB:60, CIRCUIT1:3;
hence  (Following s) | the carrier of S1 = Following s1 by FUNCT_4:23; ::_thesis: verum
end;

theorem Th29: :: FACIRC_1:29
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
proof
let S1, S2 be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: ( InnerVertices S1 misses InputVertices S2 implies for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2 )
assume A1: InnerVertices S1 misses InputVertices S2 ; ::_thesis: for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let s be State of (A1 +* A2); ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 implies (Following s) | the carrier of S2 = Following s2 )
assume A2: s2 = s | the carrier of S2 ; ::_thesis: (Following s) | the carrier of S2 = Following 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, CIRCCOMB:60, CIRCUIT1:3;
hence  (Following s) | the carrier of S2 = Following s2 by FUNCT_4:23; ::_thesis: verum
end;

theorem Th30: :: FACIRC_1:30
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
proof
let S1, S2 be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: ( InnerVertices S2 misses InputVertices S1 implies for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A1: InnerVertices S2 misses InputVertices S1 ; ::_thesis: for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let s be State of (A1 +* A2); ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 implies for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A2: s1 = s | the carrier of S1 ; ::_thesis: for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
defpred S1[ Nat] means (Following (s,$1)) | the carrier of S1 = Following (s1,$1);
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: (Following (s,n)) | the carrier of S1 = Following (s1,n) ; ::_thesis: S1[n + 1]
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 ; ::_thesis: verum
end;
 Following (s,0) = s by Th11;
then A5: S1[ 0 ] by A2, Th11;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A5, A3); ::_thesis: verum
end;

theorem Th31: :: FACIRC_1:31
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
proof
let S1, S2 be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: ( InnerVertices S1 misses InputVertices S2 implies for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume A1: InnerVertices S1 misses InputVertices S2 ; ::_thesis: for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s be State of (A1 +* A2); ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 implies for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume A2: s2 = s | the carrier of S2 ; ::_thesis: for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
defpred S1[ Nat] means (Following (s,$1)) | the carrier of S2 = Following (s2,$1);
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: (Following (s,n)) | the carrier of S2 = Following (s2,n) ; ::_thesis: S1[n + 1]
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 ; ::_thesis: verum
end;
 Following (s,0) = s by Th11;
then A5: S1[ 0 ] by A2, Th11;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A5, A3); ::_thesis: verum
end;

theorem Th32: :: FACIRC_1:32
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
proof
let S1, S2 be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: ( InnerVertices S2 misses InputVertices S1 implies for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v )
assume A1: InnerVertices S2 misses InputVertices S1 ; ::_thesis: for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let s be State of (A1 +* A2); ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 implies for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v )
assume A2: s1 = s | the carrier of S1 ; ::_thesis: for v being set st v in the carrier of S1 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let v be set ; ::_thesis: ( v in the carrier of S1 implies for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v )
assume A3: v in the carrier of S1 ; ::_thesis: for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let n be Nat; ::_thesis: (Following (s,n)) . v = (Following (s1,n)) . v
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  (Following (s,n)) . v = (Following (s1,n)) . v by A3, A4, FUNCT_1:47; ::_thesis: verum
end;

theorem Th33: :: FACIRC_1:33
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s2,n)) . v
proof
let S1, S2 be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: ( InnerVertices S1 misses InputVertices S2 implies for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s2,n)) . v )
assume A1: InnerVertices S1 misses InputVertices S2 ; ::_thesis: for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s2,n)) . v
let A1 be gate`2=den Boolean Circuit of S1; ::_thesis: for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s2,n)) . v
let A2 be gate`2=den Boolean Circuit of S2; ::_thesis: for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s2,n)) . v
let s be State of (A1 +* A2); ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s2,n)) . v
let s1 be State of A2; ::_thesis: ( s1 = s | the carrier of S2 implies for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v )
assume A2: s1 = s | the carrier of S2 ; ::_thesis: for v being set st v in the carrier of S2 holds
for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let v be set ; ::_thesis: ( v in the carrier of S2 implies for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v )
assume A3: v in the carrier of S2 ; ::_thesis: for n being Nat holds (Following (s,n)) . v = (Following (s1,n)) . v
let n be Nat; ::_thesis: (Following (s,n)) . v = (Following (s1,n)) . v
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  (Following (s,n)) . v = (Following (s1,n)) . v by A3, A4, FUNCT_1:47; ::_thesis: verum
end;

registration
let S be non empty non void gate`2=den ManySortedSign ;
let g be Gate of S;
clusterg `2  ->  Relation-like Function-like ;
coherence
 ( g `2 is Function-like & g `2 is Relation-like )
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, CIRCCOMB:def_10
.= the Charact of A . g
.= Den (g,A) by MSUALG_1:def_6 ;
hence  ( g `2 is Function-like & g `2 is Relation-like ) ; ::_thesis: verum
end;
end;

theorem Th34: :: FACIRC_1:34
for S being non empty non void Circuit-like gate`2=den ManySortedSign
for A being non-empty Circuit of S st A is gate`2=den holds
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
proof
let S be non empty non void Circuit-like gate`2=den ManySortedSign ; ::_thesis: for A being non-empty Circuit of S st A is gate`2=den holds
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
let A be non-empty Circuit of S; ::_thesis: ( A is gate`2=den implies for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g)) )
assume A1: for g being set st g in the carrier' of S holds
g = [(g `1),( the Charact of A . g)] ; :: according to CIRCCOMB:def_10 ::_thesis: for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
let s be State of A; ::_thesis: for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
let g be Gate of S; ::_thesis: (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g))
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: the_result_sort_of g in InnerVertices S by MSUALG_1:def_2;
then  ( g depends_on_in s = s * (the_arity_of g) & action_at (the_result_sort_of g) = g ) by CIRCUIT1:def_3, MSAFREE2:def_7;
hence  (Following s) . (the_result_sort_of g) = (g `2) . (s * (the_arity_of g)) by A2, A3, CIRCUIT2:def_5; ::_thesis: verum
end;

theorem Th35: :: FACIRC_1:35
for S being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
proof
let S be non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let A be non-empty gate`2=den Boolean Circuit of S; ::_thesis: for s being State of A
for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let s be State of A; ::_thesis: for p being FinSequence
for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let p be FinSequence; ::_thesis: for f being Function st [p,f] in the carrier' of S holds
(Following s) . [p,f] = f . (s * p)
let f be Function; ::_thesis: ( [p,f] in the carrier' of S implies (Following s) . [p,f] = f . (s * p) )
assume  [p,f] in the carrier' of S ; ::_thesis: (Following s) . [p,f] = f . (s * p)
then reconsider g = [p,f] as Gate of S ;
A1: ( g `1 = p & g `2 = f ) by MCART_1:7;
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  (Following s) . [p,f] = f . (s * p) by A1, A2, Th34; ::_thesis: verum
end;

theorem :: FACIRC_1:36
for S being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for 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 non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ::_thesis: for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for 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]
let A be non-empty gate`2=den Boolean Circuit of S; ::_thesis: for s being State of A
for p being FinSequence
for 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]
let s be State of A; ::_thesis: for p being FinSequence
for 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]
let p be FinSequence; ::_thesis: for 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]
let f be Function; ::_thesis: ( [p,f] in the carrier' of S & ( for x being set st x in rng p holds
s is_stable_at x ) implies Following s is_stable_at [p,f] )
assume  [p,f] in the carrier' of S ; ::_thesis: ( ex x being set st
( x in rng p & not s is_stable_at x ) or Following s is_stable_at [p,f] )
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 by MCART_1:7 ;
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 ; ::_thesis: Following s is_stable_at [p,f]
hence  Following s is_stable_at [p,f] by A1, A2, Th19; ::_thesis: verum
end;

theorem Th37: :: FACIRC_1:37
for S being non empty unsplit ManySortedSign holds InnerVertices S = the carrier' of S
proof
let S be non empty unsplit ManySortedSign ; ::_thesis: InnerVertices S = the carrier' of S
 the ResultSort of S = id the carrier' of S by CIRCCOMB:def_7;
hence  InnerVertices S = the carrier' of S by RELAT_1:45; ::_thesis: verum
end;

begin

theorem Th38: :: FACIRC_1:38
for f being set
for p being FinSequence holds InnerVertices (1GateCircStr (p,f)) is Relation
proof
let f be set ; ::_thesis: for p being FinSequence holds InnerVertices (1GateCircStr (p,f)) is Relation
let p be FinSequence; ::_thesis: InnerVertices (1GateCircStr (p,f)) is Relation
 InnerVertices (1GateCircStr (p,f)) = {[p,f]} by CIRCCOMB:42;
hence  InnerVertices (1GateCircStr (p,f)) is Relation ; ::_thesis: verum
end;

theorem :: FACIRC_1:39
for f being set
for p being nonpair-yielding FinSequence holds InputVertices (1GateCircStr (p,f)) is without_pairs
proof
let f be set ; ::_thesis: for p being nonpair-yielding FinSequence holds InputVertices (1GateCircStr (p,f)) is without_pairs
let p be nonpair-yielding FinSequence; ::_thesis: InputVertices (1GateCircStr (p,f)) is without_pairs
 InputVertices (1GateCircStr (p,f)) = rng p by CIRCCOMB:42;
hence  InputVertices (1GateCircStr (p,f)) is without_pairs ; ::_thesis: verum
end;

theorem Th40: :: FACIRC_1:40
for f, x, y being set holds InputVertices (1GateCircStr (<*x,y*>,f)) = {x,y}
proof
let f be set ; ::_thesis: for x, y being set holds InputVertices (1GateCircStr (<*x,y*>,f)) = {x,y}
let x, y be set ; ::_thesis: InputVertices (1GateCircStr (<*x,y*>,f)) = {x,y}
set p = <*x,y*>;
thus  InputVertices (1GateCircStr (<*x,y*>,f)) = rng <*x,y*> by CIRCCOMB:42
.= {x,y} by FINSEQ_2:127 ; ::_thesis: verum
end;

theorem Th41: :: FACIRC_1:41
for f being set
for x, y being non pair set holds InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs
proof
let f be set ; ::_thesis: for x, y being non pair set holds InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs
let x, y be non pair set ; ::_thesis: InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs
set p = <*x,y*>;
let z be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not z in InputVertices (1GateCircStr (<*x,y*>,f))
assume A1: z in InputVertices (1GateCircStr (<*x,y*>,f)) ; ::_thesis: contradiction
 InputVertices (1GateCircStr (<*x,y*>,f)) = {x,y} by Th40;
hence  contradiction by A1, TARSKI:def_2; ::_thesis: verum
end;

theorem Th42: :: FACIRC_1:42
for f, x, y, z being set holds InputVertices (1GateCircStr (<*x,y,z*>,f)) = {x,y,z}
proof
let f be set ; ::_thesis: for x, y, z being set holds InputVertices (1GateCircStr (<*x,y,z*>,f)) = {x,y,z}
let x, y, z be set ; ::_thesis: InputVertices (1GateCircStr (<*x,y,z*>,f)) = {x,y,z}
set p = <*x,y,z*>;
thus  InputVertices (1GateCircStr (<*x,y,z*>,f)) = rng <*x,y,z*> by CIRCCOMB:42
.= {x,y,z} by FINSEQ_2:128 ; ::_thesis: verum
end;

theorem Th43: :: FACIRC_1:43
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 ; ::_thesis: ( 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)) )
set p = <*x,y*>;
 x in {x,y} by TARSKI:def_2;
then A1: x in rng <*x,y*> by FINSEQ_2:127;
 y in {x,y} by TARSKI:def_2;
then A2: y in rng <*x,y*> by FINSEQ_2:127;
 ( the carrier of (1GateCircStr (<*x,y*>,f)) = (rng <*x,y*>) \/ {[<*x,y*>,f]} & [<*x,y*>,f] in {[<*x,y*>,f]} ) by CIRCCOMB:def_6, TARSKI:def_1;
hence  ( 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)) ) by A1, A2, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th44: :: FACIRC_1:44
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 ; ::_thesis: ( 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)) )
set p = <*x,y,z*>;
set A = the carrier of (1GateCircStr (<*x,y,z*>,f));
 y in {x,y,z} by ENUMSET1:def_1;
then A1: y in rng <*x,y,z*> by FINSEQ_2:128;
 z in {x,y,z} by ENUMSET1:def_1;
then A2: z in rng <*x,y,z*> by FINSEQ_2:128;
 x in {x,y,z} by ENUMSET1:def_1;
then  ( the carrier of (1GateCircStr (<*x,y,z*>,f)) = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} & x in rng <*x,y,z*> ) by CIRCCOMB:def_6, FINSEQ_2:128;
hence  ( 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)) ) by A1, A2, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: FACIRC_1:45
for f, x being set
for 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 ; ::_thesis: for 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)) ) )
let p be FinSequence; ::_thesis: ( 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)) ) )
set A = the carrier of (1GateCircStr (p,f,x));
 ( the carrier of (1GateCircStr (p,f,x)) = (rng p) \/ {x} & x in {x} ) by CIRCCOMB:def_5, TARSKI:def_1;
hence  ( 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)) ) ) by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: FACIRC_1:46
for f, x being set
for p being FinSequence holds
( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )
proof
let f, x be set ; ::_thesis: for p being FinSequence holds
( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )
let p be FinSequence; ::_thesis: ( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )
set S = 1GateCircStr (p,f,x);
thus  1GateCircStr (p,f,x) is gate`1=arity ::_thesis: 1GateCircStr (p,f,x) is Circuit-like
proof
let g be set ; :: according to CIRCCOMB:def_8 ::_thesis: ( not g in the carrier' of (1GateCircStr (p,f,x)) or g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)] )
assume  g in the carrier' of (1GateCircStr (p,f,x)) ; ::_thesis: g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)]
then  g in {[p,f]} by CIRCCOMB:def_5;
then A1: g = [p,f] by TARSKI:def_1;
 [p,f] `2 = f ;
hence  g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)] by A1, CIRCCOMB:def_5; ::_thesis: verum
end;
thus  1GateCircStr (p,f,x) is Circuit-like ::_thesis: verum
proof
let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def_6 ::_thesis: ( not S9 = 1GateCircStr (p,f,x) or for b1, b2 being Element of the carrier' of S9 holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 ) )
assume A2: S9 = 1GateCircStr (p,f,x) ; ::_thesis: for b1, b2 being Element of the carrier' of S9 holds
( not the_result_sort_of b1 = the_result_sort_of b2 or b1 = b2 )
let o1, o2 be OperSymbol of S9; ::_thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
 o1 = [p,f] by A2, CIRCCOMB:37;
hence  ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) by A2, CIRCCOMB:37; ::_thesis: verum
end;
end;

theorem Th47: :: FACIRC_1:47
for p being FinSequence
for f being set holds [p,f] in InnerVertices (1GateCircStr (p,f))
proof
let p be FinSequence; ::_thesis: for f being set holds [p,f] in InnerVertices (1GateCircStr (p,f))
let f be set ; ::_thesis: [p,f] in InnerVertices (1GateCircStr (p,f))
 InnerVertices (1GateCircStr (p,f)) = {[p,f]} by CIRCCOMB:42;
hence  [p,f] in InnerVertices (1GateCircStr (p,f)) by TARSKI:def_1; ::_thesis: verum
end;

definition
let x, y be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
func 1GateCircuit (x,y,f) ->  strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y*>,f) equals :: FACIRC_1:def 10
 1GateCircuit (<*x,y*>,f);
coherence
 1GateCircuit (<*x,y*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y*>,f) by CIRCCOMB:61;
end;

:: deftheorem  defines 1GateCircuit FACIRC_1:def_10_:_
 for x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 1GateCircuit (x,y,f) = 1GateCircuit (<*x,y*>,f);


theorem Th48: :: FACIRC_1:48
for x, y being set
for X being non empty finite set
for 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, y be set ; ::_thesis: for X being non empty finite set
for 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 )
let X be non empty finite set ; ::_thesis: for 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 )
let f be Function of (2 -tuples_on X),X; ::_thesis: 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 )
let s be State of (1GateCircuit (<*x,y*>,f)); ::_thesis: ( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )
set p = <*x,y*>;
 dom s = the carrier of (1GateCircStr (<*x,y*>,f)) by CIRCUIT1:3;
then A1: dom s = (rng <*x,y*>) \/ {[<*x,y*>,f]} by CIRCCOMB:def_6;
 y in {x,y} by TARSKI:def_2;
then  y in rng <*x,y*> 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 <*x,y*> 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 ; ::_thesis: ( (Following s) . x = s . x & (Following s) . y = s . y )
reconsider x = x, y = y as Vertex of (1GateCircStr (<*x,y*>,f)) by Th43;
InputVertices (1GateCircStr (<*x,y*>,f)) = rng <*x,y*> by CIRCCOMB:42
.= {x,y} by FINSEQ_2:127 ;
then  ( x in InputVertices (1GateCircStr (<*x,y*>,f)) & y in InputVertices (1GateCircStr (<*x,y*>,f)) ) by TARSKI:def_2;
hence  ( (Following s) . x = s . x & (Following s) . y = s . y ) by CIRCUIT2:def_5; ::_thesis: verum
end;

theorem Th49: :: FACIRC_1:49
for x, y being set
for X being non empty finite set
for 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, y be set ; ::_thesis: for X being non empty finite set
for f being Function of (2 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y*>,f)) holds Following s is stable
let X be non empty finite set ; ::_thesis: for f being Function of (2 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y*>,f)) holds Following s is stable
let f be Function of (2 -tuples_on X),X; ::_thesis: for s being State of (1GateCircuit (<*x,y*>,f)) holds Following s is stable
set S = 1GateCircStr (<*x,y*>,f);
let s be State of (1GateCircuit (<*x,y*>,f)); ::_thesis: Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
set p = <*x,y*>;
A1: the carrier of (1GateCircStr (<*x,y*>,f)) = (rng <*x,y*>) \/ {[<*x,y*>,f]} by CIRCCOMB:def_6
.= {x,y} \/ {[<*x,y*>,f]} by FINSEQ_2:127 ;
A2: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(1GateCircStr_(<*x,y*>,f))_holds_
(Following_(Following_s))_._a_=_(Following_s)_._a
let a be set ; ::_thesis: ( a in the carrier of (1GateCircStr (<*x,y*>,f)) implies (Following (Following s)) . a = (Following s) . a )
A3: (Following (Following s)) . [<*x,y*>,f] = f . <*((Following s) . x),((Following s) . y)*> by Th48;
assume  a in the carrier of (1GateCircStr (<*x,y*>,f)) ; ::_thesis: (Following (Following s)) . a = (Following s) . a
then  ( a in {x,y} or a in {[<*x,y*>,f]} ) by A1, XBOOLE_0:def_3;
then A4: ( a = x or a = y or a = [<*x,y*>,f] ) by TARSKI:def_1, TARSKI:def_2;
 ( (Following s) . x = s . x & (Following s) . y = s . y ) by Th48;
hence  (Following (Following s)) . a = (Following s) . a by A4, A3, Th48; ::_thesis: verum
end;
 ( dom (Following s) = the carrier of (1GateCircStr (<*x,y*>,f)) & dom (Following (Following s)) = the carrier of (1GateCircStr (<*x,y*>,f)) ) by CIRCUIT1:3;
hence  Following s = Following (Following s) by A2, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem :: FACIRC_1:50
for x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
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 :: FACIRC_1:51
for x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (1GateCircuit (x,y,f)) holds Following s is stable by Th49;

definition
let x, y, z be set ;
let f be Function of (3 -tuples_on BOOLEAN),BOOLEAN;
func 1GateCircuit (x,y,z,f) ->  strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y,z*>,f) equals :: FACIRC_1:def 11
 1GateCircuit (<*x,y,z*>,f);
coherence
 1GateCircuit (<*x,y,z*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y,z*>,f) by CIRCCOMB:61;
end;

:: deftheorem  defines 1GateCircuit FACIRC_1:def_11_:_
 for x, y, z being set
for f being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds 1GateCircuit (x,y,z,f) = 1GateCircuit (<*x,y,z*>,f);

theorem Th52: :: FACIRC_1:52
for x, y, z being set
for X being non empty finite set
for 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, y, z be set ; ::_thesis: for X being non empty finite set
for 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 )
let X be non empty finite set ; ::_thesis: for 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 )
let f be Function of (3 -tuples_on X),X; ::_thesis: 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 )
let s be State of (1GateCircuit (<*x,y,z*>,f)); ::_thesis: ( (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 )
set p = <*x,y,z*>;
 dom s = the carrier of (1GateCircStr (<*x,y,z*>,f)) by CIRCUIT1:3;
then A1: dom s = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} by CIRCCOMB:def_6;
 y in {x,y,z} by ENUMSET1:def_1;
then  y in rng <*x,y,z*> 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 <*x,y,z*> 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 <*x,y,z*> by FINSEQ_2:128;
then A4: z in dom s by A1, XBOOLE_0:def_3;
thus (Following s) . [<*x,y,z*>,f] = f . (s * <*x,y,z*>) by CIRCCOMB:56
.= f . <*(s . x),(s . y),(s . z)*> by A3, A2, A4, FINSEQ_2:126 ; ::_thesis: ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
reconsider x = x, y = y, z = z as Vertex of (1GateCircStr (<*x,y,z*>,f)) by Th44;
A5: InputVertices (1GateCircStr (<*x,y,z*>,f)) = rng <*x,y,z*> by CIRCCOMB:42
.= {x,y,z} by FINSEQ_2:128 ;
then A6: z in InputVertices (1GateCircStr (<*x,y,z*>,f)) by ENUMSET1:def_1;
 ( x in InputVertices (1GateCircStr (<*x,y,z*>,f)) & y in InputVertices (1GateCircStr (<*x,y,z*>,f)) ) by A5, ENUMSET1:def_1;
hence  ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z ) by A6, CIRCUIT2:def_5; ::_thesis: verum
end;

theorem Th53: :: FACIRC_1:53
for x, y, z being set
for X being non empty finite set
for 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, y, z be set ; ::_thesis: for X being non empty finite set
for f being Function of (3 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable
let X be non empty finite set ; ::_thesis: for f being Function of (3 -tuples_on X),X
for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable
let f be Function of (3 -tuples_on X),X; ::_thesis: for s being State of (1GateCircuit (<*x,y,z*>,f)) holds Following s is stable
set p = <*x,y,z*>;
set S = 1GateCircStr (<*x,y,z*>,f);
let s be State of (1GateCircuit (<*x,y,z*>,f)); ::_thesis: Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1: the carrier of (1GateCircStr (<*x,y,z*>,f)) = (rng <*x,y,z*>) \/ {[<*x,y,z*>,f]} by CIRCCOMB:def_6
.= {x,y,z} \/ {[<*x,y,z*>,f]} by FINSEQ_2:128 ;
A2: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(1GateCircStr_(<*x,y,z*>,f))_holds_
(Following_(Following_s))_._a_=_(Following_s)_._a
let a be set ; ::_thesis: ( a in the carrier of (1GateCircStr (<*x,y,z*>,f)) implies (Following (Following s)) . a = (Following s) . a )
A3: ( (Following s) . z = s . z & (Following (Following s)) . [<*x,y,z*>,f] = f . <*((Following s) . x),((Following s) . y),((Following s) . z)*> ) by Th52;
assume  a in the carrier of (1GateCircStr (<*x,y,z*>,f)) ; ::_thesis: (Following (Following s)) . a = (Following s) . a
then  ( a in {x,y,z} or a in {[<*x,y,z*>,f]} ) by A1, XBOOLE_0:def_3;
then A4: ( a = x or a = y or a = z or a = [<*x,y,z*>,f] ) by ENUMSET1:def_1, TARSKI:def_1;
 ( (Following s) . x = s . x & (Following s) . y = s . y ) by Th52;
hence  (Following (Following s)) . a = (Following s) . a by A4, A3, Th52; ::_thesis: verum
end;
 ( dom (Following s) = the carrier of (1GateCircStr (<*x,y,z*>,f)) & dom (Following (Following s)) = the carrier of (1GateCircStr (<*x,y,z*>,f)) ) by CIRCUIT1:3;
hence  Following s = Following (Following s) by A2, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem :: FACIRC_1:54
for x, y, z being set
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 :: FACIRC_1:55
for x, y, z being set
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

definition
let x, y, c be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
func 2GatesCircStr (x,y,c,f) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign  equals :: FACIRC_1:def 12
(1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f));
correctness
coherence
(1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;

:: deftheorem  defines 2GatesCircStr FACIRC_1:def_12_:_
 for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircStr (x,y,c,f) = (1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f));

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 :: FACIRC_1:def 13
[<*[<*x,y*>,f],c*>,f];
coherence
 [<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr (x,y,c,f))
proof
set p = <*[<*x,y*>,f],c*>;
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
 [<*[<*x,y*>,f],c*>,f] in InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by Th47;
hence  [<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr (x,y,c,f)) by Th21; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines 2GatesCircOutput FACIRC_1:def_13_:_
 for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircOutput (x,y,c,f) = [<*[<*x,y*>,f],c*>,f];

registration
let x, y, c be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
cluster 2GatesCircOutput (x,y,c,f) ->  pair ;
coherence
 2GatesCircOutput (x,y,c,f) is pair ;
end;

theorem Th56: :: FACIRC_1:56
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))}
proof
let x, y, c be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))}
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))}
set p = <*[<*x,y*>,f],c*>;
set S1 = 1GateCircStr (<*x,y*>,f);
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
set S = 2GatesCircStr (x,y,c,f);
 1GateCircStr (<*x,y*>,f) tolerates 1GateCircStr (<*[<*x,y*>,f],c*>,f) by CIRCCOMB:43;
hence  InnerVertices (2GatesCircStr (x,y,c,f)) = (InnerVertices (1GateCircStr (<*x,y*>,f))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f))) by CIRCCOMB:11
.= {[<*x,y*>,f]} \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f))) by CIRCCOMB:42
.= {[<*x,y*>,f]} \/ {[<*[<*x,y*>,f],c*>,f]} by CIRCCOMB:42
.= {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by ENUMSET1:1 ;
::_thesis: verum
end;

theorem Th57: :: FACIRC_1:57
for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st c <> [<*x,y*>,f] holds
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
proof
let c, x, y be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st c <> [<*x,y*>,f] holds
InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: ( c <> [<*x,y*>,f] implies InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} )
assume A1: c <> [<*x,y*>,f] ; ::_thesis: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}
set S = 2GatesCircStr (x,y,c,f);
set S1 = 1GateCircStr (<*x,y*>,f);
set p = <*[<*x,y*>,f],c*>;
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
set R = the ResultSort of (2GatesCircStr (x,y,c,f));
A2: the carrier of (2GatesCircStr (x,y,c,f)) = the carrier of (1GateCircStr (<*x,y*>,f)) \/ the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:def_2;
A3: rng <*x,y*> = {x,y} by FINSEQ_2:127;
then A4: the carrier of (1GateCircStr (<*x,y*>,f)) = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def_6;
A5: rng the ResultSort of (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56
.= {[<*x,y*>,f],[<*[<*x,y*>,f],c*>,f]} ;
A6: rng <*[<*x,y*>,f],c*> = {[<*x,y*>,f],c} by FINSEQ_2:127;
then A7: the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) = {[<*x,y*>,f],c} \/ {[<*[<*x,y*>,f],c*>,f]} by CIRCCOMB:def_6;
thus  InputVertices (2GatesCircStr (x,y,c,f)) c= {x,y,c} :: according to XBOOLE_0:def_10 ::_thesis: {x,y,c} c= InputVertices (2GatesCircStr (x,y,c,f))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in InputVertices (2GatesCircStr (x,y,c,f)) or z in {x,y,c} )
assume A8: z in InputVertices (2GatesCircStr (x,y,c,f)) ; ::_thesis: z in {x,y,c}
then  ( z in the carrier of (1GateCircStr (<*x,y*>,f)) or z in the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) 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 {[<*[<*x,y*>,f],c*>,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 = [<*[<*x,y*>,f],c*>,f] ) by TARSKI:def_1, TARSKI:def_2;
 not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A8, XBOOLE_0:def_5;
hence  z in {x,y,c} by A5, A9, ENUMSET1:def_1, TARSKI:def_2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y,c} or z in InputVertices (2GatesCircStr (x,y,c,f)) )
assume  z in {x,y,c} ; ::_thesis: z in InputVertices (2GatesCircStr (x,y,c,f))
then A10: ( z = x or z = y or z = c ) by ENUMSET1:def_1;
then  ( z in {x,y} or z in rng <*[<*x,y*>,f],c*> ) by A6, TARSKI:def_2;
then  ( z in InputVertices (1GateCircStr (<*x,y*>,f)) or z in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by A3, CIRCCOMB:42;
then A11: z in the carrier of (2GatesCircStr (x,y,c,f)) by A2, XBOOLE_0:def_3;
 ( ( z in {x,y} & [<*x,y*>,f] in rng <*[<*x,y*>,f],c*> ) or z in {c} ) by A6, A10, TARSKI:def_1, TARSKI:def_2;
then A12: ( ( the_rank_of z in the_rank_of [<*x,y*>,f] & the_rank_of [<*x,y*>,f] in the_rank_of [<*[<*x,y*>,f],c*>,f] ) or ( z = c & c in rng <*[<*x,y*>,f],c*> ) ) by A3, A6, CLASSES1:82, TARSKI:def_1, TARSKI:def_2;
then  the_rank_of z in the_rank_of [<*[<*x,y*>,f],c*>,f] by CLASSES1:82, ORDINAL1:10;
then A13: z <> [<*[<*x,y*>,f],c*>,f] ;
 z <> [<*x,y*>,f] by A1, A12;
then  not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A5, A13, TARSKI:def_2;
hence  z in InputVertices (2GatesCircStr (x,y,c,f)) by A11, XBOOLE_0:def_5; ::_thesis: verum
end;

definition
let x, y, c be set ;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;
func 2GatesCircuit (x,y,c,f) ->  strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,f) equals :: FACIRC_1:def 14
(1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f));
coherence
 (1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f)) is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,f) ;
end;

:: deftheorem  defines 2GatesCircuit FACIRC_1:def_14_:_
 for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds 2GatesCircuit (x,y,c,f) = (1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f));

theorem Th58: :: FACIRC_1:58
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) is Relation
proof
let x, y, c be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) is Relation
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: InnerVertices (2GatesCircStr (x,y,c,f)) is Relation
 InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;
hence  InnerVertices (2GatesCircStr (x,y,c,f)) is Relation ; ::_thesis: verum
end;

theorem Th59: :: FACIRC_1:59
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for x, y, c being non pair set holds InputVertices (2GatesCircStr (x,y,c,f)) is without_pairs
proof
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: for x, y, c being non pair set holds InputVertices (2GatesCircStr (x,y,c,f)) is without_pairs
let x, y, c be non pair set ; ::_thesis: InputVertices (2GatesCircStr (x,y,c,f)) is without_pairs
 InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} by Th57;
hence  InputVertices (2GatesCircStr (x,y,c,f)) is without_pairs ; ::_thesis: verum
end;

theorem Th60: :: FACIRC_1:60
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( 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
let x, y, c be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( 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)) )
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: ( 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)) )
set S1 = 1GateCircStr (<*x,y*>,f);
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
A1: c in the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by Th43;
 ( x in the carrier of (1GateCircStr (<*x,y*>,f)) & y in the carrier of (1GateCircStr (<*x,y*>,f)) ) by Th43;
hence  ( 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)) ) by A1, Th20; ::_thesis: verum
end;

theorem :: FACIRC_1:61
for x, y, c being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( [<*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
let x, y, c be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( [<*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)) )
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: ( [<*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)) )
set S1 = 1GateCircStr (<*x,y*>,f);
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
 ( [<*x,y*>,f] in the carrier of (1GateCircStr (<*x,y*>,f)) & [<*[<*x,y*>,f],c*>,f] in the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by Th43;
hence  ( [<*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)) ) by Th20; ::_thesis: verum
end;

definition
let S be non empty non void unsplit ManySortedSign ;
let A be Boolean Circuit of S;
let s be State of A;
let v be Vertex of S;
:: original: .
redefine funcs . v ->  Element of BOOLEAN ;
coherence
 s . v is Element of BOOLEAN
proof
 s . v in the Sorts of A . v by CIRCUIT1:4;
hence  s . v is Element of BOOLEAN by CIRCCOMB:def_14; ::_thesis: verum
end;
end;

 Lm1:  for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (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
let c, x, y be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (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 )
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (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 )
let s be State of (2GatesCircuit (x,y,c,f)); ::_thesis: ( 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 ) )
set S1 = 1GateCircStr (<*x,y*>,f);
set A1 = 1GateCircuit (x,y,f);
reconsider vx = x, vy = y as Vertex of (1GateCircStr (<*x,y*>,f)) by Th43;
reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;
set p = <*[<*x,y*>,f],c*>;
set xyf = [<*x,y*>,f];
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
set A2 = 1GateCircuit ([<*x,y*>,f],c,f);
set S = 2GatesCircStr (x,y,c,f);
A1: dom s1 = the carrier of (1GateCircStr (<*x,y*>,f)) by CIRCUIT1:3;
reconsider v2 = [<*[<*x,y*>,f],c*>,f] as Element of InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by Th47;
 InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;
then reconsider xyf = [<*x,y*>,f] as Element of InnerVertices (2GatesCircStr (x,y,c,f)) by TARSKI:def_2;
A2: rng <*[<*x,y*>,f],c*> = {xyf,c} by FINSEQ_2:127;
then  c in rng <*[<*x,y*>,f],c*> by TARSKI:def_2;
then A3: c in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;
 xyf in rng <*[<*x,y*>,f],c*> by A2, TARSKI:def_2;
then  xyf in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;
then reconsider xyf9 = xyf, c9 = c as Vertex of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by A3;
reconsider xyf1 = xyf as Element of InnerVertices (1GateCircStr (<*x,y*>,f)) by Th47;
reconsider s2 = s | the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) as State of (1GateCircuit ([<*x,y*>,f],c,f)) by Th26;
A4: dom s2 = the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCUIT1:3;
assume  c <> [<*x,y*>,f] ; ::_thesis: ( (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 )
then A5: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} by Th57;
then A6: c in InputVertices (2GatesCircStr (x,y,c,f)) 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 ; ::_thesis: ( (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 )
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 ; ::_thesis: ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
 ( x in InputVertices (2GatesCircStr (x,y,c,f)) & y in InputVertices (2GatesCircStr (x,y,c,f)) ) by A5, ENUMSET1:def_1;
hence  ( (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c ) by A6, CIRCUIT2:def_5; ::_thesis: verum
end;

theorem Th62: :: FACIRC_1:62
for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (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
let c, x, y be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (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 )
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
( (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 )
let s be State of (2GatesCircuit (x,y,c,f)); ::_thesis: ( 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 ) )
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 (2GatesCircStr (x,y,c,f)) by Th60;
set p = <*[<*x,y*>,f],c*>;
set xyf = [<*x,y*>,f];
set S1 = 1GateCircStr (<*x,y*>,f);
set A1 = 1GateCircuit (x,y,f);
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
set A2 = 1GateCircuit ([<*x,y*>,f],c,f);
A2: x in {x,y} by TARSKI:def_2;
assume  c <> [<*x,y*>,f] ; ::_thesis: ( (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 )
then A3: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} by Th57;
then A4: x in InputVertices (2GatesCircStr (x,y,c,f)) by ENUMSET1:def_1;
then A5: (Following s) . xx = s . x by CIRCUIT2:def_5;
 InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56;
then reconsider xyf = [<*x,y*>,f] as Element of InnerVertices (2GatesCircStr (x,y,c,f)) by TARSKI:def_2;
A6: rng <*[<*x,y*>,f],c*> = {xyf,c} by FINSEQ_2:127;
then  c in rng <*[<*x,y*>,f],c*> by TARSKI:def_2;
then A7: c in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;
 xyf in rng <*[<*x,y*>,f],c*> by A6, TARSKI:def_2;
then  xyf in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:42;
then reconsider xyf9 = xyf, c9 = c as Vertex of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by A7;
reconsider vx = x, vy = y as Vertex of (1GateCircStr (<*x,y*>,f)) by Th43;
set fs = Following s;
reconsider fs1 = (Following s) | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;
A8: y in {x,y} by TARSKI:def_2;
reconsider fs2 = (Following s) | the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) as State of (1GateCircuit ([<*x,y*>,f],c,f)) by Th26;
reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,f)) as State of (1GateCircuit (x,y,f)) by Th26;
A9: dom fs2 = the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCUIT1:3;
A10: c in InputVertices (2GatesCircStr (x,y,c,f)) 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 (1GateCircStr (<*x,y*>,f)) by Th47;
A12: dom fs1 = the carrier of (1GateCircStr (<*x,y*>,f)) by CIRCUIT1:3;
reconsider v2 = [<*[<*x,y*>,f],c*>,f] as Element of InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by Th47;
A13: xyf in InnerVertices (1GateCircStr (<*x,y*>,f)) by Th47;
A14: ( dom s1 = the carrier of (1GateCircStr (<*x,y*>,f)) & InputVertices (1GateCircStr (<*x,y*>,f)) = 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 ;
::_thesis: ( (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 )
A16: y in InputVertices (2GatesCircStr (x,y,c,f)) 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 ; ::_thesis: ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c )
 (Following (Following s)) . xx = s . x by A4, A5, CIRCUIT2:def_5;
hence  ( (Following (s,2)) . x = s . x & (Following (s,2)) . y = s . y & (Following (s,2)) . c = s . c ) by A18, A11, Th15; ::_thesis: verum
end;

theorem Th63: :: FACIRC_1:63
for c, x, y being set
for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
Following (s,2) is stable
proof
let c, x, y be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN
for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
Following (s,2) is stable
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: for s being State of (2GatesCircuit (x,y,c,f)) st c <> [<*x,y*>,f] holds
Following (s,2) is stable
let s be State of (2GatesCircuit (x,y,c,f)); ::_thesis: ( c <> [<*x,y*>,f] implies Following (s,2) is stable )
set S = 2GatesCircStr (x,y,c,f);
assume A1: c <> [<*x,y*>,f] ; ::_thesis: Following (s,2) is stable
now__::_thesis:_(_dom_(Following_(Following_(s,2)))_=_the_carrier_of_(2GatesCircStr_(x,y,c,f))_&_dom_(Following_(s,2))_=_the_carrier_of_(2GatesCircStr_(x,y,c,f))_&_(_for_a_being_set_st_a_in_the_carrier_of_(2GatesCircStr_(x,y,c,f))_holds_
(Following_(Following_(s,2)))_._a_=_(Following_(s,2))_._a_)_)
thus  ( dom (Following (Following (s,2))) = the carrier of (2GatesCircStr (x,y,c,f)) & dom (Following (s,2)) = the carrier of (2GatesCircStr (x,y,c,f)) ) by CIRCUIT1:3; ::_thesis: for a being set st a in the carrier of (2GatesCircStr (x,y,c,f)) holds
(Following (Following (s,2))) . b2 = (Following (s,2)) . b2
let a be set ; ::_thesis: ( a in the carrier of (2GatesCircStr (x,y,c,f)) implies (Following (Following (s,2))) . b1 = (Following (s,2)) . b1 )
A2: (InputVertices (2GatesCircStr (x,y,c,f))) \/ (InnerVertices (2GatesCircStr (x,y,c,f))) = the carrier of (2GatesCircStr (x,y,c,f)) by XBOOLE_1:45;
assume  a in the carrier of (2GatesCircStr (x,y,c,f)) ; ::_thesis: (Following (Following (s,2))) . b1 = (Following (s,2)) . b1
then reconsider v = a as Vertex of (2GatesCircStr (x,y,c,f)) ;
A3: InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*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 (2GatesCircStr (x,y,c,f)) = {x,y,c} by A1, Th57;
percases ( v in InputVertices (2GatesCircStr (x,y,c,f)) or v in InnerVertices (2GatesCircStr (x,y,c,f)) ) by A2, XBOOLE_0:def_3;
suppose v in InputVertices (2GatesCircStr (x,y,c,f)) ; ::_thesis: (Following (Following (s,2))) . b1 = (Following (s,2)) . b1
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; ::_thesis: verum
end;
suppose v in InnerVertices (2GatesCircStr (x,y,c,f)) ; ::_thesis: (Following (Following (s,2))) . b1 = (Following (s,2)) . b1
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; ::_thesis: verum
end;
end;
end;
hence  Following (s,2) = Following (Following (s,2)) by FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem Th64: :: FACIRC_1:64
for c, x, y being set st c <> [<*x,y*>,'xor'] holds
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
let c, x, y be set ; ::_thesis: ( 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 )
set f = 'xor' ;
assume A1: c <> [<*x,y*>,'xor'] ; ::_thesis: 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
let s be State of (2GatesCircuit (x,y,c,'xor')); ::_thesis: 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
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies (Following (s,2)) . (2GatesCircOutput (x,y,c,'xor')) = (a1 'xor' a2) 'xor' a3 )
assume  ( a1 = s . x & a2 = s . y & a3 = s . c ) ; ::_thesis: (Following (s,2)) . (2GatesCircOutput (x,y,c,'xor')) = (a1 'xor' a2) 'xor' a3
hence (Following (s,2)) . (2GatesCircOutput (x,y,c,'xor')) = 'xor' . <*('xor' . <*a1,a2*>),a3*> by A1, Th62
.= 'xor' . <*(a1 'xor' a2),a3*> by Def4
.= (a1 'xor' a2) 'xor' a3 by Def4 ;
::_thesis: verum
end;

theorem :: FACIRC_1:65
for c, x, y being set st c <> [<*x,y*>,'or'] holds
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
let c, x, y be set ; ::_thesis: ( 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 )
set f = 'or' ;
assume A1: c <> [<*x,y*>,'or'] ; ::_thesis: 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
let s be State of (2GatesCircuit (x,y,c,'or')); ::_thesis: 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
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies (Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3 )
assume  ( a1 = s . x & a2 = s . y & a3 = s . c ) ; ::_thesis: (Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = (a1 'or' a2) 'or' a3
hence (Following (s,2)) . (2GatesCircOutput (x,y,c,'or')) = 'or' . <*('or' . <*a1,a2*>),a3*> by A1, Th62
.= 'or' . <*(a1 'or' a2),a3*> by Def5
.= (a1 'or' a2) 'or' a3 by Def5 ;
::_thesis: verum
end;

theorem :: FACIRC_1:66
for c, x, y being set st c <> [<*x,y*>,'&'] holds
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
let c, x, y be set ; ::_thesis: ( 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 )
set f = '&' ;
assume A1: c <> [<*x,y*>,'&'] ; ::_thesis: 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
let s be State of (2GatesCircuit (x,y,c,'&')); ::_thesis: 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
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies (Following (s,2)) . (2GatesCircOutput (x,y,c,'&')) = (a1 '&' a2) '&' a3 )
assume  ( a1 = s . x & a2 = s . y & a3 = s . c ) ; ::_thesis: (Following (s,2)) . (2GatesCircOutput (x,y,c,'&')) = (a1 '&' a2) '&' a3
hence (Following (s,2)) . (2GatesCircOutput (x,y,c,'&')) = '&' . <*('&' . <*a1,a2*>),a3*> by A1, Th62
.= '&' . <*(a1 '&' a2),a3*> by Def6
.= (a1 '&' a2) '&' a3 by Def6 ;
::_thesis: verum
end;

begin

definition
let x, y, c be set ;
func BitAdderOutput (x,y,c) ->  Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) equals :: FACIRC_1:def 15
 2GatesCircOutput (x,y,c,'xor');
coherence
 2GatesCircOutput (x,y,c,'xor') is Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) ;
end;

:: deftheorem  defines BitAdderOutput FACIRC_1:def_15_:_
 for x, y, c being set holds BitAdderOutput (x,y,c) = 2GatesCircOutput (x,y,c,'xor');

definition
let x, y, c be set ;
func BitAdderCirc (x,y,c) ->  strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') equals :: FACIRC_1:def 16
 2GatesCircuit (x,y,c,'xor');
coherence
 2GatesCircuit (x,y,c,'xor') is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') ;
end;

:: deftheorem  defines BitAdderCirc FACIRC_1:def_16_:_
 for x, y, c being set holds BitAdderCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor');

definition
let x, y, c be set ;
func MajorityIStr (x,y,c) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign  equals :: FACIRC_1:def 17
((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&'));
correctness
coherence
((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&')) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;

:: deftheorem  defines MajorityIStr FACIRC_1:def_17_:_
 for x, y, c being set holds MajorityIStr (x,y,c) = ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&'));

definition
let x, y, c be set ;
func MajorityStr (x,y,c) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign  equals :: FACIRC_1:def 18
(MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3));
correctness
coherence
(MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
;
end;

:: deftheorem  defines MajorityStr FACIRC_1:def_18_:_
 for x, y, c being set holds MajorityStr (x,y,c) = (MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3));

definition
let x, y, c be set ;
func MajorityICirc (x,y,c) ->  strict gate`2=den Boolean Circuit of MajorityIStr (x,y,c) equals :: FACIRC_1:def 19
((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&'));
coherence
 ((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&')) is strict gate`2=den Boolean Circuit of MajorityIStr (x,y,c) ;
end;

:: deftheorem  defines MajorityICirc FACIRC_1:def_19_:_
 for x, y, c being set holds MajorityICirc (x,y,c) = ((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&'));

theorem Th67: :: FACIRC_1:67
for x, y, c being set holds InnerVertices (MajorityStr (x,y,c)) is Relation
proof
let x, y, c be set ; ::_thesis: InnerVertices (MajorityStr (x,y,c)) is Relation
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  InnerVertices (MajorityStr (x,y,c)) is Relation by A1, Th2, CIRCCOMB:47; ::_thesis: verum
end;

theorem Th68: :: FACIRC_1:68
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 ; ::_thesis: InputVertices (MajorityStr (x,y,c)) is without_pairs
set M = MajorityStr (x,y,c);
set MI = MajorityIStr (x,y,c);
set S = 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3);
given xx being pair set  such that A1: xx in InputVertices (MajorityStr (x,y,c)) ; :: according to FACIRC_1:def_2 ::_thesis: contradiction
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, CIRCCOMB:42;
then A4: InnerVertices (MajorityIStr (x,y,c)) = ({[<*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 (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by Th42;
then A5: (InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) \ (InnerVertices (MajorityIStr (x,y,c))) = {} 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 (MajorityIStr (x,y,c)) is without_pairs by A6, Th8, CIRCCOMB:47;
 InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) is Relation by Th38;
then  InputVertices (MajorityStr (x,y,c)) = (InputVertices (MajorityIStr (x,y,c))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) \ (InnerVertices (MajorityIStr (x,y,c)))) by A7, Th6;
hence  contradiction by A7, A1, A5, Def2; ::_thesis: verum
end;

theorem :: FACIRC_1:69
for x, y, c being set
for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,'&'] = a '&' b
proof
let x, y, c be set ; ::_thesis: for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,'&'] = a '&' b
set xy = <*x,y*>;
set S1 = 1GateCircStr (<*x,y*>,'&');
set A1 = 1GateCircuit (x,y,'&');
reconsider xx = x, yy = y as Vertex of (1GateCircStr (<*x,y*>,'&')) by Th43;
reconsider v1 = [<*x,y*>,'&'] as Element of InnerVertices (1GateCircStr (<*x,y*>,'&')) by Th47;
set S2 = 1GateCircStr (<*y,c*>,'&');
set A2 = 1GateCircuit (y,c,'&');
set S3 = 1GateCircStr (<*c,x*>,'&');
set A3 = 1GateCircuit (c,x,'&');
set S = MajorityIStr (x,y,c);
set A = MajorityICirc (x,y,c);
let s be State of (MajorityICirc (x,y,c)); ::_thesis: for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,'&'] = a '&' b
let a, b be Element of BOOLEAN ; ::_thesis: ( a = s . x & b = s . y implies (Following s) . [<*x,y*>,'&'] = a '&' b )
assume A1: ( a = s . x & b = s . y ) ; ::_thesis: (Following s) . [<*x,y*>,'&'] = a '&' b
A2: MajorityICirc (x,y,c) = (1GateCircuit (x,y,'&')) +* ((1GateCircuit (y,c,'&')) +* (1GateCircuit (c,x,'&'))) by Th25;
then reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,'&')) as State of (1GateCircuit (x,y,'&')) by Th26;
A3: MajorityIStr (x,y,c) = (1GateCircStr (<*x,y*>,'&')) +* ((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) by CIRCCOMB:6;
then reconsider v = v1 as Element of InnerVertices (MajorityIStr (x,y,c)) by Th21;
reconsider xx = xx, yy = yy as Vertex of (MajorityIStr (x,y,c)) by A3, Th20;
A4: dom s1 = the carrier of (1GateCircStr (<*x,y*>,'&')) by CIRCUIT1:3;
thus (Following s) . [<*x,y*>,'&'] = (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, Def6 ; ::_thesis: verum
end;

theorem :: FACIRC_1:70
for x, y, c being set
for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,'&'] = a '&' b
proof
let x, y, c be set ; ::_thesis: for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,'&'] = a '&' b
set yc = <*y,c*>;
set S2 = 1GateCircStr (<*y,c*>,'&');
set A2 = 1GateCircuit (y,c,'&');
reconsider yy = y, cc = c as Vertex of (1GateCircStr (<*y,c*>,'&')) by Th43;
reconsider v2 = [<*y,c*>,'&'] as Element of InnerVertices (1GateCircStr (<*y,c*>,'&')) by Th47;
set S1 = 1GateCircStr (<*x,y*>,'&');
set A1 = 1GateCircuit (x,y,'&');
set S3 = 1GateCircStr (<*c,x*>,'&');
set A3 = 1GateCircuit (c,x,'&');
set S = MajorityIStr (x,y,c);
set A = MajorityICirc (x,y,c);
let s be State of (MajorityICirc (x,y,c)); ::_thesis: for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,'&'] = a '&' b
let a, b be Element of BOOLEAN ; ::_thesis: ( a = s . y & b = s . c implies (Following s) . [<*y,c*>,'&'] = a '&' b )
assume A1: ( a = s . y & b = s . c ) ; ::_thesis: (Following s) . [<*y,c*>,'&'] = a '&' b
A2: (1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')) = (1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*x,y*>,'&')) by CIRCCOMB:5, CIRCCOMB:47;
then A3: MajorityIStr (x,y,c) = (1GateCircStr (<*y,c*>,'&')) +* ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) by CIRCCOMB:6;
then reconsider v = v2 as Element of InnerVertices (MajorityIStr (x,y,c)) by Th21;
 (1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&')) = (1GateCircuit (y,c,'&')) +* (1GateCircuit (x,y,'&')) by CIRCCOMB:22, CIRCCOMB:60;
then A4: MajorityICirc (x,y,c) = (1GateCircuit (y,c,'&')) +* ((1GateCircuit (x,y,'&')) +* (1GateCircuit (c,x,'&'))) by A2, Th25;
then reconsider s2 = s | the carrier of (1GateCircStr (<*y,c*>,'&')) as State of (1GateCircuit (y,c,'&')) by Th26;
reconsider yy = yy, cc = cc as Vertex of (MajorityIStr (x,y,c)) by A3, Th20;
A5: dom s2 = the carrier of (1GateCircStr (<*y,c*>,'&')) by CIRCUIT1:3;
thus (Following s) . [<*y,c*>,'&'] = (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, Def6 ; ::_thesis: verum
end;

theorem :: FACIRC_1:71
for x, y, c being set
for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . c & b = s . x holds
(Following s) . [<*c,x*>,'&'] = a '&' b
proof
let x, y, c be set ; ::_thesis: for s being State of (MajorityICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . c & b = s . x holds
(Following s) . [<*c,x*>,'&'] = a '&' b
set cx = <*c,x*>;
set S3 = 1GateCircStr (<*c,x*>,'&');
set A3 = 1GateCircuit (c,x,'&');
reconsider cc = c, xx = x as Vertex of (1GateCircStr (<*c,x*>,'&')) by Th43;
reconsider v3 = [<*c,x*>,'&'] as Element of InnerVertices (1GateCircStr (<*c,x*>,'&')) by Th47;
set S = MajorityIStr (x,y,c);
set A = MajorityICirc (x,y,c);
let s be State of (MajorityICirc (x,y,c)); ::_thesis: for a, b being Element of BOOLEAN st a = s . c & b = s . x holds
(Following s) . [<*c,x*>,'&'] = a '&' b
let a, b be Element of BOOLEAN ; ::_thesis: ( a = s . c & b = s . x implies (Following s) . [<*c,x*>,'&'] = a '&' b )
assume A1: ( a = s . c & b = s . x ) ; ::_thesis: (Following s) . [<*c,x*>,'&'] = a '&' b
reconsider cc = cc, xx = xx as Vertex of (MajorityIStr (x,y,c)) by Th20;
reconsider s3 = s | the carrier of (1GateCircStr (<*c,x*>,'&')) as State of (1GateCircuit (c,x,'&')) by Th26;
reconsider v = v3 as Element of InnerVertices (MajorityIStr (x,y,c)) by Th21;
A2: dom s3 = the carrier of (1GateCircStr (<*c,x*>,'&')) by CIRCUIT1:3;
thus (Following s) . [<*c,x*>,'&'] = (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, Def6 ; ::_thesis: verum
end;

definition
let x, y, c be set ;
func MajorityOutput (x,y,c) ->  Element of InnerVertices (MajorityStr (x,y,c)) equals :: FACIRC_1:def 20
[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];
coherence
 [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] is Element of InnerVertices (MajorityStr (x,y,c))
proof
 [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] in InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) by Th47;
hence  [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] is Element of InnerVertices (MajorityStr (x,y,c)) by Th21; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines MajorityOutput FACIRC_1:def_20_:_
 for x, y, c being set holds MajorityOutput (x,y,c) = [<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3];

definition
let x, y, c be set ;
func MajorityCirc (x,y,c) ->  strict gate`2=den Boolean Circuit of MajorityStr (x,y,c) equals :: FACIRC_1:def 21
(MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3));
coherence
 (MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3)) is strict gate`2=den Boolean Circuit of MajorityStr (x,y,c) ;
end;

:: deftheorem  defines MajorityCirc FACIRC_1:def_21_:_
 for x, y, c being set holds MajorityCirc (x,y,c) = (MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3));

theorem Th72: :: FACIRC_1:72
for x, y, c being set holds
( 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
let x, y, c be set ; ::_thesis: ( 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)) )
 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  ( 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 A2, A1, Th20; ::_thesis: verum
end;

theorem Th73: :: FACIRC_1:73
for x, y, c being set holds
( [<*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
let x, y, c be set ; ::_thesis: ( [<*x,y*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*y,c*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*c,x*>,'&'] in InnerVertices (MajorityStr (x,y,c)) )
 [<*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  ( [<*x,y*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*y,c*>,'&'] in InnerVertices (MajorityStr (x,y,c)) & [<*c,x*>,'&'] in InnerVertices (MajorityStr (x,y,c)) ) by A1, A2, Th21; ::_thesis: verum
end;

theorem Th74: :: FACIRC_1:74
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 ; ::_thesis: ( x in InputVertices (MajorityStr (x,y,c)) & y in InputVertices (MajorityStr (x,y,c)) & c in InputVertices (MajorityStr (x,y,c)) )
assume A1: ( not x in InputVertices (MajorityStr (x,y,c)) or not y in InputVertices (MajorityStr (x,y,c)) or not c in InputVertices (MajorityStr (x,y,c)) ) ; ::_thesis: contradiction
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 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 ; ::_thesis: verum
end;

theorem Th75: :: FACIRC_1:75
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 ; ::_thesis: ( InputVertices (MajorityStr (x,y,c)) = {x,y,c} & InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} )
set xy = [<*x,y*>,'&'];
set yc = [<*y,c*>,'&'];
set cx = [<*c,x*>,'&'];
set MI = MajorityIStr (x,y,c);
set S = 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3);
set M = MajorityStr (x,y,c);
A1: 1GateCircStr (<*x,y*>,'&') tolerates 1GateCircStr (<*y,c*>,'&') by CIRCCOMB:43;
A2: InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) 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, CIRCCOMB: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 (MajorityIStr (x,y,c)) = ({[<*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 (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by Th42;
then A7: (InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) \ (InnerVertices (MajorityIStr (x,y,c))) = {} 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 (MajorityIStr (x,y,c)) is without_pairs by A9, Th8, CIRCCOMB:47;
then  InputVertices (MajorityStr (x,y,c)) = (InputVertices (MajorityIStr (x,y,c))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) \ (InnerVertices (MajorityIStr (x,y,c)))) by A2, Th6;
hence  InputVertices (MajorityStr (x,y,c)) = (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 ;
::_thesis: InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}
 MajorityIStr (x,y,c) tolerates 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3) by CIRCCOMB:47;
hence  InnerVertices (MajorityStr (x,y,c)) = (InnerVertices (MajorityIStr (x,y,c))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by CIRCCOMB:11
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} by A6, CIRCCOMB:42 ;
::_thesis: verum
end;

Lm2:  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 ; ::_thesis: 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 )
let s be State of (MajorityCirc (x,y,c)); ::_thesis: 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 )
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 ) )
assume that
A1: a1 = s . x and
A2: a2 = s . y and
A3: a3 = s . c ; ::_thesis: ( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 )
set S = MajorityStr (x,y,c);
A4: dom s = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
A5: y in the carrier of (MajorityStr (x,y,c)) by Th72;
A6: x in the carrier of (MajorityStr (x,y,c)) by Th72;
A7: InnerVertices (MajorityStr (x,y,c)) = the carrier' of (MajorityStr (x,y,c)) 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 Def6 ;
::_thesis: ( (Following s) . [<*y,c*>,'&'] = a2 '&' a3 & (Following s) . [<*c,x*>,'&'] = a3 '&' a1 )
A8: c in the carrier of (MajorityStr (x,y,c)) 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 Def6 ;
::_thesis: (Following s) . [<*c,x*>,'&'] = a3 '&' a1
 [<*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 Def6 ;
::_thesis: verum
end;

theorem :: FACIRC_1:76
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 ; ::_thesis: 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
reconsider a = c as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,'&'] = a1 '&' a2
 s . a is Element of BOOLEAN ;
hence  for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,'&'] = a1 '&' a2 by Lm2; ::_thesis: verum
end;

theorem :: FACIRC_1:77
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 ; ::_thesis: 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
reconsider a = x as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following s) . [<*y,c*>,'&'] = a2 '&' a3
 s . a is Element of BOOLEAN ;
hence  for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following s) . [<*y,c*>,'&'] = a2 '&' a3 by Lm2; ::_thesis: verum
end;

theorem :: FACIRC_1:78
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 ; ::_thesis: 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
reconsider a = y as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following s) . [<*c,x*>,'&'] = a3 '&' a1
 s . a is Element of BOOLEAN ;
hence  for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following s) . [<*c,x*>,'&'] = a3 '&' a1 by Lm2; ::_thesis: verum
end;

theorem Th79: :: FACIRC_1:79
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 ; ::_thesis: 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
set xy = [<*x,y*>,'&'];
set yc = [<*y,c*>,'&'];
set cx = [<*c,x*>,'&'];
set S = MajorityStr (x,y,c);
reconsider xy = [<*x,y*>,'&'], yc = [<*y,c*>,'&'], cx = [<*c,x*>,'&'] as Element of InnerVertices (MajorityStr (x,y,c)) by Th73;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: 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
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . [<*x,y*>,'&'] & a2 = s . [<*y,c*>,'&'] & a3 = s . [<*c,x*>,'&'] implies (Following s) . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3 )
assume A1: ( a1 = s . [<*x,y*>,'&'] & a2 = s . [<*y,c*>,'&'] & a3 = s . [<*c,x*>,'&'] ) ; ::_thesis: (Following s) . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3
A2: dom s = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
 InnerVertices (MajorityStr (x,y,c)) = the carrier' of (MajorityStr (x,y,c)) 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 Def7 ;
::_thesis: verum
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,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 ; ::_thesis: 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 )
set S = MajorityStr (x,y,c);
reconsider x9 = x, y9 = y, c9 = c as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: 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 )
set xy = [<*x,y*>,'&'];
set yc = [<*y,c*>,'&'];
set cx = [<*c,x*>,'&'];
A1: Following (s,2) = Following (Following s) by Th15;
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (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 ) )
assume A2: ( a1 = s . x & a2 = s . y & a3 = s . c ) ; ::_thesis: ( (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 )
A3: (Following s) . [<*c,x*>,'&'] = a3 '&' a1 by A2, Lm2;
 ( (Following s) . [<*x,y*>,'&'] = a1 '&' a2 & (Following s) . [<*y,c*>,'&'] = 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; ::_thesis: ( (Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2 & (Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3 & (Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1 )
 y in InputVertices (MajorityStr (x,y,c)) by Th74;
then A4: (Following s) . y9 = s . y by CIRCUIT2:def_5;
 c in InputVertices (MajorityStr (x,y,c)) by Th74;
then A5: (Following s) . c9 = s . c by CIRCUIT2:def_5;
 x in InputVertices (MajorityStr (x,y,c)) by Th74;
then  (Following s) . x9 = s . x by CIRCUIT2:def_5;
hence  ( (Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2 & (Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3 & (Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1 ) by A2, A4, A5, A1, Lm2; ::_thesis: verum
end;

theorem :: FACIRC_1:80
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 ; ::_thesis: 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
reconsider a = c as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2
 s . a is Element of BOOLEAN ;
hence  for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following (s,2)) . [<*x,y*>,'&'] = a1 '&' a2 by Lm3; ::_thesis: verum
end;

theorem :: FACIRC_1:81
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 ; ::_thesis: 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
reconsider a = x as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3
 s . a is Element of BOOLEAN ;
hence  for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following (s,2)) . [<*y,c*>,'&'] = a2 '&' a3 by Lm3; ::_thesis: verum
end;

theorem :: FACIRC_1:82
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 ; ::_thesis: 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
reconsider a = y as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1
 s . a is Element of BOOLEAN ;
hence  for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following (s,2)) . [<*c,x*>,'&'] = a3 '&' a1 by Lm3; ::_thesis: verum
end;

theorem :: FACIRC_1:83
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 Lm3;

theorem Th84: :: FACIRC_1:84
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 ; ::_thesis: for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable
set S = MajorityStr (x,y,c);
reconsider xx = x, yy = y, cc = c as Vertex of (MajorityStr (x,y,c)) by Th72;
let s be State of (MajorityCirc (x,y,c)); ::_thesis: Following (s,2) is stable
set a1 = s . xx;
set a2 = s . yy;
set a3 = s . cc;
set ffs = Following (s,2);
set fffs = Following (Following (s,2));
A1: Following (s,2) = Following (Following s) by Th15;
A2: y in InputVertices (MajorityStr (x,y,c)) by Th74;
then  (Following s) . y = s . yy by CIRCUIT2:def_5;
then A3: (Following (s,2)) . y = s . yy by A1, A2, CIRCUIT2:def_5;
 s . yy = s . y ;
then A4: (Following (s,2)) . [<*c,x*>,'&'] = (s . cc) '&' (s . xx) by Lm3;
A5: x in InputVertices (MajorityStr (x,y,c)) by Th74;
then  (Following s) . x = s . xx by CIRCUIT2:def_5;
then A6: (Following (s,2)) . x = s . xx by A1, A5, CIRCUIT2:def_5;
 s . xx = s . x ;
then A7: (Following (s,2)) . [<*y,c*>,'&'] = (s . yy) '&' (s . cc) by Lm3;
A8: c in InputVertices (MajorityStr (x,y,c)) by Th74;
then  (Following s) . c = s . cc by CIRCUIT2:def_5;
then A9: (Following (s,2)) . c = s . cc by A1, A8, CIRCUIT2:def_5;
 s . cc = s . c ;
then A10: (Following (s,2)) . [<*x,y*>,'&'] = (s . xx) '&' (s . yy) by Lm3;
A11: (Following (s,2)) . (MajorityOutput (x,y,c)) = (((s . xx) '&' (s . yy)) 'or' ((s . yy) '&' (s . cc))) 'or' ((s . cc) '&' (s . xx)) by Lm3;
A12: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(MajorityStr_(x,y,c))_holds_
(Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a
let a be set ; ::_thesis: ( a in the carrier of (MajorityStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )
assume A13: a in the carrier of (MajorityStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then reconsider v = a as Vertex of (MajorityStr (x,y,c)) ;
A14: v in (InputVertices (MajorityStr (x,y,c))) \/ (InnerVertices (MajorityStr (x,y,c))) by A13, XBOOLE_1:45;
thus  (Following (s,2)) . a = (Following (Following (s,2))) . a ::_thesis: verum
proof
percases ( v in InputVertices (MajorityStr (x,y,c)) or v in InnerVertices (MajorityStr (x,y,c)) ) by A14, XBOOLE_0:def_3;
suppose v in InputVertices (MajorityStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
hence  (Following (s,2)) . a = (Following (Following (s,2))) . a by CIRCUIT2:def_5; ::_thesis: verum
end;
suppose v in InnerVertices (MajorityStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
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  (Following (s,2)) . a = (Following (Following (s,2))) . a by A11, A10, A7, A4, A6, A3, A9, Lm2, Th79; ::_thesis: verum
end;
end;
end;
end;
 ( dom (Following (Following (s,2))) = the carrier of (MajorityStr (x,y,c)) & dom (Following (s,2)) = the carrier of (MajorityStr (x,y,c)) ) by CIRCUIT1:3;
hence  Following (s,2) = Following (Following (s,2)) by A12, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

definition
let x, y, c be set ;
func BitAdderWithOverflowStr (x,y,c) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign  equals :: FACIRC_1:def 22
(2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));
coherence
 (2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
end;

:: deftheorem  defines BitAdderWithOverflowStr FACIRC_1:def_22_:_
 for x, y, c being set holds BitAdderWithOverflowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));

theorem Th85: :: FACIRC_1:85
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 ; ::_thesis: InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c}
set S = BitAdderWithOverflowStr (x,y,c);
set S1 = 2GatesCircStr (x,y,c,'xor');
set S2 = MajorityStr (x,y,c);
A1: ( InputVertices (2GatesCircStr (x,y,c,'xor')) = {x,y,c} & InputVertices (MajorityStr (x,y,c)) = {x,y,c} ) by Th57, Th75;
 ( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (MajorityStr (x,y,c)) is Relation ) by Th58, Th67;
hence  InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c} \/ {x,y,c} by A1, Th7
.= {x,y,c} ;
::_thesis: verum
end;

theorem :: FACIRC_1:86
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 ; ::_thesis: InnerVertices (BitAdderWithOverflowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}) \/ {(MajorityOutput (x,y,c))}
set S1 = 2GatesCircStr (x,y,c,'xor');
set S2 = MajorityStr (x,y,c);
A1: InnerVertices (MajorityStr (x,y,c)) = {[<*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 (2GatesCircStr (x,y,c,'xor')) = {[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} ) by Th56, XBOOLE_1:4;
hence  InnerVertices (BitAdderWithOverflowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}) \/ {(MajorityOutput (x,y,c))} by A1, Th27; ::_thesis: verum
end;

theorem :: FACIRC_1:87
for x, y, c being set
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
let x, y, c be set ; ::_thesis: 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 )
set S1 = 2GatesCircStr (x,y,c,'xor');
let S be non empty ManySortedSign ; ::_thesis: ( S = BitAdderWithOverflowStr (x,y,c) implies ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) )
assume A1: S = BitAdderWithOverflowStr (x,y,c) ; ::_thesis: ( x in the carrier of S & y in the carrier of S & c in the carrier of S )
A2: c in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;
 ( x in the carrier of (2GatesCircStr (x,y,c,'xor')) & y in the carrier of (2GatesCircStr (x,y,c,'xor')) ) by Th60;
hence  ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) by A1, A2, Th20; ::_thesis: verum
end;

definition
let x, y, c be set ;
func BitAdderWithOverflowCirc (x,y,c) ->  strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr (x,y,c) equals :: FACIRC_1:def 23
(BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));
coherence
 (BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c)) is strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr (x,y,c) ;
end;

:: deftheorem  defines BitAdderWithOverflowCirc FACIRC_1:def_23_:_
 for x, y, c being set holds BitAdderWithOverflowCirc (x,y,c) = (BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));

theorem :: FACIRC_1:88
for x, y, c being set holds InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation
proof
let x, y, c be set ; ::_thesis: InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation
 ( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (MajorityStr (x,y,c)) is Relation ) by Th58, Th67;
hence  InnerVertices (BitAdderWithOverflowStr (x,y,c)) is Relation by Th2, CIRCCOMB:47; ::_thesis: verum
end;

theorem :: FACIRC_1:89
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 ; ::_thesis: InputVertices (BitAdderWithOverflowStr (x,y,c)) is without_pairs
 InputVertices (BitAdderWithOverflowStr (x,y,c)) = {x,y,c} by Th85;
hence  InputVertices (BitAdderWithOverflowStr (x,y,c)) is without_pairs ; ::_thesis: verum
end;

theorem :: FACIRC_1:90
for x, y, c being set holds
( BitAdderOutput (x,y,c) in InnerVertices (BitAdderWithOverflowStr (x,y,c)) & MajorityOutput (x,y,c) in InnerVertices (BitAdderWithOverflowStr (x,y,c)) ) by Th21;

theorem :: FACIRC_1:91
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 ; ::_thesis: 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) )
set S1 = 2GatesCircStr (x,y,c,'xor');
set S2 = MajorityStr (x,y,c);
set A = BitAdderWithOverflowCirc (x,y,c);
set A1 = BitAdderCirc (x,y,c);
set A2 = MajorityCirc (x,y,c);
let s be State of (BitAdderWithOverflowCirc (x,y,c)); ::_thesis: 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) )
reconsider t = s as State of ((BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c))) ;
reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitAdderCirc (x,y,c)) by Th26;
set f = 'xor' ;
let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (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) ) )
assume that
A1: a1 = s . x and
A2: a2 = s . y and
A3: a3 = s . c ; ::_thesis: ( (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) )
A4: dom s1 = the carrier of (2GatesCircStr (x,y,c,'xor')) by CIRCUIT1:3;
 y in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;
then A5: a2 = s1 . y by A2, A4, FUNCT_1:47;
 InputVertices (2GatesCircStr (x,y,c,'xor')) is without_pairs by Th59;
then  InnerVertices (MajorityStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by Th5, Th67;
then A6: (Following (t,2)) . (2GatesCircOutput (x,y,c,'xor')) = (Following (s1,2)) . (2GatesCircOutput (x,y,c,'xor')) by Th32;
 c in the carrier of (2GatesCircStr (x,y,c,'xor')) by Th60;
then A7: a3 = s1 . c by A3, A4, FUNCT_1:47;
reconsider s2 = s | the carrier of (MajorityStr (x,y,c)) as State of (MajorityCirc (x,y,c)) by Th26;
A8: dom s2 = the carrier of (MajorityStr (x,y,c)) by CIRCUIT1:3;
 x in the carrier of (2GatesCircStr (x,y,c,'xor')) 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; ::_thesis: (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)
 InputVertices (MajorityStr (x,y,c)) is without_pairs by Th68;
then  InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (MajorityStr (x,y,c)) 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 (MajorityStr (x,y,c)) by Th72;
then A10: a3 = s2 . c by A3, A8, FUNCT_1:47;
 y in the carrier of (MajorityStr (x,y,c)) by Th72;
then A11: a2 = s2 . y by A2, A8, FUNCT_1:47;
 x in the carrier of (MajorityStr (x,y,c)) by Th72;
then  a1 = s2 . x by A1, A8, FUNCT_1:47;
hence  (Following (s,2)) . (MajorityOutput (x,y,c)) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) by A11, A10, A9, Lm3; ::_thesis: verum
end;

theorem :: FACIRC_1:92
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 ; ::_thesis: for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable
set S1 = 2GatesCircStr (x,y,c,'xor');
set S2 = MajorityStr (x,y,c);
set A = BitAdderWithOverflowCirc (x,y,c);
set A1 = BitAdderCirc (x,y,c);
set A2 = MajorityCirc (x,y,c);
let s be State of (BitAdderWithOverflowCirc (x,y,c)); ::_thesis: Following (s,2) is stable
reconsider s2 = s | the carrier of (MajorityStr (x,y,c)) as State of (MajorityCirc (x,y,c)) by Th26;
reconsider t = s as State of ((BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c))) ;
reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitAdderCirc (x,y,c)) by Th26;
set S = BitAdderWithOverflowStr (x,y,c);
A1: dom (Following (s,3)) = the carrier of (BitAdderWithOverflowStr (x,y,c)) by CIRCUIT1:3;
A2: the carrier of (BitAdderWithOverflowStr (x,y,c)) = the carrier of (2GatesCircStr (x,y,c,'xor')) \/ the carrier of (MajorityStr (x,y,c)) by CIRCCOMB:def_2;
 InputVertices (2GatesCircStr (x,y,c,'xor')) is without_pairs by Th59;
then  InnerVertices (MajorityStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by Th5, Th67;
then A3: ( Following (s1,2) = (Following (t,2)) | the carrier of (2GatesCircStr (x,y,c,'xor')) & Following (s1,3) = (Following (t,3)) | the carrier of (2GatesCircStr (x,y,c,'xor')) ) by Th30;
 Following (s1,2) is stable by Th63;
then A4: Following (s1,2) = Following (Following (s1,2)) by CIRCUIT2:def_6
.= Following (s1,(2 + 1)) by Th12 ;
 InputVertices (MajorityStr (x,y,c)) is without_pairs by Th68;
then  InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (MajorityStr (x,y,c)) by Th5, Th58;
then A5: ( Following (s2,2) = (Following (t,2)) | the carrier of (MajorityStr (x,y,c)) & Following (s2,3) = (Following (t,3)) | the carrier of (MajorityStr (x,y,c)) ) by Th31;
 Following (s2,2) is stable by Th84;
then A6: Following (s2,2) = Following (Following (s2,2)) by CIRCUIT2:def_6
.= Following (s2,(2 + 1)) by Th12 ;
A7: ( dom (Following (s1,2)) = the carrier of (2GatesCircStr (x,y,c,'xor')) & dom (Following (s2,2)) = the carrier of (MajorityStr (x,y,c)) ) by CIRCUIT1:3;
A8: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(BitAdderWithOverflowStr_(x,y,c))_holds_
(Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a
let a be set ; ::_thesis: ( a in the carrier of (BitAdderWithOverflowStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )
assume  a in the carrier of (BitAdderWithOverflowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a
then  ( a in the carrier of (2GatesCircStr (x,y,c,'xor')) or a in the carrier of (MajorityStr (x,y,c)) ) 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; ::_thesis: verum
end;
 ( Following (s,(2 + 1)) = Following (Following (s,2)) & dom (Following (s,2)) = the carrier of (BitAdderWithOverflowStr (x,y,c)) ) by Th12, CIRCUIT1:3;
hence  Following (s,2) = Following (Following (s,2)) by A1, A8, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;