:: SCMPDS_9 semantic presentation

theorem Th1: :: SCMPDS_9:1

for b₁ being real number holds 0 <= b₁ + (abs b₁)

proof end;

theorem Th2: :: SCMPDS_9:2

for b₁ being real number holds 0 <= (- b₁) + (abs b₁)

proof end;

theorem Th3: :: SCMPDS_9:3

for b₁, b₂ being real number holds
( not abs b₁ = abs b₂ or b₁ = b₂ or b₁ = - b₂ )

proof end;

theorem Th4: :: SCMPDS_9:4

for b₁, b₂ being natural number st b₁ < b₂ & b₁ <> 0 holds
not b₁ / b₂ is integer

proof end;

theorem Th5: :: SCMPDS_9:5

not { (2 * b₁) where B is Nat : b₁ > 1 } is finite

proof end;

theorem Th6: :: SCMPDS_9:6

for b₁ being Function
for b₂, b₃, b₄ being set st b₂ <> b₄ holds
(b₁ +* (b₂ .--> b₃)) . b₄ = b₁ . b₄

proof end;

theorem Th7: :: SCMPDS_9:7

for b₁ being Function
for b₂, b₃, b₄, b₅ being set st b₂ <> b₃ holds
( (b₁ +* (b₂,b₃ --> b₄,b₅)) . b₂ = b₄ & (b₁ +* (b₂,b₃ --> b₄,b₅)) . b₃ = b₅ )

proof end;

Lemma8: for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Instruction of b₂ holds (Exec (b₃ . (IC b₃)),b₃) . (IC b₂) = IC (Following b₃)

proof end;

definition

let c₁, c₂ be Int_position ;
let c₃, c₄ be Integer;
redefine func --> as c₁,c₂ --> c₃,c₄ -> FinPartState of SCMPDS ;
coherence

proof end;

end;

registration

cluster SCMPDS -> with-non-trivial-Instruction-Locations ;
coherence

proof end;

end;

definition

let c₁ be Instruction-Location of SCMPDS ;
func locnum c₁ -> natural number means :Def1: :: SCMPDS_9:def 1
il. a₂ = a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines locnum SCMPDS_9:def 1 :

definition

let c₁ be Instruction-Location of SCMPDS ;
redefine func locnum as locnum c₁ -> Nat;
coherence by ORDINAL2:def 21;

end;

theorem Th8: :: SCMPDS_9:8

for b₁ being Instruction-Location of SCMPDS holds b₁ = (2 * (locnum b₁)) + 2

proof end;

theorem Th9: :: SCMPDS_9:9

for b₁, b₂ being Instruction-Location of SCMPDS st b₁ <> b₂ holds
locnum b₁ <> locnum b₂

proof end;

theorem Th10: :: SCMPDS_9:10

for b₁, b₂ being Instruction-Location of SCMPDS st b₁ <> b₂ holds
Next b₁ <> Next b₂

proof end;

theorem Th11: :: SCMPDS_9:11

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃ being Instruction of b₂
for b₄ being Instruction-Location of b₂ holds JUMP b₃ c= NIC b₃,b₄

proof end;

theorem Th12: :: SCMPDS_9:12

for b₁ being Instruction of SCMPDS
for b₂ being Instruction-Location of SCMPDS st ( for b₃ being State of SCMPDS st IC b₃ = b₂ & b₃ . b₂ = b₁ holds
(Exec b₁,b₃) . (IC SCMPDS ) = Next (IC b₃) ) holds
NIC b₁,b₂ = {(Next b₂)}

proof end;

theorem Th13: :: SCMPDS_9:13

for b₁ being Instruction of SCMPDS st ( for b₂ being Instruction-Location of SCMPDS holds NIC b₁,b₂ = {(Next b₂)} ) holds
JUMP b₁ is empty

proof end;

theorem Th14: :: SCMPDS_9:14

for b₁ being Instruction-Location of SCMPDS
for b₂ being Integer holds NIC (goto b₂),b₁ = {((2 * (abs (b₂ + (locnum b₁)))) + 2)}

proof end;

Lemma16: for b₁ being natural number st b₁ > 1 holds
b₁ - 2 is Nat

proof end;

theorem Th15: :: SCMPDS_9:15

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS holds NIC (return b₁),b₂ = { (2 * b₃) where B is Nat : b₃ > 1 }

proof end;

