theorem :: GFACIRC2:13

for n being Nat
for x, y being nonpair-yielding FinSeqLen of n holds InputVertices (n -BitGFA0Str (x,y)) = (rng x) \/ (rng y)