let a, b be Int-Location ; :: thesis: for I, J being Program of SCM+FSA
for k being Element of NAT st k = card I holds
( ((I ';' (a := b)) ';' J) . (insloc k) = a := b & ((I ';' (a := b)) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) )
let I, J be Program of SCM+FSA ; :: thesis: for k being Element of NAT st k = card I holds
( ((I ';' (a := b)) ';' J) . (insloc k) = a := b & ((I ';' (a := b)) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) )
let k be Element of NAT ; :: thesis: ( k = card I implies ( ((I ';' (a := b)) ';' J) . (insloc k) = a := b & ((I ';' (a := b)) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) ) )
assume A1: k = card I ; :: thesis: ( ((I ';' (a := b)) ';' J) . (insloc k) = a := b & ((I ';' (a := b)) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) )
set i = a := b;
A2: for n being Element of NAT holds IncAddr (a := b),n = a := b by SCMFSA_4:9;
a := b <> halt SCM+FSA by SCMFSA_2:42, SCMFSA_2:124;
hence ( ((I ';' (a := b)) ';' J) . (insloc k) = a := b & ((I ';' (a := b)) ';' J) . (insloc (k + 1)) = goto (insloc ((card I) + 2)) ) by A1, A2, Th50; :: thesis: verum