let I be Program of ; :: thesis: for a being Int-Location holds card (while>0 (a,I)) = (card I) + 6
let a be Int-Location ; :: thesis: card (while>0 (a,I)) = (card I) + 6
set i = ((card I) + 4) .--> (goto 0);
set C = if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA));
set P = (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0));
A1: card (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (card I) + 6 by Th2;
(card I) + 4 < (card I) + 6 by XREAL_1:6;
then (card I) + 4 in dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by A1, AFINSQ_1:66;
then A2: {((card I) + 4)} c= dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by ZFMISC_1:31;
dom ((if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0))) = (dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card I) + 4) .--> (goto 0))) by FUNCT_4:def 1
.= (dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) \/ {((card I) + 4)} by FUNCOP_1:13
.= dom (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by A2, XBOOLE_1:12 ;
hence card (while>0 (a,I)) = (card I) + 6 by A1; :: thesis: verum