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