set C = if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))));
set i = ((card I) + 4) .--> (goto 0);
set P = (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0));
( card (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) = (card I) + 11 & (card I) + 4 < (card I) + 11 ) by Th3, XREAL_1:6;
then (card I) + 4 in dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) by AFINSQ_1:66;
then A1: {((card I) + 4)} c= dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) by ZFMISC_1:31;
A2: dom ((if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0))) = (dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0))))))) \/ (dom (((card I) + 4) .--> (goto 0))) by FUNCT_4:def 1
.= (dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0))))))) \/ {((card I) + 4)} by FUNCOP_1:13
.= dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) by A1, XBOOLE_1:12 ;
(if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0)) is initial

proof

let m, n be Nat; :: according to AFINSQ_1:def 12 :: thesis: ( not n in proj1 ((if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0))) or n <= m or m in proj1 ((if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0))) )
thus ( not n in proj1 ((if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0))) or n <= m or m in proj1 ((if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0))) ) by A2, AFINSQ_1:def 12; :: thesis: verum

end;

hence (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ';' (Goto 0)))))) +* (((card I) + 4) .--> (goto 0)) is Program of ; :: thesis: verum