let N be non empty with_non-empty_elements set ; :: thesis: for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for I being Program of S st I +* (Start-At (n,S)) c= s holds
I c= s
let n be Element of NAT ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s being State of S
for I being Program of S st I +* (Start-At (n,S)) c= s holds
I c= s
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s being State of S
for I being Program of S st I +* (Start-At (n,S)) c= s holds
I c= s
let s be State of S; :: thesis: for I being Program of S st I +* (Start-At (n,S)) c= s holds
I c= s
let I be Program of S; :: thesis: ( I +* (Start-At (n,S)) c= s implies I c= s )
dom I misses dom (Start-At (n,S)) by Th54;
then A1: I +* (Start-At (n,S)) = I \/ (Start-At (n,S)) by FUNCT_4:32;
assume I +* (Start-At (n,S)) c= s ; :: thesis: I c= s
hence I c= s by A1, XBOOLE_1:11; :: thesis: verum