:: On the Instructions of { \bf SCM+FSA }
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001-2011 Association of Mizar Users

begin

definition

let la, lb be Int-Location ;
let a, b be Integer;
:: original: -->
redefine func (la,lb) --> (a,b) -> FinPartState of SCM+FSA;
coherence
(la,lb) --> (a,b) is FinPartState of SCM+FSA

proof end;

end;

theorem :: SCMFSA10:1

canceled;

theorem :: SCMFSA10:2

canceled;

theorem Th3: :: SCMFSA10:3

for a being Int-Location holds not a in NAT

proof end;

theorem Th4: :: SCMFSA10:4

for f being FinSeq-Location holds not f in NAT

proof end;

theorem :: SCMFSA10:5

SCM+FSA-Data-Loc <> NAT

proof end;

theorem :: SCMFSA10:6

SCM+FSA-Data*-Loc <> NAT

proof end;

theorem Th7: :: SCMFSA10:7

for o being Object of SCM+FSA holds
( not o in Data-Locations SCM+FSA or o is Int-Location or o is FinSeq-Location )

proof end;

theorem :: SCMFSA10:8

canceled;

theorem Th9: :: SCMFSA10:9

for a, b being Int-Location holds a := b = [1,{},<*a,b*>]

proof end;

theorem Th10: :: SCMFSA10:10

for a, b being Int-Location holds AddTo (a,b) = [2,{},<*a,b*>]

proof end;

theorem Th11: :: SCMFSA10:11

for a, b being Int-Location holds SubFrom (a,b) = [3,{},<*a,b*>]

proof end;

theorem Th12: :: SCMFSA10:12

for a, b being Int-Location holds MultBy (a,b) = [4,{},<*a,b*>]

proof end;

theorem Th13: :: SCMFSA10:13

for a, b being Int-Location holds Divide (a,b) = [5,{},<*a,b*>]

proof end;

theorem :: SCMFSA10:14

canceled;

theorem Th15: :: SCMFSA10:15

for a being Int-Location
for il being Element of NAT holds a =0_goto il = [7,<*il*>,<*a*>]

proof end;

theorem Th16: :: SCMFSA10:16

for a being Int-Location
for il being Element of NAT holds a >0_goto il = [8,<*il*>,<*a*>]

proof end;

Lm1: for T being InsType of SCM+FSA holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 or T = 13 )

proof end;

theorem Th17: :: SCMFSA10:17

JumpPart (halt SCM+FSA) = {} ;

theorem Th18: :: SCMFSA10:18

for a, b being Int-Location holds JumpPart (a := b) = {}

proof end;

theorem Th19: :: SCMFSA10:19

for a, b being Int-Location holds JumpPart (AddTo (a,b)) = {}

proof end;

theorem Th20: :: SCMFSA10:20

for a, b being Int-Location holds JumpPart (SubFrom (a,b)) = {}

proof end;

theorem Th21: :: SCMFSA10:21

for a, b being Int-Location holds JumpPart (MultBy (a,b)) = {}

proof end;

theorem Th22: :: SCMFSA10:22

for a, b being Int-Location holds JumpPart (Divide (a,b)) = {}

proof end;

theorem :: SCMFSA10:23

canceled;

theorem Th24: :: SCMFSA10:24

for i1 being Element of NAT
for a being Int-Location holds JumpPart (a =0_goto i1) = <*i1*>

proof end;

theorem Th25: :: SCMFSA10:25

for i1 being Element of NAT
for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>

proof end;

theorem :: SCMFSA10:26

canceled;

theorem :: SCMFSA10:27

canceled;

theorem :: SCMFSA10:28

canceled;

theorem :: SCMFSA10:29

canceled;

theorem Th30: :: SCMFSA10:30

for T being InsType of SCM+FSA st T = 0 holds
JumpParts T = {0}

proof end;

theorem Th31: :: SCMFSA10:31

for T being InsType of SCM+FSA st T = 1 holds
JumpParts T = {{}}

proof end;

theorem Th32: :: SCMFSA10:32

for T being InsType of SCM+FSA st T = 2 holds
JumpParts T = {{}}

proof end;

theorem Th33: :: SCMFSA10:33

for T being InsType of SCM+FSA st T = 3 holds
JumpParts T = {{}}

proof end;

theorem Th34: :: SCMFSA10:34

for T being InsType of SCM+FSA st T = 4 holds
JumpParts T = {{}}

