:: GFACIRC2 semantic presentation begin 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 ) ; funcn -BitGFA0Str (x,y) -> non empty non void strict 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 non void strict 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 reconsider n = n as Nat ; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA0CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st ( S1 = 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 x being set st S = f . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & h . (n + 1) = H2(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st ( S2 = 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 x being set st S = f . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & h . (n + 1) = H2(x,n) ) ) ) holds S1 = S2 from CIRCCMB2:sch_9(); hence for b1, b2 being non empty non void strict 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 ; ::_thesis: verum end; existence ex b1 being non empty non void strict 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 reconsider n = n as Nat ; deffunc H1( set , Nat) -> ManySortedSign = BitGFA0Str ((x . ($2 + 1)),(y . ($2 + 1)),$1); deffunc H2( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA0CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st ( S = 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 x being set st S = f . n & x = h . n holds ( f . (n + 1) = S +* H1(x,n) & h . (n + 1) = H2(x,n) ) ) ) from CIRCCMB2:sch_8(A1); hence ex b1 being non empty non void strict 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) ) ) ) ; ::_thesis: verum end; end; :: deftheorem Def1 defines -BitGFA0Str GFACIRC2:def_1_:_ for n being Nat for x, y being FinSequence for b4 being non empty non void strict 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; funcn -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 over 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 over 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 over 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 set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set Sn = n -BitGFA0Str (x,y); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA0Str ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitGFA0Circ ((x . ($4 + 1)),(y . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA0CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); A1: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ; for A1, A2 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 & A1 = 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 over S for x being set st S = f . n & A = g . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = H3(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st ( n -BitGFA0Str (x,y) = f . n & A2 = 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 over S for x being set st S = f . n & A = g . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = H3(x,n) ) ) ) holds A1 = A2 from CIRCCMB2:sch_21(A1); hence 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 over 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 over 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 ; ::_thesis: verum 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 over 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 set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set Sn = n -BitGFA0Str (x,y); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA0Str ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitGFA0Circ ((x . ($4 + 1)),(y . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA0CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign for x being set for n being Nat holds ( H1(S,x,n) is unsplit & H1(S,x,n) is gate`1=arity & H1(S,x,n) is gate`2isBoolean & not H1(S,x,n) is void & H1(S,x,n) is strict ) ; A3: ex f, h being ManySortedSet of NAT st ( n -BitGFA0Str (x,y) = 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 x being set st S = f . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & h . (n + 1) = H3(x,n) ) ) ) by Def1; A4: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ; A5: for S, S1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign for A being strict gate`2=den Boolean Circuit of S for x being set for n being Nat st S1 = H1(S,x,n) holds H2(S,A,x,n) is strict gate`2=den Boolean Circuit of S1 ; ex A 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 & A = 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 over S for x being set st S = f . n & A = g . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = H3(x,n) ) ) ) from CIRCCMB2:sch_19(A2, A3, A4, A5); hence 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 over 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) ) ) ) ; ::_thesis: verum 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 over 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; funcn -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 set o0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; deffunc H1( Nat, set ) -> Element of InnerVertices (GFA0CarryStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = GFA0CarryOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2); let o1, o2 be Element of InnerVertices (n -BitGFA0Str (x,y)); ::_thesis: ( ex h being ManySortedSet of NAT st ( o1 = 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 ( o2 = 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)) ) ) implies o1 = o2 ) given h1 being ManySortedSet of NAT such that A1: o1 = h1 . n and A2: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A3: for n being Nat holds h1 . (n + 1) = H1(n,h1 . n) ; ::_thesis: ( for h being ManySortedSet of NAT holds ( not o2 = h . n or not h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] or ex n being Nat st not h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) or o1 = o2 ) given h2 being ManySortedSet of NAT such that A4: o2 = h2 . n and A5: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A6: for n being Nat holds h2 . (n + 1) = H1(n,h2 . n) ; ::_thesis: o1 = o2 A7: dom h1 = NAT by PARTFUN1:def_2; A8: dom h2 = NAT by PARTFUN1:def_2; h1 = h2 from NAT_1:sch_15(A7, A2, A3, A8, A5, A6); hence o1 = o2 by A1, A4; ::_thesis: verum 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 defpred S1[ set , set , set ] means verum; set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set Sn = n -BitGFA0Str (x,y); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA0CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); consider f, g being ManySortedSet of NAT such that A9: n -BitGFA0Str (x,y) = f . n and A10: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A11: g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A12: 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) = H1(S,z,n) & g . (n + 1) = H2(z,n) ) by Def1; defpred S2[ Nat] means ex S being non empty ManySortedSign st ( S = f . $1 & g . $1 in InnerVertices S ); InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by CIRCCOMB:42; then [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) by TARSKI:def_1; then A13: S2[ 0 ] by A10, A11; A14: for i being Nat st S2[i] holds S2[i + 1] proof let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] ) assume that A15: ex S being non empty ManySortedSign st ( S = f . i & g . i in InnerVertices S ) and A16: for S being non empty ManySortedSign st S = f . (i + 1) holds not g . (i + 1) in InnerVertices S ; ::_thesis: contradiction consider S being non empty ManySortedSign such that A17: S = f . i and g . i in InnerVertices S by A15; GFA0CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) in InnerVertices (BitGFA0Str ((x . (i + 1)),(y . (i + 1)),(g . i))) by GFACIRC1:37; then A18: GFA0CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) in InnerVertices (S +* (BitGFA0Str ((x . (i + 1)),(y . (i + 1)),(g . i)))) by FACIRC_1:22; A19: f . (i + 1) = S +* (BitGFA0Str ((x . (i + 1)),(y . (i + 1)),(g . i))) by A12, A17; g . (i + 1) = GFA0CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) by A12, A17; hence contradiction by A16, A18, A19; ::_thesis: verum end; for i being Nat holds S2[i] from NAT_1:sch_2(A13, A14); then ex S being non empty ManySortedSign st ( S = f . n & g . n in InnerVertices S ) ; then reconsider o = g . n as Element of InnerVertices (n -BitGFA0Str (x,y)) by A9; take o ; ::_thesis: ex h being ManySortedSet of NAT st ( o = 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)) ) ) take g ; ::_thesis: ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds g . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(g . n)) ) ) thus ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] ) by A11; ::_thesis: for n being Nat holds g . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(g . n)) let i be Nat; ::_thesis: g . (i + 1) = GFA0CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) A20: ex S being non empty ManySortedSign ex x being set st ( S = f . 0 & x = g . 0 & S1[S,x, 0 ] ) by A10; A21: for n being Nat for S being non empty ManySortedSign for x being set st S = f . n & x = g . n & S1[S,x,n] holds S1[H1(S,x,n),H2(x,n),n + 1] ; for n being Nat ex S being non empty ManySortedSign st ( S = f . n & S1[S,g . n,n] ) from CIRCCMB2:sch_2(A20, A12, A21); then ex S being non empty ManySortedSign st S = f . i ; hence g . (i + 1) = GFA0CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) by A12; ::_thesis: verum 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 over 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 let x, y be FinSequence; ::_thesis: 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 over 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 ) let f, g, h be ManySortedSet of NAT ; ::_thesis: ( 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 over 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) ) ) implies for n being Nat holds ( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n & n -BitGFA0CarryOutput (x,y) = h . n ) ) set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA0Str ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitGFA0Circ ((x . ($4 + 1)),(y . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA0CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); deffunc H4( Nat, set ) -> Element of InnerVertices (GFA0CarryStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = GFA0CarryOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2); assume that A1: ( f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) ) and A2: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A3: 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) = H1(S,z,n) & g . (n + 1) = H2(S,A,z,n) & h . (n + 1) = H3(z,n) ) ; ::_thesis: for n being Nat holds ( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n & n -BitGFA0CarryOutput (x,y) = h . n ) let n be Nat; ::_thesis: ( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n & n -BitGFA0CarryOutput (x,y) = h . n ) consider f1, g1, h1 being ManySortedSet of NAT such that A4: n -BitGFA0Str (x,y) = f1 . n and A5: n -BitGFA0Circ (x,y) = g1 . n and A6: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A7: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A8: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A9: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds ( f1 . (n + 1) = H1(S,z,n) & g1 . (n + 1) = H2(S,A,z,n) & h1 . (n + 1) = H3(z,n) ) by Def2; A10: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st ( S = f . 0 & A = g . 0 ) by A1; A11: ( f . 0 = f1 . 0 & g . 0 = g1 . 0 & h . 0 = h1 . 0 ) by A1, A2, A6, A7, A8; A12: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set for n being Nat holds H2(S,A,z,n) is non-empty MSAlgebra over H1(S,z,n) ; ( f = f1 & g = g1 & h = h1 ) from CIRCCMB2:sch_14(A10, A11, A3, A9, A12); hence ( n -BitGFA0Str (x,y) = f . n & n -BitGFA0Circ (x,y) = g . n ) by A4, A5; ::_thesis: n -BitGFA0CarryOutput (x,y) = h . n A13: 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) = H1(S,z,n) & h . (n + 1) = H3(z,n) ) from CIRCCMB2:sch_15(A1, A3, A12); A14: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by A1; A15: for n being Nat for z being set st z = h . n holds h . (n + 1) = H3(z,n) from CIRCCMB2:sch_3(A14, A13); A16: dom h = NAT by PARTFUN1:def_2; A17: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by A2; A18: for n being Nat holds h . (n + 1) = H4(n,h . n) by A15; consider h1 being ManySortedSet of NAT such that A19: n -BitGFA0CarryOutput (x,y) = h1 . n and A20: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A21: for n being Nat holds h1 . (n + 1) = H4(n,h1 . n) by Def3; A22: dom h1 = NAT by PARTFUN1:def_2; A23: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by A20; A24: for n being Nat holds h1 . (n + 1) = H4(n,h1 . n) by A21; h = h1 from NAT_1:sch_15(A16, A17, A18, A22, A23, A24); hence n -BitGFA0CarryOutput (x,y) = h . n by A19; ::_thesis: verum 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 let a, b be FinSequence; ::_thesis: ( 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)] ) set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; A1: ex f, g, h being ManySortedSet of NAT st ( 0 -BitGFA0Str (a,b) = f . 0 & 0 -BitGFA0Circ (a,b) = g . 0 & 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 over S for z being set st S = f . n & A = g . n & z = h . n holds ( f . (n + 1) = S +* (BitGFA0Str ((a . (n + 1)),(b . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA0Circ ((a . (n + 1)),(b . (n + 1)),z)) & h . (n + 1) = GFA0CarryOutput ((a . (n + 1)),(b . (n + 1)),z) ) ) ) by Def2; hence 0 -BitGFA0Str (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) ; ::_thesis: ( 0 -BitGFA0Circ (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & 0 -BitGFA0CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] ) thus 0 -BitGFA0Circ (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by A1; ::_thesis: 0 -BitGFA0CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] InnerVertices (0 -BitGFA0Str (a,b)) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by A1, CIRCCOMB:42; hence 0 -BitGFA0CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by TARSKI:def_1; ::_thesis: verum 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 set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; let a, b be FinSequence; ::_thesis: 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) ) let c be set ; ::_thesis: ( c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] implies ( 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) ) ) assume A1: c = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] ; ::_thesis: ( 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) ) consider f, g, h being ManySortedSet of NAT such that A2: 1 -BitGFA0Str (a,b) = f . 1 and A3: 1 -BitGFA0Circ (a,b) = g . 1 and A4: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A5: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A6: h . 0 = c and A7: 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 +* (BitGFA0Str ((a . (n + 1)),(b . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA0Circ ((a . (n + 1)),(b . (n + 1)),z)) & h . (n + 1) = GFA0CarryOutput ((a . (n + 1)),(b . (n + 1)),z) ) by A1, Def2; 1 -BitGFA0CarryOutput (a,b) = h . (0 + 1) by A1, A4, A5, A6, A7, Th1; hence ( 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) ) by A2, A3, A4, A5, A6, A7; ::_thesis: verum 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 let a, b be set ; ::_thesis: for 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) ) A1: <*a*> . 1 = a by FINSEQ_1:40; <*b*> . 1 = b by FINSEQ_1:40; hence for 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) ) by A1, Th3; ::_thesis: verum 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 let n be Nat; ::_thesis: 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)) ) let p, q be FinSeqLen of n; ::_thesis: 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)) ) let p1, p2, q1, q2 be FinSequence; ::_thesis: ( 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)) ) set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; set Sn1 = n -BitGFA0Str ((p ^ p1),(q ^ q1)); set An1 = n -BitGFA0Circ ((p ^ p1),(q ^ q1)); set On1 = n -BitGFA0CarryOutput ((p ^ p1),(q ^ q1)); deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str (((p ^ p1) . ($3 + 1)),((q ^ q1) . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA0Str (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)) = $2 +* (BitGFA0Circ (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA0CarryStr (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1)) = GFA0CarryOutput (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1); consider f1, g1, h1 being ManySortedSet of NAT such that A1: n -BitGFA0Str ((p ^ p1),(q ^ q1)) = f1 . n and A2: n -BitGFA0Circ ((p ^ p1),(q ^ q1)) = g1 . n and A3: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A4: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A5: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A6: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds ( f1 . (n + 1) = H1(S,z,n) & g1 . (n + 1) = H2(S,A,z,n) & h1 . (n + 1) = H3(z,n) ) by Def2; set Sn2 = n -BitGFA0Str ((p ^ p2),(q ^ q2)); set An2 = n -BitGFA0Circ ((p ^ p2),(q ^ q2)); set On2 = n -BitGFA0CarryOutput ((p ^ p2),(q ^ q2)); deffunc H4( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA0Str (((p ^ p2) . ($3 + 1)),((q ^ q2) . ($3 + 1)),$2)); deffunc H5( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA0Str (((p ^ p2) . ($4 + 1)),((q ^ q2) . ($4 + 1)),$3)) = $2 +* (BitGFA0Circ (((p ^ p2) . ($4 + 1)),((q ^ q2) . ($4 + 1)),$3)); deffunc H6( set , Nat) -> Element of InnerVertices (GFA0CarryStr (((p ^ p2) . ($2 + 1)),((q ^ q2) . ($2 + 1)),$1)) = GFA0CarryOutput (((p ^ p2) . ($2 + 1)),((q ^ q2) . ($2 + 1)),$1); consider f2, g2, h2 being ManySortedSet of NAT such that A7: n -BitGFA0Str ((p ^ p2),(q ^ q2)) = f2 . n and A8: n -BitGFA0Circ ((p ^ p2),(q ^ q2)) = g2 . n and A9: f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A10: g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A12: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f2 . n & A = g2 . n & z = h2 . n holds ( f2 . (n + 1) = H4(S,z,n) & g2 . (n + 1) = H5(S,A,z,n) & h2 . (n + 1) = H6(z,n) ) by Def2; defpred S1[ Nat] means ( $1 <= n implies ( h1 . $1 = h2 . $1 & f1 . $1 = f2 . $1 & g1 . $1 = g2 . $1 ) ); A13: S1[ 0 ] by A3, A4, A5, A9, A10, A11; A14: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that A15: ( i <= n implies ( h1 . i = h2 . i & f1 . i = f2 . i & g1 . i = g2 . i ) ) and A16: i + 1 <= n ; ::_thesis: ( h1 . (i + 1) = h2 . (i + 1) & f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) ) A17: len p = n by CARD_1:def_7; A18: len q = n by CARD_1:def_7; A19: dom p = Seg n by A17, FINSEQ_1:def_3; A20: dom q = Seg n by A18, FINSEQ_1:def_3; 0 + 1 <= i + 1 by XREAL_1:6; then A21: i + 1 in Seg n by A16, FINSEQ_1:1; then A22: (p ^ p1) . (i + 1) = p . (i + 1) by A19, FINSEQ_1:def_7; A23: (p ^ p2) . (i + 1) = p . (i + 1) by A19, A21, FINSEQ_1:def_7; A24: (q ^ q1) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def_7; A25: (q ^ q2) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def_7; defpred S2[ set , set , set , set ] means verum; A26: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st ( S = f1 . 0 & A = g1 . 0 & x = h1 . 0 & S2[S,A,x, 0 ] ) by A3, A4; A27: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set st S = f1 . n & A = g1 . n & x = h1 . n & S2[S,A,x,n] holds S2[H1(S,x,n),H2(S,A,x,n),H3(x,n),n + 1] ; A28: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ; for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st ( S = f1 . n & A = g1 . n & S2[S,A,h1 . n,n] ) from CIRCCMB2:sch_13(A26, A6, A27, A28); then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that A29: S = f1 . i and A30: A = g1 . i ; thus h1 . (i + 1) = H6(h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13 .= h2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: ( f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) ) thus f1 . (i + 1) = H4(S,h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13 .= f2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: g1 . (i + 1) = g2 . (i + 1) thus g1 . (i + 1) = H5(S,A,h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13 .= g2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: verum end; A31: for i being Nat holds S1[i] from NAT_1:sch_2(A13, A14); hence ( n -BitGFA0Str ((p ^ p1),(q ^ q1)) = n -BitGFA0Str ((p ^ p2),(q ^ q2)) & n -BitGFA0Circ ((p ^ p1),(q ^ q1)) = n -BitGFA0Circ ((p ^ p2),(q ^ q2)) ) by A1, A2, A7, A8; ::_thesis: n -BitGFA0CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA0CarryOutput ((p ^ p2),(q ^ q2)) A32: n -BitGFA0CarryOutput ((p ^ p1),(q ^ q1)) = h1 . n by A3, A4, A5, A6, Th1; n -BitGFA0CarryOutput ((p ^ p2),(q ^ q2)) = h2 . n by A9, A10, A11, A12, Th1; hence n -BitGFA0CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA0CarryOutput ((p ^ p2),(q ^ q2)) by A31, A32; ::_thesis: verum 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 set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; let n be Nat; ::_thesis: 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))) ) let x, y be FinSeqLen of n; ::_thesis: 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))) ) let a, b be set ; ::_thesis: ( (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))) ) set p = x ^ <*a*>; set q = y ^ <*b*>; consider f, g, h being ManySortedSet of NAT such that A1: n -BitGFA0Str ((x ^ <*a*>),(y ^ <*b*>)) = f . n and A2: n -BitGFA0Circ ((x ^ <*a*>),(y ^ <*b*>)) = g . n and A3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A4: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A5: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A6: 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 +* (BitGFA0Str (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA0Circ (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & h . (n + 1) = GFA0CarryOutput (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z) ) by Def2; A7: n -BitGFA0CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = h . n by A3, A4, A5, A6, Th1; A8: (n + 1) -BitGFA0Str ((x ^ <*a*>),(y ^ <*b*>)) = f . (n + 1) by A3, A4, A5, A6, Th1; A9: (n + 1) -BitGFA0Circ ((x ^ <*a*>),(y ^ <*b*>)) = g . (n + 1) by A3, A4, A5, A6, Th1; A10: (n + 1) -BitGFA0CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = h . (n + 1) by A3, A4, A5, A6, Th1; A11: len x = n by CARD_1:def_7; A12: len y = n by CARD_1:def_7; A13: (x ^ <*a*>) . (n + 1) = a by A11, FINSEQ_1:42; A14: (y ^ <*b*>) . (n + 1) = b by A12, FINSEQ_1:42; A15: x ^ <*> = x by FINSEQ_1:34; A16: y ^ <*> = y by FINSEQ_1:34; then A17: n -BitGFA0Str ((x ^ <*a*>),(y ^ <*b*>)) = n -BitGFA0Str (x,y) by A15, Th5; A18: n -BitGFA0Circ ((x ^ <*a*>),(y ^ <*b*>)) = n -BitGFA0Circ (x,y) by A15, A16, Th5; n -BitGFA0CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = n -BitGFA0CarryOutput (x,y) by A15, A16, Th5; hence ( (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))) ) by A1, A2, A6, A7, A8, A9, A10, A13, A14, A17, A18; ::_thesis: verum end; theorem Th7: :: GFACIRC2:7 for n being Nat for x, y being FinSequence holds ( (n + 1) -BitGFA0Str (x,y) = (n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0Circ (x,y) = (n -BitGFA0Circ (x,y)) +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0CarryOutput (x,y) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) ) proof set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; let n be Nat; ::_thesis: for x, y being FinSequence holds ( (n + 1) -BitGFA0Str (x,y) = (n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0Circ (x,y) = (n -BitGFA0Circ (x,y)) +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0CarryOutput (x,y) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) ) let x, y be FinSequence; ::_thesis: ( (n + 1) -BitGFA0Str (x,y) = (n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0Circ (x,y) = (n -BitGFA0Circ (x,y)) +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0CarryOutput (x,y) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) ) consider f, g, h being ManySortedSet of NAT such that A1: n -BitGFA0Str (x,y) = f . n and A2: n -BitGFA0Circ (x,y) = g . n and A3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A4: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A5: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A6: 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 +* (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) ) by Def2; A7: n -BitGFA0CarryOutput (x,y) = h . n by A3, A4, A5, A6, Th1; A8: (n + 1) -BitGFA0Str (x,y) = f . (n + 1) by A3, A4, A5, A6, Th1; A9: (n + 1) -BitGFA0Circ (x,y) = g . (n + 1) by A3, A4, A5, A6, Th1; (n + 1) -BitGFA0CarryOutput (x,y) = h . (n + 1) by A3, A4, A5, A6, Th1; hence ( (n + 1) -BitGFA0Str (x,y) = (n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0Circ (x,y) = (n -BitGFA0Circ (x,y)) +* (BitGFA0Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))) & (n + 1) -BitGFA0CarryOutput (x,y) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) ) by A1, A2, A6, A7, A8, A9; ::_thesis: verum end; theorem Th8: :: GFACIRC2:8 for n, m being Nat st n <= m holds for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y)) proof let n, m be Nat; ::_thesis: ( n <= m implies for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y)) ) assume A1: n <= m ; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y)) let x, y be FinSequence; ::_thesis: InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y)) consider i being Nat such that A2: m = n + i by A1, NAT_1:10; defpred S1[ Nat] means InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices ((n + $1) -BitGFA0Str (x,y)); A3: S1[ 0 ] ; A4: for j being Nat st S1[j] holds S1[j + 1] proof let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] ) set Sn = n -BitGFA0Str (x,y); set Snj = (n + j) -BitGFA0Str (x,y); set SSnj = BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y))); assume A5: InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices ((n + j) -BitGFA0Str (x,y)) ; ::_thesis: S1[j + 1] A6: InnerVertices (n -BitGFA0Str (x,y)) c= (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y))))) by XBOOLE_1:7; (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y))))) c= (InnerVertices ((n + j) -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y))))) by A5, XBOOLE_1:9; then InnerVertices (n -BitGFA0Str (x,y)) c= (InnerVertices ((n + j) -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y))))) by A6, XBOOLE_1:1; then InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (((n + j) -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y))))) by FACIRC_1:27; hence S1[j + 1] by Th7; ::_thesis: verum end; for j being Nat holds S1[j] from NAT_1:sch_2(A3, A4); hence InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y)) by A2; ::_thesis: verum end; theorem :: GFACIRC2:9 for n being Nat for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA0Str (x,y)) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) proof let n be Nat; ::_thesis: for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA0Str (x,y)) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) let x, y be FinSequence; ::_thesis: InnerVertices ((n + 1) -BitGFA0Str (x,y)) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) set Sn = n -BitGFA0Str (x,y); set SSn = BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))); InnerVertices ((n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) by FACIRC_1:27; hence InnerVertices ((n + 1) -BitGFA0Str (x,y)) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) by Th7; ::_thesis: verum end; definition let k, n be Nat; assume that B1: k >= 1 and B2: k <= n ; let x, y be FinSequence; func(k,n) -BitGFA0AdderOutput (x,y) -> Element of InnerVertices (n -BitGFA0Str (x,y)) means :Def4: :: GFACIRC2:def 4 ex i being Nat st ( k = i + 1 & it = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ); uniqueness for b1, b2 being Element of InnerVertices (n -BitGFA0Str (x,y)) st ex i being Nat st ( k = i + 1 & b1 = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ) & ex i being Nat st ( k = i + 1 & b2 = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ) holds b1 = b2 ; existence ex b1 being Element of InnerVertices (n -BitGFA0Str (x,y)) ex i being Nat st ( k = i + 1 & b1 = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ) proof consider i being Nat such that A1: k = 1 + i by B1, NAT_1:10; reconsider i = i as Nat ; deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA0Str (x,y); deffunc H2( Nat) -> ManySortedSign = BitGFA0Str ((x . ($1 + 1)),(y . ($1 + 1)),($1 -BitGFA0CarryOutput (x,y))); set o = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))); A2: InnerVertices H1(k) c= InnerVertices H1(n) by B2, Th8; A3: GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) in InnerVertices H2(i) by A1, GFACIRC1:37; A4: H1(k) = H1(i) +* H2(i) by A1, Th7; reconsider o = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) as Element of H2(i) by A3; the carrier of H1(k) = the carrier of H2(i) \/ the carrier of H1(i) by A4, CIRCCOMB:def_2; then o in the carrier of H1(k) by XBOOLE_0:def_3; then o in InnerVertices H1(k) by A3, A4, CIRCCOMB:15; hence ex b1 being Element of InnerVertices (n -BitGFA0Str (x,y)) ex i being Nat st ( k = i + 1 & b1 = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ) by A1, A2; ::_thesis: verum end; end; :: deftheorem Def4 defines -BitGFA0AdderOutput GFACIRC2:def_4_:_ for k, n being Nat st k >= 1 & k <= n holds for x, y being FinSequence for b5 being Element of InnerVertices (n -BitGFA0Str (x,y)) holds ( b5 = (k,n) -BitGFA0AdderOutput (x,y) iff ex i being Nat st ( k = i + 1 & b5 = GFA0AdderOutput ((x . k),(y . k),(i -BitGFA0CarryOutput (x,y))) ) ); theorem :: GFACIRC2:10 for n, k being Nat st k < n holds for x, y being FinSequence holds ((k + 1),n) -BitGFA0AdderOutput (x,y) = GFA0AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput (x,y))) proof let n, k be Nat; ::_thesis: ( k < n implies for x, y being FinSequence holds ((k + 1),n) -BitGFA0AdderOutput (x,y) = GFA0AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput (x,y))) ) assume A1: k < n ; ::_thesis: for x, y being FinSequence holds ((k + 1),n) -BitGFA0AdderOutput (x,y) = GFA0AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput (x,y))) let x, y be FinSequence; ::_thesis: ((k + 1),n) -BitGFA0AdderOutput (x,y) = GFA0AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput (x,y))) A2: k + 1 >= 1 by NAT_1:11; k + 1 <= n by A1, NAT_1:13; then ex i being Nat st ( k + 1 = i + 1 & ((k + 1),n) -BitGFA0AdderOutput (x,y) = GFA0AdderOutput ((x . (k + 1)),(y . (k + 1)),(i -BitGFA0CarryOutput (x,y))) ) by A2, Def4; hence ((k + 1),n) -BitGFA0AdderOutput (x,y) = GFA0AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput (x,y))) ; ::_thesis: verum end; theorem :: GFACIRC2:11 for n being Nat for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) is Relation proof let n be Nat; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) is Relation let x, y be FinSequence; ::_thesis: InnerVertices (n -BitGFA0Str (x,y)) is Relation set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA0Str (x,y); deffunc H2( Nat) -> ManySortedSign = BitGFA0Str ((x . ($1 + 1)),(y . ($1 + 1)),($1 -BitGFA0CarryOutput (x,y))); defpred S1[ Nat] means InnerVertices H1($1) is Relation; H1( 0 ) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by Th2; then A1: S1[ 0 ] by FACIRC_1:38; A2: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_ S1[i_+_1] let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: S1[i] ; ::_thesis: S1[i + 1] A4: H1(i + 1) = H1(i) +* H2(i) by Th7; InnerVertices H2(i) is Relation by GFACIRC1:32; hence S1[i + 1] by A3, A4, FACIRC_1:3; ::_thesis: verum end; for i being Nat holds S1[i] from NAT_1:sch_2(A1, A2); hence InnerVertices (n -BitGFA0Str (x,y)) is Relation ; ::_thesis: verum end; registration let n be Nat; let x, y be FinSequence; clustern -BitGFA0CarryOutput (x,y) -> pair ; coherence n -BitGFA0CarryOutput (x,y) is pair proof set f1 = and2 ; set f2 = and2 ; set f3 = and2 ; set f4 = or3 ; set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; deffunc H1( Nat) -> Element of InnerVertices (n -BitGFA0Str (x,y)) = n -BitGFA0CarryOutput (x,y); A1: ex h being ManySortedSet of NAT st ( H1( 0 ) = h . 0 & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] & ( for n being Nat holds h . (n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) by Def3; defpred S1[ Nat] means n -BitGFA0CarryOutput (x,y) is pair ; A2: S1[ 0 ] by A1; A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) set c = n -BitGFA0CarryOutput (x,y); H1(n + 1) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) by Th7 .= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2],[<*(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))*>,and2],[<*(n -BitGFA0CarryOutput (x,y)),(x . (n + 1))*>,and2]*>,or3] ; hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3); hence n -BitGFA0CarryOutput (x,y) is pair ; ::_thesis: verum end; end; Lm1: for x, y being FinSequence for n being Nat holds ( ( (n -BitGFA0CarryOutput (x,y)) `1 = <*> & (n -BitGFA0CarryOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> FALSE & proj1 ((n -BitGFA0CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitGFA0CarryOutput (x,y)) `1) = 3 & (n -BitGFA0CarryOutput (x,y)) `2 = or3 & proj1 ((n -BitGFA0CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) ) proof set f1 = and2 ; set f2 = and2 ; set f3 = and2 ; set f4 = or3 ; let x, y be FinSequence; ::_thesis: for n being Nat holds ( ( (n -BitGFA0CarryOutput (x,y)) `1 = <*> & (n -BitGFA0CarryOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> FALSE & proj1 ((n -BitGFA0CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitGFA0CarryOutput (x,y)) `1) = 3 & (n -BitGFA0CarryOutput (x,y)) `2 = or3 & proj1 ((n -BitGFA0CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) ) defpred S1[ Nat] means ( ( ($1 -BitGFA0CarryOutput (x,y)) `1 = <*> & ($1 -BitGFA0CarryOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> FALSE & proj1 (($1 -BitGFA0CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card (($1 -BitGFA0CarryOutput (x,y)) `1) = 3 & ($1 -BitGFA0CarryOutput (x,y)) `2 = or3 & proj1 (($1 -BitGFA0CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) ); A1: dom ((0 -tuples_on BOOLEAN) --> FALSE) = 0 -tuples_on BOOLEAN by FUNCOP_1:13; 0 -BitGFA0CarryOutput (x,y) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by Th2; then A2: S1[ 0 ] by A1, MCART_1:7; A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] set c = n -BitGFA0CarryOutput (x,y); A4: (n + 1) -BitGFA0CarryOutput (x,y) = GFA0CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))) by Th7 .= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2],[<*(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))*>,and2],[<*(n -BitGFA0CarryOutput (x,y)),(x . (n + 1))*>,and2]*>,or3] ; A5: dom or3 = 3 -tuples_on BOOLEAN by FUNCT_2:def_1; ((n + 1) -BitGFA0CarryOutput (x,y)) `1 = <*[<*(x . (n + 1)),(y . (n + 1))*>,and2],[<*(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))*>,and2],[<*(n -BitGFA0CarryOutput (x,y)),(x . (n + 1))*>,and2]*> by A4, MCART_1:7; hence S1[n + 1] by A4, A5, FINSEQ_1:45, MCART_1:7; ::_thesis: verum end; thus for i being Nat holds S1[i] from NAT_1:sch_2(A2, A3); ::_thesis: verum end; Lm2: for n being Nat for x, y being FinSequence for p being set for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA0CarryOutput (x,y) <> [p,f] proof let n be Nat; ::_thesis: for x, y being FinSequence for p being set for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA0CarryOutput (x,y) <> [p,f] let x, y be FinSequence; ::_thesis: for p being set for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA0CarryOutput (x,y) <> [p,f] let p be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA0CarryOutput (x,y) <> [p,f] let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: n -BitGFA0CarryOutput (x,y) <> [p,f] dom f = 2 -tuples_on BOOLEAN by FUNCT_2:def_1; then A1: proj1 ([p,f] `2) = 2 -tuples_on BOOLEAN ; ( proj1 ((n -BitGFA0CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN or proj1 ((n -BitGFA0CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) by Lm1; hence n -BitGFA0CarryOutput (x,y) <> [p,f] by A1, FINSEQ_2:110; ::_thesis: verum end; theorem Th12: :: GFACIRC2:12 for f, g being nonpair-yielding FinSequence for n being Nat holds ( InputVertices ((n + 1) -BitGFA0Str (f,g)) = (InputVertices (n -BitGFA0Str (f,g))) \/ ((InputVertices (BitGFA0Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA0CarryOutput (f,g))))) \ {(n -BitGFA0CarryOutput (f,g))}) & InnerVertices (n -BitGFA0Str (f,g)) is Relation & InputVertices (n -BitGFA0Str (f,g)) is without_pairs ) proof set f1 = and2 ; set f2 = and2 ; set f3 = and2 ; set f0 = xor2 ; let f, g be nonpair-yielding FinSequence; ::_thesis: for n being Nat holds ( InputVertices ((n + 1) -BitGFA0Str (f,g)) = (InputVertices (n -BitGFA0Str (f,g))) \/ ((InputVertices (BitGFA0Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA0CarryOutput (f,g))))) \ {(n -BitGFA0CarryOutput (f,g))}) & InnerVertices (n -BitGFA0Str (f,g)) is Relation & InputVertices (n -BitGFA0Str (f,g)) is without_pairs ) deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA0Str (f,g); deffunc H2( set , Nat) -> ManySortedSign = BitGFA0Str ((f . ($2 + 1)),(g . ($2 + 1)),$1); deffunc H3( Nat) -> Element of InnerVertices ($1 -BitGFA0Str (f,g)) = $1 -BitGFA0CarryOutput (f,g); consider h being ManySortedSet of NAT such that A1: for n being Element of NAT holds h . n = H3(n) from PBOOLE:sch_5(); deffunc H4( Nat) -> set = h . $1; deffunc H5( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = GFA0CarryOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1); set k = (0 -tuples_on BOOLEAN) --> FALSE; A2: H1( 0 ) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by Th2; then A3: InnerVertices H1( 0 ) is Relation by FACIRC_1:38; A4: InputVertices H1( 0 ) is without_pairs by A2, FACIRC_1:39; H4( 0 ) = H3( 0 ) by A1; then A5: h . 0 in InnerVertices H1( 0 ) ; A6: for n being Nat for x being set holds InnerVertices H2(x,n) is Relation by GFACIRC1:32; A7: now__::_thesis:_for_n_being_Nat for_x_being_set_st_x_=_H4(n)_holds_ InputVertices_H2(x,n)_=_{(f_._(n_+_1)),(g_._(n_+_1)),x} let n be Nat; ::_thesis: for x being set st x = H4(n) holds InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} let x be set ; ::_thesis: ( x = H4(n) implies InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} ) assume A8: x = H4(n) ; ::_thesis: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} n in NAT by ORDINAL1:def_12; then A9: H4(n) = H3(n) by A1; then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2] by A8, Lm2; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2] by A8, A9, Lm2; hence InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A10, GFACIRC1:33; ::_thesis: verum end; A11: for n being Nat for x being set st x = h . n holds (InputVertices H2(x,n)) \ {x} is without_pairs proof let n be Nat; ::_thesis: for x being set st x = h . n holds (InputVertices H2(x,n)) \ {x} is without_pairs let x be set ; ::_thesis: ( x = h . n implies (InputVertices H2(x,n)) \ {x} is without_pairs ) assume x = H4(n) ; ::_thesis: (InputVertices H2(x,n)) \ {x} is without_pairs then A12: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7; thus (InputVertices H2(x,n)) \ {x} is without_pairs ::_thesis: verum proof let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in (InputVertices H2(x,n)) \ {x} assume A13: a in (InputVertices H2(x,n)) \ {x} ; ::_thesis: contradiction then a in InputVertices H2(x,n) by XBOOLE_0:def_5; then A14: ( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A12, ENUMSET1:def_1; not a in {x} by A13, XBOOLE_0:def_5; hence contradiction by A14, TARSKI:def_1; ::_thesis: verum end; end; A15: now__::_thesis:_for_n_being_Nat for_S_being_non_empty_ManySortedSign_ for_x_being_set_st_S_=_H1(n)_&_x_=_h_._n_holds_ (_H1(n_+_1)_=_S_+*_H2(x,n)_&_h_._(n_+_1)_=_H5(x,n)_&_x_in_InputVertices_H2(x,n)_&_H5(x,n)_in_InnerVertices_H2(x,n)_) let n be Nat; ::_thesis: for S being non empty ManySortedSign for x being set st S = H1(n) & x = h . n holds ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) let S be non empty ManySortedSign ; ::_thesis: for x being set st S = H1(n) & x = h . n holds ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) let x be set ; ::_thesis: ( S = H1(n) & x = h . n implies ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) ) assume that A16: S = H1(n) and A17: x = h . n ; ::_thesis: ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) n in NAT by ORDINAL1:def_12; then A18: x = n -BitGFA0CarryOutput (f,g) by A1, A17; A19: H4(n + 1) = (n + 1) -BitGFA0CarryOutput (f,g) by A1; thus H1(n + 1) = S +* H2(x,n) by A16, A18, Th7; ::_thesis: ( h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) thus h . (n + 1) = H5(x,n) by A18, A19, Th7; ::_thesis: ( x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7, A17; hence x in InputVertices H2(x,n) by ENUMSET1:def_1; ::_thesis: H5(x,n) in InnerVertices H2(x,n) A20: InnerVertices H2(x,n) = (({[<*(f . (n + 1)),(g . (n + 1))*>,xor2]} \/ {(GFA0AdderOutput ((f . (n + 1)),(g . (n + 1)),x))}) \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2],[<*(g . (n + 1)),x*>,and2],[<*x,(f . (n + 1))*>,and2]}) \/ {(GFA0CarryOutput ((f . (n + 1)),(g . (n + 1)),x))} by GFACIRC1:31; H5(x,n) in {H5(x,n)} by TARSKI:def_1; hence H5(x,n) in InnerVertices H2(x,n) by A20, XBOOLE_0:def_3; ::_thesis: verum end; A21: for n being Nat holds ( InputVertices H1(n + 1) = (InputVertices H1(n)) \/ ((InputVertices H2(h . n,n)) \ {(h . n)}) & InnerVertices H1(n) is Relation & InputVertices H1(n) is without_pairs ) from CIRCCMB2:sch_11(A3, A4, A5, A6, A11, A15); let n be Nat; ::_thesis: ( InputVertices ((n + 1) -BitGFA0Str (f,g)) = (InputVertices (n -BitGFA0Str (f,g))) \/ ((InputVertices (BitGFA0Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA0CarryOutput (f,g))))) \ {(n -BitGFA0CarryOutput (f,g))}) & InnerVertices (n -BitGFA0Str (f,g)) is Relation & InputVertices (n -BitGFA0Str (f,g)) is without_pairs ) n in NAT by ORDINAL1:def_12; then h . n = n -BitGFA0CarryOutput (f,g) by A1; hence ( InputVertices ((n + 1) -BitGFA0Str (f,g)) = (InputVertices (n -BitGFA0Str (f,g))) \/ ((InputVertices (BitGFA0Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA0CarryOutput (f,g))))) \ {(n -BitGFA0CarryOutput (f,g))}) & InnerVertices (n -BitGFA0Str (f,g)) is Relation & InputVertices (n -BitGFA0Str (f,g)) is without_pairs ) by A21; ::_thesis: verum end; theorem :: GFACIRC2:13 for n being Nat for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitGFA0Str (x,y)) = (rng x) \/ (rng y) proof set f1 = and2 ; set f0 = xor2 ; defpred S1[ Nat] means for x, y being nonpair-yielding FinSeqLen of $1 holds InputVertices ($1 -BitGFA0Str (x,y)) = (rng x) \/ (rng y); A1: S1[ 0 ] proof let x, y be nonpair-yielding FinSeqLen of 0 ; ::_thesis: InputVertices (0 -BitGFA0Str (x,y)) = (rng x) \/ (rng y) set f = (0 -tuples_on BOOLEAN) --> FALSE; 0 -BitGFA0Str (x,y) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by Th2; hence InputVertices (0 -BitGFA0Str (x,y)) = rng <*> by CIRCCOMB:42 .= (rng x) \/ (rng y) ; ::_thesis: verum end; A2: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: S1[i] ; ::_thesis: S1[i + 1] A4: i in NAT by ORDINAL1:def_12; let x, y be nonpair-yielding FinSeqLen of i + 1; ::_thesis: InputVertices ((i + 1) -BitGFA0Str (x,y)) = (rng x) \/ (rng y) consider x9 being nonpair-yielding FinSeqLen of i, z1 being non pair set such that A5: x = x9 ^ <*z1*> by A4, FACIRC_2:34; consider y9 being nonpair-yielding FinSeqLen of i, z2 being non pair set such that A6: y = y9 ^ <*z2*> by A4, FACIRC_2:34; A7: 1 in Seg 1 by FINSEQ_1:1; then A8: 1 in dom <*z1*> by FINSEQ_1:def_8; len x9 = i by CARD_1:def_7; then A9: x . (i + 1) = <*z1*> . 1 by A5, A8, FINSEQ_1:def_7 .= z1 by FINSEQ_1:def_8 ; A10: 1 in dom <*z2*> by A7, FINSEQ_1:def_8; len y9 = i by CARD_1:def_7; then A11: y . (i + 1) = <*z2*> . 1 by A6, A10, FINSEQ_1:def_7 .= z2 by FINSEQ_1:def_8 ; deffunc H1( Nat) -> Element of InnerVertices ($1 -BitGFA0Str (x,y)) = $1 -BitGFA0CarryOutput (x,y); A12: {z1,z2,H1(i)} = {H1(i),z1,z2} by ENUMSET1:59; A13: rng x = (rng x9) \/ (rng <*z1*>) by A5, FINSEQ_1:31 .= (rng x9) \/ {z1} by FINSEQ_1:38 ; A14: rng y = (rng y9) \/ (rng <*z2*>) by A6, FINSEQ_1:31 .= (rng y9) \/ {z2} by FINSEQ_1:38 ; A15: H1(i) <> [<*z1,z2*>,and2] by Lm2; A16: H1(i) <> [<*z1,z2*>,xor2] by Lm2; A17: x9 = x9 ^ {} by FINSEQ_1:34; y9 = y9 ^ {} by FINSEQ_1:34; then i -BitGFA0Str (x,y) = i -BitGFA0Str (x9,y9) by A5, A6, A17, Th5; hence InputVertices ((i + 1) -BitGFA0Str (x,y)) = (InputVertices (i -BitGFA0Str (x9,y9))) \/ ((InputVertices (BitGFA0Str (z1,z2,H1(i)))) \ {H1(i)}) by A9, A11, Th12 .= ((rng x9) \/ (rng y9)) \/ ((InputVertices (BitGFA0Str (z1,z2,H1(i)))) \ {H1(i)}) by A3 .= ((rng x9) \/ (rng y9)) \/ ({z1,z2,H1(i)} \ {H1(i)}) by A15, A16, GFACIRC1:33 .= ((rng x9) \/ (rng y9)) \/ {z1,z2} by A12, ENUMSET1:86 .= ((rng x9) \/ (rng y9)) \/ ({z1} \/ {z2}) by ENUMSET1:1 .= (((rng x9) \/ (rng y9)) \/ {z1}) \/ {z2} by XBOOLE_1:4 .= (((rng x9) \/ {z1}) \/ (rng y9)) \/ {z2} by XBOOLE_1:4 .= (rng x) \/ (rng y) by A13, A14, XBOOLE_1:4 ; ::_thesis: verum end; thus for i being Nat holds S1[i] from NAT_1:sch_2(A1, A2); ::_thesis: verum end; theorem :: GFACIRC2:14 for n being Nat for x, y being nonpair-yielding FinSeqLen of n for s being State of (n -BitGFA0Circ (x,y)) holds Following (s,(1 + (2 * n))) is stable proof let n be Nat; ::_thesis: for x, y being nonpair-yielding FinSeqLen of n for s being State of (n -BitGFA0Circ (x,y)) holds Following (s,(1 + (2 * n))) is stable let f, g be nonpair-yielding FinSeqLen of n; ::_thesis: for s being State of (n -BitGFA0Circ (f,g)) holds Following (s,(1 + (2 * n))) is stable deffunc H1( set , Nat) -> ManySortedSign = BitGFA0Str ((f . ($2 + 1)),(g . ($2 + 1)),$1); deffunc H2( set , Nat) -> MSAlgebra over BitGFA0Str ((f . ($2 + 1)),(g . ($2 + 1)),$1) = BitGFA0Circ ((f . ($2 + 1)),(g . ($2 + 1)),$1); deffunc H3( set , Nat) -> Element of InnerVertices (GFA0CarryStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = GFA0CarryOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1); set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]; n in NAT by ORDINAL1:def_12; then consider N being Function of NAT,NAT such that A1: N . 0 = 1 and A2: N . 1 = 2 and A3: N . 2 = n by FACIRC_2:35; deffunc H4( Nat) -> Element of NAT = N . $1; A4: for x being set for n being Nat holds H2(x,n) is strict gate`2=den Boolean Circuit of H1(x,n) ; A5: now__::_thesis:_for_s_being_State_of_(1GateCircuit_(<*>,((0_-tuples_on_BOOLEAN)_-->_FALSE)))_holds_Following_(s,H4(_0_))_is_stable let s be State of (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))); ::_thesis: Following (s,H4( 0 )) is stable Following (s,1) = Following s by FACIRC_1:14; hence Following (s,H4( 0 )) is stable by A1, CIRCCMB2:2; ::_thesis: verum end; deffunc H5( Nat) -> Element of InnerVertices ($1 -BitGFA0Str (f,g)) = $1 -BitGFA0CarryOutput (f,g); consider h being ManySortedSet of NAT such that A6: for n being Element of NAT holds h . n = H5(n) from PBOOLE:sch_5(); A7: for n being Nat for x being set for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds for s being State of A holds Following (s,H4(1)) is stable proof set f1 = and2 ; set f0 = xor2 ; let n be Nat; ::_thesis: for x being set for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds for s being State of A holds Following (s,H4(1)) is stable let x be set ; ::_thesis: for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds for s being State of A holds Following (s,H4(1)) is stable let A be non-empty Circuit of H1(x,n); ::_thesis: ( x = h . n & A = H2(x,n) implies for s being State of A holds Following (s,H4(1)) is stable ) assume A8: x = h . n ; ::_thesis: ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable ) n in NAT by ORDINAL1:def_12; then A9: x = H5(n) by A6, A8; then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2] by Lm2; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2] by A9, Lm2; hence ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable ) by A2, A10, GFACIRC1:40; ::_thesis: verum end; set Sn = n -BitGFA0Str (f,g); set An = n -BitGFA0Circ (f,g); set o0 = 0 -BitGFA0CarryOutput (f,g); consider f1, g1, h1 being ManySortedSet of NAT such that A11: n -BitGFA0Str (f,g) = f1 . n and A12: n -BitGFA0Circ (f,g) = g1 . n and A13: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A14: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and A15: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and A16: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds ( f1 . (n + 1) = S +* H1(z,n) & g1 . (n + 1) = A +* H2(z,n) & h1 . (n + 1) = H3(z,n) ) by Def2; now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_ h1_._i_=_h_._i let i be set ; ::_thesis: ( i in NAT implies h1 . i = h . i ) assume A17: i in NAT ; ::_thesis: h1 . i = h . i then reconsider j = i as Nat ; thus h1 . i = H5(j) by A13, A14, A15, A16, Th1 .= h . i by A6, A17 ; ::_thesis: verum end; then A18: h1 = h by PBOOLE:3; A19: ex u, v being ManySortedSet of NAT st ( n -BitGFA0Str (f,g) = u . H4(2) & n -BitGFA0Circ (f,g) = v . H4(2) & u . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitGFA0CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = u . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds ( u . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) proof take f1 ; ::_thesis: ex v being ManySortedSet of NAT st ( n -BitGFA0Str (f,g) = f1 . H4(2) & n -BitGFA0Circ (f,g) = v . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitGFA0CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds ( f1 . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) take g1 ; ::_thesis: ( n -BitGFA0Str (f,g) = f1 . H4(2) & n -BitGFA0Circ (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitGFA0CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds ( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) thus ( n -BitGFA0Str (f,g) = f1 . H4(2) & n -BitGFA0Circ (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) & h . 0 = 0 -BitGFA0CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds ( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) by A3, A6, A11, A12, A13, A14, A16, A18; ::_thesis: verum end; A20: ( InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is Relation & InputVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) is without_pairs ) by FACIRC_1:38, FACIRC_1:39; A21: 0 -BitGFA0CarryOutput (f,g) = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] by Th2; InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) = {[<*>,((0 -tuples_on BOOLEAN) --> FALSE)]} by CIRCCOMB:42; then A22: ( h . 0 = 0 -BitGFA0CarryOutput (f,g) & 0 -BitGFA0CarryOutput (f,g) in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) ) by A6, A21, TARSKI:def_1; A23: for n being Nat for x being set holds InnerVertices H1(x,n) is Relation by GFACIRC1:32; A24: for n being Nat for x being set st x = h . n holds (InputVertices H1(x,n)) \ {x} is without_pairs proof set f1 = and2 ; set f0 = xor2 ; let n be Nat; ::_thesis: for x being set st x = h . n holds (InputVertices H1(x,n)) \ {x} is without_pairs let x be set ; ::_thesis: ( x = h . n implies (InputVertices H1(x,n)) \ {x} is without_pairs ) assume A25: x = h . n ; ::_thesis: (InputVertices H1(x,n)) \ {x} is without_pairs n in NAT by ORDINAL1:def_12; then A26: x = H5(n) by A6, A25; then A27: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2] by Lm2; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2] by A26, Lm2; then A28: InputVertices H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A27, GFACIRC1:33; let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in (InputVertices H1(x,n)) \ {x} assume A29: a in (InputVertices H1(x,n)) \ {x} ; ::_thesis: contradiction then A30: a in {(f . (n + 1)),(g . (n + 1)),x} by A28, XBOOLE_0:def_5; A31: not a in {x} by A29, XBOOLE_0:def_5; ( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A30, ENUMSET1:def_1; hence contradiction by A31, TARSKI:def_1; ::_thesis: verum end; A32: for n being Nat for x being set st x = h . n holds ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) proof set f1 = and2 ; set f2 = and2 ; set f3 = and2 ; set f0 = xor2 ; let n be Nat; ::_thesis: for x being set st x = h . n holds ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) let x be set ; ::_thesis: ( x = h . n implies ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) ) assume A33: x = h . n ; ::_thesis: ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) n in NAT by ORDINAL1:def_12; then A34: x = H5(n) by A6, A33; h . (n + 1) = H5(n + 1) by A6; hence h . (n + 1) = H3(x,n) by A34, Th7; ::_thesis: ( x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) A35: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2] by A34, Lm2; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2] by A34, Lm2; then InputVertices H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A35, GFACIRC1:33; hence x in InputVertices H1(x,n) by ENUMSET1:def_1; ::_thesis: H3(x,n) in InnerVertices H1(x,n) A36: InnerVertices H1(x,n) = (({[<*(f . (n + 1)),(g . (n + 1))*>,xor2]} \/ {(GFA0AdderOutput ((f . (n + 1)),(g . (n + 1)),x))}) \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2],[<*(g . (n + 1)),x*>,and2],[<*x,(f . (n + 1))*>,and2]}) \/ {(GFA0CarryOutput ((f . (n + 1)),(g . (n + 1)),x))} by GFACIRC1:31; H3(x,n) in {H3(x,n)} by TARSKI:def_1; hence H3(x,n) in InnerVertices H1(x,n) by A36, XBOOLE_0:def_3; ::_thesis: verum end; for s being State of (n -BitGFA0Circ (f,g)) holds Following (s,(H4( 0 ) + (H4(2) * H4(1)))) is stable from CIRCCMB2:sch_22(A4, A5, A7, A19, A20, A22, A23, A24, A32); hence for s being State of (n -BitGFA0Circ (f,g)) holds Following (s,(1 + (2 * n))) is stable by A1, A2, A3; ::_thesis: verum end; begin definition let n be Nat; let x, y be FinSequence; A1: ( 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is unsplit & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is gate`1=arity & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is gate`2isBoolean & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is void & not 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is empty & 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) is strict ) ; funcn -BitGFA1Str (x,y) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def5: :: GFACIRC2:def 5 ex f, h being ManySortedSet of NAT st ( it = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ); uniqueness for b1, b2 being non empty non void strict 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) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((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) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds b1 = b2 proof reconsider n = n as Nat ; set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA1CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st ( S1 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat for S being non empty ManySortedSign for x being set st S = f . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & h . (n + 1) = H2(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st ( S2 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat for S being non empty ManySortedSign for x being set st S = f . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & h . (n + 1) = H2(x,n) ) ) ) holds S1 = S2 from CIRCCMB2:sch_9(); hence for b1, b2 being non empty non void strict 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) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((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) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds b1 = b2 ; ::_thesis: verum end; existence ex b1 being non empty non void strict 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) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) proof reconsider n = n as Nat ; set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( set , Nat) -> ManySortedSign = BitGFA1Str ((x . ($2 + 1)),(y . ($2 + 1)),$1); deffunc H2( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA1CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st ( S = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat for S being non empty ManySortedSign for x being set st S = f . n & x = h . n holds ( f . (n + 1) = S +* H1(x,n) & h . (n + 1) = H2(x,n) ) ) ) from CIRCCMB2:sch_8(A1); hence ex b1 being non empty non void strict 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) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) ; ::_thesis: verum end; end; :: deftheorem Def5 defines -BitGFA1Str GFACIRC2:def_5_:_ for n being Nat for x, y being FinSequence for b4 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign holds ( b4 = n -BitGFA1Str (x,y) iff ex f, h being ManySortedSet of NAT st ( b4 = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) ); definition let n be Nat; let x, y be FinSequence; funcn -BitGFA1Circ (x,y) -> strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) means :Def6: :: GFACIRC2:def 6 ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & it = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ); uniqueness for b1, b2 being strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) st ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) & ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & b2 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds b1 = b2 proof set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set Sn = n -BitGFA1Str (x,y); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitGFA1Circ ((x . ($4 + 1)),(y . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA1CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); A1: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ; for A1, A2 being strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) st ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & A1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set st S = f . n & A = g . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = H3(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & A2 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set st S = f . n & A = g . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = H3(x,n) ) ) ) holds A1 = A2 from CIRCCMB2:sch_21(A1); hence for b1, b2 being strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) st ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) & ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & b2 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) holds b1 = b2 ; ::_thesis: verum end; existence ex b1 being strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) proof set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set Sn = n -BitGFA1Str (x,y); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitGFA1Circ ((x . ($4 + 1)),(y . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA1CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign for x being set for n being Nat holds ( H1(S,x,n) is unsplit & H1(S,x,n) is gate`1=arity & H1(S,x,n) is gate`2isBoolean & not H1(S,x,n) is void & H1(S,x,n) is strict ) ; A3: ex f, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat for S being non empty ManySortedSign for x being set st S = f . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & h . (n + 1) = H3(x,n) ) ) ) by Def5; A4: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ; A5: for S, S1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign for A being strict gate`2=den Boolean Circuit of S for x being set for n being Nat st S1 = H1(S,x,n) holds H2(S,A,x,n) is strict gate`2=den Boolean Circuit of S1 ; ex A being strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & A = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set st S = f . n & A = g . n & x = h . n holds ( f . (n + 1) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = H3(x,n) ) ) ) from CIRCCMB2:sch_19(A2, A3, A4, A5); hence ex b1 being strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & b1 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) ; ::_thesis: verum end; end; :: deftheorem Def6 defines -BitGFA1Circ GFACIRC2:def_6_:_ for n being Nat for x, y being FinSequence for b4 being strict gate`2=den Boolean Circuit of n -BitGFA1Str (x,y) holds ( b4 = n -BitGFA1Circ (x,y) iff ex f, g, h being ManySortedSet of NAT st ( n -BitGFA1Str (x,y) = f . n & b4 = g . n & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) ) ); definition let n be Nat; let x, y be FinSequence; funcn -BitGFA1CarryOutput (x,y) -> Element of InnerVertices (n -BitGFA1Str (x,y)) means :Def7: :: GFACIRC2:def 7 ex h being ManySortedSet of NAT st ( it = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ); uniqueness for b1, b2 being Element of InnerVertices (n -BitGFA1Str (x,y)) st ex h being ManySortedSet of NAT st ( b1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) & ex h being ManySortedSet of NAT st ( b2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) holds b1 = b2 proof set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( Nat, set ) -> Element of InnerVertices (GFA1CarryStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = GFA1CarryOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2); let o1, o2 be Element of InnerVertices (n -BitGFA1Str (x,y)); ::_thesis: ( ex h being ManySortedSet of NAT st ( o1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) & ex h being ManySortedSet of NAT st ( o2 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) implies o1 = o2 ) given h1 being ManySortedSet of NAT such that A1: o1 = h1 . n and A2: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A3: for n being Nat holds h1 . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h1 . n)) ; ::_thesis: ( for h being ManySortedSet of NAT holds ( not o2 = h . n or not h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] or ex n being Nat st not h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) or o1 = o2 ) given h2 being ManySortedSet of NAT such that A4: o2 = h2 . n and A5: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A6: for n being Nat holds h2 . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h2 . n)) ; ::_thesis: o1 = o2 A7: dom h1 = NAT by PARTFUN1:def_2; A8: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A2; A9: for n being Nat holds h1 . (n + 1) = H1(n,h1 . n) by A3; A10: dom h2 = NAT by PARTFUN1:def_2; A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A5; A12: for n being Nat holds h2 . (n + 1) = H1(n,h2 . n) by A6; h1 = h2 from NAT_1:sch_15(A7, A8, A9, A10, A11, A12); hence o1 = o2 by A1, A4; ::_thesis: verum end; existence ex b1 being Element of InnerVertices (n -BitGFA1Str (x,y)) ex h being ManySortedSet of NAT st ( b1 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) proof defpred S1[ set , set , set ] means verum; set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set Sn = n -BitGFA1Str (x,y); set o0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA1CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); consider f, g being ManySortedSet of NAT such that A13: n -BitGFA1Str (x,y) = f . n and A14: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A15: g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A16: 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) = H1(S,z,n) & g . (n + 1) = H2(z,n) ) by Def5; defpred S2[ Nat] means ex S being non empty ManySortedSign st ( S = f . $1 & g . $1 in InnerVertices S ); InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) = {[<*>,((0 -tuples_on BOOLEAN) --> TRUE)]} by CIRCCOMB:42; then [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) by TARSKI:def_1; then A17: S2[ 0 ] by A14, A15; A18: for i being Nat st S2[i] holds S2[i + 1] proof let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] ) assume that A19: ex S being non empty ManySortedSign st ( S = f . i & g . i in InnerVertices S ) and A20: for S being non empty ManySortedSign st S = f . (i + 1) holds not g . (i + 1) in InnerVertices S ; ::_thesis: contradiction consider S being non empty ManySortedSign such that A21: S = f . i and g . i in InnerVertices S by A19; GFA1CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) in InnerVertices (BitGFA1Str ((x . (i + 1)),(y . (i + 1)),(g . i))) by GFACIRC1:69; then A22: GFA1CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) in InnerVertices (S +* (BitGFA1Str ((x . (i + 1)),(y . (i + 1)),(g . i)))) by FACIRC_1:22; A23: f . (i + 1) = S +* (BitGFA1Str ((x . (i + 1)),(y . (i + 1)),(g . i))) by A16, A21; g . (i + 1) = GFA1CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) by A16, A21; hence contradiction by A20, A22, A23; ::_thesis: verum end; for i being Nat holds S2[i] from NAT_1:sch_2(A17, A18); then ex S being non empty ManySortedSign st ( S = f . n & g . n in InnerVertices S ) ; then reconsider o = g . n as Element of InnerVertices (n -BitGFA1Str (x,y)) by A13; take o ; ::_thesis: ex h being ManySortedSet of NAT st ( o = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) take g ; ::_thesis: ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds g . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(g . n)) ) ) thus ( o = g . n & g . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] ) by A15; ::_thesis: for n being Nat holds g . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(g . n)) let i be Nat; ::_thesis: g . (i + 1) = GFA1CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) A24: ex S being non empty ManySortedSign ex x being set st ( S = f . 0 & x = g . 0 & S1[S,x, 0 ] ) by A14; A25: for n being Nat for S being non empty ManySortedSign for x being set st S = f . n & x = g . n & S1[S,x,n] holds S1[H1(S,x,n),H2(x,n),n + 1] ; for n being Nat ex S being non empty ManySortedSign st ( S = f . n & S1[S,g . n,n] ) from CIRCCMB2:sch_2(A24, A16, A25); then ex S being non empty ManySortedSign st S = f . i ; hence g . (i + 1) = GFA1CarryOutput ((x . (i + 1)),(y . (i + 1)),(g . i)) by A16; ::_thesis: verum end; end; :: deftheorem Def7 defines -BitGFA1CarryOutput GFACIRC2:def_7_:_ for n being Nat for x, y being FinSequence for b4 being Element of InnerVertices (n -BitGFA1Str (x,y)) holds ( b4 = n -BitGFA1CarryOutput (x,y) iff ex h being ManySortedSet of NAT st ( b4 = h . n & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) ); theorem Th15: :: GFACIRC2:15 for x, y being FinSequence for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds for n being Nat holds ( n -BitGFA1Str (x,y) = f . n & n -BitGFA1Circ (x,y) = g . n & n -BitGFA1CarryOutput (x,y) = h . n ) proof let x, y be FinSequence; ::_thesis: for f, g, h being ManySortedSet of NAT st f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) holds for n being Nat holds ( n -BitGFA1Str (x,y) = f . n & n -BitGFA1Circ (x,y) = g . n & n -BitGFA1CarryOutput (x,y) = h . n ) let f, g, h be ManySortedSet of NAT ; ::_thesis: ( f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) ) implies for n being Nat holds ( n -BitGFA1Str (x,y) = f . n & n -BitGFA1Circ (x,y) = g . n & n -BitGFA1CarryOutput (x,y) = h . n ) ) set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str ((x . ($3 + 1)),(y . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str ((x . ($4 + 1)),(y . ($4 + 1)),$3)) = $2 +* (BitGFA1Circ ((x . ($4 + 1)),(y . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((x . ($2 + 1)),(y . ($2 + 1)),$1)) = GFA1CarryOutput ((x . ($2 + 1)),(y . ($2 + 1)),$1); deffunc H4( Nat, set ) -> Element of InnerVertices (GFA1CarryStr ((x . ($1 + 1)),(y . ($1 + 1)),$2)) = GFA1CarryOutput ((x . ($1 + 1)),(y . ($1 + 1)),$2); assume that A1: ( f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) ) and A2: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A3: 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) = H1(S,z,n) & g . (n + 1) = H2(S,A,z,n) & h . (n + 1) = H3(z,n) ) ; ::_thesis: for n being Nat holds ( n -BitGFA1Str (x,y) = f . n & n -BitGFA1Circ (x,y) = g . n & n -BitGFA1CarryOutput (x,y) = h . n ) let n be Nat; ::_thesis: ( n -BitGFA1Str (x,y) = f . n & n -BitGFA1Circ (x,y) = g . n & n -BitGFA1CarryOutput (x,y) = h . n ) consider f1, g1, h1 being ManySortedSet of NAT such that A4: n -BitGFA1Str (x,y) = f1 . n and A5: n -BitGFA1Circ (x,y) = g1 . n and A6: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A7: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A8: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A9: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds ( f1 . (n + 1) = H1(S,z,n) & g1 . (n + 1) = H2(S,A,z,n) & h1 . (n + 1) = H3(z,n) ) by Def6; A10: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st ( S = f . 0 & A = g . 0 ) by A1; A11: ( f . 0 = f1 . 0 & g . 0 = g1 . 0 & h . 0 = h1 . 0 ) by A1, A2, A6, A7, A8; A12: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set for n being Nat holds H2(S,A,z,n) is non-empty MSAlgebra over H1(S,z,n) ; ( f = f1 & g = g1 & h = h1 ) from CIRCCMB2:sch_14(A10, A11, A3, A9, A12); hence ( n -BitGFA1Str (x,y) = f . n & n -BitGFA1Circ (x,y) = g . n ) by A4, A5; ::_thesis: n -BitGFA1CarryOutput (x,y) = h . n A13: 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) = H1(S,z,n) & h . (n + 1) = H3(z,n) ) from CIRCCMB2:sch_15(A1, A3, A12); A14: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by A1; A15: dom h = NAT by PARTFUN1:def_2; A16: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A2; for n being Nat for z being set st z = h . n holds h . (n + 1) = H3(z,n) from CIRCCMB2:sch_3(A14, A13); then A17: for n being Nat holds h . (n + 1) = H4(n,h . n) ; consider h1 being ManySortedSet of NAT such that A18: n -BitGFA1CarryOutput (x,y) = h1 . n and A19: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A20: for n being Nat holds h1 . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h1 . n)) by Def7; A21: dom h1 = NAT by PARTFUN1:def_2; A22: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by A19; A23: for n being Nat holds h1 . (n + 1) = H4(n,h1 . n) by A20; h = h1 from NAT_1:sch_15(A15, A16, A17, A21, A22, A23); hence n -BitGFA1CarryOutput (x,y) = h . n by A18; ::_thesis: verum end; theorem Th16: :: GFACIRC2:16 for a, b being FinSequence holds ( 0 -BitGFA1Str (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitGFA1Circ (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitGFA1CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] ) proof let a, b be FinSequence; ::_thesis: ( 0 -BitGFA1Str (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitGFA1Circ (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitGFA1CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] ) set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; A1: ex f, g, h being ManySortedSet of NAT st ( 0 -BitGFA1Str (a,b) = f . 0 & 0 -BitGFA1Circ (a,b) = g . 0 & f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( 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 +* (BitGFA1Str ((a . (n + 1)),(b . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((a . (n + 1)),(b . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((a . (n + 1)),(b . (n + 1)),z) ) ) ) by Def6; hence 0 -BitGFA1Str (a,b) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) ; ::_thesis: ( 0 -BitGFA1Circ (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & 0 -BitGFA1CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] ) thus 0 -BitGFA1Circ (a,b) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by A1; ::_thesis: 0 -BitGFA1CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] InnerVertices (0 -BitGFA1Str (a,b)) = {[<*>,((0 -tuples_on BOOLEAN) --> TRUE)]} by A1, CIRCCOMB:42; hence 0 -BitGFA1CarryOutput (a,b) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by TARSKI:def_1; ::_thesis: verum end; theorem Th17: :: GFACIRC2:17 for a, b being FinSequence for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds ( 1 -BitGFA1Str (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str ((a . 1),(b . 1),c)) & 1 -BitGFA1Circ (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ ((a . 1),(b . 1),c)) & 1 -BitGFA1CarryOutput (a,b) = GFA1CarryOutput ((a . 1),(b . 1),c) ) proof set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; let a, b be FinSequence; ::_thesis: for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds ( 1 -BitGFA1Str (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str ((a . 1),(b . 1),c)) & 1 -BitGFA1Circ (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ ((a . 1),(b . 1),c)) & 1 -BitGFA1CarryOutput (a,b) = GFA1CarryOutput ((a . 1),(b . 1),c) ) let c be set ; ::_thesis: ( c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] implies ( 1 -BitGFA1Str (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str ((a . 1),(b . 1),c)) & 1 -BitGFA1Circ (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ ((a . 1),(b . 1),c)) & 1 -BitGFA1CarryOutput (a,b) = GFA1CarryOutput ((a . 1),(b . 1),c) ) ) assume A1: c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] ; ::_thesis: ( 1 -BitGFA1Str (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str ((a . 1),(b . 1),c)) & 1 -BitGFA1Circ (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ ((a . 1),(b . 1),c)) & 1 -BitGFA1CarryOutput (a,b) = GFA1CarryOutput ((a . 1),(b . 1),c) ) consider f, g, h being ManySortedSet of NAT such that A2: 1 -BitGFA1Str (a,b) = f . 1 and A3: 1 -BitGFA1Circ (a,b) = g . 1 and A4: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A5: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A6: h . 0 = c and A7: 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 +* (BitGFA1Str ((a . (n + 1)),(b . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((a . (n + 1)),(b . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((a . (n + 1)),(b . (n + 1)),z) ) by A1, Def6; 1 -BitGFA1CarryOutput (a,b) = h . (0 + 1) by A1, A4, A5, A6, A7, Th15; hence ( 1 -BitGFA1Str (a,b) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str ((a . 1),(b . 1),c)) & 1 -BitGFA1Circ (a,b) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ ((a . 1),(b . 1),c)) & 1 -BitGFA1CarryOutput (a,b) = GFA1CarryOutput ((a . 1),(b . 1),c) ) by A2, A3, A4, A5, A6, A7; ::_thesis: verum end; theorem :: GFACIRC2:18 for a, b, c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds ( 1 -BitGFA1Str (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str (a,b,c)) & 1 -BitGFA1Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ (a,b,c)) & 1 -BitGFA1CarryOutput (<*a*>,<*b*>) = GFA1CarryOutput (a,b,c) ) proof let a, b be set ; ::_thesis: for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds ( 1 -BitGFA1Str (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str (a,b,c)) & 1 -BitGFA1Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ (a,b,c)) & 1 -BitGFA1CarryOutput (<*a*>,<*b*>) = GFA1CarryOutput (a,b,c) ) A1: <*a*> . 1 = a by FINSEQ_1:40; <*b*> . 1 = b by FINSEQ_1:40; hence for c being set st c = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] holds ( 1 -BitGFA1Str (<*a*>,<*b*>) = (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Str (a,b,c)) & 1 -BitGFA1Circ (<*a*>,<*b*>) = (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) +* (BitGFA1Circ (a,b,c)) & 1 -BitGFA1CarryOutput (<*a*>,<*b*>) = GFA1CarryOutput (a,b,c) ) by A1, Th17; ::_thesis: verum end; theorem Th19: :: GFACIRC2:19 for n being Nat for p, q being FinSeqLen of n for p1, p2, q1, q2 being FinSequence holds ( n -BitGFA1Str ((p ^ p1),(q ^ q1)) = n -BitGFA1Str ((p ^ p2),(q ^ q2)) & n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = n -BitGFA1Circ ((p ^ p2),(q ^ q2)) & n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) ) proof let n be Nat; ::_thesis: for p, q being FinSeqLen of n for p1, p2, q1, q2 being FinSequence holds ( n -BitGFA1Str ((p ^ p1),(q ^ q1)) = n -BitGFA1Str ((p ^ p2),(q ^ q2)) & n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = n -BitGFA1Circ ((p ^ p2),(q ^ q2)) & n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) ) let p, q be FinSeqLen of n; ::_thesis: for p1, p2, q1, q2 being FinSequence holds ( n -BitGFA1Str ((p ^ p1),(q ^ q1)) = n -BitGFA1Str ((p ^ p2),(q ^ q2)) & n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = n -BitGFA1Circ ((p ^ p2),(q ^ q2)) & n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) ) let p1, p2, q1, q2 be FinSequence; ::_thesis: ( n -BitGFA1Str ((p ^ p1),(q ^ q1)) = n -BitGFA1Str ((p ^ p2),(q ^ q2)) & n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = n -BitGFA1Circ ((p ^ p2),(q ^ q2)) & n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) ) set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; set Sn1 = n -BitGFA1Str ((p ^ p1),(q ^ q1)); set An1 = n -BitGFA1Circ ((p ^ p1),(q ^ q1)); set On1 = n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)); deffunc H1( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str (((p ^ p1) . ($3 + 1)),((q ^ q1) . ($3 + 1)),$2)); deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)) = $2 +* (BitGFA1Circ (((p ^ p1) . ($4 + 1)),((q ^ q1) . ($4 + 1)),$3)); deffunc H3( set , Nat) -> Element of InnerVertices (GFA1CarryStr (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1)) = GFA1CarryOutput (((p ^ p1) . ($2 + 1)),((q ^ q1) . ($2 + 1)),$1); deffunc H4( Nat, set ) -> Element of InnerVertices (GFA1CarryStr (((p ^ p1) . ($1 + 1)),((q ^ q1) . ($1 + 1)),$2)) = GFA1CarryOutput (((p ^ p1) . ($1 + 1)),((q ^ q1) . ($1 + 1)),$2); consider f1, g1, h1 being ManySortedSet of NAT such that A1: n -BitGFA1Str ((p ^ p1),(q ^ q1)) = f1 . n and A2: n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = g1 . n and A3: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A4: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A5: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A6: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds ( f1 . (n + 1) = H1(S,z,n) & g1 . (n + 1) = H2(S,A,z,n) & h1 . (n + 1) = H3(z,n) ) by Def6; set Sn2 = n -BitGFA1Str ((p ^ p2),(q ^ q2)); set An2 = n -BitGFA1Circ ((p ^ p2),(q ^ q2)); set On2 = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)); deffunc H5( non empty ManySortedSign , set , Nat) -> ManySortedSign = $1 +* (BitGFA1Str (((p ^ p2) . ($3 + 1)),((q ^ q2) . ($3 + 1)),$2)); deffunc H6( non empty ManySortedSign , non-empty MSAlgebra over $1, set , Nat) -> MSAlgebra over $1 +* (BitGFA1Str (((p ^ p2) . ($4 + 1)),((q ^ q2) . ($4 + 1)),$3)) = $2 +* (BitGFA1Circ (((p ^ p2) . ($4 + 1)),((q ^ q2) . ($4 + 1)),$3)); deffunc H7( set , Nat) -> Element of InnerVertices (GFA1CarryStr (((p ^ p2) . ($2 + 1)),((q ^ q2) . ($2 + 1)),$1)) = GFA1CarryOutput (((p ^ p2) . ($2 + 1)),((q ^ q2) . ($2 + 1)),$1); deffunc H8( Nat, set ) -> Element of InnerVertices (GFA1CarryStr (((p ^ p2) . ($1 + 1)),((q ^ q2) . ($1 + 1)),$2)) = GFA1CarryOutput (((p ^ p2) . ($1 + 1)),((q ^ q2) . ($1 + 1)),$2); consider f2, g2, h2 being ManySortedSet of NAT such that A7: n -BitGFA1Str ((p ^ p2),(q ^ q2)) = f2 . n and A8: n -BitGFA1Circ ((p ^ p2),(q ^ q2)) = g2 . n and A9: f2 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A10: g2 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A11: h2 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A12: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f2 . n & A = g2 . n & z = h2 . n holds ( f2 . (n + 1) = H5(S,z,n) & g2 . (n + 1) = H6(S,A,z,n) & h2 . (n + 1) = H7(z,n) ) by Def6; defpred S1[ Nat] means ( $1 <= n implies ( h1 . $1 = h2 . $1 & f1 . $1 = f2 . $1 & g1 . $1 = g2 . $1 ) ); A13: S1[ 0 ] by A3, A4, A5, A9, A10, A11; A14: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that A15: ( i <= n implies ( h1 . i = h2 . i & f1 . i = f2 . i & g1 . i = g2 . i ) ) and A16: i + 1 <= n ; ::_thesis: ( h1 . (i + 1) = h2 . (i + 1) & f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) ) A17: len p = n by CARD_1:def_7; A18: len q = n by CARD_1:def_7; A19: dom p = Seg n by A17, FINSEQ_1:def_3; A20: dom q = Seg n by A18, FINSEQ_1:def_3; 0 + 1 <= i + 1 by XREAL_1:6; then A21: i + 1 in Seg n by A16, FINSEQ_1:1; then A22: (p ^ p1) . (i + 1) = p . (i + 1) by A19, FINSEQ_1:def_7; A23: (p ^ p2) . (i + 1) = p . (i + 1) by A19, A21, FINSEQ_1:def_7; A24: (q ^ q1) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def_7; A25: (q ^ q2) . (i + 1) = q . (i + 1) by A20, A21, FINSEQ_1:def_7; defpred S2[ set , set , set , set ] means verum; A26: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st ( S = f1 . 0 & A = g1 . 0 & x = h1 . 0 & S2[S,A,x, 0 ] ) by A3, A4; A27: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set st S = f1 . n & A = g1 . n & x = h1 . n & S2[S,A,x,n] holds S2[H1(S,x,n),H2(S,A,x,n),H3(x,n),n + 1] ; A28: for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for x being set for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ; for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st ( S = f1 . n & A = g1 . n & S2[S,A,h1 . n,n] ) from CIRCCMB2:sch_13(A26, A6, A27, A28); then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that A29: S = f1 . i and A30: A = g1 . i ; thus h1 . (i + 1) = H7(h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13 .= h2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: ( f1 . (i + 1) = f2 . (i + 1) & g1 . (i + 1) = g2 . (i + 1) ) thus f1 . (i + 1) = H5(S,h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13 .= f2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: g1 . (i + 1) = g2 . (i + 1) thus g1 . (i + 1) = H6(S,A,h2 . i,i) by A6, A15, A16, A22, A23, A24, A25, A29, A30, NAT_1:13 .= g2 . (i + 1) by A12, A15, A16, A29, A30, NAT_1:13 ; ::_thesis: verum end; A31: for i being Nat holds S1[i] from NAT_1:sch_2(A13, A14); hence ( n -BitGFA1Str ((p ^ p1),(q ^ q1)) = n -BitGFA1Str ((p ^ p2),(q ^ q2)) & n -BitGFA1Circ ((p ^ p1),(q ^ q1)) = n -BitGFA1Circ ((p ^ p2),(q ^ q2)) ) by A1, A2, A7, A8; ::_thesis: n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) A32: n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = h1 . n by A3, A4, A5, A6, Th15; n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) = h2 . n by A9, A10, A11, A12, Th15; hence n -BitGFA1CarryOutput ((p ^ p1),(q ^ q1)) = n -BitGFA1CarryOutput ((p ^ p2),(q ^ q2)) by A31, A32; ::_thesis: verum end; theorem :: GFACIRC2:20 for n being Nat for x, y being FinSeqLen of n for a, b being set holds ( (n + 1) -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = GFA1CarryOutput (a,b,(n -BitGFA1CarryOutput (x,y))) ) proof set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; let n be Nat; ::_thesis: for x, y being FinSeqLen of n for a, b being set holds ( (n + 1) -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = GFA1CarryOutput (a,b,(n -BitGFA1CarryOutput (x,y))) ) let x, y be FinSeqLen of n; ::_thesis: for a, b being set holds ( (n + 1) -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = GFA1CarryOutput (a,b,(n -BitGFA1CarryOutput (x,y))) ) let a, b be set ; ::_thesis: ( (n + 1) -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = GFA1CarryOutput (a,b,(n -BitGFA1CarryOutput (x,y))) ) set p = x ^ <*a*>; set q = y ^ <*b*>; consider f, g, h being ManySortedSet of NAT such that A1: n -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = f . n and A2: n -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = g . n and A3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A4: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A5: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A6: 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 +* (BitGFA1Str (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput (((x ^ <*a*>) . (n + 1)),((y ^ <*b*>) . (n + 1)),z) ) by Def6; A7: n -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = h . n by A3, A4, A5, A6, Th15; A8: (n + 1) -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = f . (n + 1) by A3, A4, A5, A6, Th15; A9: (n + 1) -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = g . (n + 1) by A3, A4, A5, A6, Th15; A10: (n + 1) -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = h . (n + 1) by A3, A4, A5, A6, Th15; A11: len x = n by CARD_1:def_7; A12: len y = n by CARD_1:def_7; A13: (x ^ <*a*>) . (n + 1) = a by A11, FINSEQ_1:42; A14: (y ^ <*b*>) . (n + 1) = b by A12, FINSEQ_1:42; A15: x ^ <*> = x by FINSEQ_1:34; A16: y ^ <*> = y by FINSEQ_1:34; then A17: n -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = n -BitGFA1Str (x,y) by A15, Th19; A18: n -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = n -BitGFA1Circ (x,y) by A15, A16, Th19; n -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = n -BitGFA1CarryOutput (x,y) by A15, A16, Th19; hence ( (n + 1) -BitGFA1Str ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ ((x ^ <*a*>),(y ^ <*b*>)) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ (a,b,(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput ((x ^ <*a*>),(y ^ <*b*>)) = GFA1CarryOutput (a,b,(n -BitGFA1CarryOutput (x,y))) ) by A1, A2, A6, A7, A8, A9, A10, A13, A14, A17, A18; ::_thesis: verum end; theorem Th21: :: GFACIRC2:21 for n being Nat for x, y being FinSequence holds ( (n + 1) -BitGFA1Str (x,y) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ (x,y) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput (x,y) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))) ) proof set f0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set g0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; let n be Nat; ::_thesis: for x, y being FinSequence holds ( (n + 1) -BitGFA1Str (x,y) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ (x,y) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput (x,y) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))) ) let x, y be FinSequence; ::_thesis: ( (n + 1) -BitGFA1Str (x,y) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ (x,y) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput (x,y) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))) ) consider f, g, h being ManySortedSet of NAT such that A1: n -BitGFA1Str (x,y) = f . n and A2: n -BitGFA1Circ (x,y) = g . n and A3: f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A4: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A5: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A6: 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 +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),z)) & g . (n + 1) = A +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),z)) & h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),z) ) by Def6; A7: n -BitGFA1CarryOutput (x,y) = h . n by A3, A4, A5, A6, Th15; A8: (n + 1) -BitGFA1Str (x,y) = f . (n + 1) by A3, A4, A5, A6, Th15; A9: (n + 1) -BitGFA1Circ (x,y) = g . (n + 1) by A3, A4, A5, A6, Th15; (n + 1) -BitGFA1CarryOutput (x,y) = h . (n + 1) by A3, A4, A5, A6, Th15; hence ( (n + 1) -BitGFA1Str (x,y) = (n -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1Circ (x,y) = (n -BitGFA1Circ (x,y)) +* (BitGFA1Circ ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y)))) & (n + 1) -BitGFA1CarryOutput (x,y) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))) ) by A1, A2, A6, A7, A8, A9; ::_thesis: verum end; theorem Th22: :: GFACIRC2:22 for n, m being Nat st n <= m holds for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y)) proof let n, m be Nat; ::_thesis: ( n <= m implies for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y)) ) assume A1: n <= m ; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y)) let x, y be FinSequence; ::_thesis: InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y)) consider i being Nat such that A2: m = n + i by A1, NAT_1:10; defpred S1[ Nat] means InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices ((n + $1) -BitGFA1Str (x,y)); A3: S1[ 0 ] ; A4: for j being Nat st S1[j] holds S1[j + 1] proof let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] ) set Sn = n -BitGFA1Str (x,y); set Snj = (n + j) -BitGFA1Str (x,y); set SSnj = BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))); assume A5: InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices ((n + j) -BitGFA1Str (x,y)) ; ::_thesis: S1[j + 1] A6: InnerVertices (n -BitGFA1Str (x,y)) c= (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by XBOOLE_1:7; (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) c= (InnerVertices ((n + j) -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by A5, XBOOLE_1:9; then InnerVertices (n -BitGFA1Str (x,y)) c= (InnerVertices ((n + j) -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by A6, XBOOLE_1:1; then InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (((n + j) -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by FACIRC_1:27; hence S1[j + 1] by Th21; ::_thesis: verum end; for j being Nat holds S1[j] from NAT_1:sch_2(A3, A4); hence InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y)) by A2; ::_thesis: verum end; theorem :: GFACIRC2:23 for n being Nat for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA1Str (x,y)) = (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))))) proof let n be Nat; ::_thesis: for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA1Str (x,y)) = (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))))) let x, y be FinSequence; ::_thesis: InnerVertices ((n + 1) -BitGFA1Str (x,y)) = (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))))) set Sn = n -BitGFA1Str (x,y); set SSn = BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))); InnerVertices ((n -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))))) = (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))))) by FACIRC_1:27; hence InnerVertices ((n + 1) -BitGFA1Str (x,y)) = (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))))) by Th21; ::_thesis: verum end; definition let k, n be Nat; assume that B1: k >= 1 and B2: k <= n ; let x, y be FinSequence; func(k,n) -BitGFA1AdderOutput (x,y) -> Element of InnerVertices (n -BitGFA1Str (x,y)) means :Def8: :: GFACIRC2:def 8 ex i being Nat st ( k = i + 1 & it = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ); uniqueness for b1, b2 being Element of InnerVertices (n -BitGFA1Str (x,y)) st ex i being Nat st ( k = i + 1 & b1 = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ) & ex i being Nat st ( k = i + 1 & b2 = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ) holds b1 = b2 ; existence ex b1 being Element of InnerVertices (n -BitGFA1Str (x,y)) ex i being Nat st ( k = i + 1 & b1 = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ) proof consider i being Nat such that A1: k = 1 + i by B1, NAT_1:10; reconsider i = i as Nat ; deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA1Str (x,y); deffunc H2( Nat) -> ManySortedSign = BitGFA1Str ((x . ($1 + 1)),(y . ($1 + 1)),($1 -BitGFA1CarryOutput (x,y))); set o = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))); A2: InnerVertices H1(k) c= InnerVertices H1(n) by B2, Th22; A3: GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) in InnerVertices H2(i) by A1, GFACIRC1:69; A4: H1(k) = H1(i) +* H2(i) by A1, Th21; reconsider o = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) as Element of H2(i) by A3; the carrier of H1(k) = the carrier of H2(i) \/ the carrier of H1(i) by A4, CIRCCOMB:def_2; then o in the carrier of H1(k) by XBOOLE_0:def_3; then o in InnerVertices H1(k) by A3, A4, CIRCCOMB:15; hence ex b1 being Element of InnerVertices (n -BitGFA1Str (x,y)) ex i being Nat st ( k = i + 1 & b1 = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ) by A1, A2; ::_thesis: verum end; end; :: deftheorem Def8 defines -BitGFA1AdderOutput GFACIRC2:def_8_:_ for k, n being Nat st k >= 1 & k <= n holds for x, y being FinSequence for b5 being Element of InnerVertices (n -BitGFA1Str (x,y)) holds ( b5 = (k,n) -BitGFA1AdderOutput (x,y) iff ex i being Nat st ( k = i + 1 & b5 = GFA1AdderOutput ((x . k),(y . k),(i -BitGFA1CarryOutput (x,y))) ) ); theorem :: GFACIRC2:24 for n, k being Nat st k < n holds for x, y being FinSequence holds ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y))) proof let n, k be Nat; ::_thesis: ( k < n implies for x, y being FinSequence holds ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y))) ) assume A1: k < n ; ::_thesis: for x, y being FinSequence holds ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y))) let x, y be FinSequence; ::_thesis: ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y))) A2: k + 1 >= 1 by NAT_1:11; k + 1 <= n by A1, NAT_1:13; then ex i being Nat st ( k + 1 = i + 1 & ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(i -BitGFA1CarryOutput (x,y))) ) by A2, Def8; hence ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y))) ; ::_thesis: verum end; theorem :: GFACIRC2:25 for n being Nat for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) is Relation proof let n be Nat; ::_thesis: for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) is Relation let x, y be FinSequence; ::_thesis: InnerVertices (n -BitGFA1Str (x,y)) is Relation set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA1Str (x,y); deffunc H2( Nat) -> ManySortedSign = BitGFA1Str ((x . ($1 + 1)),(y . ($1 + 1)),($1 -BitGFA1CarryOutput (x,y))); defpred S1[ Nat] means InnerVertices H1($1) is Relation; H1( 0 ) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by Th16; then A1: S1[ 0 ] by FACIRC_1:38; A2: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_ S1[i_+_1] let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: S1[i] ; ::_thesis: S1[i + 1] A4: H1(i + 1) = H1(i) +* H2(i) by Th21; InnerVertices H2(i) is Relation by GFACIRC1:64; hence S1[i + 1] by A3, A4, FACIRC_1:3; ::_thesis: verum end; for i being Nat holds S1[i] from NAT_1:sch_2(A1, A2); hence InnerVertices (n -BitGFA1Str (x,y)) is Relation ; ::_thesis: verum end; registration let n be Nat; let x, y be FinSequence; clustern -BitGFA1CarryOutput (x,y) -> pair ; coherence n -BitGFA1CarryOutput (x,y) is pair proof set f1 = and2c ; set f2 = and2a ; set f3 = and2 ; set f4 = or3 ; set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; deffunc H1( Nat) -> Element of InnerVertices (n -BitGFA1Str (x,y)) = n -BitGFA1CarryOutput (x,y); A1: ex h being ManySortedSet of NAT st ( H1( 0 ) = h . 0 & h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] & ( for n being Nat holds h . (n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(h . n)) ) ) by Def7; defpred S1[ Nat] means n -BitGFA1CarryOutput (x,y) is pair ; A2: S1[ 0 ] by A1; A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) set c = n -BitGFA1CarryOutput (x,y); H1(n + 1) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))) by Th21 .= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2c],[<*(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))*>,and2a],[<*(n -BitGFA1CarryOutput (x,y)),(x . (n + 1))*>,and2]*>,or3] ; hence ( S1[n] implies S1[n + 1] ) ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A2, A3); hence n -BitGFA1CarryOutput (x,y) is pair ; ::_thesis: verum end; end; Lm3: for x, y being FinSequence for n being Nat holds ( ( (n -BitGFA1CarryOutput (x,y)) `1 = <*> & (n -BitGFA1CarryOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> TRUE & proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitGFA1CarryOutput (x,y)) `1) = 3 & (n -BitGFA1CarryOutput (x,y)) `2 = or3 & proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) ) proof set f1 = and2c ; set f2 = and2a ; set f3 = and2 ; set f4 = or3 ; let x, y be FinSequence; ::_thesis: for n being Nat holds ( ( (n -BitGFA1CarryOutput (x,y)) `1 = <*> & (n -BitGFA1CarryOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> TRUE & proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card ((n -BitGFA1CarryOutput (x,y)) `1) = 3 & (n -BitGFA1CarryOutput (x,y)) `2 = or3 & proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) ) defpred S1[ Nat] means ( ( ($1 -BitGFA1CarryOutput (x,y)) `1 = <*> & ($1 -BitGFA1CarryOutput (x,y)) `2 = (0 -tuples_on BOOLEAN) --> TRUE & proj1 (($1 -BitGFA1CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN ) or ( card (($1 -BitGFA1CarryOutput (x,y)) `1) = 3 & ($1 -BitGFA1CarryOutput (x,y)) `2 = or3 & proj1 (($1 -BitGFA1CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) ); A1: dom ((0 -tuples_on BOOLEAN) --> TRUE) = 0 -tuples_on BOOLEAN by FUNCOP_1:13; 0 -BitGFA1CarryOutput (x,y) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by Th16; then A2: S1[ 0 ] by A1, MCART_1:7; A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] set c = n -BitGFA1CarryOutput (x,y); A4: (n + 1) -BitGFA1CarryOutput (x,y) = GFA1CarryOutput ((x . (n + 1)),(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))) by Th21 .= [<*[<*(x . (n + 1)),(y . (n + 1))*>,and2c],[<*(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))*>,and2a],[<*(n -BitGFA1CarryOutput (x,y)),(x . (n + 1))*>,and2]*>,or3] ; A5: dom or3 = 3 -tuples_on BOOLEAN by FUNCT_2:def_1; ((n + 1) -BitGFA1CarryOutput (x,y)) `1 = <*[<*(x . (n + 1)),(y . (n + 1))*>,and2c],[<*(y . (n + 1)),(n -BitGFA1CarryOutput (x,y))*>,and2a],[<*(n -BitGFA1CarryOutput (x,y)),(x . (n + 1))*>,and2]*> by A4, MCART_1:7; hence S1[n + 1] by A4, A5, FINSEQ_1:45, MCART_1:7; ::_thesis: verum end; thus for i being Nat holds S1[i] from NAT_1:sch_2(A2, A3); ::_thesis: verum end; Lm4: for n being Nat for x, y being FinSequence for p being set for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f] proof let n be Nat; ::_thesis: for x, y being FinSequence for p being set for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f] let x, y be FinSequence; ::_thesis: for p being set for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f] let p be set ; ::_thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds n -BitGFA1CarryOutput (x,y) <> [p,f] let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ::_thesis: n -BitGFA1CarryOutput (x,y) <> [p,f] dom f = 2 -tuples_on BOOLEAN by FUNCT_2:def_1; then A1: proj1 ([p,f] `2) = 2 -tuples_on BOOLEAN ; ( proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 0 -tuples_on BOOLEAN or proj1 ((n -BitGFA1CarryOutput (x,y)) `2) = 3 -tuples_on BOOLEAN ) by Lm3; hence n -BitGFA1CarryOutput (x,y) <> [p,f] by A1, FINSEQ_2:110; ::_thesis: verum end; theorem Th26: :: GFACIRC2:26 for f, g being nonpair-yielding FinSequence for n being Nat holds ( InputVertices ((n + 1) -BitGFA1Str (f,g)) = (InputVertices (n -BitGFA1Str (f,g))) \/ ((InputVertices (BitGFA1Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA1CarryOutput (f,g))))) \ {(n -BitGFA1CarryOutput (f,g))}) & InnerVertices (n -BitGFA1Str (f,g)) is Relation & InputVertices (n -BitGFA1Str (f,g)) is without_pairs ) proof set f1 = and2c ; set f2 = and2a ; set f3 = and2 ; set f0 = xor2c ; let f, g be nonpair-yielding FinSequence; ::_thesis: for n being Nat holds ( InputVertices ((n + 1) -BitGFA1Str (f,g)) = (InputVertices (n -BitGFA1Str (f,g))) \/ ((InputVertices (BitGFA1Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA1CarryOutput (f,g))))) \ {(n -BitGFA1CarryOutput (f,g))}) & InnerVertices (n -BitGFA1Str (f,g)) is Relation & InputVertices (n -BitGFA1Str (f,g)) is without_pairs ) deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA1Str (f,g); deffunc H2( set , Nat) -> ManySortedSign = BitGFA1Str ((f . ($2 + 1)),(g . ($2 + 1)),$1); deffunc H3( Nat) -> Element of InnerVertices ($1 -BitGFA1Str (f,g)) = $1 -BitGFA1CarryOutput (f,g); consider h being ManySortedSet of NAT such that A1: for n being Element of NAT holds h . n = H3(n) from PBOOLE:sch_5(); deffunc H4( Nat) -> set = h . $1; deffunc H5( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = GFA1CarryOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1); set k = (0 -tuples_on BOOLEAN) --> TRUE; A2: H1( 0 ) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by Th16; then A3: InnerVertices H1( 0 ) is Relation by FACIRC_1:38; A4: InputVertices H1( 0 ) is without_pairs by A2, FACIRC_1:39; H4( 0 ) = H3( 0 ) by A1; then A5: h . 0 in InnerVertices H1( 0 ) ; A6: for n being Nat for x being set holds InnerVertices H2(x,n) is Relation by GFACIRC1:64; A7: now__::_thesis:_for_n_being_Nat for_x_being_set_st_x_=_H4(n)_holds_ InputVertices_H2(x,n)_=_{(f_._(n_+_1)),(g_._(n_+_1)),x} let n be Nat; ::_thesis: for x being set st x = H4(n) holds InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} let x be set ; ::_thesis: ( x = H4(n) implies InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} ) assume A8: x = H4(n) ; ::_thesis: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} n in NAT by ORDINAL1:def_12; then A9: H4(n) = H3(n) by A1; then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c] by A8, Lm4; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c] by A8, A9, Lm4; hence InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A10, GFACIRC1:65; ::_thesis: verum end; A11: for n being Nat for x being set st x = h . n holds (InputVertices H2(x,n)) \ {x} is without_pairs proof let n be Nat; ::_thesis: for x being set st x = h . n holds (InputVertices H2(x,n)) \ {x} is without_pairs let x be set ; ::_thesis: ( x = h . n implies (InputVertices H2(x,n)) \ {x} is without_pairs ) assume x = H4(n) ; ::_thesis: (InputVertices H2(x,n)) \ {x} is without_pairs then A12: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7; thus (InputVertices H2(x,n)) \ {x} is without_pairs ::_thesis: verum proof let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in (InputVertices H2(x,n)) \ {x} assume A13: a in (InputVertices H2(x,n)) \ {x} ; ::_thesis: contradiction then a in InputVertices H2(x,n) by XBOOLE_0:def_5; then A14: ( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A12, ENUMSET1:def_1; not a in {x} by A13, XBOOLE_0:def_5; hence contradiction by A14, TARSKI:def_1; ::_thesis: verum end; end; A15: now__::_thesis:_for_n_being_Nat for_S_being_non_empty_ManySortedSign_ for_x_being_set_st_S_=_H1(n)_&_x_=_h_._n_holds_ (_H1(n_+_1)_=_S_+*_H2(x,n)_&_h_._(n_+_1)_=_H5(x,n)_&_x_in_InputVertices_H2(x,n)_&_H5(x,n)_in_InnerVertices_H2(x,n)_) let n be Nat; ::_thesis: for S being non empty ManySortedSign for x being set st S = H1(n) & x = h . n holds ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) let S be non empty ManySortedSign ; ::_thesis: for x being set st S = H1(n) & x = h . n holds ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) let x be set ; ::_thesis: ( S = H1(n) & x = h . n implies ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) ) assume that A16: S = H1(n) and A17: x = h . n ; ::_thesis: ( H1(n + 1) = S +* H2(x,n) & h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) n in NAT by ORDINAL1:def_12; then A18: x = n -BitGFA1CarryOutput (f,g) by A1, A17; A19: H4(n + 1) = (n + 1) -BitGFA1CarryOutput (f,g) by A1; thus H1(n + 1) = S +* H2(x,n) by A16, A18, Th21; ::_thesis: ( h . (n + 1) = H5(x,n) & x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) thus h . (n + 1) = H5(x,n) by A18, A19, Th21; ::_thesis: ( x in InputVertices H2(x,n) & H5(x,n) in InnerVertices H2(x,n) ) InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7, A17; hence x in InputVertices H2(x,n) by ENUMSET1:def_1; ::_thesis: H5(x,n) in InnerVertices H2(x,n) A20: InnerVertices H2(x,n) = (({[<*(f . (n + 1)),(g . (n + 1))*>,xor2c]} \/ {(GFA1AdderOutput ((f . (n + 1)),(g . (n + 1)),x))}) \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2c],[<*(g . (n + 1)),x*>,and2a],[<*x,(f . (n + 1))*>,and2]}) \/ {(GFA1CarryOutput ((f . (n + 1)),(g . (n + 1)),x))} by GFACIRC1:63; H5(x,n) in {H5(x,n)} by TARSKI:def_1; hence H5(x,n) in InnerVertices H2(x,n) by A20, XBOOLE_0:def_3; ::_thesis: verum end; A21: for n being Nat holds ( InputVertices H1(n + 1) = (InputVertices H1(n)) \/ ((InputVertices H2(h . n,n)) \ {(h . n)}) & InnerVertices H1(n) is Relation & InputVertices H1(n) is without_pairs ) from CIRCCMB2:sch_11(A3, A4, A5, A6, A11, A15); let n be Nat; ::_thesis: ( InputVertices ((n + 1) -BitGFA1Str (f,g)) = (InputVertices (n -BitGFA1Str (f,g))) \/ ((InputVertices (BitGFA1Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA1CarryOutput (f,g))))) \ {(n -BitGFA1CarryOutput (f,g))}) & InnerVertices (n -BitGFA1Str (f,g)) is Relation & InputVertices (n -BitGFA1Str (f,g)) is without_pairs ) n in NAT by ORDINAL1:def_12; then h . n = n -BitGFA1CarryOutput (f,g) by A1; hence ( InputVertices ((n + 1) -BitGFA1Str (f,g)) = (InputVertices (n -BitGFA1Str (f,g))) \/ ((InputVertices (BitGFA1Str ((f . (n + 1)),(g . (n + 1)),(n -BitGFA1CarryOutput (f,g))))) \ {(n -BitGFA1CarryOutput (f,g))}) & InnerVertices (n -BitGFA1Str (f,g)) is Relation & InputVertices (n -BitGFA1Str (f,g)) is without_pairs ) by A21; ::_thesis: verum end; theorem :: GFACIRC2:27 for n being Nat for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitGFA1Str (x,y)) = (rng x) \/ (rng y) proof set f1 = and2c ; set f0 = xor2c ; defpred S1[ Nat] means for x, y being nonpair-yielding FinSeqLen of $1 holds InputVertices ($1 -BitGFA1Str (x,y)) = (rng x) \/ (rng y); A1: S1[ 0 ] proof let x, y be nonpair-yielding FinSeqLen of 0 ; ::_thesis: InputVertices (0 -BitGFA1Str (x,y)) = (rng x) \/ (rng y) set f = (0 -tuples_on BOOLEAN) --> TRUE; 0 -BitGFA1Str (x,y) = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) by Th16; hence InputVertices (0 -BitGFA1Str (x,y)) = rng <*> by CIRCCOMB:42 .= (rng x) \/ (rng y) ; ::_thesis: verum end; A2: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: S1[i] ; ::_thesis: S1[i + 1] let x, y be nonpair-yielding FinSeqLen of i + 1; ::_thesis: InputVertices ((i + 1) -BitGFA1Str (x,y)) = (rng x) \/ (rng y) A4: i in NAT by ORDINAL1:def_12; then consider x9 being nonpair-yielding FinSeqLen of i, z1 being non pair set such that A5: x = x9 ^ <*z1*> by FACIRC_2:34; consider y9 being nonpair-yielding FinSeqLen of i, z2 being non pair set such that A6: y = y9 ^ <*z2*> by A4, FACIRC_2:34; A7: 1 in Seg 1 by FINSEQ_1:1; then A8: 1 in dom <*z1*> by FINSEQ_1:def_8; len x9 = i by CARD_1:def_7; then A9: x . (i + 1) = <*z1*> . 1 by A5, A8, FINSEQ_1:def_7 .= z1 by FINSEQ_1:def_8 ; A10: 1 in dom <*z2*> by A7, FINSEQ_1:def_8; len y9 = i by CARD_1:def_7; then A11: y . (i + 1) = <*z2*> . 1 by A6, A10, FINSEQ_1:def_7 .= z2 by FINSEQ_1:def_8 ; deffunc H1( Nat) -> Element of InnerVertices ($1 -BitGFA1Str (x,y)) = $1 -BitGFA1CarryOutput (x,y); A12: {z1,z2,H1(i)} = {H1(i),z1,z2} by ENUMSET1:59; A13: rng x = (rng x9) \/ (rng <*z1*>) by A5, FINSEQ_1:31 .= (rng x9) \/ {z1} by FINSEQ_1:38 ; A14: rng y = (rng y9) \/ (rng <*z2*>) by A6, FINSEQ_1:31 .= (rng y9) \/ {z2} by FINSEQ_1:38 ; A15: H1(i) <> [<*z1,z2*>,and2c] by Lm4; A16: H1(i) <> [<*z1,z2*>,xor2c] by Lm4; A17: x9 = x9 ^ {} by FINSEQ_1:34; y9 = y9 ^ {} by FINSEQ_1:34; then i -BitGFA1Str (x,y) = i -BitGFA1Str (x9,y9) by A5, A6, A17, Th19; hence InputVertices ((i + 1) -BitGFA1Str (x,y)) = (InputVertices (i -BitGFA1Str (x9,y9))) \/ ((InputVertices (BitGFA1Str (z1,z2,H1(i)))) \ {H1(i)}) by A9, A11, Th26 .= ((rng x9) \/ (rng y9)) \/ ((InputVertices (BitGFA1Str (z1,z2,H1(i)))) \ {H1(i)}) by A3 .= ((rng x9) \/ (rng y9)) \/ ({z1,z2,H1(i)} \ {H1(i)}) by A15, A16, GFACIRC1:65 .= ((rng x9) \/ (rng y9)) \/ {z1,z2} by A12, ENUMSET1:86 .= ((rng x9) \/ (rng y9)) \/ ({z1} \/ {z2}) by ENUMSET1:1 .= (((rng x9) \/ (rng y9)) \/ {z1}) \/ {z2} by XBOOLE_1:4 .= (((rng x9) \/ {z1}) \/ (rng y9)) \/ {z2} by XBOOLE_1:4 .= (rng x) \/ (rng y) by A13, A14, XBOOLE_1:4 ; ::_thesis: verum end; thus for i being Nat holds S1[i] from NAT_1:sch_2(A1, A2); ::_thesis: verum end; theorem :: GFACIRC2:28 for n being Nat for x, y being nonpair-yielding FinSeqLen of n for s being State of (n -BitGFA1Circ (x,y)) holds Following (s,(1 + (2 * n))) is stable proof let n be Nat; ::_thesis: for x, y being nonpair-yielding FinSeqLen of n for s being State of (n -BitGFA1Circ (x,y)) holds Following (s,(1 + (2 * n))) is stable let f, g be nonpair-yielding FinSeqLen of n; ::_thesis: for s being State of (n -BitGFA1Circ (f,g)) holds Following (s,(1 + (2 * n))) is stable deffunc H1( set , Nat) -> ManySortedSign = BitGFA1Str ((f . ($2 + 1)),(g . ($2 + 1)),$1); deffunc H2( set , Nat) -> MSAlgebra over BitGFA1Str ((f . ($2 + 1)),(g . ($2 + 1)),$1) = BitGFA1Circ ((f . ($2 + 1)),(g . ($2 + 1)),$1); deffunc H3( set , Nat) -> Element of InnerVertices (GFA1CarryStr ((f . ($2 + 1)),(g . ($2 + 1)),$1)) = GFA1CarryOutput ((f . ($2 + 1)),(g . ($2 + 1)),$1); set S0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)); set h0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)]; n in NAT by ORDINAL1:def_12; then consider N being Function of NAT,NAT such that A1: N . 0 = 1 and A2: N . 1 = 2 and A3: N . 2 = n by FACIRC_2:35; deffunc H4( Nat) -> Element of NAT = N . $1; A4: for x being set for n being Nat holds H2(x,n) is strict gate`2=den Boolean Circuit of H1(x,n) ; A5: now__::_thesis:_for_s_being_State_of_(1GateCircuit_(<*>,((0_-tuples_on_BOOLEAN)_-->_TRUE)))_holds_Following_(s,H4(_0_))_is_stable let s be State of (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE))); ::_thesis: Following (s,H4( 0 )) is stable Following (s,1) = Following s by FACIRC_1:14; hence Following (s,H4( 0 )) is stable by A1, CIRCCMB2:2; ::_thesis: verum end; deffunc H5( Nat) -> Element of InnerVertices ($1 -BitGFA1Str (f,g)) = $1 -BitGFA1CarryOutput (f,g); consider h being ManySortedSet of NAT such that A6: for n being Element of NAT holds h . n = H5(n) from PBOOLE:sch_5(); A7: for n being Nat for x being set for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds for s being State of A holds Following (s,H4(1)) is stable proof set f1 = and2c ; set f0 = xor2c ; let n be Nat; ::_thesis: for x being set for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds for s being State of A holds Following (s,H4(1)) is stable let x be set ; ::_thesis: for A being non-empty Circuit of H1(x,n) st x = h . n & A = H2(x,n) holds for s being State of A holds Following (s,H4(1)) is stable let A be non-empty Circuit of H1(x,n); ::_thesis: ( x = h . n & A = H2(x,n) implies for s being State of A holds Following (s,H4(1)) is stable ) assume A8: x = h . n ; ::_thesis: ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable ) n in NAT by ORDINAL1:def_12; then A9: x = H5(n) by A6, A8; then A10: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c] by Lm4; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c] by A9, Lm4; hence ( not A = H2(x,n) or for s being State of A holds Following (s,H4(1)) is stable ) by A2, A10, GFACIRC1:72; ::_thesis: verum end; set Sn = n -BitGFA1Str (f,g); set An = n -BitGFA1Circ (f,g); set o0 = 0 -BitGFA1CarryOutput (f,g); consider f1, g1, h1 being ManySortedSet of NAT such that A11: n -BitGFA1Str (f,g) = f1 . n and A12: n -BitGFA1Circ (f,g) = g1 . n and A13: f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A14: g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) and A15: h1 . 0 = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] and A16: for n being Nat for S being non empty ManySortedSign for A being non-empty MSAlgebra over S for z being set st S = f1 . n & A = g1 . n & z = h1 . n holds ( f1 . (n + 1) = S +* H1(z,n) & g1 . (n + 1) = A +* H2(z,n) & h1 . (n + 1) = H3(z,n) ) by Def6; now__::_thesis:_for_i_being_set_st_i_in_NAT_holds_ h1_._i_=_h_._i let i be set ; ::_thesis: ( i in NAT implies h1 . i = h . i ) assume A17: i in NAT ; ::_thesis: h1 . i = h . i then reconsider j = i as Nat ; thus h1 . i = H5(j) by A13, A14, A15, A16, Th15 .= h . i by A6, A17 ; ::_thesis: verum end; then A18: h1 = h by PBOOLE:3; A19: ex u, v being ManySortedSet of NAT st ( n -BitGFA1Str (f,g) = u . H4(2) & n -BitGFA1Circ (f,g) = v . H4(2) & u . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitGFA1CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = u . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds ( u . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) proof take f1 ; ::_thesis: ex v being ManySortedSet of NAT st ( n -BitGFA1Str (f,g) = f1 . H4(2) & n -BitGFA1Circ (f,g) = v . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & v . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitGFA1CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = v . n & x = h . n & A2 = H2(x,n) holds ( f1 . (n + 1) = S +* H1(x,n) & v . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) take g1 ; ::_thesis: ( n -BitGFA1Str (f,g) = f1 . H4(2) & n -BitGFA1Circ (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitGFA1CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds ( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) thus ( n -BitGFA1Str (f,g) = f1 . H4(2) & n -BitGFA1Circ (f,g) = g1 . H4(2) & f1 . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & g1 . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> TRUE)) & h . 0 = 0 -BitGFA1CarryOutput (f,g) & ( for n being Nat for S being non empty ManySortedSign for A1 being non-empty MSAlgebra over S for x being set for A2 being non-empty MSAlgebra over H1(x,n) st S = f1 . n & A1 = g1 . n & x = h . n & A2 = H2(x,n) holds ( f1 . (n + 1) = S +* H1(x,n) & g1 . (n + 1) = A1 +* A2 & h . (n + 1) = H3(x,n) ) ) ) by A3, A6, A11, A12, A13, A14, A16, A18; ::_thesis: verum end; A20: ( InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) is Relation & InputVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) is without_pairs ) by FACIRC_1:38, FACIRC_1:39; A21: 0 -BitGFA1CarryOutput (f,g) = [<*>,((0 -tuples_on BOOLEAN) --> TRUE)] by Th16; InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) = {[<*>,((0 -tuples_on BOOLEAN) --> TRUE)]} by CIRCCOMB:42; then A22: ( h . 0 = 0 -BitGFA1CarryOutput (f,g) & 0 -BitGFA1CarryOutput (f,g) in InnerVertices (1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> TRUE))) ) by A6, A21, TARSKI:def_1; A23: for n being Nat for x being set holds InnerVertices H1(x,n) is Relation by GFACIRC1:64; A24: for n being Nat for x being set st x = h . n holds (InputVertices H1(x,n)) \ {x} is without_pairs proof set f1 = and2c ; set f0 = xor2c ; let n be Nat; ::_thesis: for x being set st x = h . n holds (InputVertices H1(x,n)) \ {x} is without_pairs let x be set ; ::_thesis: ( x = h . n implies (InputVertices H1(x,n)) \ {x} is without_pairs ) assume A25: x = h . n ; ::_thesis: (InputVertices H1(x,n)) \ {x} is without_pairs n in NAT by ORDINAL1:def_12; then A26: x = H5(n) by A6, A25; then A27: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c] by Lm4; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c] by A26, Lm4; then A28: InputVertices H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A27, GFACIRC1:65; let a be pair set ; :: according to FACIRC_1:def_2 ::_thesis: not a in (InputVertices H1(x,n)) \ {x} assume A29: a in (InputVertices H1(x,n)) \ {x} ; ::_thesis: contradiction then A30: a in {(f . (n + 1)),(g . (n + 1)),x} by A28, XBOOLE_0:def_5; A31: not a in {x} by A29, XBOOLE_0:def_5; ( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A30, ENUMSET1:def_1; hence contradiction by A31, TARSKI:def_1; ::_thesis: verum end; A32: for n being Nat for x being set st x = h . n holds ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) proof set f1 = and2c ; set f2 = and2a ; set f3 = and2 ; set f0 = xor2c ; let n be Nat; ::_thesis: for x being set st x = h . n holds ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) let x be set ; ::_thesis: ( x = h . n implies ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) ) assume A33: x = h . n ; ::_thesis: ( h . (n + 1) = H3(x,n) & x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) n in NAT by ORDINAL1:def_12; then A34: x = H5(n) by A6, A33; h . (n + 1) = H5(n + 1) by A6; hence h . (n + 1) = H3(x,n) by A34, Th21; ::_thesis: ( x in InputVertices H1(x,n) & H3(x,n) in InnerVertices H1(x,n) ) A35: x <> [<*(f . (n + 1)),(g . (n + 1))*>,and2c] by A34, Lm4; x <> [<*(f . (n + 1)),(g . (n + 1))*>,xor2c] by A34, Lm4; then InputVertices H1(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A35, GFACIRC1:65; hence x in InputVertices H1(x,n) by ENUMSET1:def_1; ::_thesis: H3(x,n) in InnerVertices H1(x,n) A36: InnerVertices H1(x,n) = (({[<*(f . (n + 1)),(g . (n + 1))*>,xor2c]} \/ {(GFA1AdderOutput ((f . (n + 1)),(g . (n + 1)),x))}) \/ {[<*(f . (n + 1)),(g . (n + 1))*>,and2c],[<*(g . (n + 1)),x*>,and2a],[<*x,(f . (n + 1))*>,and2]}) \/ {(GFA1CarryOutput ((f . (n + 1)),(g . (n + 1)),x))} by GFACIRC1:63; H3(x,n) in {H3(x,n)} by TARSKI:def_1; hence H3(x,n) in InnerVertices H1(x,n) by A36, XBOOLE_0:def_3; ::_thesis: verum end; for s being State of (n -BitGFA1Circ (f,g)) holds Following (s,(H4( 0 ) + (H4(2) * H4(1)))) is stable from CIRCCMB2:sch_22(A4, A5, A7, A19, A20, A22, A23, A24, A32); hence for s being State of (n -BitGFA1Circ (f,g)) holds Following (s,(1 + (2 * n))) is stable by A1, A2, A3; ::_thesis: verum end;