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 Element of NAT st I = goto i1 or ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 or ex i1 being Element of NAT 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

hence I is IC-good ; :: thesis: verum

end;

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

hence I is IC-good ; :: thesis: verum

end;

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

hence I is IC-good ; :: thesis: verum

end;

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

hence I is IC-good ; :: thesis: verum

end;

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

hence I is IC-good ; :: thesis: verum

end;

suppose A1: ex i1 being Element of NAT st I = goto i1 ; :: thesis: I is IC-good

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

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a =0_goto i1 ; :: thesis: I is IC-good

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

suppose ex i1 being Element of NAT ex a being Int-Location st I = a >0_goto i1 ; :: thesis: I is IC-good

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

now

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

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

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

end;

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

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

end;

end;

end;

hence (IC (Exec I,s1)) + k,SCM+FSA = 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

hence I is IC-good ; :: 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

hence I is IC-good ; :: thesis: verum

end;

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

hence I is IC-good ; :: 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

hence I is IC-good ; :: 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 K53() or Exec I,s1, Exec I,s2 equal_outside K53() )
assume s1,s2 equal_outside NAT ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K53()
hence Exec I,s1, Exec I,s2 equal_outside K53() by SCMFSA6A:32; :: thesis: verum