let a, b be Int-Location ; :: thesis: for I, J being Program of
for k being Element of NAT st k = card I holds
( ((I ';' (a := b)) ';' J) . k = a := b & ((I ';' (a := b)) ';' J) . (k + 1) = goto ((card I) + 2) )
let I, J be Program of ; :: thesis: for k being Element of NAT st k = card I holds
( ((I ';' (a := b)) ';' J) . k = a := b & ((I ';' (a := b)) ';' J) . (k + 1) = goto ((card I) + 2) )
let k be Element of NAT ; :: thesis: ( k = card I implies ( ((I ';' (a := b)) ';' J) . k = a := b & ((I ';' (a := b)) ';' J) . (k + 1) = goto ((card I) + 2) ) )
assume A1: k = card I ; :: thesis: ( ((I ';' (a := b)) ';' J) . k = a := b & ((I ';' (a := b)) ';' J) . (k + 1) = goto ((card I) + 2) )
set i = a := b;
for n being Element of NAT holds IncAddr ((a := b),n) = a := b by COMPOS_1:11;
hence ( ((I ';' (a := b)) ';' J) . k = a := b & ((I ';' (a := b)) ';' J) . (k + 1) = goto ((card I) + 2) ) by A1, Th50; :: thesis: verum