let I be Program of SCM+FSA ; :: thesis: for a being Int-Location holds card (while<0 a,I) = (card I) + 11
let a be Int-Location ; :: thesis: card (while<0 a,I) = (card I) + 11
set i = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set C = if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))));
set P = (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )));
A1: card (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) = (card I) + 11 by Th3;
(card I) + 4 < (card I) + 11 by XREAL_1:8;
then insloc ((card I) + 4) in dom (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) by A1, SCMFSA6A:15;
then A2: {(insloc ((card I) + 4))} c= dom (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) by ZFMISC_1:37;
dom ((if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) = (dom (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 )))))) \/ (dom ((insloc ((card I) + 4)) .--> (goto (insloc 0 )))) by FUNCT_4:def 1
.= (dom (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 )))))) \/ {(insloc ((card I) + 4))} by FUNCOP_1:19
.= dom (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 ))))) by A2, XBOOLE_1:12 ;
hence card (while<0 a,I) = card (dom (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto (insloc 0 )))))) by CARD_1:104
.= (card I) + 11 by A1, CARD_1:104 ;
:: thesis: verum