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_{1} -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

for l being Nat

for I being Instruction of S

for P being NAT -defined the InstructionsF of b

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