:: by Grzegorz Bancerek and Yatsuka Nakamura

::

:: Received August 10, 1995

:: Copyright (c) 1995-2012 Association of Mizar Users

begin

registration
end;

registration
end;

:: 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 );

for IT being set holds

( IT is with_pair iff ex x being pair set st x in IT );

registration

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is without_pairs

coherence

not {x} is with_pair

coherence

not {x,y} is with_pair

coherence

not {x,y,z} is with_pair

end;
for b

b

proof end;

let x be non pair set ;coherence

not {x} is with_pair

proof end;

let y be non pair set ;coherence

not {x,y} is with_pair

proof end;

let z be non pair set ;coherence

not {x,y,z} is with_pair

proof end;

registration

let X be without_pairs set ;

let Y be set ;

coherence

not X \ Y is with_pair

not X /\ Y is with_pair

not Y /\ X is with_pair ;

end;
let Y be set ;

coherence

not X \ Y is with_pair

proof end;

coherence not X /\ Y is with_pair

proof end;

coherence not Y /\ X is with_pair ;

registration

let x be pair set ;

coherence

{x} is Relation-like

coherence

{x,y} is Relation-like

coherence

{x,y,z} is Relation-like

end;
coherence

{x} is Relation-like

proof end;

let y be pair set ;coherence

{x,y} is Relation-like

proof end;

let z be pair set ;coherence

{x,y,z} is Relation-like

proof end;

registration

coherence

for b_{1} being set st b_{1} is without_pairs & b_{1} is Relation-like holds

b_{1} is empty

end;
for b

b

proof end;

definition

let IT be Function;

end;
attr IT is nonpair-yielding means :: FACIRC_1:def 3

for x being set st x in dom IT holds

not IT . x is pair ;

for x being set st x in dom IT holds

not IT . x is pair ;

:: 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 );

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 ;

coherence

<*x*> is nonpair-yielding

coherence

<*x,y*> is nonpair-yielding

coherence

<*x,y,z*> is nonpair-yielding

end;
coherence

<*x*> is nonpair-yielding

proof end;

let y be non pair set ;coherence

<*x,y*> is nonpair-yielding

proof end;

let z be non pair set ;coherence

<*x,y,z*> is nonpair-yielding

proof end;

registration

let n be Nat;

ex b_{1} being FinSeqLen of n st

( b_{1} is one-to-one & b_{1} is nonpair-yielding )

end;
cluster Relation-like NAT -defined Function-like one-to-one finite V46(n) FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;

existence ex b

( b

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is one-to-one & b_{1} is nonpair-yielding )
end;

cluster Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like countable nonpair-yielding for set ;

existence ex b

( b

proof 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

InnerVertices (S1 +* S2) is Relation

proof 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;

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)) )

( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )

proof 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)) )

( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )

proof 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)

InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2)

proof 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

InputVertices (S1 +* S2) is without_pairs

proof 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;

InputVertices (S1 +* S2) is without_pairs by Th8, CIRCCOMB:47;

begin

definition
end;

scheme :: FACIRC_1:sch 2

2AryBooleUniq{ F_{1}( set , set ) -> Element of BOOLEAN } :

2AryBooleUniq{ F

for f1, f2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F_{1}(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F_{1}(x,y) ) holds

f1 = f2

f1 = f2

proof end;

scheme :: FACIRC_1:sch 3

2AryBooleDef{ F_{1}( set , set ) -> Element of BOOLEAN } :

2AryBooleDef{ F

( ex f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st

for x, y being Element of BOOLEAN holds f . <*x,y*> = F_{1}(x,y) & ( for f1, f2 being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F_{1}(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F_{1}(x,y) ) holds

f1 = f2 ) )

for x, y being Element of BOOLEAN holds f . <*x,y*> = F

f1 = f2 ) )

proof end;

scheme :: FACIRC_1:sch 5

3AryBooleUniq{ F_{1}( set , set , set ) -> Element of BOOLEAN } :

3AryBooleUniq{ F

for f1, f2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F_{1}(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F_{1}(x,y,z) ) holds

f1 = f2

f1 = f2

proof end;

scheme :: FACIRC_1:sch 6

3AryBooleDef{ F_{1}( set , set , set ) -> Element of BOOLEAN } :

3AryBooleDef{ F

( ex f being Function of (3 -tuples_on BOOLEAN),BOOLEAN st

for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F_{1}(x,y,z) & ( for f1, f2 being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F_{1}(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F_{1}(x,y,z) ) holds

f1 = f2 ) )

for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F

f1 = f2 ) )

proof end;

definition

existence

ex b_{1} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st

for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x 'xor' y;

uniqueness

for b_{1}, b_{2} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b_{2} . <*x,y*> = x 'xor' y ) holds

b_{1} = b_{2};

existence

ex b_{1} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st

for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x 'or' y;

uniqueness

for b_{1}, b_{2} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b_{2} . <*x,y*> = x 'or' y ) holds

b_{1} = b_{2};

existence

ex b_{1} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st

for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x '&' y;

uniqueness

