:: SCMFSA_4 semantic presentation

begin


registration
let a, b be Int-Location;
clustera := b ->  ins-loc-free ;
coherence
 a := b is ins-loc-free
proof
 a := b = [1,{},<*a,b*>] by SCMFSA10:2;
hence  JumpPart (a := b) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
cluster AddTo (a,b) ->  ins-loc-free ;
coherence
 AddTo (a,b) is ins-loc-free
proof
 AddTo (a,b) = [2,{},<*a,b*>] by SCMFSA10:3;
hence  JumpPart (AddTo (a,b)) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
cluster SubFrom (a,b) ->  ins-loc-free ;
coherence
 SubFrom (a,b) is ins-loc-free
proof
 SubFrom (a,b) = [3,{},<*a,b*>] by SCMFSA10:4;
hence  JumpPart (SubFrom (a,b)) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
cluster MultBy (a,b) ->  ins-loc-free ;
coherence
 MultBy (a,b) is ins-loc-free
proof
 MultBy (a,b) = [4,{},<*a,b*>] by SCMFSA10:5;
hence  JumpPart (MultBy (a,b)) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
cluster Divide (a,b) ->  ins-loc-free ;
coherence
 Divide (a,b) is ins-loc-free
proof
 Divide (a,b) = [5,{},<*a,b*>] by SCMFSA10:6;
hence  JumpPart (Divide (a,b)) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;

theorem Th1: :: SCMFSA_4:1
for k, loc being Element of NAT holds IncAddr ((goto loc),k) = goto (loc + k)
proof
let k, loc be Element of NAT ; ::_thesis: IncAddr ((goto loc),k) = goto (loc + k)
A1: InsCode (IncAddr ((goto loc),k)) = InsCode (goto loc) by COMPOS_0:def_9
.= 6 by RECDEF_2:def_1
.= InsCode (goto (loc + k)) by RECDEF_2:def_1 ;
A2: AddressPart (IncAddr ((goto loc),k)) = AddressPart (goto loc) by COMPOS_0:def_9
.= {} by RECDEF_2:def_3
.= AddressPart (goto (loc + k)) by RECDEF_2:def_3 ;
A3: JumpPart (IncAddr ((goto loc),k)) = k + (JumpPart (goto loc)) by COMPOS_0:def_9;
 JumpPart (IncAddr ((goto loc),k)) = JumpPart (goto (loc + k))
proof
thus A4: dom (JumpPart (IncAddr ((goto loc),k))) = dom (JumpPart (goto (loc + k))) by A1, COMPOS_0:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in proj1 (JumpPart (IncAddr ((goto loc),k))) or (JumpPart (IncAddr ((goto loc),k))) . b1 = (JumpPart (goto (loc + k))) . b1 )
A5: JumpPart (goto loc) = <*loc*> by RECDEF_2:def_2;
A6: JumpPart (goto (loc + k)) = <*(loc + k)*> by RECDEF_2:def_2;
let x be set ; ::_thesis: ( not x in proj1 (JumpPart (IncAddr ((goto loc),k))) or (JumpPart (IncAddr ((goto loc),k))) . x = (JumpPart (goto (loc + k))) . x )
assume A7: x in dom (JumpPart (IncAddr ((goto loc),k))) ; ::_thesis: (JumpPart (IncAddr ((goto loc),k))) . x = (JumpPart (goto (loc + k))) . x
 dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A8: x = 1 by A7, A4, A6, TARSKI:def_1;
thus (JumpPart (IncAddr ((goto loc),k))) . x = k + ((JumpPart (goto loc)) . x) by A3, A7, VALUED_1:def_2
.= loc + k by A5, A8, FINSEQ_1:40
.= (JumpPart (goto (loc + k))) . x by A6, A8, FINSEQ_1:40 ; ::_thesis: verum
end;
hence  IncAddr ((goto loc),k) = goto (loc + k) by A1, A2, COMPOS_0:1; ::_thesis: verum
end;

