let f be FinSeq-Location ; :: thesis: for a being Int-Location
for I, J being Program of {INT,(INT *)}
for k being Element of NAT st k = card I holds
( ((I ';' (a :=len f)) ';' J) . k = a :=len f & ((I ';' (a :=len f)) ';' J) . (k + 1) = goto ((card I) + 2) )
let a be Int-Location ; :: thesis: for I, J being Program of {INT,(INT *)}
for k being Element of NAT st k = card I holds
( ((I ';' (a :=len f)) ';' J) . k = a :=len f & ((I ';' (a :=len f)) ';' J) . (k + 1) = goto ((card I) + 2) )
let I, J be Program of {INT,(INT *)}; :: thesis: for k being Element of NAT st k = card I holds
( ((I ';' (a :=len f)) ';' J) . k = a :=len f & ((I ';' (a :=len f)) ';' J) . (k + 1) = goto ((card I) + 2) )
let k be Element of NAT ; :: thesis: ( k = card I implies ( ((I ';' (a :=len f)) ';' J) . k = a :=len f & ((I ';' (a :=len f)) ';' J) . (k + 1) = goto ((card I) + 2) ) )
assume A1: k = card I ; :: thesis: ( ((I ';' (a :=len f)) ';' J) . k = a :=len f & ((I ';' (a :=len f)) ';' J) . (k + 1) = goto ((card I) + 2) )
set i = a :=len f;
for n being Element of NAT holds IncAddr ((a :=len f),n) = a :=len f by SCMFSA_4:19;
hence ( ((I ';' (a :=len f)) ';' J) . k = a :=len f & ((I ';' (a :=len f)) ';' J) . (k + 1) = goto ((card I) + 2) ) by A1, Th50; :: thesis: verum