let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f, g being Instruction-Location of T st NextLoc f = NextLoc g holds
f = g
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for f, g being Instruction-Location of T st NextLoc f = NextLoc g holds
f = g
let f, g be Instruction-Location of T; :: thesis: ( NextLoc f = NextLoc g implies f = g )
assume A1: NextLoc f = NextLoc g ; :: thesis: f = g
set k = locnum f;
set m = locnum g;
(locnum f) + 0 = ((locnum f) + 1) - 1
.= ((locnum g) + 1) - 1 by A1, Th25
.= (locnum g) + 0 ;
hence f = g by Th27; :: thesis: verum