let n, m be Nat; ( n <= m implies for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y)) )
assume A1:
n <= m
; for x, y being FinSequence holds InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y))
let x, y be FinSequence; InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y))
consider i being Nat such that
A2:
m = n + i
by A1, NAT_1:10;
defpred S1[ Nat] means InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices ((n + $1) -BitGFA0Str (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] )
set Sn =
n -BitGFA0Str (
x,
y);
set Snj =
(n + j) -BitGFA0Str (
x,
y);
set SSnj =
BitGFA0Str (
(x . ((n + j) + 1)),
(y . ((n + j) + 1)),
((n + j) -BitGFA0CarryOutput (x,y)));
assume A5:
InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices ((n + j) -BitGFA0Str (x,y))
;
S1[j + 1]
A6:
InnerVertices (n -BitGFA0Str (x,y)) c= (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y)))))
by XBOOLE_1:7;
(InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y))))) c= (InnerVertices ((n + j) -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y)))))
by A5, XBOOLE_1:9;
then
InnerVertices (n -BitGFA0Str (x,y)) c= (InnerVertices ((n + j) -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y)))))
by A6, XBOOLE_1:1;
then
InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (((n + j) -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . ((n + j) + 1)),(y . ((n + j) + 1)),((n + j) -BitGFA0CarryOutput (x,y)))))
by FACIRC_1:27;
hence
S1[
j + 1]
by Th7;
verum
end;
for j being Nat holds S1[j]
from NAT_1:sch 2(A3, A4);
hence
InnerVertices (n -BitGFA0Str (x,y)) c= InnerVertices (m -BitGFA0Str (x,y))
by A2; verum