let I, J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA holds s +* (Initialized I),s +* (Initialized J) equal_outside NAT
let s be State of SCM+FSA; :: thesis: s +* (Initialized I),s +* (Initialized J) equal_outside NAT
A1: IC SCM+FSA in dom (Initialized I) by Th24;
A2: intloc 0 in dom (Initialized J) by Th45;
A3: intloc 0 in dom (Initialized I) by Th45;

A4: now

let a be Int-Location ; :: thesis: (s +* (Initialized J)) . b₁ = (s +* (Initialized I)) . b₁

per cases ( a = intloc 0 or a <> intloc 0 ) ;

suppose A5: a = intloc 0 ; :: thesis: (s +* (Initialized J)) . b₁ = (s +* (Initialized I)) . b₁

hence (s +* (Initialized J)) . a = (Initialized J) . a by A2, FUNCT_4:14
.= 1 by A5, Th46
.= (Initialized I) . a by A5, Th46
.= (s +* (Initialized I)) . a by A3, A5, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A6: a <> intloc 0 ; :: thesis: (s +* (Initialized J)) . b₁ = (s +* (Initialized I)) . b₁

then A7: not a in dom (Initialized I) by Th48;
not a in dom (Initialized J) by A6, Th48;
hence (s +* (Initialized J)) . a = s . a by FUNCT_4:12
.= (s +* (Initialized I)) . a by A7, FUNCT_4:12 ;
:: thesis: verum

end;

end;

end;

A8: now

let f be FinSeq-Location ; :: thesis: (s +* (Initialized J)) . f = (s +* (Initialized I)) . f
A9: not f in dom (Initialized I) by Th49;
not f in dom (Initialized J) by Th49;
hence (s +* (Initialized J)) . f = s . f by FUNCT_4:12
.= (s +* (Initialized I)) . f by A9, FUNCT_4:12 ;
:: thesis: verum

end;

IC SCM+FSA in dom (Initialized J) by Th24;
then IC (s +* (Initialized J)) = (Initialized J) . (IC SCM+FSA) by FUNCT_4:14
.= 0 by Th46
.= (Initialized I) . (IC SCM+FSA) by Th46
.= IC (s +* (Initialized I)) by A1, FUNCT_4:14 ;
hence s +* (Initialized I),s +* (Initialized J) equal_outside NAT by A4, A8, SCMFSA10:91; :: thesis: verum