let I, J be Program of ; :: thesis: for i being ins-loc-free Instruction of SCM+FSA st i <> halt SCM+FSA holds
((I ";" i) ";" J) . (card I) = i
let i be ins-loc-free Instruction of SCM+FSA; :: thesis: ( i <> halt SCM+FSA implies ((I ";" i) ";" J) . (card I) = i )
assume A1: i <> halt SCM+FSA ; :: thesis: ((I ";" i) ";" J) . (card I) = i
set x1 = card I;
A2: card (I ";" i) = (card I) + 2 by SCMFSA6A:34;
(card I) + 0 < (card I) + 2 by XREAL_1:6;
then A3: card I in dom (I ";" i) by A2, AFINSQ_1:66;
A4: (Macro i) . 0 = i by COMPOS_1:58;
A5: card (Macro i) = 2 by COMPOS_1:56;
A6: (I ";" i) . (card I) = (I ";" (Macro i)) . ((card I) + 0) by SCMFSA6A:def 6
.= IncAddr (i,(card I)) by A4, A5, Th16
.= i by COMPOS_0:4 ;
thus ((I ";" i) ";" J) . (card I) = (Directed (I ";" i)) . (card I) by A3, SCMFSA8A:14
.= i by A1, A3, A6, SCMFSA8A:16 ; :: thesis: verum