theorem Th2: :: SCMFSA_4:2
for k, loc being Element of NAT
for a being Int-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
proof
let k, loc be Element of NAT ; ::_thesis: for a being Int-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
let a be Int-Location; ::_thesis: IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)
A1: a =0_goto loc = [7,<*loc*>,<*a*>] by SCMFSA10:7;
A2: a =0_goto (loc + k) = [7,<*(loc + k)*>,<*a*>] by SCMFSA10:7;
A3: InsCode (IncAddr ((a =0_goto loc),k)) = InsCode (a =0_goto loc) by COMPOS_0:def_9
.= 7 by A1, RECDEF_2:def_1
.= InsCode (a =0_goto (loc + k)) by A2, RECDEF_2:def_1 ;
A4: AddressPart (IncAddr ((a =0_goto loc),k)) = AddressPart (a =0_goto loc) by COMPOS_0:def_9
.= <*a*> by A1, RECDEF_2:def_3
.= AddressPart (a =0_goto (loc + k)) by A2, RECDEF_2:def_3 ;
A5: JumpPart (IncAddr ((a =0_goto loc),k)) = k + (JumpPart (a =0_goto loc)) by COMPOS_0:def_9;
 JumpPart (IncAddr ((a =0_goto loc),k)) = JumpPart (a =0_goto (loc + k))
proof
thus A6: dom (JumpPart (IncAddr ((a =0_goto loc),k))) = dom (JumpPart (a =0_goto (loc + k))) by A3, COMPOS_0:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in proj1 (JumpPart (IncAddr ((a =0_goto loc),k))) or (JumpPart (IncAddr ((a =0_goto loc),k))) . b1 = (JumpPart (a =0_goto (loc + k))) . b1 )
A7: JumpPart (a =0_goto loc) = <*loc*> by A1, RECDEF_2:def_2;
A8: JumpPart (a =0_goto (loc + k)) = <*(loc + k)*> by A2, RECDEF_2:def_2;
let x be set ; ::_thesis: ( not x in proj1 (JumpPart (IncAddr ((a =0_goto loc),k))) or (JumpPart (IncAddr ((a =0_goto loc),k))) . x = (JumpPart (a =0_goto (loc + k))) . x )
assume A9: x in dom (JumpPart (IncAddr ((a =0_goto loc),k))) ; ::_thesis: (JumpPart (IncAddr ((a =0_goto loc),k))) . x = (JumpPart (a =0_goto (loc + k))) . x
 dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A10: x = 1 by A9, A6, A8, TARSKI:def_1;
thus (JumpPart (IncAddr ((a =0_goto loc),k))) . x = k + ((JumpPart (a =0_goto loc)) . x) by A5, A9, VALUED_1:def_2
.= loc + k by A7, A10, FINSEQ_1:40
.= (JumpPart (a =0_goto (loc + k))) . x by A8, A10, FINSEQ_1:40 ; ::_thesis: verum
end;
hence  IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k) by A3, A4, COMPOS_0:1; ::_thesis: verum
end;

theorem Th3: :: SCMFSA_4:3
for k, loc being Element of NAT
for a being Int-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)
proof
let k, loc be Element of NAT ; ::_thesis: for a being Int-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)
let a be Int-Location; ::_thesis: IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)
A1: a >0_goto loc = [8,<*loc*>,<*a*>] by SCMFSA10:8;
A2: a >0_goto (loc + k) = [8,<*(loc + k)*>,<*a*>] by SCMFSA10:8;
A3: InsCode (IncAddr ((a >0_goto loc),k)) = InsCode (a >0_goto loc) by COMPOS_0:def_9
.= 8 by A1, RECDEF_2:def_1
.= InsCode (a >0_goto (loc + k)) by A2, RECDEF_2:def_1 ;
A4: AddressPart (IncAddr ((a >0_goto loc),k)) = AddressPart (a >0_goto loc) by COMPOS_0:def_9
.= <*a*> by A1, RECDEF_2:def_3
.= AddressPart (a >0_goto (loc + k)) by A2, RECDEF_2:def_3 ;
A5: JumpPart (IncAddr ((a >0_goto loc),k)) = k + (JumpPart (a >0_goto loc)) by COMPOS_0:def_9;
 JumpPart (IncAddr ((a >0_goto loc),k)) = JumpPart (a >0_goto (loc + k))
