let F be NAT -defined the InstructionsF of SCM -valued total Function; :: thesis: for k, n being Element of NAT

for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let k, n be Element of NAT ; :: thesis: for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let s be State of SCM; :: thesis: for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let a be Data-Location; :: thesis: for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let il be Element of NAT ; :: thesis: ( IC (Comput (F,s,k)) = n & F . n = a >0_goto il implies ( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )

assume that

A1: IC (Comput (F,s,k)) = n and

A2: F . n = a >0_goto il ; :: thesis: ( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

set csk1 = Comput (F,s,(k + 1));

set csk = Comput (F,s,k);

A3: dom F = NAT by PARTFUN1:def 2;

Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1

.= Exec ((a >0_goto il),(Comput (F,s,k))) by A1, A2, A3, PARTFUN1:def 6 ;

hence ( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) by A1, AMI_3:9; :: thesis: verum

for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let k, n be Element of NAT ; :: thesis: for s being State of SCM

for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let s be State of SCM; :: thesis: for a being Data-Location

for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let a be Data-Location; :: thesis: for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds

( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

let il be Element of NAT ; :: thesis: ( IC (Comput (F,s,k)) = n & F . n = a >0_goto il implies ( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) )

assume that

A1: IC (Comput (F,s,k)) = n and

A2: F . n = a >0_goto il ; :: thesis: ( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) )

set csk1 = Comput (F,s,(k + 1));

set csk = Comput (F,s,k);

A3: dom F = NAT by PARTFUN1:def 2;

Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1

.= Exec ((a >0_goto il),(Comput (F,s,k))) by A1, A2, A3, PARTFUN1:def 6 ;

hence ( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) by A1, AMI_3:9; :: thesis: verum