let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l being Nat
for I being Instruction of S
for P being NAT -defined the InstructionsF of b₁ -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for l being Nat
for I being Instruction of S
for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let l be Nat; :: thesis: for I being Instruction of S
for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let I be Instruction of S; :: thesis: for P being NAT -defined the InstructionsF of S -valued Function st l .--> I c= P holds
for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let P be NAT -defined the InstructionsF of S -valued Function; :: thesis: ( l .--> I c= P implies for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I )
assume A1: l .--> I c= P ; :: thesis: for s being State of S st (IC ) .--> l c= s holds
CurInstr (P,s) = I
let s be State of S; :: thesis: ( (IC ) .--> l c= s implies CurInstr (P,s) = I )
assume A2: (IC ) .--> l c= s ; :: thesis: CurInstr (P,s) = I
IC in dom ((IC ) .--> l) by TARSKI:def 1;
then A3: IC s = ((IC ) .--> l) . (IC ) by A2, GRFUNC_1:2
.= l by FUNCOP_1:72 ;
A4: IC s in dom (l .--> I) by A3, TARSKI:def 1;
dom (l .--> I) c= dom P by A1, RELAT_1:11;
hence CurInstr (P,s) = P . (IC s) by A4, PARTFUN1:def 6
.= (l .--> I) . (IC s) by A4, A1, GRFUNC_1:2
.= I by A3, FUNCOP_1:72 ;
:: thesis: verum