let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for p being PartState of S
for P being the Instructions of b₁ -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (P,s,i)
let S be non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N; :: thesis: for p being PartState of S
for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (P,s,i)
let p be PartState of S; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (P,s,i)
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: for s being State of S st p c= s holds
for i being Element of NAT holds ProgramPart p c= Comput (P,s,i)
let s be State of S; :: thesis: ( p c= s implies for i being Element of NAT holds ProgramPart p c= Comput (P,s,i) )
assume A1: p c= s ; :: thesis: for i being Element of NAT holds ProgramPart p c= Comput (P,s,i)
let i be Element of NAT ; :: thesis: ProgramPart p c= Comput (P,s,i)
ProgramPart p c= p by RELAT_1:88;
then ProgramPart p c= s by A1, XBOOLE_1:1;
hence ProgramPart p c= Comput (P,s,i) by Th81; :: thesis: verum