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:49
.= (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)
A4: i in NAT by ORDINAL1:def 13;
then consider x9 being nonpair-yielding FinSeqLen of i, z1 being non pair set such that
A5: x = x9 ^ <*z1*> by FACIRC_2:36;
consider y9 being nonpair-yielding FinSeqLen of i, z2 being non pair set such that
A6: y = y9 ^ <*z2*> by A4, FACIRC_2:36;
A7: 1 in Seg 1 by FINSEQ_1:3;
then A8: 1 in dom <*z1*> by FINSEQ_1:def 8;
len x9 = i by FINSEQ_1:def 18;
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 FINSEQ_1:def 18;
then A11: y . (i + 1) = <*z2*> . 1 by A6, A10, FINSEQ_1:def 7
.= z2 by FINSEQ_1:def 8 ;
deffunc H₁( Nat) -> Element of InnerVertices ($1 -BitGFA1Str (x,y)) = $1 -BitGFA1CarryOutput (x,y);
A12: {z1,z2,H₁(i)} = {H₁(i),z1,z2} by ENUMSET1:100;
A13: rng x = (rng x9) \/ (rng <*z1*>) by A5, FINSEQ_1:44
.= (rng x9) \/ {z1} by FINSEQ_1:55 ;
A14: rng y = (rng y9) \/ (rng <*z2*>) by A6, FINSEQ_1:44
.= (rng y9) \/ {z2} by FINSEQ_1:55 ;
A15: H₁(i) <> [<*z1,z2*>,and2c] by Lm4;
A16: H₁(i) <> [<*z1,z2*>,xor2c] by Lm4;
A17: x9 = x9 ^ {} by FINSEQ_1:47;
y9 = y9 ^ {} by FINSEQ_1:47;
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,H₁(i)))) \ {H₁(i)}) by A9, A11, 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 A15, A16, GFACIRC1:78
.= ((rng x9) \/ (rng y9)) \/ {z1,z2} by A12, ENUMSET1:136
.= ((rng x9) \/ (rng y9)) \/ ({z1} \/ {z2}) by ENUMSET1:41
.= (((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 S₁[i] from NAT_1:sch 2(A1, A2); :: thesis: verum