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