let I, J be Program of ; :: thesis: for k being Element of NAT
for i being Instruction of st ( for n being Element of NAT holds IncAddr i,n = i ) & i <> halt SCM+FSA & k = card I holds
( ((I ';' i) ';' J) . (insloc k) = i & ((I ';' i) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) )
let k be Element of NAT ; :: thesis: for i being Instruction of st ( for n being Element of NAT holds IncAddr i,n = i ) & i <> halt SCM+FSA & k = card I holds
( ((I ';' i) ';' J) . (insloc k) = i & ((I ';' i) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) )
let i be Instruction of ; :: thesis: ( ( for n being Element of NAT holds IncAddr i,n = i ) & i <> halt SCM+FSA & k = card I implies ( ((I ';' i) ';' J) . (insloc k) = i & ((I ';' i) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) ) )
assume that
A1: for n being Element of NAT holds IncAddr i,n = i and
A2: i <> halt SCM+FSA and
A3: k = card I ; :: thesis: ( ((I ';' i) ';' J) . (insloc k) = i & ((I ';' i) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) )
set x1 = insloc k;
A4: card (I ';' i) = (card I) + (card (Macro i)) by SCMFSA6A:61
.= (card I) + 2 by SCMFSA7B:6 ;
(card I) + 0 < (card I) + 2 by XREAL_1:8;
then A5: insloc k in dom (I ';' i) by A3, A4, SCMFSA6A:15;
A6: (Macro i) . (insloc 0 ) = i by SCMFSA6B:33;
A7: card (Macro i) = 2 by SCMFSA7B:6;
A8: (I ';' i) . (insloc k) = (I ';' (Macro i)) . (insloc ((card I) + 0 )) by A3
.= IncAddr i,(card I) by A6, A7, Th48
.= i by A1 ;
thus ((I ';' i) ';' J) . (insloc k) = (Directed (I ';' i)) . (insloc k) by A5, SCMFSA8A:28
.= i by A2, A5, A8, SCMFSA8A:30 ; :: thesis: ((I ';' i) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2))
set x2 = insloc (k + 1);
(card I) + 1 < (card I) + 2 by XREAL_1:8;
then A9: insloc (k + 1) in dom (I ';' i) by A3, A4, SCMFSA6A:15;
(Macro i) . (insloc 1) = halt SCM+FSA by SCMFSA6B:33;
then A10: (I ';' i) . (insloc (k + 1)) = IncAddr (halt SCM+FSA ),(card I) by A3, A7, Th48
.= halt SCM+FSA by SCMFSA_4:8 ;
thus ((I ';' i) ';' J) . (insloc (k + 1)) = (Directed (I ';' i)) . (insloc (k + 1)) by A9, SCMFSA8A:28
.= goto (insloc ((card I) + 2)) by A4, A9, A10, SCMFSA8A:30 ; :: thesis: verum