let N be with_zero set ; :: thesis: for I being Instruction of (STC N)

for s being State of (STC N)

for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

let I be Instruction of (STC N); :: thesis: for s being State of (STC N)

for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

let s be State of (STC N); :: thesis: for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

let k be Nat; :: thesis: Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

for s being State of (STC N)

for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

let I be Instruction of (STC N); :: thesis: for s being State of (STC N)

for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

let s be State of (STC N); :: thesis: for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

let k be Nat; :: thesis: Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

per cases
( InsCode I = 1 or InsCode I = 0 )
by AMISTD_1:6;

end;

suppose A1:
InsCode I = 1
; :: thesis: Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

hence Exec (I,(IncIC (s,k))) =
IncIC ((IncIC (s,k)),1)
by AMISTD_1:20

.= IncIC (s,(1 + k)) by MEMSTR_0:57

.= IncIC ((IncIC (s,1)),k) by MEMSTR_0:57

.= IncIC ((Exec (I,s)),k) by A1, AMISTD_1:20 ;

:: thesis: verum

end;.= IncIC (s,(1 + k)) by MEMSTR_0:57

.= IncIC ((IncIC (s,1)),k) by MEMSTR_0:57

.= IncIC ((Exec (I,s)),k) by A1, AMISTD_1:20 ;

:: thesis: verum

suppose
InsCode I = 0
; :: thesis: Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

then A2:
I is halting
by AMISTD_1:4;

hence Exec (I,(IncIC (s,k))) = IncIC (s,k)

.= IncIC ((Exec (I,s)),k) by A2 ;

:: thesis: verum

end;hence Exec (I,(IncIC (s,k))) = IncIC (s,k)

.= IncIC ((Exec (I,s)),k) by A2 ;

:: thesis: verum