:: SCMFSA6A semantic presentation

begin


definition
let P be NAT -defined the InstructionsF of SCM+FSA -valued finite Function;
let l be Element of NAT ;
func Directed (P,l) ->  preProgram of SCM+FSA equals :: SCMFSA6A:def 1
P +~ ((halt SCM+FSA),(goto l));
coherence
 P +~ ((halt SCM+FSA),(goto l)) is preProgram of SCM+FSA ;
end;

:: deftheorem  defines Directed SCMFSA6A:def_1_:_
 for P being NAT -defined the InstructionsF of SCM+FSA -valued finite Function
for l being Element of NAT holds Directed (P,l) = P +~ ((halt SCM+FSA),(goto l));

definition
let P be NAT -defined the InstructionsF of SCM+FSA -valued finite Function;
func Directed P ->  preProgram of SCM+FSA equals :: SCMFSA6A:def 2
 Directed (P,(card P));
coherence
 Directed (P,(card P)) is preProgram of SCM+FSA ;
end;

:: deftheorem  defines Directed SCMFSA6A:def_2_:_
 for P being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds Directed P = Directed (P,(card P));

registration
let I be Program of ;
cluster Directed I ->  non empty initial ;
coherence
 ( Directed I is initial & not Directed I is empty )
proof
thus  Directed I is initial ::_thesis: not Directed I is empty
proof
let m, n be Nat; :: according to AFINSQ_1:def_12 ::_thesis: ( not n in dom (Directed I) or n <= m or m in dom (Directed I) )
assume that
A1: n in dom (Directed I) and
A2: m < n ; ::_thesis: m in dom (Directed I)
 n in dom I by A1, FUNCT_4:99;
then  m in dom I by A2, AFINSQ_1:def_12;
hence  m in dom (Directed I) by FUNCT_4:99; ::_thesis: verum
end;
thus  not Directed I is empty ; ::_thesis: verum
end;
end;

theorem :: SCMFSA6A:1
for I being Program of holds not halt SCM+FSA in rng (Directed I) by FUNCT_4:100;

theorem :: SCMFSA6A:2
for m being Element of NAT
for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))
proof
let m be Element of NAT ; ::_thesis: for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))
let I be Program of ; ::_thesis: Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))
 rng ((halt SCM+FSA) .--> (goto (card I))) = {(goto (card I))} by FUNCOP_1:8;
then A2: rng ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card I)))) c= (rng (id the InstructionsF of SCM+FSA)) \/ {(goto (card I))} by FUNCT_4:17;
A3: (rng (id the InstructionsF of SCM+FSA)) \/ {(goto (card I))} = the InstructionsF of SCM+FSA by ZFMISC_1:40;
 dom ((halt SCM+FSA) .--> (goto (card I))) = {(halt SCM+FSA)} by FUNCOP_1:13;
then  dom ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card I)))) = (dom (id the InstructionsF of SCM+FSA)) \/ {(halt SCM+FSA)} by FUNCT_4:def_1
.= the InstructionsF of SCM+FSA by ZFMISC_1:40 ;
then reconsider f = (id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card I))) as Function of the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA by A2, A3, FUNCT_2:def_1, RELSET_1:4;
A4: IncAddr ((goto (card I)),m) = goto (m + (card I)) by SCMFSA_4:1;
 dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ;
then A5: f = (id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))) by FUNCT_7:def_3;
A7: rng I c= the InstructionsF of SCM+FSA by RELAT_1:def_19;
X1: Reloc ((Directed I),m) = IncAddr ((Shift ((Directed I),m)),m) by COMPOS_1:34;
X2: Reloc (I,m) = IncAddr ((Shift (I,m)),m) by COMPOS_1:34;
Directed I = Directed I
.= f * I by A5, A7, FUNCT_7:116 ;
hence  Reloc ((Directed I),m) = IncAddr ((f * (Shift (I,m))),m) by VALUED_1:22, X1
.= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m)) by A4, COMPOS_1:47, X2 ;
::_thesis: verum
end;

      set q = (intloc 0) .--> 1;

set f = the_Values_of SCM+FSA;

theorem Th23: :: SCMFSA6A:3
for i being Instruction of SCM+FSA
for s being State of SCM+FSA holds
( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = succ (IC s) )
proof
let i be Instruction of SCM+FSA; ::_thesis: for s being State of SCM+FSA holds
( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = succ (IC s) )
let s be State of SCM+FSA; ::_thesis: ( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = succ (IC s) )
A1: InsCode i <= 12 by SCMFSA_2:16;
assume A4: not InsCode i in {0,6,7,8} ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then A5: ( InsCode i <> 0 & InsCode i <> 6 ) by ENUMSET1:def_2;
A6: ( InsCode i <> 7 & InsCode i <> 8 ) by A4, ENUMSET1:def_2;
percases ( 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 A5, A6, SCMFSA_2:16, NAT_1:36;
suppose InsCode i = 1 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a, b being Int-Location st i = a := b by SCMFSA_2:30;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:63; ::_thesis: verum
end;
suppose InsCode i = 2 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:31;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:64; ::_thesis: verum
end;
suppose InsCode i = 3 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:32;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:65; ::_thesis: verum
end;
suppose InsCode i = 4 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:33;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:66; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:34;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:67; ::_thesis: verum
end;
suppose InsCode i = 9 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) by SCMFSA_2:38;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:72; ::_thesis: verum
end;
suppose InsCode i = 10 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:73; ::_thesis: verum
end;
suppose InsCode i = 11 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a being Int-Location ex f being FinSeq-Location st i = a :=len f by SCMFSA_2:40;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:74; ::_thesis: verum
end;
suppose InsCode i = 12 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then  ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41;
hence  (Exec (i,s)) . (IC ) = succ (IC s) by SCMFSA_2:75; ::_thesis: verum
end;
end;
end;

