thus SCM+FSA is IC-good :: thesis: SCM+FSA is Exec-preserving

proof

let I be Instruction of SCM+FSA ; :: according to AMISTD_2:def 18 :: thesis: I is IC-good

per cases ( I = [0 ,{} ] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo a,b or ex a, b being Int-Location st I = SubFrom a,b or ex a, b being Int-Location st I = MultBy a,b or ex a, b being Int-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM+FSA st I = goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 or ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 or ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a or ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by SCMFSA_2:120;

suppose I = [0 ,{} ] ; :: thesis: I is IC-good

hence I is IC-good by AMI_3:71, SCMFSA_2:123; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = a := b ; :: thesis: I is IC-good

then consider a, b being Int-Location such that
A1: I = a := b ;
thus I is IC-good by A1; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = AddTo a,b ; :: thesis: I is IC-good

then consider a, b being Int-Location such that
A2: I = AddTo a,b ;
thus I is IC-good by A2; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = SubFrom a,b ; :: thesis: I is IC-good

then consider a, b being Int-Location such that
A3: I = SubFrom a,b ;
thus I is IC-good by A3; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = MultBy a,b ; :: thesis: I is IC-good

then consider a, b being Int-Location such that
A4: I = MultBy a,b ;
thus I is IC-good by A4; :: thesis: verum

end;

suppose ex a, b being Int-Location st I = Divide a,b ; :: thesis: I is IC-good

then consider a, b being Int-Location such that
A5: I = Divide a,b ;
thus I is IC-good by A5; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA st I = goto i1 ; :: thesis: I is IC-good

then consider i1 being Instruction-Location of SCM+FSA such that
A6: I = goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b₁, b₂ being Element of product the Object-Kind of SCM+FSA holds
( not b₂ = b₁ +* ((IC SCM+FSA ) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of SCM+FSA ; :: thesis: ( not s2 = s1 +* ((IC SCM+FSA ) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume s2 = s1 +* ((IC SCM+FSA ) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
IC (Exec I,s1) = i1 by A6, SCMFSA_2:95;
hence (IC (Exec I,s1)) + k = IC (Exec (goto (il. SCM+FSA ,((locnum i1) + k))),s2) by SCMFSA_2:95
.= IC (Exec (IncAddr I,k),s2) by A6, Th89 ;
:: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a =0_goto i1 ; :: thesis: I is IC-good

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A7: I = a =0_goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b₁, b₂ being Element of product the Object-Kind of SCM+FSA holds
( not b₂ = b₁ +* ((IC SCM+FSA ) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of SCM+FSA ; :: thesis: ( not s2 = s1 +* ((IC SCM+FSA ) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume A8: s2 = s1 +* ((IC SCM+FSA ) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
A9: a <> IC SCM+FSA by SCMFSA_2:81;
dom ((IC SCM+FSA ) .--> ((IC s1) + k)) = {(IC SCM+FSA )} by FUNCOP_1:19;
then not a in dom ((IC SCM+FSA ) .--> ((IC s1) + k)) by A9, TARSKI:def 1;
then A10: s1 . a = s2 . a by A8, FUNCT_4:12;

now

per cases ( s1 . a = 0 or s1 . a <> 0 ) ;

suppose A11: s1 . a = 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

then IC (Exec I,s1) = i1 by A7, SCMFSA_2:96;
hence (IC (Exec I,s1)) + k = IC (Exec (a =0_goto (il. SCM+FSA ,((locnum i1) + k))),s2) by A10, A11, SCMFSA_2:96
.= IC (Exec (IncAddr I,k),s2) by A7, Th90 ;
:: thesis: verum

end;

suppose A12: s1 . a <> 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

dom ((IC SCM+FSA ) .--> ((IC s1) + k)) = {(IC SCM+FSA )} by FUNCOP_1:19;
then IC SCM+FSA in dom ((IC SCM+FSA ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A13: IC s2 = ((IC SCM+FSA ) .--> ((IC s1) + k)) . (IC SCM+FSA ) by A8, FUNCT_4:14
.= il. SCM+FSA ,((locnum (IC s1)) + k) by FUNCOP_1:87 ;
A14: IC (Exec I,s2) = Next (IC s2) by A7, A10, A12, SCMFSA_2:96
.= NextLoc (IC s2) by Th88
.= il. SCM+FSA ,(((locnum (IC s1)) + k) + 1) by A13, AMISTD_1:def 13
.= il. SCM+FSA ,(((locnum (IC s1)) + 1) + k) ;
IC (Exec I,s1) = Next (IC s1) by A7, A12, SCMFSA_2:96
.= NextLoc (IC s1) by Th88
.= il. SCM+FSA ,((locnum (IC s1)) + 1) ;
hence (IC (Exec I,s1)) + k = (Exec I,s2) . (IC SCM+FSA ) by A14, AMISTD_1:def 13
.= Next (IC s2) by A7, A10, A12, SCMFSA_2:96
.= IC (Exec (a =0_goto (il. SCM+FSA ,((locnum i1) + k))),s2) by A10, A12, SCMFSA_2:96
.= IC (Exec (IncAddr I,k),s2) by A7, Th90 ;
:: thesis: verum

end;

end;

end;

hence (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) ; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM+FSA ex a being Int-Location st I = a >0_goto i1 ; :: thesis: I is IC-good

then consider a being Int-Location , i1 being Instruction-Location of SCM+FSA such that
A15: I = a >0_goto i1 ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b₁, b₂ being Element of product the Object-Kind of SCM+FSA holds
( not b₂ = b₁ +* ((IC SCM+FSA ) .--> ((IC b₁) + k)) or (IC (Exec I,b₁)) + k = IC (Exec (IncAddr I,k),b₂) )
let s1, s2 be State of SCM+FSA ; :: thesis: ( not s2 = s1 +* ((IC SCM+FSA ) .--> ((IC s1) + k)) or (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) )
assume A16: s2 = s1 +* ((IC SCM+FSA ) .--> ((IC s1) + k)) ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)
A17: a <> IC SCM+FSA by SCMFSA_2:81;
dom ((IC SCM+FSA ) .--> ((IC s1) + k)) = {(IC SCM+FSA )} by FUNCOP_1:19;
then not a in dom ((IC SCM+FSA ) .--> ((IC s1) + k)) by A17, TARSKI:def 1;
then A18: s1 . a = s2 . a by A16, FUNCT_4:12;

now

per cases ( s1 . a > 0 or s1 . a <= 0 ) ;

suppose A19: s1 . a > 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

then IC (Exec I,s1) = i1 by A15, SCMFSA_2:97;
hence (IC (Exec I,s1)) + k = IC (Exec (a >0_goto (il. SCM+FSA ,((locnum i1) + k))),s2) by A18, A19, SCMFSA_2:97
.= IC (Exec (IncAddr I,k),s2) by A15, Th91 ;
:: thesis: verum

end;

suppose A20: s1 . a <= 0 ; :: thesis: (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2)

dom ((IC SCM+FSA ) .--> ((IC s1) + k)) = {(IC SCM+FSA )} by FUNCOP_1:19;
then IC SCM+FSA in dom ((IC SCM+FSA ) .--> ((IC s1) + k)) by TARSKI:def 1;
then A21: IC s2 = ((IC SCM+FSA ) .--> ((IC s1) + k)) . (IC SCM+FSA ) by A16, FUNCT_4:14
.= il. SCM+FSA ,((locnum (IC s1)) + k) by FUNCOP_1:87 ;
A22: IC (Exec I,s2) = Next (IC s2) by A15, A18, A20, SCMFSA_2:97
.= NextLoc (IC s2) by Th88
.= il. SCM+FSA ,(((locnum (IC s1)) + k) + 1) by A21, AMISTD_1:def 13
.= il. SCM+FSA ,(((locnum (IC s1)) + 1) + k) ;
IC (Exec I,s1) = Next (IC s1) by A15, A20, SCMFSA_2:97
.= NextLoc (IC s1) by Th88
.= il. SCM+FSA ,((locnum (IC s1)) + 1) ;
hence (IC (Exec I,s1)) + k = (Exec I,s2) . (IC SCM+FSA ) by A22, AMISTD_1:def 13
.= Next (IC s2) by A15, A18, A20, SCMFSA_2:97
.= IC (Exec (a >0_goto (il. SCM+FSA ,((locnum i1) + k))),s2) by A18, A20, SCMFSA_2:97
.= IC (Exec (IncAddr I,k),s2) by A15, Th91 ;
:: thesis: verum

end;

end;

end;

hence (IC (Exec I,s1)) + k = IC (Exec (IncAddr I,k),s2) ; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = b := f,a ; :: thesis: I is IC-good

then consider a, b being Int-Location , f being FinSeq-Location such that
A23: I = b := f,a ;
thus I is IC-good by A23; :: thesis: verum

end;

suppose ex a, b being Int-Location ex f being FinSeq-Location st I = f,a := b ; :: thesis: I is IC-good

then consider a, b being Int-Location , f being FinSeq-Location such that
A24: I = f,a := b ;
thus I is IC-good by A24; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = a :=len f ; :: thesis: I is IC-good

then consider a being Int-Location , f being FinSeq-Location such that
A25: I = a :=len f ;
thus I is IC-good by A25; :: thesis: verum

end;

suppose ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ; :: thesis: I is IC-good

then consider a being Int-Location , f being FinSeq-Location such that
A26: I = f :=<0,...,0> a ;
thus I is IC-good by A26; :: thesis: verum

end;

end;

end;

let I be Instruction of SCM+FSA ; :: according to AMISTD_2:def 20 :: thesis: I is Exec-preserving
let s1, s2 be State of SCM+FSA ; :: according to AMISTD_2:def 19 :: thesis: ( not s1,s2 equal_outside K52() or Exec I,s1, Exec I,s2 equal_outside K52() )
assume s1,s2 equal_outside NAT ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K52()
hence Exec I,s1, Exec I,s2 equal_outside K52() by SCMFSA6A:32; :: thesis: verum