set J = Stop SCM+FSA ;
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds (while>0 a,I) . 2 = goto 3
let I be Program of SCM+FSA ; :: thesis: (while>0 a,I) . 2 = goto 3
set I1 = I ';' (Goto 0 );
set f = ((card I) + 4) .--> (goto 0 );
set i = a >0_goto ((card (Stop SCM+FSA )) + 3);
set Mi = Macro (a >0_goto ((card (Stop SCM+FSA )) + 3));
set J2 = (Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ));
set J1 = (Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )));
( dom (((card I) + 4) .--> (goto 0 )) = {((card I) + 4)} & 2 <> (card I) + 4 ) by FUNCOP_1:19, NAT_1:11;
then A1: not 2 in dom (((card I) + 4) .--> (goto 0 )) by TARSKI:def 1;
dom ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) = (dom (Directed (Stop SCM+FSA ))) \/ (dom (ProgramPart (Relocated ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))),(card (Stop SCM+FSA ))))) by FUNCT_4:def 1
.= (dom (Stop SCM+FSA )) \/ (dom (ProgramPart (Relocated ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))),(card (Stop SCM+FSA ))))) by FUNCT_4:105 ;
then A2: 0 in dom ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) by JJ, XBOOLE_0:def 3;
then 0 + 2 in { (il + 2) where il is Element of NAT : il in dom ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) } ;
then A3: 2 in dom (Shift ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2) by VALUED_1:def 12;
then A4: (Shift ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2) /. 2 = (Shift ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2) . (0 + 2) by PARTFUN1:def 8
.= ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) . 0 by A2, VALUED_1:def 12
.= (Directed (Stop SCM+FSA )) . 0 by JJ, SCMFSA8A:28
.= goto (card (Stop SCM+FSA )) by KK, JJ, SCMFSA8A:30 ;
card (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) = 2 by SCMFSA7B:6;
then A5: not 2 in dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))) ;
A6: ( 2 in dom (while>0 a,I) & dom (while>0 a,I) = (dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ))) \/ (dom (((card I) + 4) .--> (goto 0 ))) ) by Th37, FUNCT_4:def 1;
then A7: 2 in dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) by A1, XBOOLE_0:def 3;
A8: if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA ) = ((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' (I ';' (Goto 0 ))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2
.= (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= ((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))) by SCMFSA6A:67
.= (a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))) by SCMFSA6A:71
.= (Directed (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3)))) +* (ProgramPart (Relocated ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2)) by SCMFSA7B:6 ;
then A9: dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (dom (Directed (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3))))) \/ (dom (ProgramPart (Relocated ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2))) by FUNCT_4:def 1;
then dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (dom (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3)))) \/ (dom (ProgramPart (Relocated ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2))) by FUNCT_4:105;
then A10: 2 in dom (ProgramPart (Relocated ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2)) by A7, A5, XBOOLE_0:def 3;
thus (while>0 a,I) . 2 = ((Directed (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3)))) +* (ProgramPart (Relocated ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2))) . 2 by A1, A6, A8, FUNCT_4:def 1
.= (ProgramPart (Relocated ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2)) . 2 by A7, A9, A10, FUNCT_4:def 1
.= (Reloc (ProgramPart ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA ))))),2) . 2 by AMISTD_2:69
.= (Reloc ((Stop SCM+FSA ) ';' ((Goto ((card (I ';' (Goto 0 ))) + 1)) ';' ((I ';' (Goto 0 )) ';' (Stop SCM+FSA )))),2) . 2 by RELAT_1:209
.= IncAddr (goto (card (Stop SCM+FSA ))),2 by A3, A4, SCMFSA_4:24
.= goto (1 + 2) by LL, SCMFSA_4:14
.= goto 3 ; :: thesis: verum