:: SCMFSA_4 semantic presentation

registration

let N be set ;
let S be AMI-Struct of N;
cluster -> finite FinPartState of S;
coherence by AMI_1:def 24;

end;

registration

let N be set ;
let S be AMI-Struct of N;
cluster finite programmed FinPartState of S;
existence

proof end;

end;

theorem Th1: :: SCMFSA_4:1

for N being with_non-empty_elements set
for S being non empty non void definite AMI-Struct of N
for p being programmed FinPartState of S holds rng p c= the Instructions of S

proof end;

definition

let N be set ;
let S be AMI-Struct of N;
let I, J be programmed FinPartState of S;
:: original: +*
redefine func I +* J -> programmed FinPartState of S;
coherence by AMI_3:35;

end;

theorem Th2: :: SCMFSA_4:2

for N being with_non-empty_elements set
for S being non empty non void definite AMI-Struct of N
for f being Function of the Instructions of S,the Instructions of S
for s being programmed FinPartState of S holds dom (f * s) = dom s

proof end;

definition

let loc be Instruction-Location of SCM+FSA ;
let k be Nat;
func loc + k -> Instruction-Location of SCM+FSA means :Def1: :: SCMFSA_4:def 1
ex m being Nat st
( loc = insloc m & it = insloc (m + k) );
existence

proof end;

uniqueness by SCMFSA_2:18;
func loc -' k -> Instruction-Location of SCM+FSA means :Def2: :: SCMFSA_4:def 2
ex m being Nat st
( loc = insloc m & it = insloc (m -' k) );
existence

proof end;

uniqueness by SCMFSA_2:18;

end;

:: deftheorem Def1 defines + SCMFSA_4:def 1 :

:: deftheorem Def2 defines -' SCMFSA_4:def 2 :

theorem Th3: :: SCMFSA_4:3

for l being Instruction-Location of SCM+FSA
for m, n being Nat holds (l + m) + n = l + (m + n)

proof end;

theorem Th4: :: SCMFSA_4:4

for loc being Instruction-Location of SCM+FSA
for k being Nat holds (loc + k) -' k = loc

proof end;

theorem Th5: :: SCMFSA_4:5

for k being Nat
for l being Instruction-Location of SCM+FSA
for L being Instruction-Location of SCM st L = l holds
l + k = L + k

proof end;

theorem :: SCMFSA_4:6

for l1, l2 being Instruction-Location of SCM+FSA
for k being Nat holds
( Start-At (l1 + k) = Start-At (l2 + k) iff Start-At l1 = Start-At l2 )

proof end;

theorem :: SCMFSA_4:7

for l1, l2 being Instruction-Location of SCM+FSA
for k being Nat st Start-At l1 = Start-At l2 holds
Start-At (l1 -' k) = Start-At (l2 -' k)

proof end;

definition

let i be Instruction of SCM+FSA ;
let k be Nat;
func IncAddr i,k -> Instruction of SCM+FSA means :Def3: :: SCMFSA_4:def 3
ex I being Instruction of SCM st
( I = i & it = IncAddr I,k ) if InsCode i in {6,7,8}
otherwise it = i;
existence

proof end;

correctness ;

end;

:: deftheorem Def3 defines IncAddr SCMFSA_4:def 3 :

theorem Th8: :: SCMFSA_4:8

for k being Nat holds IncAddr (halt SCM+FSA ),k = halt SCM+FSA

proof end;

theorem Th9: :: SCMFSA_4:9

for k being Nat
for a, b being Int-Location holds IncAddr (a := b),k = a := b

proof end;

theorem Th10: :: SCMFSA_4:10

for k being Nat
for a, b being Int-Location holds IncAddr (AddTo a,b),k = AddTo a,b

proof end;

theorem Th11: :: SCMFSA_4:11

for k being Nat
for a, b being Int-Location holds IncAddr (SubFrom a,b),k = SubFrom a,b

proof end;

theorem Th12: :: SCMFSA_4:12

for k being Nat
for a, b being Int-Location holds IncAddr (MultBy a,b),k = MultBy a,b

proof end;

theorem Th13: :: SCMFSA_4:13

for k being Nat
for a, b being Int-Location holds IncAddr (Divide a,b),k = Divide a,b

proof end;

theorem Th14: :: SCMFSA_4:14

for k being Nat
for loc being Instruction-Location of SCM+FSA holds IncAddr (goto loc),k = goto (loc + k)

proof end;

theorem Th15: :: SCMFSA_4:15

for k being Nat
for loc being Instruction-Location of SCM+FSA
for a being Int-Location holds IncAddr (a =0_goto loc),k = a =0_goto (loc + k)

proof end;

theorem Th16: :: SCMFSA_4:16

for k being Nat
for loc being Instruction-Location of SCM+FSA
for a being Int-Location holds IncAddr (a >0_goto loc),k = a >0_goto (loc + k)

proof end;

theorem Th17: :: SCMFSA_4:17

for k being Nat
for a, b being Int-Location
for f being FinSeq-Location holds IncAddr (b := f,a),k = b := f,a

proof end;

theorem Th18: :: SCMFSA_4:18

for k being Nat
for a, b being Int-Location
for f being FinSeq-Location holds IncAddr (f,a := b),k = f,a := b

proof end;

theorem Th19: :: SCMFSA_4:19

for k being Nat
for a being Int-Location
for f being FinSeq-Location holds IncAddr (a :=len f),k = a :=len f

proof end;

theorem Th20: :: SCMFSA_4:20

for k being Nat
for a being Int-Location
for f being FinSeq-Location holds IncAddr (f :=<0,...,0> a),k = f :=<0,...,0> a

proof end;

theorem Th21: :: SCMFSA_4:21

for k being Nat
for i being Instruction of SCM+FSA
for I being Instruction of SCM st i = I holds
IncAddr i,k = IncAddr I,k

proof end;

theorem Th22: :: SCMFSA_4:22

for I being Instruction of SCM+FSA
for k being Nat holds InsCode (IncAddr I,k) = InsCode I

proof end;

definition

let IT be FinPartState of SCM+FSA ;
attr IT is initial means :: SCMFSA_4:def 4
for m, n being Nat st insloc n in dom IT & m < n holds
insloc m in dom IT;

end;

:: deftheorem defines initial SCMFSA_4:def 4 :

definition

func SCM+FSA-Stop -> FinPartState of SCM+FSA equals :: SCMFSA_4:def 5
(insloc 0) .--> (halt SCM+FSA );
correctness ;

end;

:: deftheorem defines SCM+FSA-Stop SCMFSA_4:def 5 :

registration

cluster SCM+FSA-Stop -> non empty finite programmed initial ;
coherence

proof end;

end;

registration

cluster non empty finite programmed initial FinPartState of SCM+FSA ;
existence

proof end;

end;

registration

let f be Function;
let g be finite Function;
cluster g * f -> finite ;
coherence

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty non void definite AMI-Struct of N;
let s be programmed FinPartState of S;
let f be Function of the Instructions of S,the Instructions of S;
:: original: *
redefine func f * s -> programmed FinPartState of S;
coherence

proof end;

end;

theorem Th23: :: SCMFSA_4:23

for m, n being Nat
for i being Instruction of SCM+FSA holds IncAddr (IncAddr i,m),n = IncAddr i,(m + n)

proof end;

definition

let p be programmed FinPartState of SCM+FSA ;
let k be Nat;
func IncAddr p,k -> programmed FinPartState of SCM+FSA means :Def6: :: SCMFSA_4:def 6
( dom it = dom p & ( for m being Nat st insloc m in dom p holds
it . (insloc m) = IncAddr (pi p,(insloc m)),k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines IncAddr SCMFSA_4:def 6 :

theorem Th24: :: SCMFSA_4:24

for p being programmed FinPartState of SCM+FSA
for k being Nat
for l being Instruction-Location of SCM+FSA st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k

proof end;

theorem :: SCMFSA_4:25

for n being Nat
for I, J being programmed FinPartState of SCM+FSA holds IncAddr (I +* J),n = (IncAddr I,n) +* (IncAddr J,n)

proof end;

theorem :: SCMFSA_4:26

for n being Nat
for i being Instruction of SCM+FSA
for f being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA st f = (id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> i) holds
for s being programmed FinPartState of SCM+FSA holds IncAddr (f * s),n = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (IncAddr i,n))) * (IncAddr s,n)

proof end;

theorem :: SCMFSA_4:27

for m, n being Nat
for I being programmed FinPartState of SCM+FSA holds IncAddr (IncAddr I,m),n = IncAddr I,(m + n)

proof end;

theorem :: SCMFSA_4:28

for k being Nat
for s being State of SCM+FSA holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

proof end;

theorem :: SCMFSA_4:29

for INS being Instruction of SCM+FSA
for s being State of SCM+FSA
for p being FinPartState of SCM+FSA
for i, j, k being Nat st IC s = insloc (j + k) holds
Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))