theorem :: SCMFSA6A:4
canceled;

theorem :: SCMFSA6A:5
canceled;

theorem :: SCMFSA6A:6
canceled;

theorem :: SCMFSA6A:7
canceled;

theorem :: SCMFSA6A:8
for s1, s2 being State of SCM+FSA
for n being Element of NAT
for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
proof
set D = Data-Locations ;
let s1, s2 be State of SCM+FSA; ::_thesis: for n being Element of NAT
for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
let n be Element of NAT ; ::_thesis: for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
let i be Instruction of SCM+FSA; ::_thesis: ( (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 implies ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) ) )
assume that
A1: (IC s1) + n = IC s2 and
A2: DataPart s1 = DataPart s2 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
reconsider k1 = IC s1 as Element of NAT ;
A3: (succ (IC s1)) + n = (k1 + 1) + n by NAT_1:38
.= (k1 + n) + 1
.= succ (IC s2) by A1, NAT_1:38 ;
A4: now__::_thesis:_(_(_InsCode_i_<_6_or_8_<_InsCode_i_)_&_InsCode_i_<>_0_implies_(IC_(Exec_(i,s1)))_+_n_=_IC_(Exec_((IncAddr_(i,n)),s2))_)
set I = InsCode i;
assume that
A5: ( InsCode i < 6 or 8 < InsCode i ) and
A6: InsCode i <> 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))
 ( not InsCode i = 6 & not InsCode i = 7 & not InsCode i = 8 ) by A5;
then  not InsCode i in {6,7,8} by ENUMSET1:def_1;
then A7: IncAddr (i,n) = i by SCMFSA_4:4;
 ( not InsCode i = 0 & not InsCode i = 6 & not InsCode i = 7 & not InsCode i = 8 ) by A5, A6;
then A8: not InsCode i in {0,6,7,8} by ENUMSET1:def_2;
then  IC (Exec (i,s1)) = succ (IC s1) by Th23;
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A8, A7, Th23; ::_thesis: verum
end;
A12: InsCode i <= 12 by SCMFSA_2:16;
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 = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by SCMFSA_2:16, NAT_1:36;
suppose InsCode i = 0 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
then A13: i = halt SCM+FSA by SCMFSA_2:95;
then  ( Exec (i,s1) = s1 & Exec (i,s2) = s2 ) by EXTPRO_1:def_3;
hence  ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) ) by A1, A2, A13, COMPOS_0:4; ::_thesis: verum
end;
supposeA14: InsCode i = 1 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A15: i = da := db by A14, SCMFSA_2:30;
A16: IncAddr (i,n) = i by A15, COMPOS_0:4;
A17: now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( c = da or c <> da ) ;
supposeA18: c = da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . db by A15, SCMFSA_2:63
.= s2 . db by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A15, A16, A18, SCMFSA_2:63 ;
::_thesis: verum
end;
supposeA19: c <> da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . c by A15, SCMFSA_2:63
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A15, A16, A19, SCMFSA_2:63 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A15, SCMFSA_2:63
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A15, A16, SCMFSA_2:63 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A17, SCMFSA_M:2; ::_thesis: verum
end;
supposeA20: InsCode i = 2 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A21: i = AddTo (da,db) by A20, SCMFSA_2:31;
A22: IncAddr (i,n) = i by A21, COMPOS_0:4;
A23: now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( c = da or c <> da ) ;
supposeA24: c = da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
 ( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) + (s2 . db) by A21, A24, SCMFSA_2:64
.= (Exec ((IncAddr (i,n)),s2)) . c by A21, A22, A24, SCMFSA_2:64 ;
::_thesis: verum
end;
supposeA25: c <> da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . c by A21, SCMFSA_2:64
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A21, A22, A25, SCMFSA_2:64 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A21, SCMFSA_2:64
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A21, A22, SCMFSA_2:64 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A23, SCMFSA_M:2; ::_thesis: verum
end;
supposeA26: InsCode i = 3 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A27: i = SubFrom (da,db) by A26, SCMFSA_2:32;
A28: IncAddr (i,n) = i by A27, COMPOS_0:4;
A29: now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( c = da or c <> da ) ;
supposeA30: c = da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
 ( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) - (s2 . db) by A27, A30, SCMFSA_2:65
