let f, g be nonpair-yielding FinSequence; :: thesis: for n being Element of NAT holds
( InputVertices ((n + 1) -BitAdderStr f,g) = (InputVertices (n -BitAdderStr f,g)) \/ ((InputVertices (BitAdderWithOverflowStr (f . (n + 1)),(g . (n + 1)),(n -BitMajorityOutput f,g))) \ {(n -BitMajorityOutput f,g)}) & InnerVertices (n -BitAdderStr f,g) is Relation & not InputVertices (n -BitAdderStr f,g) is with_pair )
deffunc H1( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitAdderStr f,g;
deffunc H2( set , Nat) -> ManySortedSign = BitAdderWithOverflowStr (f . ($2 + 1)),(g . ($2 + 1)),$1;
deffunc H3( Nat) -> Element of InnerVertices ($1 -BitAdderStr f,g) = $1 -BitMajorityOutput 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 (MajorityStr (f . ($2 + 1)),(g . ($2 + 1)),$1) = MajorityOutput (f . ($2 + 1)),(g . ($2 + 1)),$1;
set k = (0 -tuples_on BOOLEAN ) --> FALSE ;
A2: 0 -BitAdderStr f,g = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) by Th8;
then A3: InnerVertices H1( 0 ) is Relation by FACIRC_1:38;
A4: not InputVertices H1( 0 ) is with_pair by A2, FACIRC_1:39;
H4( 0 ) = 0 -BitMajorityOutput f,g 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 FACIRC_1:88;
A7: now
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}
A9: n in NAT by ORDINAL1:def 13;
then A10: H4(n) = n -BitMajorityOutput f,g by A1;
then A11: x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&' ] by A8, A9, Th26;
x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor' ] by A8, A9, A10, Th26;
hence InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A11, Th23; :: thesis: verum
end;
A12: for n being Nat
for x being set st x = h . n holds
not (InputVertices H2(x,n)) \ {x} is with_pair
proof
let n be Nat; :: thesis: for x being set st x = h . n holds
not (InputVertices H2(x,n)) \ {x} is with_pair
let x be set ; :: thesis: ( x = h . n implies not (InputVertices H2(x,n)) \ {x} is with_pair )
assume x = H4(n) ; :: thesis: not (InputVertices H2(x,n)) \ {x} is with_pair
then A13: InputVertices H2(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7;
thus not (InputVertices H2(x,n)) \ {x} is with_pair :: thesis: verum
proof
let a be pair set ; :: according to FACIRC_1:def 2 :: thesis: not a in (InputVertices H2(x,n)) \ {x}
assume A14: a in (InputVertices H2(x,n)) \ {x} ; :: thesis: contradiction
then a in InputVertices H2(x,n) by XBOOLE_0:def 5;
then A15: ( a = f . (n + 1) or a = g . (n + 1) or a = x ) by A13, ENUMSET1:def 1;
not a in {x} by A14, XBOOLE_0:def 5;
hence contradiction by A15, TARSKI:def 1; :: thesis: verum
end;
end;
A16: now
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) ) )
A17: n in NAT by ORDINAL1:def 13;
assume that
A18: S = H1(n) and
A19: 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) )
A20: x = n -BitMajorityOutput f,g by A1, A17, A19;
A21: H4(n + 1) = (n + 1) -BitMajorityOutput f,g by A1;
thus H1(n + 1) = S +* H2(x,n) by A17, A18, A20, Th13; :: 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 A17, A20, A21, Th13; :: 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, A19;
hence x in InputVertices H2(x,n) by ENUMSET1:def 1; :: thesis: H5(x,n) in InnerVertices H2(x,n)
A22: InnerVertices H2(x,n) = ({[<*(f . (n + 1)),(g . (n + 1))*>,'xor' ],(2GatesCircOutput (f . (n + 1)),(g . (n + 1)),x,'xor' )} \/ {[<*(f . (n + 1)),(g . (n + 1))*>,'&' ],[<*(g . (n + 1)),x*>,'&' ],[<*x,(f . (n + 1))*>,'&' ]}) \/ {(MajorityOutput (f . (n + 1)),(g . (n + 1)),x)} by Th24;
H5(x,n) in {H5(x,n)} by TARSKI:def 1;
hence H5(x,n) in InnerVertices H2(x,n) by A22, XBOOLE_0:def 3; :: thesis: verum
end;
A23: for n being Nat holds
( InputVertices H1(n + 1) = (InputVertices H1(n)) \/ ((InputVertices H2(h . n,n)) \ {(h . n)}) & InnerVertices H1(n) is Relation & not InputVertices H1(n) is with_pair ) from CIRCCMB2:sch 11(A3, A4, A5, A6, A12, A16);
 let n be Element of NAT ; :: thesis: ( InputVertices ((n + 1) -BitAdderStr f,g) = (InputVertices (n -BitAdderStr f,g)) \/ ((InputVertices (BitAdderWithOverflowStr (f . (n + 1)),(g . (n + 1)),(n -BitMajorityOutput f,g))) \ {(n -BitMajorityOutput f,g)}) & InnerVertices (n -BitAdderStr f,g) is Relation & not InputVertices (n -BitAdderStr f,g) is with_pair )
h . n = n -BitMajorityOutput f,g by A1;
hence ( InputVertices ((n + 1) -BitAdderStr f,g) = (InputVertices (n -BitAdderStr f,g)) \/ ((InputVertices (BitAdderWithOverflowStr (f . (n + 1)),(g . (n + 1)),(n -BitMajorityOutput f,g))) \ {(n -BitMajorityOutput f,g)}) & InnerVertices (n -BitAdderStr f,g) is Relation & not InputVertices (n -BitAdderStr f,g) is with_pair ) by A23; :: thesis: verum