let I, J be MacroInstruction of SCM+FSA ; :: thesis: for a being Int-Location holds (if=0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA
let a be Int-Location; :: thesis: (if=0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA
set II = (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I;
A1: card ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) = (card (((Macro (a =0_goto ((card J) + 3))) ";" J) ";" (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:21
.= ((card ((Macro (a =0_goto ((card J) + 3))) ";" J)) + (card (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:21
.= ((card ((Macro (a =0_goto ((card J) + 3))) ";" J)) + 1) + (card I) by SCMFSA8A:15
.= (((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1) + (card I) by SCMFSA6A:21
.= ((2 + (card J)) + 1) + (card I) by COMPOS_1:56
.= ((card I) + (card J)) + 3 ;
then A2: (((card I) + (card J)) + 3) -' (card ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) = 0 by XREAL_1:232;
A3: (Stop SCM+FSA) . 0 = halt SCM+FSA ;
card (Stop SCM+FSA) = 1 by AFINSQ_1:34;
then ((card I) + (card J)) + 3 < (card ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) + (card (Stop SCM+FSA)) by A1, NAT_1:13;
hence (if=0 (a,I,J)) . (((card I) + (card J)) + 3) = IncAddr ((halt SCM+FSA),(card ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I))) by A1, A2, Th2, A3
.= halt SCM+FSA by COMPOS_0:4 ;
:: thesis: verum