let n, m be Nat; :: thesis: ( n <= m implies for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y)) )
assume A1: n <= m ; :: thesis: for x, y being FinSequence holds InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y))
let x, y be FinSequence; :: thesis: InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y))
consider i being Nat such that
A2: m = n + i by A1, NAT_1:10;
defpred S₁[ Nat] means InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices ((n + $1) -BitGFA1Str (x,y));
A3: S₁[ 0 ] ;
A4: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
set Sn = n -BitGFA1Str (x,y);
set Snj = (n + j) -BitGFA1Str (x,y);
set SSnj = BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y)));
assume A5: InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices ((n + j) -BitGFA1Str (x,y)) ; :: thesis: S₁[j + 1]
A6: InnerVertices (n -BitGFA1Str (x,y)) c= (InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by XBOOLE_1:7;
(InnerVertices (n -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) c= (InnerVertices ((n + j) -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by A5, XBOOLE_1:9;
then InnerVertices (n -BitGFA1Str (x,y)) c= (InnerVertices ((n + j) -BitGFA1Str (x,y))) \/ (InnerVertices (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by A6, XBOOLE_1:1;
then InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (((n + j) -BitGFA1Str (x,y)) +* (BitGFA1Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA1CarryOutput (x,y))))) by FACIRC_1:27;
hence S₁[j + 1] by Th21; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A3, A4);
hence InnerVertices (n -BitGFA1Str (x,y)) c= InnerVertices (m -BitGFA1Str (x,y)) by A2; :: thesis: verum