let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of
for k being Element of NAT
for d being data-only FinPartState of st IC S in dom p holds
IncrIC (p +* d),k = (IncrIC p,k) +* d
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for p being FinPartState of
for k being Element of NAT
for d being data-only FinPartState of st IC S in dom p holds
IncrIC (p +* d),k = (IncrIC p,k) +* d
let p be FinPartState of ; :: thesis: for k being Element of NAT
for d being data-only FinPartState of st IC S in dom p holds
IncrIC (p +* d),k = (IncrIC p,k) +* d
let k be Element of NAT ; :: thesis: for d being data-only FinPartState of st IC S in dom p holds
IncrIC (p +* d),k = (IncrIC p,k) +* d
let d be data-only FinPartState of ; :: thesis: ( IC S in dom p implies IncrIC (p +* d),k = (IncrIC p,k) +* d )
A1: d tolerates Start-At ((IC p) + k) by Th24;
assume IC S in dom p ; :: thesis: IncrIC (p +* d),k = (IncrIC p,k) +* d
hence IncrIC (p +* d),k = (p +* d) +* (Start-At ((IC p) + k)) by Th23
.= p +* (d +* (Start-At ((IC p) + k))) by FUNCT_4:15
.= p +* ((Start-At ((IC p) + k)) +* d) by A1, FUNCT_4:35
.= (IncrIC p,k) +* d by FUNCT_4:15 ;
:: thesis: verum