let n be Nat; :: thesis: for x, y being FinSequence holds InnerVertices ((n + 1) -BitGFA0Str (x,y)) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))))
let x, y be FinSequence; :: thesis: InnerVertices ((n + 1) -BitGFA0Str (x,y)) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)))))
set Sn = n -BitGFA0Str (x,y);
set SSn = BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y)));
InnerVertices ((n -BitGFA0Str (x,y)) +* (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) by FACIRC_1:27;
hence InnerVertices ((n + 1) -BitGFA0Str (x,y)) = (InnerVertices (n -BitGFA0Str (x,y))) \/ (InnerVertices (BitGFA0Str ((x . (n + 1)),(y . (n + 1)),(n -BitGFA0CarryOutput (x,y))))) by Th7; :: thesis: verum