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 FinPartState of S
for k being Element of NAT
for d being data-only FinPartState of S holds IncrIC ((p +* d),k) = (IncrIC (p,k)) +* d
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being FinPartState of S
for k being Element of NAT
for d being data-only FinPartState of S holds IncrIC ((p +* d),k) = (IncrIC (p,k)) +* d
let p be FinPartState of S; :: thesis: for k being Element of NAT
for d being data-only FinPartState of S holds IncrIC ((p +* d),k) = (IncrIC (p,k)) +* d
let k be Element of NAT ; :: thesis: for d being data-only FinPartState of S holds IncrIC ((p +* d),k) = (IncrIC (p,k)) +* d
let d be data-only FinPartState of S; :: thesis: IncrIC ((p +* d),k) = (IncrIC (p,k)) +* d
A1: d tolerates Start-At (((IC p) + k),S) by Th24;
thus IncrIC ((p +* d),k) = (p +* d) +* (Start-At (((IC p) + k),S)) by Th58
.= p +* (d +* (Start-At (((IC p) + k),S))) by FUNCT_4:15
.= p +* ((Start-At (((IC p) + k),S)) +* d) by A1, FUNCT_4:35
.= (IncrIC (p,k)) +* d by FUNCT_4:15 ; :: thesis: verum