set J = Stop SCM+FSA ;
set G = Goto (insloc 0 );
let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) & (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto ((insloc 0 ) + ((card I) + 4)) )
let I be Program of SCM+FSA ; :: thesis: ( (card I) + 4 in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) & (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto ((insloc 0 ) + ((card I) + 4)) )
set I1 = I ';' (Goto (insloc 0 ));
set i = a >0_goto (insloc ((card (Stop SCM+FSA )) + 3));
set c4 = (card I) + 4;
set Lc4 = (card I) + 4;
set Mi = (((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I;
A1: card ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) = (card (Goto (insloc 0 ))) + (card (Stop SCM+FSA )) by SCMFSA6A:61
.= 1 + 1 by SCMFSA8A:17, SCMFSA8A:29
.= 2 ;
A2: if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ) = ((((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' (I ';' (Goto (insloc 0 )))) ';' (Stop SCM+FSA ) by SCMFSA8B:def 2
.= (((((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I) ';' (Goto (insloc 0 ))) ';' (Stop SCM+FSA ) by SCMFSA6A:67
.= ((((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I) ';' ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) by SCMFSA6A:67 ;
then card (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (card ((((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I)) + (card ((Goto (insloc 0 )) ';' (Stop SCM+FSA ))) by SCMFSA6A:61;
then A3: card ((((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I) = (card (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ))) - (card ((Goto (insloc 0 )) ';' (Stop SCM+FSA )))
.= ((card I) + 6) - 2 by A1, SCMFSA_9:2
.= (card I) + 4 ;
then A4: not (card I) + 4 in dom ((((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I) by SCMFSA6A:15;
set GJ = (Goto (insloc 0 )) ';' (Stop SCM+FSA );
A5: InsCode (goto (insloc 0 )) = 6 by SCMFSA_2:47;
A6: Goto (insloc 0 ) = (insloc 0 ) .--> (goto (insloc 0 )) by SCMFSA8A:def 2;
then A7: (Goto (insloc 0 )) . (insloc 0 ) = goto (insloc 0 ) by FUNCOP_1:87;
dom (Goto (insloc 0 )) = {(insloc 0 )} by A6, FUNCOP_1:19;
then A8: insloc 0 in dom (Goto (insloc 0 )) by TARSKI:def 1;
A9: dom (Goto (insloc 0 )) c= dom ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) by SCMFSA6A:56;
then (insloc 0 ) + ((card I) + 4) in { (il + ((card I) + 4)) where il is Element of NAT : il in dom ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) } by A8;
then A10: insloc ((card I) + 4) in dom (Shift ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4)) by VALUED_1:def 12;
then A11: pi (Shift ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4)),((card I) + 4) = (Shift ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4)) . ((insloc 0 ) + ((card I) + 4)) by AMI_1:def 47
.= ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) . (insloc 0 ) by A8, A9, VALUED_1:def 12
.= goto (insloc 0 ) by A8, A7, A5, SCMFSA6A:54, SCMFSA_2:124 ;
card (I ';' (Goto (insloc 0 ))) = (card I) + (card (Goto (insloc 0 ))) by SCMFSA6A:61
.= (card I) + 1 by SCMFSA8A:29 ;
then ((card (I ';' (Goto (insloc 0 )))) + (card (Stop SCM+FSA ))) + 3 = ((card I) + 4) + 1 by SCMFSA8A:17;
then (card I) + 4 < ((card (I ';' (Goto (insloc 0 )))) + (card (Stop SCM+FSA ))) + 3 by NAT_1:13;
hence A12: (card I) + 4 in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by SCMFSA8C:57; :: thesis: (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto ((insloc 0 ) + ((card I) + 4))
A13: dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom (Directed ((((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I))) \/ (dom (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4)))) by A2, A3, FUNCT_4:def 1;
then dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom ((((Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3)))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I)) \/ (dom (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4)))) by FUNCT_4:105;
then (card I) + 4 in dom (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4))) by A12, A4, XBOOLE_0:def 3;
hence (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4))) . ((card I) + 4) by A12, A2, A3, A13, FUNCT_4:def 1
.= (IncAddr [(Shift (ProgramPart ((Goto (insloc 0 )) ';' (Stop SCM+FSA ))),((card I) + 4))],((card I) + 4)) . ((card I) + 4) by SCMFSA_5:2
.= (IncAddr (Shift ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4)),((card I) + 4)) . ((card I) + 4) by AMI_1:105
.= IncAddr (goto (insloc 0 )),((card I) + 4) by A10, A11, SCMFSA_4:24
.= goto ((insloc 0 ) + ((card I) + 4)) by SCMFSA_4:14 ;
:: thesis: verum