:: FACIRC_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: FACIRC_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set st x <> z & y <> z holds
{x,y} \ {z} = {x,y}
proof end;

theorem :: FACIRC_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FACIRC_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set holds
( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )
proof end;

registration
cluster void -> unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
coherence
for b1 being ManySortedSign st b1 is void holds
( b1 is unsplit & b1 is gate`1=arity & b1 is gate`2isBoolean )
proof end;
end;

registration
cluster strict void unsplit gate`1=arity gate`2isBoolean ManySortedSign ;
existence
ex b1 being ManySortedSign st
( b1 is strict & b1 is void )
proof end;
end;

definition
let x be set ;
func SingleMSS x -> strict void ManySortedSign means :Def1: :: FACIRC_2:def 1
the carrier of it = {x};
existence
ex b1 being strict void ManySortedSign st the carrier of b1 = {x}
proof end;
uniqueness
for b1, b2 being strict void 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 strict void ManySortedSign holds
( b2 = SingleMSS x iff the carrier of b2 = {x} );

registration
let x be set ;
cluster SingleMSS x -> non empty strict void unsplit gate`1=arity gate`2isBoolean ;
coherence
not SingleMSS x is empty
proof end;
end;

definition
let x be set ;
func SingleMSA x -> strict Boolean MSAlgebra of SingleMSS x means :: FACIRC_2:def 2
verum;
existence
ex b1 being strict Boolean MSAlgebra of SingleMSS x st verum ;
uniqueness
for b1, b2 being strict Boolean MSAlgebra of 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 of SingleMSS x holds
( b2 = SingleMSA x iff verum );

theorem :: FACIRC_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being ManySortedSign holds SingleMSS x tolerates S
proof end;

theorem Th5: :: FACIRC_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non empty ManySortedSign st x in the carrier of S holds
(SingleMSS x) +* S = ManySortedSign(# the carrier of S,the OperSymbols of S,the Arity of S,the ResultSort of S #)
proof end;

theorem :: FACIRC_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for S being non empty strict ManySortedSign
for A being Boolean MSAlgebra of S st x in the carrier of S holds
(SingleMSA x) +* A = MSAlgebra(# the Sorts of A,the Charact of A #)
proof end;

notation
synonym <*> for {} ;
end;

definition
:: original: <*>
redefine func <*> -> FinSeqLen of 0;
coherence
<*> is FinSeqLen of 0
proof end;
end;

definition
let n be Nat;
let x, y be FinSequence;
A1: ( 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is unsplit & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is gate`1=arity & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is gate`2isBoolean & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is void & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is empty & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is strict ) ;
func n -BitAdderStr x,y -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def3: :: FACIRC_2:def 3
 ex f, g being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, g being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign holds
( b4 = n -BitAdderStr x,y iff ex f, g being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 gate`2=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 <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 gate`2=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 <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 gate`2=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 <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 gate`2=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 <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )];
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 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( 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 Th7: :: FACIRC_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being FinSequence
for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & g . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of 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 Th8: :: FACIRC_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being FinSequence holds
( 0 -BitAdderStr a,b = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitAdderCirc a,b = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitMajorityOutput a,b = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )
proof end;

theorem Th9: :: FACIRC_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being FinSequence
for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitAdderStr a,b = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowStr (a . 1),(b . 1),c) & 1 -BitAdderCirc a,b = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowCirc (a . 1),(b . 1),c) & 1 -BitMajorityOutput a,b = MajorityOutput (a . 1),(b . 1),c )
proof end;

theorem :: FACIRC_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitAdderStr <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowStr a,b,c) & 1 -BitAdderCirc <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowCirc a,b,c) & 1 -BitMajorityOutput <*a*>,<*b*> = MajorityOutput a,b,c )
proof end;

theorem Th11: :: FACIRC_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th13: :: FACIRC_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th14: :: FACIRC_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being 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:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 A1: ( k >= 1 & 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 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 Nat st
( k = i + 1 & b1 = BitAdderOutput (x . k),(y . k),(i -BitMajorityOutput x,y) ) & ex i being 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 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 Nat st
( k = i + 1 & b5 = BitAdderOutput (x . k),(y . k),(i -BitMajorityOutput x,y) ) );

