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;
reconsider i = i as Nat ;
defpred S1[ Nat] means InnerVertices (n -BitGFA1Str x,y) c= InnerVertices ((n + $1) -BitGFA1Str x,y);
A3:
S1[ 0 ]
;
A4:
for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be
Nat;
:: thesis: ( S1[j] implies S1[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: S1[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
S1[
j + 1]
by Th21;
:: thesis: 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 -BitGFA1Str x,y) c= InnerVertices (m -BitGFA1Str x,y)
by A7; :: thesis: verum