(card (Stop S)) -' 1 = 0 by Lm2;
hence (Stop S) ';' F = {} +* (Reloc (F,0))
.= Reloc (F,0)
.= F ;
:: thesis: verum