.= (Exec ((IncAddr (i,n)),s2)) . c by A27, A28, A30, SCMFSA_2:65 ;
::_thesis: verum
end;
supposeA31: c <> da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . c by A27, SCMFSA_2:65
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A27, A28, A31, SCMFSA_2:65 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A27, SCMFSA_2:65
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A27, A28, SCMFSA_2:65 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A29, SCMFSA_M:2; ::_thesis: verum
end;
supposeA32: InsCode i = 4 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A33: i = MultBy (da,db) by A32, SCMFSA_2:33;
A34: IncAddr (i,n) = i by A33, COMPOS_0:4;
A35: now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( c = da or c <> da ) ;
supposeA36: c = da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
 ( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) * (s2 . db) by A33, A36, SCMFSA_2:66
.= (Exec ((IncAddr (i,n)),s2)) . c by A33, A34, A36, SCMFSA_2:66 ;
::_thesis: verum
end;
supposeA37: c <> da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . c by A33, SCMFSA_2:66
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A33, A34, A37, SCMFSA_2:66 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A33, SCMFSA_2:66
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A33, A34, SCMFSA_2:66 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A35, SCMFSA_M:2; ::_thesis: verum
end;
supposeA38: InsCode i = 5 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A39: i = Divide (da,db) by A38, SCMFSA_2:34;
A40: IncAddr (i,n) = i by A39, COMPOS_0:4;
A41: now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( c = db or ( c = da & c <> db ) or ( c <> da & c <> db ) ) ;
supposeA42: c = db ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
 ( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) mod (s2 . db) by A39, A42, SCMFSA_2:67
.= (Exec ((IncAddr (i,n)),s2)) . c by A39, A40, A42, SCMFSA_2:67 ;
::_thesis: verum
end;
supposeA43: ( c = da & c <> db ) ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
 ( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) div (s2 . db) by A39, A43, SCMFSA_2:67
.= (Exec ((IncAddr (i,n)),s2)) . c by A39, A40, A43, SCMFSA_2:67 ;
::_thesis: verum
end;
supposeA44: ( c <> da & c <> db ) ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . c by A39, SCMFSA_2:67
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A39, A40, A44, SCMFSA_2:67 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A39, SCMFSA_2:67
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A39, A40, SCMFSA_2:67 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A41, SCMFSA_M:2; ::_thesis: verum
end;
suppose InsCode i = 6 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
then consider loc being Element of NAT  such that
A45: i = goto loc by SCMFSA_2:35;
A46: IncAddr (i,n) = goto (loc + n) by A45, SCMFSA_4:1;
A47: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A45, SCMFSA_2:69
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A46, SCMFSA_2:69 ; ::_thesis: verum
end;
 IC (Exec (i,s1)) = loc by A45, SCMFSA_2:69;
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A46, SCMFSA_2:69; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A45, SCMFSA_2:69
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A46, SCMFSA_2:69 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A47, SCMFSA_M:2; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
then consider loc being Element of NAT , da being Int-Location such that
A48: i = da =0_goto loc by SCMFSA_2:36;
A49: IncAddr (i,n) = da =0_goto (loc + n) by A48, SCMFSA_4:2;
A50: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A48, SCMFSA_2:70
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A49, SCMFSA_2:70 ; ::_thesis: verum
end;
hereby  ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
percases ( s1 . da = 0 or s1 . da <> 0 ) ;
suppose s1 . da = 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))
then  ( s2 . da = 0 & IC (Exec (i,s1)) = loc ) by A2, A48, SCMFSA_M:2, SCMFSA_2:70;
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A49, SCMFSA_2:70; ::_thesis: verum
end;
suppose s1 . da <> 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))
then  ( s2 . da <> 0 & IC (Exec (i,s1)) = succ (IC s1) ) by A2, A48, SCMFSA_M:2, SCMFSA_2:70;
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A49, SCMFSA_2:70; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A48, SCMFSA_2:70
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A49, SCMFSA_2:70 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A50, SCMFSA_M:2; ::_thesis: verum
end;
suppose InsCode i = 8 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
then consider loc being Element of NAT , da being Int-Location such that
A51: i = da >0_goto loc by SCMFSA_2:37;
A52: IncAddr (i,n) = da >0_goto (loc + n) by A51, SCMFSA_4:3;
A53: now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A51, SCMFSA_2:71
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A52, SCMFSA_2:71 ; ::_thesis: verum
end;
hereby  ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
percases ( s1 . da > 0 or s1 . da <= 0 ) ;
suppose s1 . da > 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))
then  ( s2 . da > 0 & IC (Exec (i,s1)) = loc ) by A2, A51, SCMFSA_M:2, SCMFSA_2:71;
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A52, SCMFSA_2:71; ::_thesis: verum
end;
suppose s1 . da <= 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))
then  ( s2 . da <= 0 & IC (Exec (i,s1)) = succ (IC s1) ) by A2, A51, SCMFSA_M:2, SCMFSA_2:71;
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A52, SCMFSA_2:71; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A51, SCMFSA_2:71
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A52, SCMFSA_2:71 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A53, SCMFSA_M:2; ::_thesis: verum
end;
supposeA54: InsCode i = 9 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider db, da being Int-Location, f being FinSeq-Location  such that
A55: i = da := (f,db) by A54, SCMFSA_2:38;
A56: IncAddr (i,n) = i by A55, COMPOS_0:4;
A57: now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( c = da or c <> da ) ;
supposeA58: c = da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
then consider m being Element of NAT  such that
A59: m = abs (s1 . db) and
A60: (Exec ((da := (f,db)),s1)) . c = (s1 . f) /. m by SCMFSA_2:72;
A61: s1 . f = s2 . f by A2, SCMFSA_M:2;
consider m2 being Element of NAT  such that
A62: m2 = abs (s2 . db) and
A63: (Exec ((da := (f,db)),s2)) . c = (s2 . f) /. m2 by A58, SCMFSA_2:72;
 m = m2 by A2, A59, A62, SCMFSA_M:2;