for b_{1}, b_{2} being Function of (2 -tuples_on BOOLEAN),BOOLEAN st ( for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b_{2} . <*x,y*> = x '&' y ) holds

b_{1} = b_{2};

end;

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 for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'xor' y;

existence

ex b

for x, y being Element of BOOLEAN holds b

uniqueness

for b

b

proof 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 for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'or' y;

existence

ex b

for x, y being Element of BOOLEAN holds b

uniqueness

for b

b

proof 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 for x, y being Element of BOOLEAN holds it . <*x,y*> = x '&' y;

existence

ex b

for x, y being Element of BOOLEAN holds b

uniqueness

for b

b

proof end;

:: deftheorem Def4 defines 'xor' FACIRC_1:def 4 :

for b_{1} being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds

( b_{1} = 'xor' iff for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x 'xor' y );

for b

( b

:: deftheorem Def5 defines 'or' FACIRC_1:def 5 :

for b_{1} being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds

( b_{1} = 'or' iff for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x 'or' y );

for b

( b

:: deftheorem Def6 defines '&' FACIRC_1:def 6 :

for b_{1} being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds

( b_{1} = '&' iff for x, y being Element of BOOLEAN holds b_{1} . <*x,y*> = x '&' y );

for b

( b

definition

existence

ex b_{1} being Function of (3 -tuples_on BOOLEAN),BOOLEAN st

for x, y, z being Element of BOOLEAN holds b_{1} . <*x,y,z*> = (x 'or' y) 'or' z;

uniqueness

for b_{1}, b_{2} being Function of (3 -tuples_on BOOLEAN),BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b_{1} . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b_{2} . <*x,y,z*> = (x 'or' y) 'or' z ) holds

b_{1} = b_{2};

end;

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 for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x 'or' y) 'or' z;

existence

ex b

for x, y, z being Element of BOOLEAN holds b

uniqueness

for b

b

proof end;

:: deftheorem Def7 defines or3 FACIRC_1:def 7 :

for b_{1} being Function of (3 -tuples_on BOOLEAN),BOOLEAN holds

( b_{1} = or3 iff for x, y, z being Element of BOOLEAN holds b_{1} . <*x,y,z*> = (x 'or' y) 'or' z );

for b

( b

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))

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 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;

existence

ex b_{1} being State of A ex f being Function of NAT,(product the Sorts of A) st

( b_{1} = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) );

uniqueness

for b_{1}, b_{2} being State of A st ex f being Function of NAT,(product the Sorts of A) st

( b_{1} = 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

( b_{2} = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) holds

b_{1} = b_{2};

end;
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 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) ) );

existence

ex b

( b

uniqueness

for b

( b

( b

b

proof 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 b_{5} being State of A holds

( b_{5} = Following (s,n) iff ex f being Function of NAT,(product the Sorts of A) st

( b_{5} = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) );

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 b

( b

( b

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

for A being non-empty Circuit of S

for s being State of A holds Following (s,0) = s

proof 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))

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 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)

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 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

for A being non-empty Circuit of S

for s being State of A holds Following (s,1) = Following s

proof 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)

for A being non-empty Circuit of S

for s being State of A holds Following (s,2) = Following (Following s)

proof 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)

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 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 ;

end;
let A be non-empty Circuit of S;

let s be State of A;

let x be set ;

pred s is_stable_at x means :Def9: :: FACIRC_1:def 9

for n being Nat holds (Following (s,n)) . x = s . x;

for n being Nat holds (Following (s,n)) . x = s . x;

:: 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 );

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

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 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

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 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

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 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) )

for v being Vertex of S1 holds

( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) )

proof 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) )

for x being set st x in InnerVertices S1 holds

( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) )

proof 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)

for x being set st x in InnerVertices S2 holds

x in InnerVertices (S1 +* S2)

proof 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;

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)

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 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 )

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 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 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

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 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

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 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)

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 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)

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 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

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 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

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 end;

registration

let S be non empty non void gate`2=den ManySortedSign ;

let g be Gate of S;

coherence

( g `2 is Function-like & g `2 is Relation-like )

end;
let g be Gate of S;

coherence

( g `2 is Function-like & g `2 is Relation-like )

proof 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))

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 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)

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 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]

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 end;

begin

theorem :: FACIRC_1:39

for f being set

for p being nonpair-yielding FinSequence holds InputVertices (1GateCircStr (p,f)) is without_pairs

for p being nonpair-yielding FinSequence holds InputVertices (1GateCircStr (p,f)) is without_pairs

proof 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

for x, y being non pair set holds InputVertices (1GateCircStr (<*x,y*>,f)) is without_pairs

proof 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)) )

( 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 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)) )

( 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 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)) ) )

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 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 )

for p being FinSequence holds

( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )

proof end;

definition

let x, y be set ;

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;

1GateCircuit (<*x,y*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y*>,f) by CIRCCOMB:61;

end;
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);

1GateCircuit (<*x,y*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y*>,f) by CIRCCOMB:61;

:: 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);

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 )

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 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

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 end;

theorem :: FACIRC_1:50

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;

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;

1GateCircuit (<*x,y,z*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y,z*>,f) by CIRCCOMB:61;

end;
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);

1GateCircuit (<*x,y,z*>,f) is strict gate`2=den Boolean Circuit of 1GateCircStr (<*x,y,z*>,f) by CIRCCOMB:61;

