:: GFACIRC2 semantic presentation

definition
let n be Nat;
let x, y be FinSequence;
set S0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE );
set o0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )];
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 -BitGFA0Str x,y -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def1: :: GFACIRC2:def 1
 ex f, h being ManySortedSet of NAT st
( it = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 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 = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (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, h being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 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 = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, h being ManySortedSet of NAT st
( b2 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 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 = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (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, h being ManySortedSet of NAT st
( b1 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 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 = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
proof end;
end;

:: deftheorem Def1 defines -BitGFA0Str GFACIRC2:def 1 :
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 -BitGFA0Str x,y iff ex f, h being ManySortedSet of NAT st
( b4 = f . n & f . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & h . 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 = h . n holds
( f . (n + 1) = S +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
func n -BitGFA0Circ x,y -> strict gate`2=den Boolean Circuit of n -BitGFA0Str x,y means :Def2: :: GFACIRC2:def 2
 ex f, g, h being ManySortedSet of NAT st
( n -BitGFA0Str 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 +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) );
uniqueness
for b1, b2 being strict gate`2=den Boolean Circuit of n -BitGFA0Str x,y st ex f, g, h being ManySortedSet of NAT st
( n -BitGFA0Str 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 +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) & ex f, g, h being ManySortedSet of NAT st
( n -BitGFA0Str 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 +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) holds
b1 = b2
proof end;
existence
ex b1 being strict gate`2=den Boolean Circuit of n -BitGFA0Str x,y ex f, g, h being ManySortedSet of NAT st
( n -BitGFA0Str 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 +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) )
proof end;
end;

:: deftheorem Def2 defines -BitGFA0Circ GFACIRC2:def 2 :
for n being Nat
for x, y being FinSequence
for b4 being strict gate`2=den Boolean Circuit of n -BitGFA0Str x,y holds
( b4 = n -BitGFA0Circ x,y iff ex f, g, h being ManySortedSet of NAT st
( n -BitGFA0Str 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 +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) ) );

definition
let n be Nat;
let x, y be FinSequence;
func n -BitGFA0CarryOutput x,y -> Element of InnerVertices (n -BitGFA0Str x,y) means :Def3: :: GFACIRC2:def 3
 ex h being ManySortedSet of NAT st
( it = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) );
uniqueness
for b1, b2 being Element of InnerVertices (n -BitGFA0Str x,y) st ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) & ex h being ManySortedSet of NAT st
( b2 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) holds
b1 = b2
proof end;
existence
ex b1 being Element of InnerVertices (n -BitGFA0Str x,y) ex h being ManySortedSet of NAT st
( b1 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) )
proof end;
end;

:: deftheorem Def3 defines -BitGFA0CarryOutput GFACIRC2:def 3 :
for n being Nat
for x, y being FinSequence
for b4 being Element of InnerVertices (n -BitGFA0Str x,y) holds
( b4 = n -BitGFA0CarryOutput x,y iff ex h being ManySortedSet of NAT st
( b4 = h . n & h . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),(h . n) ) ) );

theorem Th1: :: GFACIRC2:1
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 +* (BitGFA0Str (x . (n + 1)),(y . (n + 1)),z) & g . (n + 1) = A +* (BitGFA0Circ (x . (n + 1)),(y . (n + 1)),z) & h . (n + 1) = GFA0CarryOutput (x . (n + 1)),(y . (n + 1)),z ) ) holds
for n being Nat holds
( n -BitGFA0Str x,y = f . n & n -BitGFA0Circ x,y = g . n & n -BitGFA0CarryOutput x,y = h . n )
proof end;

theorem Th2: :: GFACIRC2:2
for a, b being FinSequence holds
( 0 -BitGFA0Str a,b = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitGFA0Circ a,b = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitGFA0CarryOutput a,b = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )
proof end;

theorem Th3: :: GFACIRC2:3
for a, b being FinSequence
for c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitGFA0Str a,b = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Str (a . 1),(b . 1),c) & 1 -BitGFA0Circ a,b = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Circ (a . 1),(b . 1),c) & 1 -BitGFA0CarryOutput a,b = GFA0CarryOutput (a . 1),(b . 1),c )
proof end;

theorem :: GFACIRC2:4
for a, b, c being set st c = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitGFA0Str <*a*>,<*b*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Str a,b,c) & 1 -BitGFA0Circ <*a*>,<*b*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitGFA0Circ a,b,c) & 1 -BitGFA0CarryOutput <*a*>,<*b*> = GFA0CarryOutput a,b,c )
proof end;

theorem Th5: :: GFACIRC2:5
for n being Nat
for p, q being FinSeqLen of n
for p1, p2, q1, q2 being FinSequence holds
( n -BitGFA0Str (p ^ p1),(q ^ q1) = n -BitGFA0Str (p ^ p2),(q ^ q2) & n -BitGFA0Circ (p ^ p1),(q ^ q1) = n -BitGFA0Circ (p ^ p2),(q ^ q2) & n -BitGFA0CarryOutput (p ^ p1),(q ^ q1) = n -BitGFA0CarryOutput (p ^ p2),(q ^ q2) )
proof end;

theorem :: GFACIRC2:6
for n being Nat
for x, y being FinSeqLen of n
for a, b being set holds
( (n + 1) -BitGFA0Str (x ^ <*a*>),(y ^ <*b*>) = (n -BitGFA0Str x,y) +* (BitGFA0Str a,b,(n -BitGFA0CarryOutput x,y)) & (n + 1) -BitGFA0Circ (x ^ <*a*>),(y ^ <*b*>) = (n -BitGFA0Circ x,y) +* (BitGFA0Circ a,b,(n -BitGFA0CarryOutput x,y)) & (n + 1) -BitGFA0CarryOutput (x ^ <*a*>),(y ^ <*b*>) = GFA0CarryOutput a,b,(n -BitGFA0CarryOutput x,y) )
proof end;

theorem Th