hence  (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c by A55, A60, A63, A61, COMPOS_0:4; ::_thesis: verum
end;
supposeA64: c <> da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . c by A55, SCMFSA_2:72
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A55, A56, A64, SCMFSA_2:72 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A55, SCMFSA_2:72
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A55, A56, SCMFSA_2:72 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A57, SCMFSA_M:2; ::_thesis: verum
end;
supposeA65: InsCode i = 10 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider db, da being Int-Location, f being FinSeq-Location  such that
A66: i = (f,db) := da by A65, SCMFSA_2:39;
A67: IncAddr (i,n) = i by A66, COMPOS_0:4;
A68: now__::_thesis:_for_g_being_FinSeq-Location_holds_(Exec_(i,s1))_._g_=_(Exec_((IncAddr_(i,n)),s2))_._g
let g be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( g = f or g <> f ) ;
supposeA69: g = f ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
A70: ( s1 . da = s2 . da & s1 . f = s2 . f ) by A2, SCMFSA_M:2;
consider m2 being Element of NAT  such that
A71: m2 = abs (s2 . db) and
A72: (Exec (((f,db) := da),s2)) . f = (s2 . f) +* (m2,(s2 . da)) by SCMFSA_2:73;
consider m1 being Element of NAT  such that
A73: m1 = abs (s1 . db) and
A74: (Exec (((f,db) := da),s1)) . f = (s1 . f) +* (m1,(s1 . da)) by SCMFSA_2:73;
 m1 = m2 by A2, A73, A71, SCMFSA_M:2;
hence  (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g by A66, A69, A74, A72, A70, COMPOS_0:4; ::_thesis: verum
end;
supposeA75: g <> f ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . g = s1 . g by A66, SCMFSA_2:73
.= s2 . g by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . g by A66, A67, A75, SCMFSA_2:73 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A66, SCMFSA_2:73
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A66, A67, SCMFSA_2:73 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A68, SCMFSA_M:2; ::_thesis: verum
end;
supposeA76: InsCode i = 11 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da being Int-Location, f being FinSeq-Location  such that
A77: i = da :=len f by A76, SCMFSA_2:40;
A78: IncAddr (i,n) = i by A77, COMPOS_0:4;
A79: now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( c = da or c <> da ) ;
supposeA80: c = da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = len (s1 . f) by A77, SCMFSA_2:74
.= len (s2 . f) by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A77, A78, A80, SCMFSA_2:74 ;
::_thesis: verum
end;
supposeA81: c <> da ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . c = s1 . c by A77, SCMFSA_2:74
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A77, A78, A81, SCMFSA_2:74 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_f_being_FinSeq-Location_holds_(Exec_(i,s1))_._f_=_(Exec_((IncAddr_(i,n)),s2))_._f
let f be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A77, SCMFSA_2:74
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A77, A78, SCMFSA_2:74 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A79, SCMFSA_M:2; ::_thesis: verum
end;
supposeA82: InsCode i = 12 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
hence  (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da being Int-Location, f being FinSeq-Location  such that
A83: i = f :=<0,...,0> da by A82, SCMFSA_2:41;
A84: IncAddr (i,n) = i by A83, COMPOS_0:4;
A85: now__::_thesis:_for_g_being_FinSeq-Location_holds_(Exec_(i,s1))_._g_=_(Exec_((IncAddr_(i,n)),s2))_._g
let g be FinSeq-Location ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
percases ( g = f or g <> f ) ;
supposeA86: g = f ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
 ( ex m1 being Element of NAT st
( m1 = abs (s1 . da) & (Exec ((f :=<0,...,0> da),s1)) . f = m1 |-> 0 ) & ex m2 being Element of NAT st
( m2 = abs (s2 . da) & (Exec ((f :=<0,...,0> da),s2)) . f = m2 |-> 0 ) ) by SCMFSA_2:75;
hence  (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g by A2, A83, A84, A86, SCMFSA_M:2; ::_thesis: verum
end;
supposeA87: g <> f ; ::_thesis: (Exec (i,s1)) . b1 = (Exec ((IncAddr (i,n)),s2)) . b1
hence (Exec (i,s1)) . g = s1 . g by A83, SCMFSA_2:75
.= s2 . g by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . g by A83, A84, A87, SCMFSA_2:75 ;
::_thesis: verum
end;
end;
end;
now__::_thesis:_for_c_being_Int-Location_holds_(Exec_(i,s1))_._c_=_(Exec_((IncAddr_(i,n)),s2))_._c
let c be Int-Location; ::_thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A83, SCMFSA_2:75
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A83, A84, SCMFSA_2:75 ; ::_thesis: verum
end;
hence  DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A85, SCMFSA_M:2; ::_thesis: verum
end;
end;
end;

theorem :: SCMFSA6A:9
canceled;

theorem :: SCMFSA6A:10
canceled;

theorem :: SCMFSA6A:11
canceled;

theorem :: SCMFSA6A:12
canceled;

theorem :: SCMFSA6A:13
canceled;

theorem :: SCMFSA6A:14
canceled;

begin

definition
canceled;
let I, J be Program of ;
funcI ";" J ->  Program of  equals :: SCMFSA6A:def 4
(Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I)));
coherence
 (Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I))) is Program of
