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:6;
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:66;
A3: 0 + ((card I) + 4) = 0 + ((card I) + 4) ;
A4: (Goto 0) . 0 = goto 0 by SCMFSA8A:31;
A5: 0 in dom (Goto 0) by SCMFSA8A:31;
then A6: ((Goto 0) ';' (Stop SCM+FSA)) . 0 = (Directed (Goto 0)) . 0 by SCMFSA8A:14
.= goto 0 by A5, A4, SCMFSA8A:16 ;
A7: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
card ((Goto 0) ';' (Stop SCM+FSA)) = (card (Goto 0)) + (card (Stop SCM+FSA)) by SCMFSA6A:21
.= 1 + 1 by A7, SCMFSA8A:15
.= 2 ;
then A8: 0 in dom ((Goto 0) ';' (Stop SCM+FSA)) by AFINSQ_1:66;
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 6
.= goto 0 by A6, A8, VALUED_1:def 12 ;
A11: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A12: 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:21
.= ((card ((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA))) + (card (Goto ((card (I ';' (Goto 0))) + 1)))) + (card I) by SCMFSA6A:21
.= ((card ((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA))) + 1) + (card I) by SCMFSA8A:15
.= ((2 + 1) + 1) + (card I) by A11, SCMFSA6A:33
.= (card I) + 4 ;
then A13: 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:66;
A14: 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:25
.= ((((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:25
.= (Directed ((((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I)) +* (Reloc (((Goto 0) ';' (Stop SCM+FSA)),((card I) + 4))) by A12, SCMFSA6A:def 4 ;
then A15: 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 (Reloc (((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 (Directed (((((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))) ';' I))))) \/ (dom (Reloc (((Goto 0) ';' (Stop SCM+FSA)),((card I) + 4)))) by SCMFSA6A:def 2
.= (dom (((((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I) +~ ((halt SCM+FSA),(goto (card ((((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I)))))) \/ (dom (Reloc (((Goto 0) ';' (Stop SCM+FSA)),((card I) + 4)))) by SCMFSA6A:def 1
.= (dom ((((a >0_goto ((card (Stop SCM+FSA)) + 3)) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I)) \/ (dom (Reloc (((Goto 0) ';' (Stop SCM+FSA)),((card I) + 4)))) by FUNCT_4:99 ;
then (card I) + 4 in dom (Reloc (((Goto 0) ';' (Stop SCM+FSA)),((card I) + 4))) by A2, A13, XBOOLE_0:def 3;
hence (if>0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = (Reloc (((Goto 0) ';' (Stop SCM+FSA)),((card I) + 4))) . ((card I) + 4) by A2, A14, A15, FUNCT_4:def 1
.= IncAddr ((goto 0),((card I) + 4)) by A9, A10, COMPOS_1:def 19
.= goto ((card I) + 4) by A3, SCMFSA_4:1 ;
:: thesis: verum