let I, J be MacroInstruction of SCM+FSA ; :: thesis: for a being Int-Location holds (if>0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)
let a be Int-Location; :: thesis: (if>0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)
set JJ = (a >0_goto ((card J) + 3)) ";" J;
set J3 = ((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1));
A1: card ((a >0_goto ((card J) + 3)) ";" J) = (card (Macro (a >0_goto ((card J) + 3)))) + (card J) by SCMFSA6A:21
.= 2 + (card J) by COMPOS_1:56 ;
then ((card J) + 2) -' (card ((a >0_goto ((card J) + 3)) ";" J)) = 0 by XREAL_1:232;
then A2: goto ((card I) + 1) = (Goto ((card I) + 1)) . (((card J) + 2) -' (card ((a >0_goto ((card J) + 3)) ";" J))) ;
card (Goto ((card I) + 1)) = 1 by SCMFSA8A:15;
then (card J) + 2 < (card ((a >0_goto ((card J) + 3)) ";" J)) + (card (Goto ((card I) + 1))) by A1, NAT_1:13;
then A3: (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) . ((card J) + 2) = IncAddr ((goto ((card I) + 1)),(card ((a >0_goto ((card J) + 3)) ";" J))) by A1, A2, Th2
.= goto (((card I) + 1) + ((card J) + 2)) by A1, SCMFSA_4:1
.= goto (((card I) + (card J)) + (1 + 2)) ;
card (Goto ((card I) + 1)) = 1 by SCMFSA8A:15;
then card (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) = ((card J) + 2) + 1 by A1, SCMFSA6A:21
.= (card J) + (2 + 1) ;
then card (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) = ((card J) + 2) + 1 ;
then (card J) + 2 < card (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) by NAT_1:13;
then A4: (card J) + 2 in dom (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) by AFINSQ_1:66;
then ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))) . ((card J) + 2) = (Directed (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1)))) . ((card J) + 2) by SCMFSA8A:14
.= goto (((card I) + (card J)) + 3) by A3, A4, SCMFSA8A:16 ;
hence (if>0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3) by SCMFSA6A:25; :: thesis: verum