proof
set P = (Directed I) +* (Reloc (J,(card I)));
 (Directed I) +* (Reloc (J,(card I))) is initial
proof
set D =  {  (l + (card I)) where l is Element of NAT : l in dom J  }  ;
let m, n be Nat; :: according to AFINSQ_1:def_12 ::_thesis: ( not n in dom ((Directed I) +* (Reloc (J,(card I)))) or n <= m or m in dom ((Directed I) +* (Reloc (J,(card I)))) )
assume that
A1: n in dom ((Directed I) +* (Reloc (J,(card I)))) and
A2: m < n ; ::_thesis: m in dom ((Directed I) +* (Reloc (J,(card I))))
 ( dom (Directed I) = dom I & dom (Reloc (J,(card I))) =  {  (l + (card I)) where l is Element of NAT : l in dom J  }  ) by COMPOS_1:33, FUNCT_4:99;
then A3: dom ((Directed I) +* (Reloc (J,(card I)))) = (dom I) \/  {  (l + (card I)) where l is Element of NAT : l in dom J  }  by FUNCT_4:def_1;
percases ( n in dom I or n in  {  (l + (card I)) where l is Element of NAT : l in dom J  }  ) by A1, A3, XBOOLE_0:def_3;
suppose n in dom I ; ::_thesis: m in dom ((Directed I) +* (Reloc (J,(card I))))
then  m in dom I by A2, AFINSQ_1:def_12;
hence  m in dom ((Directed I) +* (Reloc (J,(card I)))) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose n in  {  (l + (card I)) where l is Element of NAT : l in dom J  }  ; ::_thesis: m in dom ((Directed I) +* (Reloc (J,(card I))))
then consider l being Element of NAT  such that
A4: n = l + (card I) and
A5: l in dom J ;
now__::_thesis:_(_(_m_<_card_I_&_m_in_dom_((Directed_I)_+*_(Reloc_(J,(card_I))))_)_or_(_m_>=_card_I_&_m_in__{__(l_+_(card_I))_where_l_is_Element_of_NAT_:_l_in_dom_J__}__)_)
percases ( m < card I or m >= card I ) ;
case m < card I ; ::_thesis: m in dom ((Directed I) +* (Reloc (J,(card I))))
then  m in dom I by AFINSQ_1:66;
hence  m in dom ((Directed I) +* (Reloc (J,(card I)))) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
case m >= card I ; ::_thesis: m in  {  (l + (card I)) where l is Element of NAT : l in dom J  }
then consider l1 being Nat such that
A6: m = (card I) + l1 by NAT_1:10;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def_12;
 l1 < l by A2, A4, A6, XREAL_1:6;
then  l1 in dom J by A5, AFINSQ_1:def_12;
hence  m in  {  (l + (card I)) where l is Element of NAT : l in dom J  }  by A6; ::_thesis: verum
end;
end;
end;
hence  m in dom ((Directed I) +* (Reloc (J,(card I)))) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  (Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I))) is Program of ; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  SCMFSA6A:def_3_:_
canceled;

:: deftheorem  defines ";" SCMFSA6A:def_4_:_
 for I, J being Program of holds I ";" J = (Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I)));

registration
let I be Program of ;
let J be non halt-free Program of ;
clusterI ";" J ->  non halt-free ;
coherence
 not I ";" J is halt-free ;
end;

theorem :: SCMFSA6A:15
for I, J being Program of
for l being Element of NAT st l in dom I & I . l <> halt SCM+FSA holds
(I ";" J) . l = I . l
proof
let I, J be Program of ; ::_thesis: for l being Element of NAT st l in dom I & I . l <> halt SCM+FSA holds
(I ";" J) . l = I . l
let l be Element of NAT ; ::_thesis: ( l in dom I & I . l <> halt SCM+FSA implies (I ";" J) . l = I . l )
assume that
A1: l in dom I and
A2: I . l <> halt SCM+FSA ; ::_thesis: (I ";" J) . l = I . l
 Reloc (J,(card I)) = IncAddr ((Shift (J,(card I))),(card I)) by COMPOS_1:34;
