:: Full Adder Circuit. Part { II }
:: by Grzegorz Bancerek , Shin'nosuke Yamaguchi and Katsumi Wasaki
::
:: Copyright (c) 2002-2021 Association of Mizar Users

theorem Th1: :: FACIRC_2:1
for x, y, z being set st x <> z & y <> z holds
{x,y} \ {z} = {x,y}
proof end;

theorem :: FACIRC_2:2
for x, y, z being set holds
( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )
proof end;

registration
coherence
for b1 being ManySortedSign st b1 is void holds
( b1 is unsplit & b1 is gate1=arity & b1 is gate2isBoolean )
proof end;
end;

registration
existence
ex b1 being ManySortedSign st
( b1 is strict & b1 is void )
proof end;
end;

definition
let x be set ;
func SingleMSS x -> void strict ManySortedSign means :Def1: :: FACIRC_2:def 1
the carrier of it = {x};
existence
ex b1 being void strict ManySortedSign st the carrier of b1 = {x}
proof end;
uniqueness
for b1, b2 being void strict ManySortedSign st the carrier of b1 = {x} & the carrier of b2 = {x} holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines SingleMSS FACIRC_2:def 1 :
for x being set
for b2 being void strict ManySortedSign holds
( b2 = SingleMSS x iff the carrier of b2 = {x} );

registration
let x be set ;
coherence
not SingleMSS x is empty
proof end;
end;

definition
let x be set ;
func SingleMSA x -> strict Boolean MSAlgebra over SingleMSS x means :: FACIRC_2:def 2
verum;
existence
ex b1 being strict Boolean MSAlgebra over SingleMSS x st verum
;
uniqueness
for b1, b2 being strict Boolean MSAlgebra over SingleMSS x holds b1 = b2
proof end;
end;

:: deftheorem defines SingleMSA FACIRC_2:def 2 :
for x being set
for b2 being strict Boolean MSAlgebra over SingleMSS x holds
( b2 = SingleMSA x iff verum );

theorem :: FACIRC_2:3
for x being set
for S being ManySortedSign holds SingleMSS x tolerates S by PARTFUN1:59;

theorem Th4: :: FACIRC_2:4
for x being set
for S being non empty ManySortedSign st x in the carrier of S holds
() +* S = ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #)
proof end;

theorem :: FACIRC_2:5
for x being set
for S being non empty strict ManySortedSign
for A being Boolean MSAlgebra over S st x in the carrier of S holds
() +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
proof end;

notation
synonym <*> for {} ;
end;

definition
let n be Nat;
let x, y be FinSequence;
A1: ( 1GateCircStr (<*>,()) is unsplit & 1GateCircStr (<*>,()) is gate1=arity & 1GateCircStr (<*>,()) is gate2isBoolean & not 1GateCircStr (<*>,()) is void & not 1GateCircStr (<*>,()) is empty & 1GateCircStr (<*>,()) is strict ) ;
func n -BitAdderStr (x,y) -> non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign means :Def3: :: FACIRC_2:def 3
ex f, g being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );
uniqueness
for b1, b2 being non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) & ex f, g being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) )
proof end;
end;

:: deftheorem Def3 defines -BitAdderStr FACIRC_2:def 3 :
for n being Nat
for x, y being FinSequence
for b4 being non empty non void strict unsplit gate1=arity gate2isBoolean ManySortedSign holds
( b4 = n -BitAdderStr (x,y) iff ex f, g being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for z being set st S = f . n & z = g . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
func n -BitAdderCirc (x,y) -> strict gate2=den Boolean Circuit of n -BitAdderStr (x,y) means :Def4: :: FACIRC_2:def 4
ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & it = g . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );
uniqueness
for b1, b2 being strict gate2=den Boolean Circuit of n -BitAdderStr (x,y) st ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b2 = g . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate2=den Boolean Circuit of n -BitAdderStr (x,y) ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) )
proof end;
end;

