let n be Element of NAT ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for i being Instruction of S
for f being Function of the Instructions of S, the Instructions of S st f = (id the Instructions of S) +* ((halt S) .--> i) holds
for s being NAT -defined the Instructions of b₂ -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for i being Instruction of S
for f being Function of the Instructions of S, the Instructions of S st f = (id the Instructions of S) +* ((halt S) .--> i) holds
for s being NAT -defined the Instructions of b₁ -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let S be non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N; :: thesis: for i being Instruction of S
for f being Function of the Instructions of S, the Instructions of S st f = (id the Instructions of S) +* ((halt S) .--> i) holds
for s being NAT -defined the Instructions of S -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
A1: dom (id the Instructions of S) = the Instructions of S by RELAT_1:71;
let i be Instruction of S; :: thesis: for f being Function of the Instructions of S, the Instructions of S st f = (id the Instructions of S) +* ((halt S) .--> i) holds
for s being NAT -defined the Instructions of S -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let f be Function of the Instructions of S, the Instructions of S; :: thesis: ( f = (id the Instructions of S) +* ((halt S) .--> i) implies for s being NAT -defined the Instructions of S -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n)) )
assume A2: f = (id the Instructions of S) +* ((halt S) .--> i) ; :: thesis: for s being NAT -defined the Instructions of S -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let s be NAT -defined the Instructions of S -valued finite Function; :: thesis: IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
rng ((halt S) .--> (IncAddr (i,n))) = {(IncAddr (i,n))} by FUNCOP_1:14;
then A3: rng ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) c= (rng (id the Instructions of S)) \/ {(IncAddr (i,n))} by FUNCT_4:18;
rng (id the Instructions of S) = the Instructions of S by RELAT_1:71;
then A4: (rng (id the Instructions of S)) \/ {(IncAddr (i,n))} = the Instructions of S by ZFMISC_1:46;
A5: dom ((halt S) .--> (IncAddr (i,n))) = {(halt S)} by FUNCOP_1:19;
then dom ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) = (dom (id the Instructions of S)) \/ {(halt S)} by FUNCT_4:def 1
.= the Instructions of S by A1, ZFMISC_1:46 ;
then reconsider g = (id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n))) as Function of the Instructions of S, the Instructions of S by A3, A4, RELSET_1:11;
A6: dom (IncAddr (s,n)) = dom s by Def40
.= dom (f * s) by FUNCT_2:200 ;
A7: dom ((halt S) .--> i) = {(halt S)} by FUNCOP_1:19;

A8: now

let m be Nat; :: thesis: ( m in dom (f * s) implies (g * (IncAddr (s,n))) . b₁ = IncAddr (((f * s) /. b₁),n) )
assume A9: m in dom (f * s) ; :: thesis: (g * (IncAddr (s,n))) . b₁ = IncAddr (((f * s) /. b₁),n)
then A10: m in dom s by FUNCT_2:200;

per cases ( s . m = halt S or s . m <> halt S ) ;

suppose A11: s . m = halt S ; :: thesis: (g * (IncAddr (s,n))) . b₁ = IncAddr (((f * s) /. b₁),n)

reconsider mm = m as Element of NAT by ORDINAL1:def 13;
A12: (IncAddr (s,n)) . m = IncAddr ((s /. mm),n) by A10, Def40
.= IncAddr ((halt S),n) by A10, A11, PARTFUN1:def 8
.= halt S by Th92 ;
A13: halt S in {(halt S)} by TARSKI:def 1;
A14: (f * s) /. m = (f * s) . m by A9, PARTFUN1:def 8
.= f . (halt S) by A10, A11, FUNCT_1:23
.= ((halt S) .--> i) . (halt S) by A2, A7, A13, FUNCT_4:14
.= i by FUNCOP_1:87 ;
thus (g * (IncAddr (s,n))) . m = g . ((IncAddr (s,n)) . m) by A6, A9, FUNCT_1:23
.= ((halt S) .--> (IncAddr (i,n))) . ((IncAddr (s,n)) . m) by A5, A12, A13, FUNCT_4:14
.= IncAddr (((f * s) /. m),n) by A12, A14, FUNCOP_1:87 ; :: thesis: verum

end;

suppose A15: s . m <> halt S ; :: thesis: (g * (IncAddr (s,n))) . b₁ = IncAddr (((f * s) /. b₁),n)

A16: s /. m = s . m by A10, PARTFUN1:def 8;

A17: now

assume IncAddr ((s /. m),n) = halt S ; :: thesis: contradiction
then s /. m = halt S by Th96;
hence contradiction by A15, A16; :: thesis: verum

end;

A18: not s /. m in {(halt S)} by A15, A16, TARSKI:def 1;
A19: not IncAddr ((s /. m),n) in {(halt S)} by A17, TARSKI:def 1;
A20: (f * s) /. m = (f * s) . m by A9, PARTFUN1:def 8
.= f . (s . m) by A10, FUNCT_1:23
.= (id the Instructions of S) . (s /. m) by A2, A7, A16, A18, FUNCT_4:12
.= s /. m by FUNCT_1:35 ;
thus (g * (IncAddr (s,n))) . m = g . ((IncAddr (s,n)) . m) by A6, A9, FUNCT_1:23
.= g . (IncAddr ((s /. m),n)) by A10, Def40
.= (id the Instructions of S) . (IncAddr ((s /. m),n)) by A5, A19, FUNCT_4:12
.= IncAddr (((f * s) /. m),n) by A20, FUNCT_1:35 ; :: thesis: verum

end;

end;

end;

dom (g * (IncAddr (s,n))) = dom (IncAddr (s,n)) by FUNCT_2:200;
hence IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n)) by A6, A8, Def40; :: thesis: verum