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 Nat
for I being Instruction of S
for p being PartState of S
for s being State of S st p = (IC S),l --> l,I & p c= s holds
CurInstr (ProgramPart s),s = I
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for l being Nat
for I being Instruction of S
for p being PartState of S
for s being State of S st p = (IC S),l --> l,I & p c= s holds
CurInstr (ProgramPart s),s = I
let l be Nat; :: thesis: for I being Instruction of S
for p being PartState of S
for s being State of S st p = (IC S),l --> l,I & p c= s holds
CurInstr (ProgramPart s),s = I
let I be Instruction of S; :: thesis: for p being PartState of S
for s being State of S st p = (IC S),l --> l,I & p c= s holds
CurInstr (ProgramPart s),s = I
let p be PartState of S; :: thesis: for s being State of S st p = (IC S),l --> l,I & p c= s holds
CurInstr (ProgramPart s),s = I
let s be State of S; :: thesis: ( p = (IC S),l --> l,I & p c= s implies CurInstr (ProgramPart s),s = I )
assume that
Z: p = (IC S),l --> l,I and
A3: p c= s ; :: thesis: CurInstr (ProgramPart s),s = I
l in NAT by ORDINAL1:def 13;
then A4: IC S <> l by Def21;
Y: (ProgramPart s) /. (IC s) = s . (IC s) by BWL1;
A5: dom ((IC S),l --> l,I) = {(IC S),l} by FUNCT_4:65;
then l in dom ((IC S),l --> l,I) by TARSKI:def 2;
then A6: ((IC S),l --> l,I) . (IC S) in dom ((IC S),l --> l,I) by A4, FUNCT_4:66;
IC S in dom ((IC S),l --> l,I) by A5, TARSKI:def 2;
hence CurInstr (ProgramPart s),s = s . (((IC S),l --> l,I) . (IC S)) by A3, Z, Y, GRFUNC_1:8
.= ((IC S),l --> l,I) . (((IC S),l --> l,I) . (IC S)) by A3, A6, Z, GRFUNC_1:8
.= ((IC S),l --> l,I) . l by A4, FUNCT_4:66
.= I by FUNCT_4:66 ;
:: thesis: verum