:: deftheorem Def4 defines -BitAdderCirc FACIRC_2:def 4 :
for n being Nat
for x, y being FinSequence
for b4 being strict gate2=den Boolean Circuit of n -BitAdderStr (x,y) holds
( b4 = n -BitAdderCirc (x,y) iff ex f, g, h being ManySortedSet of NAT st
( n -BitAdderStr (x,y) = f . n & b4 = g . n & f . 0 = 1GateCircStr (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
set c = [<*>,()];
func n -BitMajorityOutput (x,y) -> Element of InnerVertices (n -BitAdderStr (x,y)) means :Def5: :: FACIRC_2:def 5
ex h being ManySortedSet of NAT st
( it = h . n & h . 0 = [<*>,()] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitAdderStr (x,y)) st ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,()] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) & ex h being ManySortedSet of NAT st
( b2 = h . n & h . 0 = [<*>,()] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds
b1 = b2
proof end;
existence
ex b1 being Element of InnerVertices (n -BitAdderStr (x,y)) ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*>,()] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) )
proof end;
end;

:: deftheorem Def5 defines -BitMajorityOutput FACIRC_2:def 5 :
for n being Nat
for x, y being FinSequence
for b4 being Element of InnerVertices (n -BitAdderStr (x,y)) holds
( b4 = n -BitMajorityOutput (x,y) iff ex h being ManySortedSet of NAT st
( b4 = h . n & h . 0 = [<*>,()] & ( for n being Nat
for z being set st z = h . n holds
h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) );

theorem Th6: :: FACIRC_2:6
for x, y being FinSequence
for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr (<*>,()) & g . 0 = 1GateCircuit (<*>,()) & h . 0 = [<*>,()] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for z being set st S = f . n & A = g . n & z = h . n holds
( f . (n + 1) = S +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds
for n being Nat holds
( n -BitAdderStr (x,y) = f . n & n -BitAdderCirc (x,y) = g . n & n -BitMajorityOutput (x,y) = h . n )
proof end;

theorem Th7: :: FACIRC_2:7
for a, b being FinSequence holds
( 0 -BitAdderStr (a,b) = 1GateCircStr (<*>,()) & 0 -BitAdderCirc (a,b) = 1GateCircuit (<*>,()) & 0 -BitMajorityOutput (a,b) = [<*>,()] )
proof end;

theorem Th8: :: FACIRC_2:8
for a, b being FinSequence
for c being set st c = [<*>,()] holds
( 1 -BitAdderStr (a,b) = (1GateCircStr (<*>,())) +* (BitAdderWithOverflowStr ((a . 1),(b . 1),c)) & 1 -BitAdderCirc (a,b) = (1GateCircuit (<*>,())) +* (BitAdderWithOverflowCirc ((a . 1),(b . 1),c)) & 1 -BitMajorityOutput (a,b) = MajorityOutput ((a . 1),(b . 1),c) )
proof end;

theorem :: FACIRC_2:9
for a, b, c being set st c = [<*>,()] holds
( 1 -BitAdderStr (<*a*>,<*b*>) = (1GateCircStr (<*>,())) +* (BitAdderWithOverflowStr (a,b,c)) & 1 -BitAdderCirc (<*a*>,<*b*>) = (1GateCircuit (<*>,())) +* (BitAdderWithOverflowCirc (a,b,c)) & 1 -BitMajorityOutput (<*a*>,<*b*>) = MajorityOutput (a,b,c) )
proof end;

theorem Th10: :: FACIRC_2:10
for n being Nat
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitAdderStr ((p ^ p1),(q ^ q1)) = n -BitAdderStr ((p ^ p2),(q ^ q2)) & n -BitAdderCirc ((p ^ p1),(q ^ q1)) = n -BitAdderCirc ((p ^ p2),(q ^ q2)) & n -BitMajorityOutput ((p ^ p1),(q ^ q1)) = n -BitMajorityOutput ((p ^ p2),(q ^ q2)) )
proof end;

theorem :: FACIRC_2:11
for n being Nat
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitAdderStr ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr (a,b,(n -BitMajorityOutput (x,y)))) & (n + 1) -BitAdderCirc ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitAdderCirc (x,y)) +* (BitAdderWithOverflowCirc (a,b,(n -BitMajorityOutput (x,y)))) & (n + 1) -BitMajorityOutput ((x ^ <*a*>),(y ^ <*b*>)) = MajorityOutput (a,b,(n -BitMajorityOutput (x,y))) )
proof end;

theorem Th12: :: FACIRC_2:12
for n being Nat
for x, y being FinSequence holds
( (n + 1) -BitAdderStr (x,y) = (n -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) & (n + 1) -BitAdderCirc (x,y) = (n -BitAdderCirc (x,y)) +* (BitAdderWithOverflowCirc ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))) & (n + 1) -BitMajorityOutput (x,y) = MajorityOutput ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y))) )
proof end;

