let n be Nat; :: thesis: for x, y being FinSequence holds InnerVertices (n -BitGFA0Str x,y) is Relation
let x, y be FinSequence; :: thesis: InnerVertices (n -BitGFA0Str x,y) is Relation
set S0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE );
deffunc H₁( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitGFA0Str x,y;
deffunc H₂( Nat) -> ManySortedSign = BitGFA0Str (x . ($1 + 1)),(y . ($1 + 1)),($1 -BitGFA0CarryOutput x,y);
defpred S₁[ Nat] means InnerVertices H₁($1) is Relation;
H₁( 0 ) = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) by Th2;
then A1: S₁[ 0 ] by FACIRC_1:38;

A2: now

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
A4: H₁(i + 1) = H₁(i) +* H₂(i) by Th7;
InnerVertices H₂(i) is Relation by GFACIRC1:40;
hence S₁[i + 1] by A3, A4, FACIRC_1:3; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
hence InnerVertices (n -BitGFA0Str x,y) is Relation ; :: thesis: verum