theorem :: FACIRC_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, k being 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
let i be Nat; :: thesis: for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being set st x = y ^ <*a*>
let x be FinSeqLen of i + 1; :: thesis: ex y being FinSeqLen of i ex a being set st x = y ^ <*a*>
i >= 0 by NAT_1:18;
then A1: ( i + 1 <> 0 & len x = i + 1 ) by CIRCCOMB:def 12, NAT_1:38;
then x <> <*> by FINSEQ_1:25;
then consider y being FinSequence, a being set such that
A2: x = y ^ <*a*> by FINSEQ_1:63;
len <*a*> = 1 by FINSEQ_1:57;
then i + 1 = (len y) + 1 by A1, A2, FINSEQ_1:35;
then len y = i ;
then reconsider y = y as FinSeqLen of i by CIRCCOMB:def 12;
take y = y; :: thesis: ex a being set st x = y ^ <*a*>
take a = a; :: thesis: x = y ^ <*a*>
thus x = y ^ <*a*> by A2; :: thesis: verum
end;

Lm2: now
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 set such that
A1: x = y ^ <*a*> by Lm1;
A2: ( dom y c= dom x & y = x | (dom y) ) by A1, FINSEQ_1:33, FINSEQ_1:39;
y is nonpair-yielding
proof
let z be set ; :: according to FACIRC_1:def 3 :: thesis: ( not z in dom y or not y . z is pair )
assume z in dom y ; :: thesis: not y . z is pair
then ( z in dom x & y . z = x . z ) by A2, FUNCT_1:70;
hence not y . z is pair by FACIRC_1:def 3; :: thesis: verum
end;
then reconsider y = y as nonpair-yielding FinSeqLen of i ;
( i + 1 in Seg (i + 1) & dom x = Seg (len x) ) by FINSEQ_1:6, FINSEQ_1:def 3;
then ( i + 1 in dom x & x . ((len y) + 1) = a & len y = i ) by A1, CIRCCOMB:def 12, FINSEQ_1:59;
then reconsider a = a as non pair set by FACIRC_1:def 3;
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:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y being FinSequence holds InnerVertices (n -BitAdderStr x,y) is Relation
proof end;

theorem Th18: :: FACIRC_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds InnerVertices (MajorityIStr x,y,c) = {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]}
proof end;

theorem Th19: :: FACIRC_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th20: :: FACIRC_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th21: :: FACIRC_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th22: :: FACIRC_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InputVertices S1 = InputVertices S2 holds
InputVertices (S1 +* S2) = InputVertices S1
proof end;

theorem Th23: :: FACIRC_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set st x <> [<*y,c*>,'&' ] & y <> [<*c,x*>,'&' ] & c <> [<*x,y*>,'&' ] & c <> [<*x,y*>,'xor' ] holds
InputVertices (BitAdderWithOverflowStr x,y,c) = {x,y,c}
proof end;

theorem Th24: :: FACIRC_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 set ;
coherence
for b1 being set st b1 is empty holds
not b1 is pair
proof end;
end;

registration
cluster <*> -> non pair nonpair-yielding ;
coherence
{} 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 Th25: :: FACIRC_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being FinSequence
for n being Nat holds
( ( (n -BitMajorityOutput x,y) `1 = <*> & (n -BitMajorityOutput x,y) `2 = (0 -tuples_on BOOLEAN ) --> 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 Th26: :: FACIRC_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th27: :: FACIRC_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & not InputVertices (n -BitAdderStr f,g) is with_pair )
proof end;

theorem :: FACIRC_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
( (Following s) . [<*x,y*>,'&' ] = a1 '&' a2 & (Following s) . [<*y,c*>,'&' ] = a2 '&' a3 & (Following s) . [<*c,x*>,'&' ] = a3 '&' a1 )
proof end;

theorem Th29: :: FACIRC_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
(Following s) . (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 Th30: :: FACIRC_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 (MajorityCirc x,y,c) holds Following s,2 is stable
proof end;

theorem :: FACIRC_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th32: :: FACIRC_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

Lm5: for n being Nat ex N being Function of NAT , NAT st
( N . 0 = 1 & N . 1 = 2 & N . 2 = n )
proof end;

theorem :: FACIRC_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for x being FinSeqLen of i + 1 ex y being FinSeqLen of i ex a being set st x = y ^ <*a*> by Lm1;

theorem :: FACIRC_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FACIRC_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: FACIRC_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat ex N being Function of NAT , NAT st
( N . 0 = 1 & N . 1 = 2 & N . 2 = n ) by Lm5;