proof end;

definition

let p be FinPartState of SCM+FSA ;
let k be Nat;
func Shift p,k -> programmed FinPartState of SCM+FSA means :Def7: :: SCMFSA_4:def 7
( dom it = { (insloc (m + k)) where m is Nat : insloc m in dom p } & ( for m being Nat st insloc m in dom p holds
it . (insloc (m + k)) = p . (insloc m) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Shift SCMFSA_4:def 7 :

theorem Th30: :: SCMFSA_4:30

for l being Instruction-Location of SCM+FSA
for k being Nat
for p being FinPartState of SCM+FSA st l in dom p holds
(Shift p,k) . (l + k) = p . l

proof end;

theorem :: SCMFSA_4:31

for p being FinPartState of SCM+FSA
for k being Nat holds dom (Shift p,k) = { (il + k) where il is Instruction-Location of SCM+FSA : il in dom p }

proof end;

theorem :: SCMFSA_4:32

for m, n being Nat
for I being FinPartState of SCM+FSA holds Shift (Shift I,m),n = Shift I,(m + n)

proof end;

theorem :: SCMFSA_4:33

for s being programmed FinPartState of SCM+FSA
for f being Function of the Instructions of SCM+FSA ,the Instructions of SCM+FSA
for n being Nat holds Shift (f * s),n = f * (Shift s,n)

proof end;

theorem :: SCMFSA_4:34

for n being Nat
for I, J being FinPartState of SCM+FSA holds Shift (I +* J),n = (Shift I,n) +* (Shift J,n)

proof end;

theorem :: SCMFSA_4:35

for i, j being Nat
for p being programmed FinPartState of SCM+FSA holds Shift (IncAddr p,i),j = IncAddr (Shift p,j),i

proof end;