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 13;
A3: m = n + i by A2;
defpred S₁[ Element of NAT ] means InnerVertices (n -BitAdderStr x,y) c= InnerVertices ((n + $1) -BitAdderStr x,y);
A4: S₁[ 0 ] ;
A5: for j being Element of NAT st S₁[j] holds
S₁[j + 1]

proof

let j be Element of 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 Th13;
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 Element of NAT holds S₁[j] from NAT_1:sch 1(A4, A5);
hence InnerVertices (n -BitAdderStr x,y) c= InnerVertices (m -BitAdderStr x,y) by A3; :: thesis: verum