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 p being PartState of S
for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being PartState of S
for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let p be PartState of S; :: thesis: for k being Nat st IC in dom p holds
DecIC ((IncIC (p,k)),k) = p
let k be Nat; :: thesis: ( IC in dom p implies DecIC ((IncIC (p,k)),k) = p )
assume Z: IC in dom p ; :: thesis: DecIC ((IncIC (p,k)),k) = p
thus DecIC ((IncIC (p,k)),k) = (IncIC (p,k)) +* (Start-At ((((IC p) + k) -' k),S)) by Th54
.= (IncIC (p,k)) +* (Start-At ((IC p),S)) by NAT_D:34
.= (IncIC (p,k)) +* (Start-At ((IC p),S))
.= p +* (Start-At ((IC p),S)) by Th199
.= p by Z, Th200 ; :: thesis: verum