:: SCMFSA10 semantic presentation

theorem Th1: :: SCMFSA10:1

for f being Function
for a, A, b, B, c, C being set st a <> b & a <> c holds
(((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A

proof end;

theorem Th2: :: SCMFSA10:2

for a, b being set holds <*a*> +* 1,b = <*b*>

proof end;

definition

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

proof end;

end;

theorem Th3: :: SCMFSA10:3

for a being Int-Location holds not a in the Instruction-Locations of SCM+FSA

proof end;

theorem Th4: :: SCMFSA10:4

for f being FinSeq-Location holds not f in the Instruction-Locations of SCM+FSA

proof end;

theorem Th5: :: SCMFSA10:5

SCM+FSA-Data-Loc <> the Instruction-Locations of SCM+FSA

proof end;

theorem Th6: :: SCMFSA10:6

SCM+FSA-Data*-Loc <> the Instruction-Locations of SCM+FSA

proof end;

theorem Th7: :: SCMFSA10:7

for o being Object of SCM+FSA holds
( o = IC SCM+FSA or o in the Instruction-Locations of SCM+FSA or o is Int-Location or o is FinSeq-Location )

proof end;

theorem Th8: :: SCMFSA10:8

for i1, i2 being Instruction-Location of SCM+FSA st i1 <> i2 holds
Next i1 <> Next i2

proof end;

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 Th14: :: SCMFSA10:14

for il being Instruction-Location of SCM+FSA holds goto il = [6,<*il*>]

proof end;

theorem Th15: :: SCMFSA10:15

for a being Int-Location
for il being Instruction-Location of SCM+FSA holds a =0_goto il = [7,<*il,a*>]

proof end;

theorem Th16: :: SCMFSA10:16

for a being Int-Location
for il being Instruction-Location of SCM+FSA holds a >0_goto il = [8,<*il,a*>]

proof end;

Lm1: for x, y being set st x in dom <*y*> holds
x = 1

proof end;

Lm2: for x, y, z being set holds
( not x in dom <*y,z*> or x = 1 or x = 2 )

proof end;

Lm3: for x, y, z, t being set holds
( not x in dom <*y,z,t*> or x = 1 or x = 2 or x = 3 )

proof end;

Lm4: 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 )

proof end;

theorem Th17: :: SCMFSA10:17

AddressPart (halt SCM+FSA ) = {} by AMI_3:71, MCART_1:def 2, SCMFSA_2:123;

theorem Th18: :: SCMFSA10:18

for a, b being Int-Location holds AddressPart (a := b) = <*a,b*>

proof end;

theorem Th19: :: SCMFSA10:19

for a, b being Int-Location holds AddressPart (AddTo a,b) = <*a,b*>

proof end;

theorem Th20: :: SCMFSA10:20

for a, b being Int-Location holds AddressPart (SubFrom a,b) = <*a,b*>

proof end;

theorem Th21: :: SCMFSA10:21

for a, b being Int-Location holds AddressPart (MultBy a,b) = <*a,b*>

proof end;

theorem Th22: :: SCMFSA10:22

for a, b being Int-Location holds AddressPart (Divide a,b) = <*a,b*>

proof end;

theorem Th23: :: SCMFSA10:23

for i1 being Instruction-Location of SCM+FSA holds AddressPart (goto i1) = <*i1*>

proof end;

theorem Th24: :: SCMFSA10:24

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds AddressPart (a =0_goto i1) = <*i1,a*>

proof end;

theorem Th25: :: SCMFSA10:25

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds AddressPart (a >0_goto i1) = <*i1,a*>

proof end;

theorem Th26: :: SCMFSA10:26

for b, a being Int-Location
for f being FinSeq-Location holds AddressPart (b := f,a) = <*b,f,a*>

proof end;

theorem Th27: :: SCMFSA10:27

for a, b being Int-Location
for f being FinSeq-Location holds AddressPart (f,a := b) = <*b,f,a*>

proof end;

theorem Th28: :: SCMFSA10:28

for a being Int-Location
for f being FinSeq-Location holds AddressPart (a :=len f) = <*a,f*>

proof end;

theorem Th29: :: SCMFSA10:29

for a being Int-Location
for f being FinSeq-Location holds AddressPart (f :=<0,...,0> a) = <*a,f*>

proof end;

theorem Th30: :: SCMFSA10:30

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

proof end;

registration

let T be InsType of SCM+FSA ;
cluster AddressParts T -> non empty ;
coherence

proof end;

end;

theorem Th31: :: SCMFSA10:31

for T being InsType of SCM+FSA st T = 1 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th32: :: SCMFSA10:32

for T being InsType of SCM+FSA st T = 2 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th33: :: SCMFSA10:33

for T being InsType of SCM+FSA st T = 3 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th34: :: SCMFSA10:34

for T being InsType of SCM+FSA st T = 4 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th35: :: SCMFSA10:35

for T being InsType of SCM+FSA st T = 5 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th36: :: SCMFSA10:36

for T being InsType of SCM+FSA st T = 6 holds
dom (PA (AddressParts T)) = {1}

proof end;

theorem Th37: :: SCMFSA10:37

for T being InsType of SCM+FSA st T = 7 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th38: :: SCMFSA10:38

for T being InsType of SCM+FSA st T = 8 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th39: :: SCMFSA10:39

for T being InsType of SCM+FSA st T = 9 holds
dom (PA (AddressParts T)) = {1,2,3}

proof end;

theorem Th40: :: SCMFSA10:40

for T being InsType of SCM+FSA st T = 10 holds
dom (PA (AddressParts T)) = {1,2,3}

proof end;

theorem Th41: :: SCMFSA10:41

for T being InsType of SCM+FSA st T = 11 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th42: :: SCMFSA10:42

for T being InsType of SCM+FSA st T = 12 holds
dom (PA (AddressParts T)) = {1,2}

proof end;

theorem Th43: :: SCMFSA10:43

for a, b being Int-Location holds (PA (AddressParts (InsCode (a := b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th44: :: SCMFSA10:44

for a, b being Int-Location holds (PA (AddressParts (InsCode (a := b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th45: :: SCMFSA10:45

for a, b being Int-Location holds (PA (AddressParts (InsCode (AddTo a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th46: :: SCMFSA10:46

for a, b being Int-Location holds (PA (AddressParts (InsCode (AddTo a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th47: :: SCMFSA10:47

for a, b being Int-Location holds (PA (AddressParts (InsCode (SubFrom a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th48: :: SCMFSA10:48

for a, b being Int-Location holds (PA (AddressParts (InsCode (SubFrom a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th49: :: SCMFSA10:49

for a, b being Int-Location holds (PA (AddressParts (InsCode (MultBy a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th50: :: SCMFSA10:50

for a, b being Int-Location holds (PA (AddressParts (InsCode (MultBy a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th51: :: SCMFSA10:51

for a, b being Int-Location holds (PA (AddressParts (InsCode (Divide a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th52: :: SCMFSA10:52

for a, b being Int-Location holds (PA (AddressParts (InsCode (Divide a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th53: :: SCMFSA10:53

for i1 being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (goto i1)))) . 1 = the Instruction-Locations of SCM+FSA

proof end;

theorem Th54: :: SCMFSA10:54

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (a =0_goto i1)))) . 1 = the Instruction-Locations of SCM+FSA

proof end;

theorem Th55: :: SCMFSA10:55

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (a =0_goto i1)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th56: :: SCMFSA10:56

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (a >0_goto i1)))) . 1 = the Instruction-Locations of SCM+FSA

proof end;

theorem Th57: :: SCMFSA10:57

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (a >0_goto i1)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th58: :: SCMFSA10:58

for b, a being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (b := f,a)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th59: :: SCMFSA10:59

for b, a being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (b := f,a)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th60: :: SCMFSA10:60

for b, a being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (b := f,a)))) . 3 = SCM+FSA-Data-Loc

proof end;

theorem Th61: :: SCMFSA10:61

for a, b being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (f,a := b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th62: :: SCMFSA10:62

for a, b being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (f,a := b)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th63: :: SCMFSA10:63

for a, b being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (f,a := b)))) . 3 = SCM+FSA-Data-Loc

proof end;

theorem Th64: :: SCMFSA10:64

for a being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (a :=len f)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th65: :: SCMFSA10:65

for a being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (a :=len f)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th66: :: SCMFSA10:66

for a being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (f :=<0,...,0> a)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th67: :: SCMFSA10:67

for a being Int-Location
for f being FinSeq-Location holds (PA (AddressParts (InsCode (f :=<0,...,0> a)))) . 2 = SCM+FSA-Data*-Loc

proof end;

Lm5: for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA st ( for s being State of SCM+FSA st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM+FSA ) = Next (IC s) ) holds
NIC i,l = {(Next l)}

proof end;

Lm6: for i being Instruction of SCM+FSA st ( for l being Instruction-Location of SCM+FSA holds NIC i,l = {(Next l)} ) holds
JUMP i is empty

proof end;

theorem Th68: :: SCMFSA10:68

for il being Instruction-Location of SCM+FSA holds NIC (halt SCM+FSA ),il = {il}

proof end;

registration

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

proof end;

end;

theorem Th69: :: SCMFSA10:69

for a, b being Int-Location
for il being Instruction-Location of SCM+FSA holds NIC (a := b),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th70: :: SCMFSA10:70

for a, b being Int-Location
for il being Instruction-Location of SCM+FSA holds NIC (AddTo a,b),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th71: :: SCMFSA10:71

for a, b being Int-Location
for il being Instruction-Location of SCM+FSA holds NIC (SubFrom a,b),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th72: :: SCMFSA10:72

for a, b being Int-Location
for il being Instruction-Location of SCM+FSA holds NIC (MultBy a,b),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th73: :: SCMFSA10:73

for a, b being Int-Location
for il being Instruction-Location of SCM+FSA holds NIC (Divide a,b),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th74: :: SCMFSA10:74

for i1, il being Instruction-Location of SCM+FSA holds NIC (goto i1),il = {i1}

proof end;

theorem Th75: :: SCMFSA10:75

for i1 being Instruction-Location of SCM+FSA holds JUMP (goto i1) = {i1}

proof end;

registration

let i1 be Instruction-Location of SCM+FSA ;
cluster JUMP (goto i1) -> non empty trivial ;
coherence

proof end;

end;

theorem Th76: :: SCMFSA10:76

for a being Int-Location
for i1, il being Instruction-Location of SCM+FSA holds NIC (a =0_goto i1),il = {i1,(Next il)}

proof end;

theorem Th77: :: SCMFSA10:77

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds JUMP (a =0_goto i1) = {i1}

proof end;

registration

let a be Int-Location ;
let i1 be Instruction-Location of SCM+FSA ;
cluster JUMP (a =0_goto i1) -> non empty trivial ;
coherence

proof end;

end;

theorem Th78: :: SCMFSA10:78

for a being Int-Location
for i1, il being Instruction-Location of SCM+FSA holds NIC (a >0_goto i1),il = {i1,(Next il)}

proof end;

theorem Th79: :: SCMFSA10:79

for a being Int-Location
for i1 being Instruction-Location of SCM+FSA holds JUMP (a >0_goto i1) = {i1}

proof end;

registration

let a be Int-Location ;
let i1 be Instruction-Location of SCM+FSA ;
cluster JUMP (a >0_goto i1) -> non empty trivial ;
coherence

proof end;

end;

theorem Th80: :: SCMFSA10:80

for a, b being Int-Location
for f being FinSeq-Location
for il being Instruction-Location of SCM+FSA holds NIC (a := f,b),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th81: :: SCMFSA10:81

for b, a being Int-Location
for f being FinSeq-Location
for il being Instruction-Location of SCM+FSA holds NIC (f,b := a),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th82: :: SCMFSA10:82

for a being Int-Location
for f being FinSeq-Location
for il being Instruction-Location of SCM+FSA holds NIC (a :=len f),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th83: :: SCMFSA10:83

for a being Int-Location
for f being FinSeq-Location
for il being Instruction-Location of SCM+FSA holds NIC (f :=<0,...,0> a),il = {(Next il)}

proof end;

registration

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

proof end;

end;

theorem Th84: :: SCMFSA10:84

for il being Instruction-Location of SCM+FSA holds SUCC il = {il,(Next il)}

proof end;

theorem Th85: :: SCMFSA10:85

for f being Function of NAT ,the Instruction-Locations of SCM+FSA st ( for k being Nat holds f . k = insloc k ) holds
( f is bijective & ( for k being Nat holds
( f . (k + 1) in SUCC (f . k) & ( for j being Nat st f . j in SUCC (f . k) holds
k <= j ) ) ) )

proof end;

registration

cluster SCM+FSA -> standard ;
coherence

proof end;

end;

theorem Th86: :: SCMFSA10:86