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