let a be Int-Location ; :: thesis: for I being Program of SCM+FSA holds (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . ((card I) + 4) = goto ((card I) + 4)
let I be Program of SCM+FSA ; :: thesis: (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . ((card I) + 4) = goto ((card I) + 4)
set I4 = (card I) + 4;
set Lc4 = (card I) + 4;
set Gi = Goto 0 ;
set SS = Stop SCM+FSA ;
set I1 = I ';' (Goto 0 );
set F = if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA );
set i = a >0_goto ((card (Stop SCM+FSA )) + 3);
set MM = (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' I;
set GS = (Goto 0 ) ';' (Stop SCM+FSA );
A1: (card I) + 4 < (card I) + 6 by XREAL_1:8;
card (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (card I) + 6 by SCMFSA_9:2;
then A2: (card I) + 4 in dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) by A1, AFINSQ_1:70;
A3: 0 + ((card I) + 4) = 0 + ((card I) + 4) ;
A4: (Goto 0 ) . 0 = goto 0 by SCMFSA8A:47;
then A5: (Goto 0 ) . 0 <> halt SCM+FSA by SCMFSA_9:9;
A6: 0 in dom (Goto 0 ) by SCMFSA8A:47;
then A7: ((Goto 0 ) ';' (Stop SCM+FSA )) . 0 = (Directed (Goto 0 )) . 0 by SCMFSA8A:28
.= goto 0 by A6, A4, A5, SCMFSA8A:30 ;
x: card (Stop SCM+FSA ) = 1 by COMPOS_1:46;
card ((Goto 0 ) ';' (Stop SCM+FSA )) = (card (Goto 0 )) + (card (Stop SCM+FSA )) by SCMFSA6A:61
.= 1 + 1 by x, SCMFSA8A:29
.= 2 ;
then A8: 0 in dom ((Goto 0 ) ';' (Stop SCM+FSA )) by AFINSQ_1:70;
then 0 + ((card I) + 4) in { (il + ((card I) + 4)) where il is Element of NAT : il in dom ((Goto 0 ) ';' (Stop SCM+FSA )) } ;
then A9: (card I) + 4 in dom (Shift ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4)) by VALUED_1:def 12;
then A10: (Shift ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4)) /. ((card I) + 4) = (Shift ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4)) . (0 + ((card I) + 4)) by PARTFUN1:def 8
.= goto 0 by A7, A8, VALUED_1:def 12 ;
x: card (Stop SCM+FSA ) = 1 by COMPOS_1:46;
A11: card ((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' I) = (card (((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1)))) + (card I) by SCMFSA6A:61
.= ((card ((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA ))) + (card (Goto ((card (I ';' (Goto 0 ))) + 1)))) + (card I) by SCMFSA6A:61
.= ((card ((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA ))) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a >0_goto ((card (Stop SCM+FSA )) + 3)))) + 1) + 1) + (card I) by x, SCMFSA6A:61
.= ((2 + 1) + 1) + (card I) by SCMFSA7B:6
.= (card I) + 4 ;
then A12: not (card I) + 4 in dom ((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' I) by AFINSQ_1:70;
A13: 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
.= (Directed ((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' I)) +* (ProgramPart (Relocated ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4))) by A11 ;
then A14: dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (dom (Directed ((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' I))) \/ (dom (ProgramPart (Relocated ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4)))) by FUNCT_4:def 1;
then dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (dom ((((a >0_goto ((card (Stop SCM+FSA )) + 3)) ';' (Stop SCM+FSA )) ';' (Goto ((card (I ';' (Goto 0 ))) + 1))) ';' I)) \/ (dom (ProgramPart (Relocated ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4)))) by FUNCT_4:105;
then (card I) + 4 in dom (ProgramPart (Relocated ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4))) by A2, A12, XBOOLE_0:def 3;
hence (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . ((card I) + 4) = (ProgramPart (Relocated ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4))) . ((card I) + 4) by A2, A13, A14, FUNCT_4:def 1
.= (Reloc (ProgramPart ((Goto 0 ) ';' (Stop SCM+FSA ))),((card I) + 4)) . ((card I) + 4) by AMISTD_2:69
.= (Reloc ((Goto 0 ) ';' (Stop SCM+FSA )),((card I) + 4)) . ((card I) + 4) by RELAT_1:209
.= IncAddr (goto 0 ),((card I) + 4) by A9, A10, SCMFSA_4:24
.= goto ((card I) + 4) by A3, SCMFSA_4:14 ;
:: thesis: verum