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)
per cases ( InsCode I = 1 or InsCode I = 0 ) by AMISTD_1:6;
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;
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;
end;