then A3: dom (Reloc (J,(card I))) = dom (Shift (J,(card I))) by COMPOS_1:def_21;
now__::_thesis:_not_l_in_dom_(Reloc_(J,(card_I)))
assume  l in dom (Reloc (J,(card I))) ; ::_thesis: contradiction
then  l in  {  (m + (card I)) where m is Element of NAT : m in dom J  }  by A3, VALUED_1:def_12;
then consider m being Element of NAT  such that
A4: l = m + (card I) and
 m in dom J ;
 m + (card I) < card I by A1, A4, AFINSQ_1:66;
hence  contradiction by NAT_1:11; ::_thesis: verum
end;
hence (I ";" J) . l = (Directed I) . l by FUNCT_4:11
.= I . l by A2, FUNCT_4:105 ;
::_thesis: verum
end;

theorem :: SCMFSA6A:16
for I, J being Program of holds Directed I c= I ";" J
proof
let I, J be Program of ; ::_thesis: Directed I c= I ";" J
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(Directed_I)_holds_
(Directed_I)_._x_=_(I_";"_J)_._x
let x be set ; ::_thesis: ( x in dom (Directed I) implies (Directed I) . x = (I ";" J) . x )
assume  x in dom (Directed I) ; ::_thesis: (Directed I) . x = (I ";" J) . x
then A2: x in dom I by FUNCT_4:99;
 dom I misses dom (Reloc (J,(card I))) by COMPOS_1:48;
then  not x in dom (Reloc (J,(card I))) by A2, XBOOLE_0:3;
hence  (Directed I) . x = (I ";" J) . x by FUNCT_4:11; ::_thesis: verum
end;
 dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def_1;
then  dom (Directed I) c= dom (I ";" J) by XBOOLE_1:7;
hence  Directed I c= I ";" J by A1, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th56: :: SCMFSA6A:17
for I, J being Program of holds dom I c= dom (I ";" J)
proof
let I, J be Program of ; ::_thesis: dom I c= dom (I ";" J)
dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def_1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
hence  dom I c= dom (I ";" J) by XBOOLE_1:7; ::_thesis: verum
end;

theorem :: SCMFSA6A:18
for I, J being Program of holds I +* (I ";" J) = I ";" J
proof
let I, J be Program of ; ::_thesis: I +* (I ";" J) = I ";" J
A1: for x being set st x in dom (I ";" J) holds
(I +* (I ";" J)) . x = (I ";" J) . x by FUNCT_4:13;
dom (I +* (I ";" J)) = (dom I) \/ (dom (I ";" J)) by FUNCT_4:def_1
.= dom (I ";" J) by Th56, XBOOLE_1:12 ;
hence  I +* (I ";" J) = I ";" J by A1, FUNCT_1:2; ::_thesis: verum
end;

begin

definition
let i be Instruction of SCM+FSA;
let J be Program of ;
funci ";" J ->  Program of  equals :: SCMFSA6A:def 5
(Macro i) ";" J;
correctness
coherence
(Macro i) ";" J is Program of ;
;
end;

:: deftheorem  defines ";" SCMFSA6A:def_5_:_
 for i being Instruction of SCM+FSA
for J being Program of holds i ";" J = (Macro i) ";" J;

definition
let I be Program of ;
let j be Instruction of SCM+FSA;
funcI ";" j ->  Program of  equals :: SCMFSA6A:def 6
I ";" (Macro j);
correctness
coherence
I ";" (Macro j) is Program of ;
;
end;

:: deftheorem  defines ";" SCMFSA6A:def_6_:_
 for I being Program of
for j being Instruction of SCM+FSA holds I ";" j = I ";" (Macro j);

definition
let i, j be Instruction of SCM+FSA;
funci ";" j ->  Program of  equals :: SCMFSA6A:def 7
(Macro i) ";" (Macro j);
correctness
coherence
(Macro i) ";" (Macro j) is Program of ;
;
end;

:: deftheorem  defines ";" SCMFSA6A:def_7_:_
 for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" (Macro j);

theorem :: SCMFSA6A:19
for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" j ;

theorem :: SCMFSA6A:20
for i, j being Instruction of SCM+FSA holds i ";" j = i ";" (Macro j) ;

theorem Th61: :: SCMFSA6A:21
for I, J being Program of holds card (I ";" J) = (card I) + (card J)
proof
let I, J be Program of ; ::_thesis: card (I ";" J) = (card I) + (card J)
A1: ( card (dom (I ";" J)) = card (I ";" J) & card (dom I) = card I ) by CARD_1:62;
A2: card (dom J) = card J by CARD_1:62;
A3: dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def_1
.= (dom I) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:99 ;
card (dom (Reloc (J,(card I)))) = card (Reloc (J,(card I))) by CARD_1:62
.= card J by COMPOS_1:49
.= card (dom J) by CARD_1:62 ;
hence  card (I ";" J) = (card I) + (card J) by A1, A2, A3, CARD_2:40, COMPOS_1:48; ::_thesis: verum
end;

registration
let P be preProgram of SCM+FSA;
let l be Element of NAT ;
cluster Directed (P,l) ->  halt-free ;
correctness
coherence
Directed (P,l) is halt-free ;
proof
 not halt SCM+FSA in rng (Directed (P,l)) by FUNCT_4:100;
hence  Directed (P,l) is halt-free by COMPOS_1:def_11; ::_thesis: verum
end;
end;