theorem Th13: :: FACIRC_2:13
for n, m being Element of NAT st n <= m holds
for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices (m -BitAdderStr (x,y))
proof end;

theorem :: FACIRC_2:14
for n being Element of NAT
for x, y being FinSequence holds InnerVertices ((n + 1) -BitAdderStr (x,y)) = (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . (n + 1)),(y . (n + 1)),(n -BitMajorityOutput (x,y)))))
proof end;

definition
let k, n be Nat;
assume that
A1: k >= 1 and
A2: k <= n ;
let x, y be FinSequence;
func (k,n) -BitAdderOutput (x,y) -> Element of InnerVertices (n -BitAdderStr (x,y)) means :Def6: :: FACIRC_2:def 6
ex i being Element of NAT st
( k = i + 1 & it = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitAdderStr (x,y)) st ex i being Element of NAT st
( k = i + 1 & b1 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) & ex i being Element of NAT st
( k = i + 1 & b2 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) holds
b1 = b2
;
existence
ex b1 being Element of InnerVertices (n -BitAdderStr (x,y)) ex i being Element of NAT st
( k = i + 1 & b1 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) )
proof end;
end;

:: deftheorem Def6 defines -BitAdderOutput FACIRC_2:def 6 :
for k, n being Nat st k >= 1 & k <= n holds
for x, y being FinSequence
for b5 being Element of InnerVertices (n -BitAdderStr (x,y)) holds
( b5 = (k,n) -BitAdderOutput (x,y) iff ex i being Element of NAT st
( k = i + 1 & b5 = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) ) );

theorem :: FACIRC_2:15
for n, k being Element of NAT st k < n holds
for x, y being FinSequence holds ((k + 1),n) -BitAdderOutput (x,y) = BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y)))
proof end;

Lm1: now :: thesis: for i being Nat
for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being object st x = y ^ <*a*>
let i be Nat; :: thesis: for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being object st x = y ^ <*a*>
let x be FinSeqLen of i + 1; :: thesis: ex y being FinSeqLen of i ex a being object st x = y ^ <*a*>
A1: len x = i + 1 by CARD_1:def 7;
consider y being FinSequence, a being object such that
A2: x = y ^ <*a*> by FINSEQ_1:46;
len <*a*> = 1 by FINSEQ_1:40;
then i + 1 = (len y) + 1 by ;
then reconsider y = y as FinSeqLen of i by CARD_1:def 7;
take y = y; :: thesis: ex a being object st x = y ^ <*a*>
take a = a; :: thesis: x = y ^ <*a*>
thus x = y ^ <*a*> by A2; :: thesis: verum
end;

Lm2: now :: thesis: for i being Nat
for x being nonpair-yielding FinSeqLen of i + 1 ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*>
let i be Nat; :: thesis: for x being nonpair-yielding FinSeqLen of i + 1 ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*>
let x be nonpair-yielding FinSeqLen of i + 1; :: thesis: ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*>
consider y being FinSeqLen of i, a being object such that
A1: x = y ^ <*a*> by Lm1;
A2: dom y c= dom x by ;
A3: y = x | (dom y) by ;
y is nonpair-yielding
proof
let z be set ; :: according to FACIRC_1:def 3 :: thesis: ( not z in proj1 y or not y . z is pair )
assume A4: z in dom y ; :: thesis: not y . z is pair
then y . z = x . z by ;
hence not y . z is pair by ; :: thesis: verum
end;
then reconsider y = y as nonpair-yielding FinSeqLen of i ;
A5: i + 1 in Seg (i + 1) by FINSEQ_1:4;
dom x = Seg (len x) by FINSEQ_1:def 3;
then A6: i + 1 in dom x by ;
A7: x . ((len y) + 1) = a by ;
len y = i by CARD_1:def 7;
then reconsider a = a as non pair set by ;
take y = y; :: thesis: ex a being non pair set st x = y ^ <*a*>
take a = a; :: thesis: x = y ^ <*a*>
thus x = y ^ <*a*> by A1; :: thesis: verum
end;

theorem :: FACIRC_2:16
for n being Element of NAT
for x, y being FinSequence holds InnerVertices (n -BitAdderStr (x,y)) is Relation
proof end;

theorem Th17: :: FACIRC_2:17
for x, y, c being set holds InnerVertices (MajorityIStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}
proof end;

