set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
let f, g be 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 )
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 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;
for x being set st x = H4(n) holds
InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x}let x be
set ;
( x = H4(n) implies InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} )assume A8:
x = H4(
n)
;
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;
verum end;
A11:
for n being Nat
for x being set st x = h . n holds
(InputVertices H2(x,n)) \ {x} is without_pairs
A15:
now 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;
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 ;
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 ;
( 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
;
( 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;
( 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;
( 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;
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;
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; ( 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; verum