proof
thus A6: dom (JumpPart (IncAddr ((a >0_goto loc),k))) = dom (JumpPart (a >0_goto (loc + k))) by A3, COMPOS_0:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in proj1 (JumpPart (IncAddr ((a >0_goto loc),k))) or (JumpPart (IncAddr ((a >0_goto loc),k))) . b1 = (JumpPart (a >0_goto (loc + k))) . b1 )
A7: JumpPart (a >0_goto loc) = <*loc*> by A1, RECDEF_2:def_2;
A8: JumpPart (a >0_goto (loc + k)) = <*(loc + k)*> by A2, RECDEF_2:def_2;
let x be set ; ::_thesis: ( not x in proj1 (JumpPart (IncAddr ((a >0_goto loc),k))) or (JumpPart (IncAddr ((a >0_goto loc),k))) . x = (JumpPart (a >0_goto (loc + k))) . x )
assume A9: x in dom (JumpPart (IncAddr ((a >0_goto loc),k))) ; ::_thesis: (JumpPart (IncAddr ((a >0_goto loc),k))) . x = (JumpPart (a >0_goto (loc + k))) . x
 dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then A10: x = 1 by A9, A6, A8, TARSKI:def_1;
thus (JumpPart (IncAddr ((a >0_goto loc),k))) . x = k + ((JumpPart (a >0_goto loc)) . x) by A5, A9, VALUED_1:def_2
.= loc + k by A7, A10, FINSEQ_1:40
.= (JumpPart (a >0_goto (loc + k))) . x by A8, A10, FINSEQ_1:40 ; ::_thesis: verum
end;
hence  IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k) by A3, A4, COMPOS_0:1; ::_thesis: verum
end;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
clusterb := (f,a) ->  ins-loc-free ;
coherence
 b := (f,a) is ins-loc-free
proof
thus  JumpPart (b := (f,a)) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
cluster(f,a) := b ->  ins-loc-free ;
coherence
 (f,a) := b is ins-loc-free
proof
thus  JumpPart ((f,a) := b) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f ->  ins-loc-free ;
coherence
 a :=len f is ins-loc-free
proof
thus  JumpPart (a :=len f) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
clusterf :=<0,...,0> a ->  ins-loc-free ;
coherence
 f :=<0,...,0> a is ins-loc-free
proof
thus  JumpPart (f :=<0,...,0> a) is empty by RECDEF_2:def_2; :: according to COMPOS_0:def_8 ::_thesis: verum
end;
end;

 begin

registration
cluster SCM+FSA  ->  relocable ;
coherence
 SCM+FSA is relocable