theorem Th18: :: FACIRC_2:18
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
InputVertices (MajorityIStr (x,y,c)) = {x,y,c}
proof end;

theorem Th19: :: FACIRC_2:19
for x, y, c being set holds InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}
proof end;

theorem Th20: :: FACIRC_2:20
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
InputVertices (MajorityStr (x,y,c)) = {x,y,c}
proof end;

theorem Th21: :: FACIRC_2:21
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InputVertices S1 = InputVertices S2 holds
InputVertices (S1 +* S2) = InputVertices S1
proof end;

theorem Th22: :: FACIRC_2:22
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
proof end;

theorem Th23: :: FACIRC_2:23
for x, y, c being 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;

registration
cluster empty -> non pair for set ;
coherence
for b1 being set st b1 is empty holds
not b1 is pair
;
end;

registration
coherence
for b1 being Function st b1 is empty holds
b1 is nonpair-yielding
proof end;
let f be nonpair-yielding Function;
let x be set ;
cluster f . x -> non pair ;
coherence
not f . x is pair
proof end;
end;

registration
let n be Nat;
let x, y be FinSequence;
cluster n -BitMajorityOutput (x,y) -> pair ;
coherence
n -BitMajorityOutput (x,y) is pair
proof end;
end;

theorem Th24: :: FACIRC_2:24
for x, y being FinSequence
for n being Nat holds
( ( (n -BitMajorityOutput (x,y)) 1 = <*> & (n -BitMajorityOutput (x,y)) 2 = --> FALSE & proj1 ((n -BitMajorityOutput (x,y)) 2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitMajorityOutput (x,y)) 1) = 3 & (n -BitMajorityOutput (x,y)) 2 = or3 & proj1 ((n -BitMajorityOutput (x,y)) 2) = 3 -tuples_on BOOLEAN ) )
proof end;

theorem Th25: :: FACIRC_2:25
for n being Nat
for x, y being FinSequence
for p being set holds
( n -BitMajorityOutput (x,y) <> [p,'&'] & n -BitMajorityOutput (x,y) <> [p,'xor'] )
proof end;

theorem Th26: :: FACIRC_2:26
for f, g being nonpair-yielding FinSequence
for n being Nat holds
( InputVertices ((n + 1) -BitAdderStr (f,g)) = (InputVertices (n -BitAdderStr (f,g))) \/ ((InputVertices (BitAdderWithOverflowStr ((f . (n + 1)),(g . (n + 1)),(n -BitMajorityOutput (f,g))))) \ {(n -BitMajorityOutput (f,g))}) & InnerVertices (n -BitAdderStr (f,g)) is Relation & InputVertices (n -BitAdderStr (f,g)) is without_pairs )
proof end;

theorem :: FACIRC_2:27
for n being Nat
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitAdderStr (x,y)) = (rng x) \/ (rng y)
proof end;

Lm3: for x, y, c being 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
( () . [<*x,y*>,'&'] = a1 '&' a2 & () . [<*y,c*>,'&'] = a2 '&' a3 & () . [<*c,x*>,'&'] = a3 '&' a1 )

proof end;

theorem Th28: :: FACIRC_2:28
for x, y, c being 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
() . (MajorityOutput (x,y,c)) = (a1 'or' a2) 'or' a3
proof end;

Lm4: for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
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 Th29: :: FACIRC_2:29
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] holds
for s being State of (MajorityCirc (x,y,c)) holds Following (s,2) is stable
proof end;

theorem :: FACIRC_2:30
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
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 Th31: :: FACIRC_2:31
for x, y, c being set st x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] & c <> [<*x,y*>,'xor'] holds
for s being State of (BitAdderWithOverflowCirc (x,y,c)) holds Following (s,2) is stable
proof end;

theorem :: FACIRC_2:32
for n being Nat
for x, y being nonpair-yielding FinSeqLen of n
for s being State of (n -BitAdderCirc (x,y)) holds Following (s,(1 + (2 * n))) is stable
proof end;

theorem :: FACIRC_2:33
for i being Nat
for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being object st x = y ^ <*a*> by Lm1;

theorem :: FACIRC_2:34
for i being Nat
for x being nonpair-yielding FinSeqLen of i + 1 ex y being nonpair-yielding FinSeqLen of i ex a being non pair set st x = y ^ <*a*> by Lm2;