:: 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);

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 )

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 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

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 end;

theorem :: FACIRC_1:54

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;

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;

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;
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 (1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f));

coherence

(1GateCircStr (<*x,y*>,f)) +* (1GateCircStr (<*[<*x,y*>,f],c*>,f)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

;

:: 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));

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;

[<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr (x,y,c,f))

;

end;
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];

[<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr (x,y,c,f))

proof end;

correctness ;

:: 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];

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;

coherence

2GatesCircOutput (x,y,c,f) is pair ;

end;
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;

coherence

2GatesCircOutput (x,y,c,f) is pair ;

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))}

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 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}

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 end;

definition

let x, y, c be set ;

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN;

(1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f)) is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,f) ;

end;
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));

(1GateCircuit (x,y,f)) +* (1GateCircuit ([<*x,y*>,f],c,f)) is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,f) ;

:: 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));

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

for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) is Relation

proof 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

for x, y, c being non pair set holds InputVertices (2GatesCircStr (x,y,c,f)) is without_pairs

proof 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)) )

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 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)) )

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 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 func s . v -> Element of BOOLEAN ;

coherence

s . v is Element of BOOLEAN

end;
let A be Boolean Circuit of S;

let s be State of A;

let v be Vertex of S;

:: original: .

redefine func s . v -> Element of BOOLEAN ;

coherence

s . v is Element of BOOLEAN

proof 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 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 )

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 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

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 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

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 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

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 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

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 end;

begin

definition

let x, y, c be set ;

2GatesCircOutput (x,y,c,'xor') is Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) ;

end;
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');

2GatesCircOutput (x,y,c,'xor') is Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) ;

:: deftheorem defines BitAdderOutput FACIRC_1:def 15 :

for x, y, c being set holds BitAdderOutput (x,y,c) = 2GatesCircOutput (x,y,c,'xor');

for x, y, c being set holds BitAdderOutput (x,y,c) = 2GatesCircOutput (x,y,c,'xor');

definition

let x, y, c be set ;

2GatesCircuit (x,y,c,'xor') is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') ;

end;
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');

2GatesCircuit (x,y,c,'xor') is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') ;

:: deftheorem defines BitAdderCirc FACIRC_1:def 16 :

for x, y, c being set holds BitAdderCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor');

for x, y, c being set holds BitAdderCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor');

definition

let x, y, c be set ;

coherence

((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&')) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

;

end;
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 ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&'));

coherence

((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) +* (1GateCircStr (<*c,x*>,'&')) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

;

:: 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*>,'&'));

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 ;

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;
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 (MajorityIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3));

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 ;

;

:: 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));

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 ;

((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&')) is strict gate`2=den Boolean Circuit of MajorityIStr (x,y,c) ;

end;
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,'&'));

((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&')) is strict gate`2=den Boolean Circuit of MajorityIStr (x,y,c) ;

:: 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,'&'));

for x, y, c being set holds MajorityICirc (x,y,c) = ((1GateCircuit (x,y,'&')) +* (1GateCircuit (y,c,'&'))) +* (1GateCircuit (c,x,'&'));

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

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 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

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 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

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 end;

definition

let x, y, c be set ;

[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] is Element of InnerVertices (MajorityStr (x,y,c))

;

end;
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];

[<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3] is Element of InnerVertices (MajorityStr (x,y,c))

proof end;

correctness ;

:: 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];

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 ;

(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;
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));

(MajorityICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&'],or3)) is strict gate`2=den Boolean Circuit of MajorityStr (x,y,c) ;

:: 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));

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)) )

( 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 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)) )

( [<*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 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)) )

( x in InputVertices (MajorityStr (x,y,c)) & y in InputVertices (MajorityStr (x,y,c)) & c in InputVertices (MajorityStr (x,y,c)) )

proof 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))} )

( InputVertices (MajorityStr (x,y,c)) = {x,y,c} & InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} )

proof 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 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

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 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

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 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

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 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

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 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 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

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 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

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 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

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 end;

theorem :: FACIRC_1:83

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

for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable

proof end;

definition

let x, y, c be set ;

(2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

end;
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));

(2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ;

:: 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));

for x, y, c being set holds BitAdderWithOverflowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (MajorityStr (x,y,c));

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 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 )

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 end;

definition

let x, y, c be set ;

(BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c)) is strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr (x,y,c) ;

end;
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));

(BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c)) is strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr (x,y,c) ;

:: 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));

for x, y, c being set holds BitAdderWithOverflowCirc (x,y,c) = (BitAdderCirc (x,y,c)) +* (MajorityCirc (x,y,c));

theorem :: FACIRC_1:89

for x, y, c being non pair set holds InputVertices (BitAdderWithOverflowStr (x,y,c)) is without_pairs

proof 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;

( 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) )

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 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

for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable

proof end;