let I, J be Program of ; :: 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) + 2 by SCMFSA6A:34;
(card I) + 0 < (card I) + 2 by XREAL_1:6;
then A5: k in dom (I ';' i) by A3, A4, AFINSQ_1:66;
A6: (Macro i) . 0 = i by COMPOS_1:58;
A7: card (Macro i) = 2 by COMPOS_1:56;
A8: (I ';' i) . k = (I ';' (Macro i)) . ((card I) + 0) by A3, SCMFSA6A:def 6
.= IncAddr (i,(card I)) by A6, A7, Th48
.= i by A1 ;
thus ((I ';' i) ';' J) . k = (Directed (I ';' i)) . k by A5, SCMFSA8A:14
.= i by A2, A5, A8, SCMFSA8A:16 ; :: thesis: ((I ';' i) ';' J) . (k + 1) = goto ((card I) + 2)
set x2 = k + 1;
(card I) + 1 < (card I) + 2 by XREAL_1:6;
then A9: k + 1 in dom (I ';' i) by A3, A4, AFINSQ_1:66;
(Macro i) . 1 = halt SCM+FSA by COMPOS_1:59;
then (I ';' (Macro i)) . (k + 1) = IncAddr ((halt SCM+FSA),(card I)) by A3, A7, Th48;
then A10: (I ';' i) . (k + 1) = IncAddr ((halt SCM+FSA),(card I)) by SCMFSA6A:def 6
.= halt SCM+FSA by COMPOS_1:11 ;
thus ((I ';' i) ';' J) . (k + 1) = (Directed (I ';' i)) . (k + 1) by A9, SCMFSA8A:14
.= goto ((card I) + 2) by A4, A9, A10, SCMFSA8A:16 ; :: thesis: verum