let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for l being Element of NAT
for I being Instruction of S
for P being NAT -defined the Instructions of b₁ -valued Function st l .--> I c= P holds
for s being State of S st (IC S) .--> l c= s holds
CurInstr (P,s) = I
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for l being Element of NAT
for I being Instruction of S
for P being NAT -defined the Instructions of S -valued Function st l .--> I c= P holds
for s being State of S st (IC S) .--> l c= s holds
CurInstr (P,s) = I
let l be Element of NAT ; :: thesis: for I being Instruction of S
for P being NAT -defined the Instructions of S -valued Function st l .--> I c= P holds
for s being State of S st (IC S) .--> l c= s holds
CurInstr (P,s) = I
let I be Instruction of S; :: thesis: for P being NAT -defined the Instructions of S -valued Function st l .--> I c= P holds
for s being State of S st (IC S) .--> l c= s holds
CurInstr (P,s) = I
let P be NAT -defined the Instructions of S -valued Function; :: thesis: ( l .--> I c= P implies for s being State of S st (IC S) .--> l c= s holds
CurInstr (P,s) = I )
assume ZZ: l .--> I c= P ; :: thesis: for s being State of S st (IC S) .--> l c= s holds
CurInstr (P,s) = I
let s be State of S; :: thesis: ( (IC S) .--> l c= s implies CurInstr (P,s) = I )
assume Z: (IC S) .--> l c= s ; :: thesis: CurInstr (P,s) = I
dom ((IC S) .--> l) = {(IC S)} by FUNCOP_1:19;
then IC S in dom ((IC S) .--> l) by TARSKI:def 1;
then A: IC s = ((IC S) .--> l) . (IC S) by Z, GRFUNC_1:8
.= l by FUNCOP_1:87 ;
dom (l .--> I) = {l} by FUNCOP_1:19;
then B: IC s in dom (l .--> I) by A, TARSKI:def 1;
dom (l .--> I) c= dom P by ZZ, RELAT_1:25;
then IC s in dom P by B;
hence CurInstr (P,s) = P . (IC s) by PARTFUN1:def 8
.= (l .--> I) . (IC s) by B, ZZ, GRFUNC_1:8
.= I by A, FUNCOP_1:87 ;
:: thesis: verum