let k be Nat; :: thesis: for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st Start-At (k,S) c= p holds
IC p = k
let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for p being PartState of S st Start-At (k,S) c= p holds
IC p = k
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; :: thesis: for p being PartState of S st Start-At (k,S) c= p holds
IC p = k
let p be PartState of S; :: thesis: ( Start-At (k,S) c= p implies IC p = k )
assume Start-At (k,S) c= p ; :: thesis: IC p = k
then p is k -started by Th29;
hence IC p = k ; :: thesis: verum