set J = Stop SCM+FSA;
set G = Goto 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 0)),(Stop SCM+FSA))) & (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
let I be Program of SCM+FSA; :: thesis: ( (card I) + 4 in dom (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) & (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
set I1 = I ';' (Goto 0);
set i = a =0_goto ((card (Stop SCM+FSA)) + 3);
set c4 = (card I) + 4;
set Lc4 = (card I) + 4;
set Mi = (((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I;
A1: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A2: card ((Goto 0) ';' (Stop SCM+FSA)) = (card (Goto 0)) + (card (Stop SCM+FSA)) by SCMFSA6A:21
.= 1 + 1 by A1, SCMFSA8A:15
.= 2 ;
A3: 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 1
.= (((((Macro (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
.= ((((Macro (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 ;
then card (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (card ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I)) + (card ((Goto 0) ';' (Stop SCM+FSA))) by SCMFSA6A:21;
then A4: card ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I) = (card (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA)))) - (card ((Goto 0) ';' (Stop SCM+FSA)))
.= ((card I) + 6) - 2 by A2, SCMFSA_9:1
.= (card I) + 4 ;
then A5: not (card I) + 4 in dom ((((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ';' (Stop SCM+FSA)) ';' (Goto ((card (I ';' (Goto 0))) + 1))) ';' I) ;
set GJ = (Goto 0) ';' (Stop SCM+FSA);
A7: Goto 0 = 0 .--> (goto 0) by SCMFSA8A:def 1;
then A8: (Goto 0) . 0 = goto 0 by FUNCOP_1:72;
dom (Goto 0) = {0} by A7, FUNCOP_1:13;
then A9: 0 in dom (Goto 0) by TARSKI:def 1;
A10: dom (Goto 0) c= dom ((Goto 0) ';' (Stop SCM+FSA)) by SCMFSA6A:17;
then 0 + ((card I) + 4) in { (il + ((card I) + 4)) where il is Element of NAT : il in dom ((Goto 0) ';' (Stop SCM+FSA)) } by A9;
then A11: (card I) + 4 in dom (Shift (((Goto 0) ';' (Stop SCM+FSA)),((card I) + 4))) by VALUED_1:def 12;
then A12: (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) ';' (Stop SCM+FSA)) . 0 by A9, A10, VALUED_1:def 12
.= goto 0 by A9, A8, SCMFSA6A:15 ;
A13: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
card (I ';' (Goto 0)) = (card I) + (card (Goto 0)) by SCMFSA6A:21
.= (card I) + 1 by SCMFSA8A:15 ;
then ((card (I ';' (Goto 0))) + (card (Stop SCM+FSA))) + 3 = ((card I) + 4) + 1 by A13;
then (card I) + 4 < ((card (I ';' (Goto 0))) + (card (Stop SCM+FSA))) + 3 by NAT_1:13;
hence A14: (card I) + 4 in dom (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) by SCMFSA8C:27; :: thesis: (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto (0 + ((card I) + 4))
A15: dom (if=0 (a,(I ';' (Goto 0)),(Stop SCM+FSA))) = (dom (Directed ((((Macro (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 A3, A4, 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))) ';' (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 A14, A5, 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 A14, A3, A4, A15, FUNCT_4:def 1
.= IncAddr ((goto 0),((card I) + 4)) by A11, A12, COMPOS_1:def 19
.= goto (0 + ((card I) + 4)) by SCMFSA_4:1 ;
:: thesis: verum