set f1 = and2c ;
set f0 = xor2c ;
defpred S₁[ Nat] means for x, y being nonpair-yielding FinSeqLen of $1 holds InputVertices ($1 -BitGFA1Str (x,y)) = (rng x) \/ (rng y);
A1: S₁[ 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 S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
let x, y be nonpair-yielding FinSeqLen of i + 1; :: thesis: InputVertices ((i + 1) -BitGFA1Str (x,y)) = (rng x) \/ (rng y)
consider x9 being nonpair-yielding FinSeqLen of i, z1 being non pair set such that
A4: x = x9 ^ <*z1*> by FACIRC_2:34;
consider y9 being nonpair-yielding FinSeqLen of i, z2 being non pair set such that
A5: y = y9 ^ <*z2*> by FACIRC_2:34;
A6: 1 in Seg 1 by FINSEQ_1:1;
then A7: 1 in dom <*z1*> by FINSEQ_1:def 8;
len x9 = i by CARD_1:def 7;
then A8: x . (i + 1) = <*z1*> . 1 by A4, A7, FINSEQ_1:def 7
.= z1 ;
A9: 1 in dom <*z2*> by A6, FINSEQ_1:def 8;
len y9 = i by CARD_1:def 7;
then A10: y . (i + 1) = <*z2*> . 1 by A5, A9, FINSEQ_1:def 7
.= z2 ;
deffunc H₁( Nat) -> Element of InnerVertices ($1 -BitGFA1Str (x,y)) = $1 -BitGFA1CarryOutput (x,y);
A11: {z1,z2,H₁(i)} = {H₁(i),z1,z2} by ENUMSET1:59;
A12: rng x = (rng x9) \/ (rng <*z1*>) by A4, FINSEQ_1:31
.= (rng x9) \/ {z1} by FINSEQ_1:38 ;
A13: rng y = (rng y9) \/ (rng <*z2*>) by A5, FINSEQ_1:31
.= (rng y9) \/ {z2} by FINSEQ_1:38 ;
A14: H₁(i) <> [<*z1,z2*>,and2c] by Lm4;
A15: H₁(i) <> [<*z1,z2*>,xor2c] by Lm4;
A16: x9 = x9 ^ {} by FINSEQ_1:34;
y9 = y9 ^ {} by FINSEQ_1:34;
then i -BitGFA1Str (x,y) = i -BitGFA1Str (x9,y9) by A4, A5, A16, Th19;
hence InputVertices ((i + 1) -BitGFA1Str (x,y)) = (InputVertices (i -BitGFA1Str (x9,y9))) \/ ((InputVertices (BitGFA1Str (z1,z2,H₁(i)))) \ {H₁(i)}) by A8, A10, Th26
.= ((rng x9) \/ (rng y9)) \/ ((InputVertices (BitGFA1Str (z1,z2,H₁(i)))) \ {H₁(i)}) by A3
.= ((rng x9) \/ (rng y9)) \/ ({z1,z2,H₁(i)} \ {H₁(i)}) by A14, A15, GFACIRC1:65
.= ((rng x9) \/ (rng y9)) \/ {z1,z2} by A11, 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 A12, A13, XBOOLE_1:4 ;
:: thesis: verum

end;

thus for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2); :: thesis: verum