let f be FinSeq-Location ; :: thesis: for a being Int-Location
for I, J being Program of
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
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 ; :: 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 COMPOS_1:11;
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