theorem Th16: :: SCMPDS_9:16

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS
for b₃ being Integer holds NIC (saveIC b₁,b₃),b₂ = {(Next b₂)}

proof end;

theorem Th17: :: SCMPDS_9:17

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS
for b₃ being Integer holds NIC (b₁ := b₃),b₂ = {(Next b₂)}

proof end;

theorem Th18: :: SCMPDS_9:18

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS
for b₃, b₄ being Integer holds NIC (b₁,b₃ := b₄),b₂ = {(Next b₂)}

proof end;

theorem Th19: :: SCMPDS_9:19

for b₁, b₂ being Int_position
for b₃ being Instruction-Location of SCMPDS
for b₄, b₅ being Integer holds NIC (b₁,b₄ := b₂,b₅),b₃ = {(Next b₃)}

proof end;

theorem Th20: :: SCMPDS_9:20

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS
for b₃, b₄ being Integer holds NIC (AddTo b₁,b₃,b₄),b₂ = {(Next b₂)}

proof end;

theorem Th21: :: SCMPDS_9:21

for b₁, b₂ being Int_position
for b₃ being Instruction-Location of SCMPDS
for b₄, b₅ being Integer holds NIC (AddTo b₁,b₄,b₂,b₅),b₃ = {(Next b₃)}

proof end;

theorem Th22: :: SCMPDS_9:22

for b₁, b₂ being Int_position
for b₃ being Instruction-Location of SCMPDS
for b₄, b₅ being Integer holds NIC (SubFrom b₁,b₄,b₂,b₅),b₃ = {(Next b₃)}

proof end;

theorem Th23: :: SCMPDS_9:23

for b₁, b₂ being Int_position
for b₃ being Instruction-Location of SCMPDS
for b₄, b₅ being Integer holds NIC (MultBy b₁,b₄,b₂,b₅),b₃ = {(Next b₃)}

proof end;

theorem Th24: :: SCMPDS_9:24

for b₁, b₂ being Int_position
for b₃ being Instruction-Location of SCMPDS
for b₄, b₅ being Integer holds NIC (Divide b₁,b₄,b₂,b₅),b₃ = {(Next b₃)}

proof end;

theorem Th25: :: SCMPDS_9:25

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS
for b₃, b₄ being Integer holds NIC (b₁,b₃ <>0_goto b₄),b₂ = {(Next b₂),((abs (2 * (b₄ + (locnum b₂)))) + 2)}

proof end;

theorem Th26: :: SCMPDS_9:26

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS
for b₃, b₄ being Integer holds NIC (b₁,b₃ <=0_goto b₄),b₂ = {(Next b₂),((abs (2 * (b₄ + (locnum b₂)))) + 2)}

proof end;

theorem Th27: :: SCMPDS_9:27

for b₁ being Int_position
for b₂ being Instruction-Location of SCMPDS
for b₃, b₄ being Integer holds NIC (b₁,b₃ >=0_goto b₄),b₂ = {(Next b₂),((abs (2 * (b₄ + (locnum b₂)))) + 2)}

proof end;

Lemma27: for b₁ being Integer holds JUMP (goto b₁) = {}

proof end;

registration

let c₁ be Integer;
cluster JUMP (goto a₁) -> empty ;
coherence by Lemma27;

end;

theorem Th28: :: SCMPDS_9:28

for b₁ being Int_position holds JUMP (return b₁) = { (2 * b₂) where B is Nat : b₂ > 1 }

proof end;

registration

let c₁ be Int_position ;
cluster JUMP (return a₁) -> infinite ;
coherence by Th5, Th28;

end;

registration

let c₁ be Int_position ;
let c₂ be Integer;
cluster JUMP (saveIC a₁,a₂) -> empty ;
coherence

proof end;

end;

registration

let c₁ be Int_position ;
let c₂ be Integer;
cluster JUMP (a₁ := a₂) -> empty ;
coherence

proof end;

end;

registration

let c₁ be Int_position ;
let c₂, c₃ be Integer;
cluster JUMP (a₁,a₂ := a₃) -> empty ;
coherence

proof end;

end;

registration

let c₁, c₂ be Int_position ;
let c₃, c₄ be Integer;
cluster JUMP (a₁,a₃ := a₂,a₄) -> empty ;
coherence

proof end;

end;

registration