proof end;

theorem Th35: :: SCMFSA10:35

for T being InsType of SCM+FSA st T = 5 holds
JumpParts T = {{}}

proof end;

theorem Th36: :: SCMFSA10:36

for T being InsType of SCM+FSA st T = 6 holds
dom (product" (JumpParts T)) = {1}

proof end;

theorem Th37: :: SCMFSA10:37

for T being InsType of SCM+FSA st T = 7 holds
dom (product" (JumpParts T)) = {1}

proof end;

theorem Th38: :: SCMFSA10:38

for T being InsType of SCM+FSA st T = 8 holds
dom (product" (JumpParts T)) = {1}

proof end;

theorem Th39: :: SCMFSA10:39

for T being InsType of SCM+FSA st T = 9 holds
JumpParts T = {{}}

proof end;

theorem Th40: :: SCMFSA10:40

for T being InsType of SCM+FSA st T = 10 holds
JumpParts T = {{}}

proof end;

theorem Th41: :: SCMFSA10:41

for T being InsType of SCM+FSA st T = 11 holds
JumpParts T = {{}}

proof end;

theorem Th42: :: SCMFSA10:42

for T being InsType of SCM+FSA st T = 12 holds
JumpParts T = {{}}

proof end;

Lm42: for T being InsType of SCM+FSA st T = 13 holds
JumpParts T = {{}}

proof end;

theorem :: SCMFSA10:43

canceled;

theorem :: SCMFSA10:44

canceled;

theorem :: SCMFSA10:45

canceled;

theorem :: SCMFSA10:46

canceled;

theorem :: SCMFSA10:47

canceled;

theorem :: SCMFSA10:48

canceled;

theorem :: SCMFSA10:49

canceled;

theorem :: SCMFSA10:50

canceled;

theorem :: SCMFSA10:51

canceled;

theorem :: SCMFSA10:52

canceled;

theorem Th53: :: SCMFSA10:53

for i1 being Element of NAT holds (product" (JumpParts (InsCode (goto i1)))) . 1 = NAT

proof end;

theorem Th54: :: SCMFSA10:54

for i1 being Element of NAT
for a being Int-Location holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT

proof end;

theorem :: SCMFSA10:55

canceled;

theorem Th56: :: SCMFSA10:56

for i1 being Element of NAT
for a being Int-Location holds (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 = NAT

proof end;

Lm3: for i being Instruction of SCM+FSA st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty

proof end;

registration

cluster JUMP (halt SCM+FSA) -> empty ;
coherence
JUMP (halt SCM+FSA) is empty ;

end;

registration

let a, b be Int-Location ;
cluster a := b -> sequential ;
coherence
a := b is sequential

proof end;

cluster AddTo (a,b) -> sequential ;
coherence
AddTo (a,b) is sequential

proof end;

cluster SubFrom (a,b) -> sequential ;
coherence
SubFrom (a,b) is sequential

proof end;

cluster MultBy (a,b) -> sequential ;
coherence
MultBy (a,b) is sequential

proof end;

cluster Divide (a,b) -> sequential ;
coherence
Divide (a,b) is sequential

proof end;

end;

registration

let a be Int-Location ;
cluster a :==1 -> sequential ;
coherence
a :==1 is sequential

proof end;

end;

registration

let a be Int-Location ;
cluster JUMP (a :==1) -> empty ;
coherence
JUMP (a :==1) is empty

proof end;

end;

registration

let a, b be Int-Location ;
cluster JUMP (a := b) -> empty ;
coherence
JUMP (a := b) is empty

proof end;

cluster JUMP (AddTo (a,b)) -> empty ;
coherence
JUMP (AddTo (a,b)) is empty

proof end;

cluster JUMP (SubFrom (a,b)) -> empty ;
coherence
JUMP (SubFrom (a,b)) is empty

proof end;

cluster JUMP (MultBy (a,b)) -> empty ;
coherence
JUMP (MultBy (a,b)) is empty

proof end;

cluster JUMP (Divide (a,b)) -> empty ;
coherence
JUMP (Divide (a,b)) is empty

proof end;

end;

theorem :: SCMFSA10:57

canceled;

theorem :: SCMFSA10:58

canceled;

theorem :: SCMFSA10:59

canceled;

theorem :: SCMFSA10:60

canceled;

theorem :: SCMFSA10:61

canceled;

theorem :: SCMFSA10:62

canceled;

theorem :: SCMFSA10:63

canceled;

theorem :: SCMFSA10:64

canceled;

theorem :: SCMFSA10:65

canceled;

theorem :: SCMFSA10:66

canceled;

theorem :: SCMFSA10:67

canceled;

theorem :: SCMFSA10:68

canceled;

theorem :: SCMFSA10:69

canceled;

theorem :: SCMFSA10:70

canceled;

theorem :: SCMFSA10:71

canceled;

theorem :: SCMFSA10:72

canceled;

theorem :: SCMFSA10:73

canceled;

theorem Th74: :: SCMFSA10:74

for i1, il being Element of NAT holds NIC ((goto i1),il) = {i1}

proof end;

theorem Th75: :: SCMFSA10:75

for i1 being Element of NAT holds JUMP (goto i1) = {i1}

proof end;

registration

let i1 be Element of NAT ;
cluster JUMP (goto i1) -> non empty trivial ;
coherence
( not JUMP (goto i1) is empty & JUMP (goto i1) is trivial )

proof end;

end;

theorem Th76: :: SCMFSA10:76

for i1, il being Element of NAT
for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(succ il)}

proof end;

theorem Th77: :: SCMFSA10:77

for i1 being Element of NAT
for a being Int-Location holds JUMP (a =0_goto i1) = {i1}

proof end;

registration

let a be Int-Location ;
let i1 be Element of NAT ;
cluster JUMP (a =0_goto i1) -> non empty trivial ;
coherence
( not JUMP (a =0_goto i1) is empty & JUMP (a =0_goto i1) is trivial )

proof end;

end;

theorem Th78: :: SCMFSA10:78

for i1, il being Element of NAT
for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(succ il)}

proof end;

theorem Th79: :: SCMFSA10:79

for i1 being Element of NAT
for a being Int-Location holds JUMP (a >0_goto i1) = {i1}

proof end;

registration

let a be Int-Location ;
let i1 be Element of NAT ;
cluster JUMP (a >0_goto i1) -> non empty trivial ;
coherence
( not JUMP (a >0_goto i1) is empty & JUMP (a >0_goto i1) is trivial )

proof end;

end;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster a := (f,b) -> sequential ;
coherence
a := (f,b) is sequential

proof end;

end;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster JUMP (a := (f,b)) -> empty ;
coherence
JUMP (a := (f,b)) is empty

proof end;

end;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster (f,b) := a -> sequential ;
coherence
(f,b) := a is sequential

proof end;

end;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster JUMP ((f,b) := a) -> empty ;
coherence
JUMP ((f,b) := a) is empty

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster a :=len f -> sequential ;
coherence
a :=len f is sequential

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster JUMP (a :=len f) -> empty ;
coherence
JUMP (a :=len f) is empty

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster f :=<0,...,0> a -> sequential ;
coherence
f :=<0,...,0> a is sequential

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster JUMP (f :=<0,...,0> a) -> empty ;
coherence
JUMP (f :=<0,...,0> a) is empty

proof end;

end;

theorem :: SCMFSA10:80

canceled;

theorem :: SCMFSA10:81

canceled;

theorem :: SCMFSA10:82

canceled;

theorem :: SCMFSA10:83

canceled;

theorem Th84: :: SCMFSA10:84

for il being Element of NAT holds SUCC (il,SCM+FSA) = {il,(succ il)}

proof end;

theorem Th85: :: SCMFSA10:85

for k being Element of NAT holds
( k + 1 in SUCC (k,SCM+FSA) & ( for j being Element of NAT st j in SUCC (k,SCM+FSA) holds
k <= j ) )

proof end;

registration

cluster SCM+FSA -> standard ;
coherence
SCM+FSA is standard by Th85, AMISTD_1:19;

end;

registration

cluster (halt SCM+FSA) `1_3 -> jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (halt SCM+FSA) holds
b₁ is jump-only

proof end;

end;

registration

cluster halt SCM+FSA -> jump-only ;
coherence
halt SCM+FSA is jump-only

proof end;

end;

registration

let i1 be Element of NAT ;
cluster (goto i1) `1_3 -> jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (goto i1) holds
b₁ is jump-only

proof end;

end;

registration

let i1 be Element of NAT ;
cluster goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( goto i1 is jump-only & not goto i1 is sequential & not goto i1 is ins-loc-free )

proof end;

end;

registration

let a be Int-Location ;
let i1 be Element of NAT ;
cluster (a =0_goto i1) `1_3 -> jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (a =0_goto i1) holds
b₁ is jump-only

proof end;

cluster (a >0_goto i1) `1_3 -> jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (a >0_goto i1) holds
b₁ is jump-only

proof end;

end;

registration

let a be Int-Location ;
let i1 be Element of NAT ;
cluster a =0_goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( a =0_goto i1 is jump-only & not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )

proof end;

cluster a >0_goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( a >0_goto i1 is jump-only & not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )

proof end;

end;

Lm4: intloc 0 <> intloc 1
by AMI_3:52;

registration

let a, b be Int-Location ;
cluster (a := b) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (a := b) holds
not b₁ is jump-only

proof end;

cluster (AddTo (a,b)) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (AddTo (a,b)) holds
not b₁ is jump-only

proof end;

cluster (SubFrom (a,b)) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (SubFrom (a,b)) holds
not b₁ is jump-only

proof end;

cluster (MultBy (a,b)) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (MultBy (a,b)) holds
not b₁ is jump-only

proof end;

cluster (Divide (a,b)) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (Divide (a,b)) holds
not b₁ is jump-only

proof end;

end;

Lm5: fsloc 0 <> intloc 0
by SCMFSA_2:126;

Lm6: fsloc 0 <> intloc 1
by SCMFSA_2:126;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster (b := (f,a)) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (b := (f,a)) holds
not b₁ is jump-only

proof end;

cluster ((f,a) := b) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode ((f,a) := b) holds
not b₁ is jump-only

proof end;

end;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster b := (f,a) -> non jump-only ;
coherence
not b := (f,a) is jump-only

proof end;

cluster (f,a) := b -> non jump-only ;
coherence
not (f,a) := b is jump-only

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster (a :=len f) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (a :=len f) holds
not b₁ is jump-only

proof end;

cluster (f :=<0,...,0> a) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (f :=<0,...,0> a) holds
not b₁ is jump-only

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster a :=len f -> non jump-only ;
coherence
not a :=len f is jump-only

proof end;

cluster f :=<0,...,0> a -> non jump-only ;
coherence
not f :=<0,...,0> a is jump-only

proof end;

end;

registration

let a be Int-Location ;
cluster (a :==1) `1_3 -> non jump-only InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (a :==1) holds
not b₁ is jump-only

proof end;

end;

registration

let a be Int-Location ;
cluster a :==1 -> non jump-only ;
coherence
not a :==1 is jump-only

proof end;

end;

registration

cluster SCM+FSA -> homogeneous with_explicit_jumps ;
coherence
( SCM+FSA is homogeneous & SCM+FSA is with_explicit_jumps )

proof end;

end;

registration

cluster SCM+FSA -> regular J/A-independent ;
coherence
( SCM+FSA is regular & SCM+FSA is J/A-independent )

proof end;

end;

theorem :: SCMFSA10:86

canceled;

theorem :: SCMFSA10:87

canceled;

theorem Th88: :: SCMFSA10:88

for i1 being Element of NAT
for k being natural number holds IncAddr ((goto i1),k) = goto (i1 + k)

proof end;

theorem Th89: :: SCMFSA10:89

for i1 being Element of NAT
for k being natural number
for a being Int-Location holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)

proof end;

theorem Th90: :: SCMFSA10:90

for i1 being Element of NAT
for k being natural number
for a being Int-Location holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)

proof end;

registration

cluster SCM+FSA -> IC-relocable ;
coherence
SCM+FSA is IC-relocable

proof end;

end;

theorem Th91: :: SCMFSA10:91

for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
NPP s1 = NPP s2

proof end;

theorem Th92: :: SCMFSA10:92

for s1, s2 being State of SCM+FSA st NPP s1 = NPP s2 holds
for a being Int-Location holds s1 . a = s2 . a

proof end;

theorem Th93: :: SCMFSA10:93

for s1, s2 being State of SCM+FSA st NPP s1 = NPP s2 holds
for f being FinSeq-Location holds s1 . f = s2 . f

proof end;

registration

cluster SCM+FSA -> Exec-preserving ;
coherence
SCM+FSA is Exec-preserving

proof end;

end;

theorem :: SCMFSA10:94

for T being InsType of SCM+FSA st T = 13 holds
JumpParts T = {{}} by Lm42;