registration
let P be preProgram of SCM+FSA;
cluster Directed P ->  halt-free ;
correctness
coherence
Directed P is halt-free ;
;
end;

theorem Th63: :: SCMFSA6A:22
for I being preProgram of SCM+FSA
for l being Element of NAT st I is halt-free holds
Directed (I,l) = I
proof
let I be preProgram of SCM+FSA; ::_thesis: for l being Element of NAT st I is halt-free holds
Directed (I,l) = I
let l be Element of NAT ; ::_thesis: ( I is halt-free implies Directed (I,l) = I )
assume  I is halt-free ; ::_thesis: Directed (I,l) = I
then  not halt SCM+FSA in rng I by COMPOS_1:def_11;
hence  Directed (I,l) = I by FUNCT_4:103; ::_thesis: verum
end;

theorem Th65: :: SCMFSA6A:23
for I being preProgram of SCM+FSA
for k being Element of NAT holds Reloc ((Directed I),k) = Directed ((Reloc (I,k)),((card I) + k))
proof
let I be preProgram of SCM+FSA; ::_thesis: for k being Element of NAT holds Reloc ((Directed I),k) = Directed ((Reloc (I,k)),((card I) + k))
let k be Element of NAT ; ::_thesis: Reloc ((Directed I),k) = Directed ((Reloc (I,k)),((card I) + k))
A1: dom (Reloc (I,k)) =  {  (m + k) where m is Element of NAT : m in dom I  }  by COMPOS_1:33;
A2: dom (Directed I) = dom I by FUNCT_4:99;
A3: dom (Reloc ((Directed I),k)) =  {  (m + k) where m is Element of NAT : m in dom I  }  by A2, COMPOS_1:33;
A4: now__::_thesis:_for_x_being_set_st_x_in__{__(m_+_k)_where_m_is_Element_of_NAT_:_m_in_dom_I__}__holds_
(Reloc_((Directed_I),k))_._x_=_(Directed_((Reloc_(I,k)),((card_I)_+_k)))_._x
let x be set ; ::_thesis: ( x in  {  (m + k) where m is Element of NAT : m in dom I  }  implies (Reloc ((Directed I),k)) . x = (Directed ((Reloc (I,k)),((card I) + k))) . x )
assume A5: x in  {  (m + k) where m is Element of NAT : m in dom I  }  ; ::_thesis: (Reloc ((Directed I),k)) . x = (Directed ((Reloc (I,k)),((card I) + k))) . x
then consider n being Element of NAT  such that
A6: x = n + k and
A7: n in dom I ;
 dom (Directed I) = dom I by FUNCT_4:99;
then reconsider i = (Directed I) . n as Instruction of SCM+FSA by A7, FUNCT_1:106;
reconsider i0 = I . n as Instruction of SCM+FSA by A7, FUNCT_1:106;
A8: now__::_thesis:_(Directed_((Reloc_(I,k)),((card_I)_+_k)))_._x_=_IncAddr_(i,k)
percases ( i0 = halt SCM+FSA or i0 <> halt SCM+FSA ) ;
supposeA9: i0 = halt SCM+FSA ; ::_thesis: (Directed ((Reloc (I,k)),((card I) + k))) . x = IncAddr (i,k)
then A10: i = goto (card I) by A7, FUNCT_4:106;
A11: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:35
.= halt SCM+FSA by A9, COMPOS_0:4 ;
then  (Reloc (I,k)) . x in {(halt SCM+FSA)} by TARSKI:def_1;
then  (Reloc (I,k)) . x in dom ((halt SCM+FSA) .--> (goto ((card I) + k))) by FUNCOP_1:13;
then  x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by A1, A5, FUNCT_1:11;
hence (Directed ((Reloc (I,k)),((card I) + k))) . x = (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) . x by FUNCT_4:13
.= ((halt SCM+FSA) .--> (goto ((card I) + k))) . ((Reloc (I,k)) . x) by A1, A5, FUNCT_1:13
.= goto ((card I) + k) by A11, FUNCOP_1:72
.= IncAddr (i,k) by A10, SCMFSA_4:1 ;
::_thesis: verum
end;
supposeA12: i0 <> halt SCM+FSA ; ::_thesis: (Directed ((Reloc (I,k)),((card I) + k))) . x = IncAddr (i,k)
A13: (Reloc (I,k)) . x = IncAddr (i0,k) by A6, A7, COMPOS_1:35;
X: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
 InsCode i0 <> 0 by A12, SCMFSA_2:95;
then  IncAddr (i0,k) <> halt SCM+FSA by COMPOS_0:def_9, X;
then  not (Reloc (I,k)) . x in {(halt SCM+FSA)} by A13, TARSKI:def_1;
then  not (Reloc (I,k)) . x in dom ((halt SCM+FSA) .--> (goto ((card I) + k))) by FUNCOP_1:13;
then  not x in dom (((halt SCM+FSA) .--> (goto ((card I) + k))) * (Reloc (I,k))) by FUNCT_1:11;
hence (Directed ((Reloc (I,k)),((card I) + k))) . x = (Reloc (I,k)) . x by FUNCT_4:11
.= IncAddr (i,k) by A12, A13, FUNCT_4:105 ;
::_thesis: verum
end;
end;
end;
thus  (Reloc ((Directed I),k)) . x = (Directed ((Reloc (I,k)),((card I) + k))) . x by A8, A2, A6, A7, COMPOS_1:35; ::_thesis: verum
end;
 dom (Directed ((Reloc (I,k)),((card I) + k))) =  {  (m + k) where m is Element of NAT : m in dom I  }  by A1, FUNCT_4:99;