proof
let INS be Instruction of SCM+FSA; :: according to AMISTD_5:def_2 ::_thesis: INS is relocable
let j, k be Nat; :: according to AMISTD_5:def_1 ::_thesis: for b1 being set holds R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (b1,k))), IncIC ((Exec ((IncAddr (INS,j)),b1)),k))
reconsider k = k as Element of NAT by ORDINAL1:def_12;
let s be State of SCM+FSA; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
A1: IC (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) = (IC (Exec ((IncAddr (INS,j)),s))) + k by MEMSTR_0:53
.= IC (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) by AMISTD_2:def_3 ;
percases ( InsCode INS = 0 or InsCode INS = 1 or InsCode INS = 2 or InsCode INS = 3 or InsCode INS = 4 or InsCode INS = 5 or InsCode INS = 6 or InsCode INS = 7 or InsCode INS = 8 or InsCode INS = 9 or InsCode INS = 10 or InsCode INS = 11 or InsCode INS = 12 ) by NAT_1:36, SCMFSA_2:16;
suppose InsCode INS = 0 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then A2: INS = halt SCM+FSA by SCMFSA_2:95;
then A3: IncAddr (INS,j) = halt SCM+FSA by COMPOS_0:4;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = Exec (INS,(IncIC (s,k))) by A2, COMPOS_0:4
.= IncIC (s,k) by A2, EXTPRO_1:def_3
.= IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A3, EXTPRO_1:def_3 ;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) ; ::_thesis: verum
end;
suppose InsCode INS = 1 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A4: INS = da := db by SCMFSA_2:30;
A5: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A4, COMPOS_0:4
.= (IncIC (s,k)) . f by A4, SCMFSA_2:63
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A4, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . f by A4, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da = d or da <> d ) ;
supposeA6: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A4, COMPOS_0:4
.= (IncIC (s,k)) . db by A4, A6, SCMFSA_2:63
.= s . db by SCMFSA_3:3
.= (Exec (INS,s)) . d by A4, A6, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . d by A4, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
supposeA7: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A4, COMPOS_0:4
.= (IncIC (s,k)) . d by A4, A7, SCMFSA_2:63
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A4, A7, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . d by A4, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A5, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 2 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A8: INS = AddTo (da,db) by SCMFSA_2:31;
A9: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A8, COMPOS_0:4
.= (IncIC (s,k)) . f by A8, SCMFSA_2:64
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A8, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . f by A8, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da = d or da <> d ) ;
supposeA10: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A8, COMPOS_0:4
.= ((IncIC (s,k)) . da) + ((IncIC (s,k)) . db) by A10, A8, SCMFSA_2:64
.= (s . da) + ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) + (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A8, A10, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . d by A8, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
supposeA11: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A8, COMPOS_0:4
.= (IncIC (s,k)) . d by A8, A11, SCMFSA_2:64
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A8, A11, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . d by A8, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A9, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 3 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A12: INS = SubFrom (da,db) by SCMFSA_2:32;
A13: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A12, COMPOS_0:4
.= (IncIC (s,k)) . f by A12, SCMFSA_2:65
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A12, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . f by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da = d or da <> d ) ;
supposeA14: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A12, COMPOS_0:4
.= ((IncIC (s,k)) . da) - ((IncIC (s,k)) . db) by A14, A12, SCMFSA_2:65
.= (s . da) - ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) - (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A12, A14, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
supposeA15: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A12, COMPOS_0:4
.= (IncIC (s,k)) . d by A12, A15, SCMFSA_2:65
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A12, A15, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A13, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 4 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A16: INS = MultBy (da,db) by SCMFSA_2:33;
A17: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A16, COMPOS_0:4
.= (IncIC (s,k)) . f by A16, SCMFSA_2:66
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A16, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . f by A16, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da = d or da <> d ) ;
supposeA18: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A16, COMPOS_0:4
.= ((IncIC (s,k)) . da) * ((IncIC (s,k)) . db) by A18, A16, SCMFSA_2:66
.= (s . da) * ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) * (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A16, A18, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
supposeA19: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A16, COMPOS_0:4
.= (IncIC (s,k)) . d by A16, A19, SCMFSA_2:66
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A16, A19, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A17, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 5 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A20: INS = Divide (da,db) by SCMFSA_2:34;
A21: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A20, COMPOS_0:4
.= (IncIC (s,k)) . f by A20, SCMFSA_2:67
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A20, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . f by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da <> db or da = db ) ;
supposeA22: da <> db ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
hereby  ::_thesis: verum
percases ( da = d or db = d or ( da <> d & db <> d ) ) ;
supposeA23: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A20, COMPOS_0:4
.= ((IncIC (s,k)) . da) div ((IncIC (s,k)) . db) by A22, A23, A20, SCMFSA_2:67
.= (s . da) div ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) div (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A22, A23, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
supposeA24: db = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A20, COMPOS_0:4
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A24, A20, SCMFSA_2:67
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) mod (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A24, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
supposeA25: ( da <> d & db <> d ) ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A20, COMPOS_0:4
.= (IncIC (s,k)) . d by A20, A25, SCMFSA_2:67
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A25, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
end;
supposeA26: da = db ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da = d or da <> d ) ;
supposeA27: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A20, COMPOS_0:4
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A26, A27, A20, SCMFSA_2:67
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) mod (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A26, A27, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
supposeA28: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A20, COMPOS_0:4
.= (IncIC (s,k)) . d by A20, A26, A28, SCMFSA_2:67
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A26, A28, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
end;
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A21, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 6 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider loc being Element of NAT  such that
A29: INS = goto loc by SCMFSA_2:35;
A30: IncAddr (INS,(j + k)) = goto (loc + (j + k)) by A29, Th1;
reconsider jj = j as Element of NAT by ORDINAL1:def_12;
A31: IncAddr (INS,jj) = goto (loc + jj) by A29, Th1;
A32: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A30, SCMFSA_2:69
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A31, SCMFSA_2:69
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A30, SCMFSA_2:69
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A31, SCMFSA_2:69
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A32, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 7 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider loc being Element of NAT , da being Int-Location such that
A33: INS = da =0_goto loc by SCMFSA_2:36;
A34: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A33, Th2;
reconsider jj = j as Element of NAT by ORDINAL1:def_12;
A35: IncAddr (INS,jj) = da =0_goto (loc + jj) by A33, Th2;
A36: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A34, SCMFSA_2:70
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A35, SCMFSA_2:70
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A34, SCMFSA_2:70
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A35, SCMFSA_2:70
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A1, A36, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 8 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider loc being Element of NAT , da being Int-Location such that
A37: INS = da >0_goto loc by SCMFSA_2:37;
A38: IncAddr (INS,(j + k)) = da >0_goto (loc + (j + k)) by A37, Th3;
reconsider jj = j as Element of NAT by ORDINAL1:def_12;
A39: IncAddr (INS,jj) = da >0_goto (loc + jj) by A37, Th3;
A40: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A38, SCMFSA_2:71
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A39, SCMFSA_2:71
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A38, SCMFSA_2:71
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A39, SCMFSA_2:71
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A40, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 9 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider db, da being Int-Location, f being FinSeq-Location  such that
A41: INS = da := (f,db) by SCMFSA_2:38;
A42: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A41, COMPOS_0:4
.= (IncIC (s,k)) . f by A41, SCMFSA_2:72
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A41, SCMFSA_2:72
.= (Exec ((IncAddr (INS,j)),s)) . f by A41, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da = d or da <> d ) ;
supposeA43: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
consider m being Element of NAT  such that
A44: m = abs (s . db) and
A45: (Exec (INS,s)) . da = (s . f) /. m by A41, SCMFSA_2:72;
A46: ex m1 being Element of NAT st
( m1 = abs ((IncIC (s,k)) . db) & (Exec (INS,(IncIC (s,k)))) . da = ((IncIC (s,k)) . f) /. m1 ) by A41, SCMFSA_2:72;
A47: (IncIC (s,k)) . db = s . db by SCMFSA_3:3;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A41, COMPOS_0:4
.= (s . f) /. m by A44, A46, A43, A47, SCMFSA_3:4
.= (IncIC ((Exec (INS,s)),k)) . d by A45, A43, SCMFSA_3:3
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A41, COMPOS_0:4 ; ::_thesis: verum
end;
supposeA48: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A41, COMPOS_0:4
.= (IncIC (s,k)) . d by A41, A48, SCMFSA_2:72
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A41, A48, SCMFSA_2:72
.= (Exec ((IncAddr (INS,j)),s)) . d by A41, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A42, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 10 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider db, da being Int-Location, f being FinSeq-Location  such that
A49: INS = (f,db) := da by SCMFSA_2:39;
A50: now__::_thesis:_for_g_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._g_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._g
let g be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
consider m being Element of NAT  such that
A51: m = abs (s . db) and
A52: (Exec (INS,s)) . f = (s . f) +* (m,(s . da)) by A49, SCMFSA_2:73;
A53: ex m1 being Element of NAT st
( m1 = abs ((IncIC (s,k)) . db) & (Exec (INS,(IncIC (s,k)))) . f = ((IncIC (s,k)) . f) +* (m1,((IncIC (s,k)) . da)) ) by A49, SCMFSA_2:73;
percases ( f = g or f <> g ) ;
supposeA54: f = g ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A55: ( (IncIC (s,k)) . f = s . f & (IncIC (s,k)) . db = s . db ) by SCMFSA_3:3, SCMFSA_3:4;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A49, COMPOS_0:4
.= (s . f) +* (m,(s . da)) by A51, A53, A54, A55, SCMFSA_3:3
.= (IncIC ((Exec (INS,s)),k)) . g by A52, A54, SCMFSA_3:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A49, COMPOS_0:4 ; ::_thesis: verum
end;
supposeA56: f <> g ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A49, COMPOS_0:4
.= (IncIC (s,k)) . g by A49, A56, SCMFSA_2:73
.= s . g by SCMFSA_3:4
.= (Exec (INS,s)) . g by A49, A56, SCMFSA_2:73
.= (Exec ((IncAddr (INS,j)),s)) . g by A49, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:4 ; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A49, COMPOS_0:4
.= (IncIC (s,k)) . d by A49, SCMFSA_2:73
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A49, SCMFSA_2:73
.= (Exec ((IncAddr (INS,j)),s)) . d by A49, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A50, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 11 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da being Int-Location, f being FinSeq-Location  such that
A57: INS = da :=len f by SCMFSA_2:40;
A58: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._f_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._f
let f be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A57, COMPOS_0:4
.= (IncIC (s,k)) . f by A57, SCMFSA_2:74
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A57, SCMFSA_2:74
.= (Exec ((IncAddr (INS,j)),s)) . f by A57, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; ::_thesis: verum
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
percases ( da = d or da <> d ) ;
supposeA59: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A57, COMPOS_0:4
.= len ((IncIC (s,k)) . f) by A59, A57, SCMFSA_2:74
.= len (s . f) by SCMFSA_3:4
.= (Exec (INS,s)) . d by A57, A59, SCMFSA_2:74
.= (IncIC ((Exec (INS,s)),k)) . d by SCMFSA_3:3
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A57, COMPOS_0:4 ; ::_thesis: verum
end;
supposeA60: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A57, COMPOS_0:4
.= (IncIC (s,k)) . d by A57, A60, SCMFSA_2:74
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A57, A60, SCMFSA_2:74
.= (Exec ((IncAddr (INS,j)),s)) . d by A57, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
end;
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A58, A1, SCMFSA_2:104; ::_thesis: verum
end;
suppose InsCode INS = 12 ; ::_thesis: R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da being Int-Location, f being FinSeq-Location  such that
A61: INS = f :=<0,...,0> da by SCMFSA_2:41;
A62: now__::_thesis:_for_g_being_FinSeq-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._g_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._g
let g be FinSeq-Location ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A63: ( ex m being Element of NAT st
( m = abs (s . da) & (Exec (INS,s)) . f = m |-> 0 ) & ex m being Element of NAT st
( m = abs ((IncIC (s,k)) . da) & (Exec (INS,(IncIC (s,k)))) . f = m |-> 0 ) ) by A61, SCMFSA_2:75;
percases ( f = g or f <> g ) ;
supposeA64: f = g ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A65: (IncIC (s,k)) . da = s . da by SCMFSA_3:3;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A61, COMPOS_0:4
.= (IncIC ((Exec (INS,s)),k)) . g by A63, A64, A65, SCMFSA_3:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A61, COMPOS_0:4 ; ::_thesis: verum
end;
supposeA66: f <> g ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A61, COMPOS_0:4
.= (IncIC (s,k)) . g by A61, A66, SCMFSA_2:75
.= s . g by SCMFSA_3:4
.= (Exec (INS,s)) . g by A61, A66, SCMFSA_2:75
.= (Exec ((IncAddr (INS,j)),s)) . g by A61, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:4 ; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_d_being_Int-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d
let d be Int-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A61, COMPOS_0:4
.= (IncIC (s,k)) . d by A61, SCMFSA_2:75
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A61, SCMFSA_2:75
.= (Exec ((IncAddr (INS,j)),s)) . d by A61, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; ::_thesis: verum
end;
hence  R41( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A62, A1, SCMFSA_2:104; ::_thesis: verum
end;
end;
end;
end;

theorem :: SCMFSA_4:4
for k being Element of NAT
for i being Instruction of SCM+FSA st not InsCode i in {6,7,8} holds
IncAddr (i,k) = i
proof
let k be Element of NAT ; ::_thesis: for i being Instruction of SCM+FSA st not InsCode i in {6,7,8} holds
IncAddr (i,k) = i
let i be Instruction of SCM+FSA; ::_thesis: ( not InsCode i in {6,7,8} implies IncAddr (i,k) = i )
assume  not InsCode i in {6,7,8} ; ::_thesis: IncAddr (i,k) = i
then A1: ( InsCode i <> 6 & InsCode i <> 7 & InsCode i <> 8 ) by ENUMSET1:def_1;
percases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A1, NAT_1:36, SCMFSA_2:16;
suppose InsCode i = 0 ; ::_thesis: IncAddr (i,k) = i
then  i = halt SCM+FSA by SCMFSA_2:95;
hence  IncAddr (i,k) = i by COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 1 ; ::_thesis: IncAddr (i,k) = i
then consider da, db being Int-Location such that
A2: i = da := db by SCMFSA_2:30;
thus  IncAddr (i,k) = i by A2, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 2 ; ::_thesis: IncAddr (i,k) = i
then consider da, db being Int-Location such that
A3: i = AddTo (da,db) by SCMFSA_2:31;
thus  IncAddr (i,k) = i by A3, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 3 ; ::_thesis: IncAddr (i,k) = i
then consider da, db being Int-Location such that
A4: i = SubFrom (da,db) by SCMFSA_2:32;
thus  IncAddr (i,k) = i by A4, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 4 ; ::_thesis: IncAddr (i,k) = i
then consider da, db being Int-Location such that
A5: i = MultBy (da,db) by SCMFSA_2:33;
thus  IncAddr (i,k) = i by A5, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: IncAddr (i,k) = i
then consider da, db being Int-Location such that
A6: i = Divide (da,db) by SCMFSA_2:34;
thus  IncAddr (i,k) = i by A6, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 9 ; ::_thesis: IncAddr (i,k) = i
then consider db, da being Int-Location, f being FinSeq-Location  such that
A7: i = da := (f,db) by SCMFSA_2:38;
thus  IncAddr (i,k) = i by A7, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 10 ; ::_thesis: IncAddr (i,k) = i
then consider db, da being Int-Location, f being FinSeq-Location  such that
A8: i = (f,db) := da by SCMFSA_2:39;
thus  IncAddr (i,k) = i by A8, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 11 ; ::_thesis: IncAddr (i,k) = i
then consider da being Int-Location, f being FinSeq-Location  such that
A9: i = da :=len f by SCMFSA_2:40;
thus  IncAddr (i,k) = i by A9, COMPOS_0:4; ::_thesis: verum
end;
suppose InsCode i = 12 ; ::_thesis: IncAddr (i,k) = i
then consider da being Int-Location, f being FinSeq-Location  such that
A10: i = f :=<0,...,0> da by SCMFSA_2:41;
thus  IncAddr (i,k) = i by A10, COMPOS_0:4; ::_thesis: verum
end;
end;
end;