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

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A6: InnerVertices (n -BitAdderStr (x,y)) c= InnerVertices ((n + j) -BitAdderStr (x,y)) ; :: thesis: S₁[j + 1]
A7: ((n + j) + 1) -BitAdderStr (x,y) = ((n + j) -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y)))) by Th12;
A8: InnerVertices (((n + j) -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y))))) = (InnerVertices ((n + j) -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y))))) by FACIRC_1:27;
A9: InnerVertices (n -BitAdderStr (x,y)) c= (InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y))))) by XBOOLE_1:7;
(InnerVertices (n -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y))))) c= (InnerVertices ((n + j) -BitAdderStr (x,y))) \/ (InnerVertices (BitAdderWithOverflowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitMajorityOutput (x,y))))) by A6, XBOOLE_1:9;
hence S₁[j + 1] by A7, A8, A9, XBOOLE_1:1; :: thesis: verum

end;

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