let c₁ be Int_position ;
let c₂, c₃ be Integer;
cluster JUMP (AddTo a₁,a₂,a₃) -> empty ;
coherence

proof end;

end;

registration

let c₁, c₂ be Int_position ;
let c₃, c₄ be Integer;
cluster JUMP (AddTo a₁,a₃,a₂,a₄) -> empty ;
coherence

proof end;

cluster JUMP (SubFrom a₁,a₃,a₂,a₄) -> empty ;
coherence

proof end;

cluster JUMP (MultBy a₁,a₃,a₂,a₄) -> empty ;
coherence

proof end;

cluster JUMP (Divide a₁,a₃,a₂,a₄) -> empty ;
coherence

proof end;

end;

Lemma29: not 5 / 3 is integer

proof end;

Lemma30: for b₁ being real number st b₁ > 0 holds
- ((2 * b₁) + (1 + b₁)) < - 0

proof end;

Lemma31: for b₁ being real number holds (((2 * ((abs b₁) + (((- b₁) + (abs b₁)) + 4))) + 2) - 2) + (2 * b₁) <> - ((((2 * (((abs b₁) + (((- b₁) + (abs b₁)) + 4)) + (((- b₁) + (abs b₁)) + 4))) + 2) - 2) + (2 * b₁))

proof end;

Lemma32: for b₁, b₂ being real number holds (2 * b₁) + 2 <> (2 * b₁) + ((2 * (((- b₂) + (abs b₂)) + 4)) + (2 * b₂))

proof end;

Lemma33: for b₁, b₂ being real number st b₁ > 0 holds
(2 * ((abs b₂) + b₁)) + 2 <> - (((2 * ((abs b₂) + b₁)) + (2 * b₁)) + (2 * b₂))

proof end;

Lemma34: for b₁ being real number
for b₂ being Integer st b₂ <> 5 holds
2 * ((b₁ + (((- b₂) + (abs b₂)) + 4)) + 1) <> 2 * (b₁ + b₂)

proof end;

Lemma35: for b₁, b₂ being real number st - ((2 * b₁) + (1 + b₁)) < - 0 holds
(2 * (((abs b₂) + b₁) + b₁)) + 2 <> - ((2 * ((abs b₂) + b₁)) + (2 * b₂))

proof end;

Lemma36: for b₁ being Int_position
for b₂ being Integer holds JUMP (b₁,b₂ <>0_goto 5) = {}

proof end;

Lemma37: for b₁ being Int_position
for b₂, b₃ being Integer st b₂ <> 5 holds
JUMP (b₁,b₃ <>0_goto b₂) = {}

proof end;

Lemma38: for b₁ being Int_position
for b₂ being Integer holds JUMP (b₁,b₂ <=0_goto 5) = {}

proof end;

Lemma39: for b₁ being Int_position
for b₂, b₃ being Integer st b₂ <> 5 holds
JUMP (b₁,b₃ <=0_goto b₂) = {}

proof end;

Lemma40: for b₁ being Int_position
for b₂ being Integer holds JUMP (b₁,b₂ >=0_goto 5) = {}

proof end;

Lemma41: for b₁ being Int_position
for b₂, b₃ being Integer st b₂ <> 5 holds
JUMP (b₁,b₃ >=0_goto b₂) = {}

proof end;

registration

let c₁ be Int_position ;
let c₂, c₃ be Integer;
cluster JUMP (a₁,a₂ <>0_goto a₃) -> empty ;
coherence

proof end;

cluster JUMP (a₁,a₂ <=0_goto a₃) -> empty ;
coherence

proof end;

cluster JUMP (a₁,a₂ >=0_goto a₃) -> empty ;
coherence

proof end;

end;

theorem Th29: :: SCMPDS_9:29

for b₁ being Instruction-Location of SCMPDS holds SUCC b₁ = the Instruction-Locations of SCMPDS

proof end;

theorem Th30: :: SCMPDS_9:30

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃, b₄ being Instruction-Location of b₂ st SUCC b₃ = the Instruction-Locations of b₂ holds
b₃ <= b₄

proof end;

registration

cluster SCMPDS -> non InsLoc-antisymmetric with-non-trivial-Instruction-Locations ;
coherence

proof end;

end;

registration

cluster SCMPDS -> non InsLoc-antisymmetric non standard with-non-trivial-Instruction-Locations ;
coherence by AMISTD_1:30;

end;