let n, m be Nat; ( n <= m implies for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y)) )
assume A1:
n <= m
; for x, y being FinSequence holds InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y))
let x, y be FinSequence; InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (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;
defpred S1[ Nat] means InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices ((n + $1) -BitSubtracterStr (x,y));
A3:
S1[ 0 ]
;
A4:
for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume A5:
InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices ((n + j) -BitSubtracterStr (x,y))
;
S1[j + 1]
A6:
InnerVertices (n -BitSubtracterStr (x,y)) c= (InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))
by XBOOLE_1:7;
(InnerVertices (n -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y))))) c= (InnerVertices ((n + j) -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))
by A5, XBOOLE_1:9;
then
InnerVertices (n -BitSubtracterStr (x,y)) c= (InnerVertices ((n + j) -BitSubtracterStr (x,y))) \/ (InnerVertices (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))
by A6;
then
InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (((n + j) -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitBorrowOutput (x,y)))))
by FACIRC_1:27;
hence
S1[
j + 1]
by Th7;
verum
end;
A7:
for j being Nat holds S1[j]
from NAT_1:sch 2(A3, A4);
m = n + i
by A2;
hence
InnerVertices (n -BitSubtracterStr (x,y)) c= InnerVertices (m -BitSubtracterStr (x,y))
by A7; verum