hence  Reloc ((Directed I),k) = Directed ((Reloc (I,k)),((card I) + k)) by A3, A4, FUNCT_1:2; ::_thesis: verum
end;

theorem Th66: :: SCMFSA6A:24
for I, J being Program of holds Directed (I ";" J) = I ";" (Directed J)
proof
let I, J be Program of ; ::_thesis: Directed (I ";" J) = I ";" (Directed J)
thus I ";" (Directed J) = (Directed I) +* (Directed ((Reloc (J,(card I))),((card I) + (card J)))) by Th65
.= (Directed I) +* (Directed ((Reloc (J,(card I))),(card (I ";" J)))) by Th61
.= (Directed ((Directed I),(card (I ";" J)))) +* (Directed ((Reloc (J,(card I))),(card (I ";" J)))) by Th63
.= Directed (I ";" J) by FUNCT_7:117 ; ::_thesis: verum
end;

theorem Th67: :: SCMFSA6A:25
for I, J, K being Program of holds (I ";" J) ";" K = I ";" (J ";" K)
proof
let I, J, K be Program of ; ::_thesis: (I ";" J) ";" K = I ";" (J ";" K)
A1: Reloc ((J ";" K),(card I)) = (Reloc ((Directed J),(card I))) +* (Reloc ((Reloc (K,(card J))),(card I))) by COMPOS_1:42
.= (Reloc ((Directed J),(card I))) +* (Reloc (K,((card J) + (card I)))) by COMPOS_1:43 ;
thus (I ";" J) ";" K = (I ";" (Directed J)) +* (Reloc (K,(card (I ";" J)))) by Th66
.= (Directed I) +* ((Reloc ((Directed J),(card I))) +* (Reloc (K,(card (I ";" J))))) by FUNCT_4:14
.= I ";" (J ";" K) by A1, Th61 ; ::_thesis: verum
end;

theorem :: SCMFSA6A:26
for k being Instruction of SCM+FSA
for I, J being Program of holds (I ";" J) ";" k = I ";" (J ";" k) by Th67;

theorem :: SCMFSA6A:27
for j being Instruction of SCM+FSA
for I, K being Program of holds (I ";" j) ";" K = I ";" (j ";" K) by Th67;

theorem :: SCMFSA6A:28
for j, k being Instruction of SCM+FSA
for I being Program of holds (I ";" j) ";" k = I ";" (j ";" k) by Th67;

theorem :: SCMFSA6A:29
for i being Instruction of SCM+FSA
for J, K being Program of holds (i ";" J) ";" K = i ";" (J ";" K) by Th67;

theorem :: SCMFSA6A:30
for i, k being Instruction of SCM+FSA
for J being Program of holds (i ";" J) ";" k = i ";" (J ";" k) by Th67;

theorem :: SCMFSA6A:31
for i, j being Instruction of SCM+FSA
for K being Program of holds (i ";" j) ";" K = i ";" (j ";" K) by Th67;

theorem :: SCMFSA6A:32
for i, j, k being Instruction of SCM+FSA holds (i ";" j) ";" k = i ";" (j ";" k) by Th67;

theorem :: SCMFSA6A:33
for i being Instruction of SCM+FSA
for J being Program of holds card (i ";" J) = (card J) + 2
proof
let i be Instruction of SCM+FSA; ::_thesis: for J being Program of holds card (i ";" J) = (card J) + 2
let J be Program of ; ::_thesis: card (i ";" J) = (card J) + 2
thus  card (i ";" J) = (card (Macro i)) + (card J) by Th61
.= (card J) + 2 by COMPOS_1:56 ; ::_thesis: verum
end;

theorem :: SCMFSA6A:34
for j being Instruction of SCM+FSA
for I being Program of holds card (I ";" j) = (card I) + 2
proof
let j be Instruction of SCM+FSA; ::_thesis: for I being Program of holds card (I ";" j) = (card I) + 2
let I be Program of ; ::_thesis: card (I ";" j) = (card I) + 2
thus  card (I ";" j) = (card (Macro j)) + (card I) by Th61
.= (card I) + 2 by COMPOS_1:56 ; ::_thesis: verum
end;

theorem :: SCMFSA6A:35
for i, j being Instruction of SCM+FSA holds card (i ";" j) = 4
proof
let i, j be Instruction of SCM+FSA; ::_thesis: card (i ";" j) = 4
thus  card (i ";" j) = (card (Macro i)) + (card (Macro j)) by Th61
.= (card (Macro i)) + 2 by COMPOS_1:56
.= 2 + 2 by COMPOS_1:56
.= 4 ; ::_thesis: verum
end;