let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto (insloc ((card I) + 4))
let I be Program of SCM+FSA ; :: thesis: (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto (insloc ((card I) + 4))
set I4 = (card I) + 4;
set Lc4 = (card I) + 4;
set Gi = Goto (insloc 0 );
set SS = Stop SCM+FSA ;
set I1 = I ';' (Goto (insloc 0 ));
set F = if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA );
set i = a >0_goto (insloc ((card (Stop SCM+FSA )) + 3));
set MM = (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I;
set GS = (Goto (insloc 0 )) ';' (Stop SCM+FSA );
A1: insloc 0 in dom (Goto (insloc 0 )) by SCMFSA8A:47;
A2: (Goto (insloc 0 )) . (insloc 0 ) = goto (insloc 0 ) by SCMFSA8A:47;
then A3: (Goto (insloc 0 )) . (insloc 0 ) <> halt SCM+FSA by SCMFSA_9:9;
A4: ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) . (insloc 0 ) = (Directed (Goto (insloc 0 ))) . (insloc 0 ) by A1, SCMFSA8A:28
.= goto (insloc 0 ) by A1, A2, A3, SCMFSA8A:30 ;
A5: card (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (card I) + 6 by SCMFSA_9:2;
(card I) + 4 < (card I) + 6 by XREAL_1:8;
then A6: (card I) + 4 in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) by A5, SCMFSA6A:15;
A7: card ((((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I) = (card (((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA ))) + (card (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1))))) + (card I) by SCMFSA6A:61
.= ((card ((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA ))) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))))) + 1) + 1) + (card I) by SCMFSA6A:61, SCMFSA8A:17
.= ((2 + 1) + 1) + (card I) by SCMFSA7B:6
.= (card I) + 4 ;
then A8: not (card I) + 4 in dom ((((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I) by SCMFSA6A:15;
A9: 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
.= (((((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
.= ((((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
.= (Directed ((((a >0_goto (insloc ((card (Stop SCM+FSA )) + 3))) ';' (Stop SCM+FSA )) ';' (Goto (insloc ((card (I ';' (Goto (insloc 0 )))) + 1)))) ';' I)) +* (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4))) by A7 ;
then A10: dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom (Directed ((((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:def 1;
then dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = (dom ((((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 A11: (card I) + 4 in dom (ProgramPart (Relocated ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4))) by A6, A8, XBOOLE_0:def 3;
A12: (insloc 0 ) + ((card I) + 4) = insloc (0 + ((card I) + 4)) ;
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 ;
then A13: insloc 0 in dom ((Goto (insloc 0 )) ';' (Stop SCM+FSA )) by SCMFSA6A:15;
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 )) } ;
then A14: (card I) + 4 in dom (Shift ((Goto (insloc 0 )) ';' (Stop SCM+FSA )),((card I) + 4)) by VALUED_1:def 12;
then A15: 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 ) by A4, A13, VALUED_1:def 12 ;
thus (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 A6, A9, A10, A11, 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 A14, A15, SCMFSA_4:24
.= goto (insloc ((card I) + 4)) by A12, SCMFSA_4:14 ; :: thesis: verum