:: SCMFSA6B semantic presentation

theorem Th1: :: SCMFSA6B:1

canceled;

theorem Th2: :: SCMFSA6B:2

canceled;

theorem Th3: :: SCMFSA6B:3

for b₁, b₂ being Function
for b₃ being set st b₃ /\ (dom b₁) c= b₃ /\ (dom b₂) holds
(b₁ +* (b₂ | b₃)) | b₃ = b₂ | b₃

proof end;

theorem Th4: :: SCMFSA6B:4

for b₁ being Macro-Instruction holds Start-At (insloc 0) c= Initialized b₁

proof end;

theorem Th5: :: SCMFSA6B:5

for b₁ being Nat
for b₂ being Macro-Instruction
for b₃ being State of SCM+FSA st b₂ +* (Start-At (insloc b₁)) c= b₃ holds
b₂ c= b₃

proof end;

theorem Th6: :: SCMFSA6B:6

for b₁ being Nat
for b₂ being Macro-Instruction holds (b₂ +* (Start-At (insloc b₁))) | the Instruction-Locations of SCM+FSA = b₂

proof end;

theorem Th7: :: SCMFSA6B:7

for b₁ being Nat
for b₂ being set
for b₃ being Macro-Instruction st b₂ in dom b₃ holds
b₃ . b₂ = (b₃ +* (Start-At (insloc b₁))) . b₂

proof end;

theorem Th8: :: SCMFSA6B:8

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA st Initialized b₁ c= b₂ holds
b₁ +* (Start-At (insloc 0)) c= b₂

proof end;

theorem Th9: :: SCMFSA6B:9

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds not b₁ in dom (Start-At b₂)

proof end;

theorem Th10: :: SCMFSA6B:10

for b₁ being FinSeq-Location
for b₂ being Instruction-Location of SCM+FSA holds not b₁ in dom (Start-At b₂)

proof end;

theorem Th11: :: SCMFSA6B:11

for b₁, b₂ being Instruction-Location of SCM+FSA holds not b₁ in dom (Start-At b₂)

proof end;

theorem Th12: :: SCMFSA6B:12

for b₁ being Macro-Instruction
for b₂ being Int-Location
for b₃ being Instruction-Location of SCM+FSA holds not b₂ in dom (b₁ +* (Start-At b₃))

proof end;

theorem Th13: :: SCMFSA6B:13

for b₁ being Macro-Instruction
for b₂ being FinSeq-Location
for b₃ being Instruction-Location of SCM+FSA holds not b₂ in dom (b₁ +* (Start-At b₃))

proof end;

theorem Th14: :: SCMFSA6B:14

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA holds (b₂ +* b₁) +* (Start-At (insloc 0)) = (b₂ +* (Start-At (insloc 0))) +* b₁

proof end;

theorem Th15: :: SCMFSA6B:15

for b₁ being State of SCM+FSA st b₁ = Following b₁ holds
for b₂ being Nat holds (Computation b₁) . b₂ = b₁

proof end;

theorem Th16: :: SCMFSA6B:16

for b₁ being non empty with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite AMI-Struct of b₁
for b₃ being State of b₂ st b₃ is halting holds
Result b₃ = (Computation b₃) . (LifeSpan b₃)

proof end;

definition

let c₁ be non empty with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
let c₄ be Instruction-Location of c₂;
let c₅ be Instruction of c₂;
redefine func +* as c₃ +* c₄,c₅ -> State of a₂;
coherence

proof end;

end;

definition

let c₁ be State of SCM+FSA ;
let c₂ be Int-Location ;
let c₃ be Integer;
redefine func +* as c₁ +* c₂,c₃ -> State of SCM+FSA ;
coherence

proof end;

end;

theorem Th17: :: SCMFSA6B:17

for b₁ being non empty with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Nat holds b₃ | the Instruction-Locations of b₂ = ((Computation b₃) . b₄) | the Instruction-Locations of b₂

proof end;

definition

let c₁ be Macro-Instruction;
let c₂ be State of SCM+FSA ;
func IExec c₁,c₂ -> State of SCM+FSA equals :: SCMFSA6B:def 1
(Result (a₂ +* (Initialized a₁))) +* (a₂ | the Instruction-Locations of SCM+FSA );
coherence by AMI_5:82;

end;

:: deftheorem Def1 defines IExec SCMFSA6B:def 1 :

definition

let c₁ be Macro-Instruction;
attr a₁ is paraclosed means :Def2: :: SCMFSA6B:def 2
for b₁ being State of SCM+FSA
for b₂ being Nat st a₁ +* (Start-At (insloc 0)) c= b₁ holds
IC ((Computation b₁) . b₂) in dom a₁;
attr a₁ is parahalting means :Def3: :: SCMFSA6B:def 3
a₁ +* (Start-At (insloc 0)) is halting;
attr a₁ is keeping_0 means :Def4: :: SCMFSA6B:def 4
for b₁ being State of SCM+FSA st a₁ +* (Start-At (insloc 0)) c= b₁ holds
for b₂ being Nat holds ((Computation b₁) . b₂) . (intloc 0) = b₁ . (intloc 0);

end;

:: deftheorem Def2 defines paraclosed SCMFSA6B:def 2 :

:: deftheorem Def3 defines parahalting SCMFSA6B:def 3 :

:: deftheorem Def4 defines keeping_0 SCMFSA6B:def 4 :

Lemma16: Macro (halt SCM+FSA ) is parahalting

proof end;

registration

cluster parahalting FinPartState of SCM+FSA ;
existence by Lemma16;

end;

theorem Th18: :: SCMFSA6B:18

for b₁ being State of SCM+FSA
for b₂ being parahalting Macro-Instruction st b₂ +* (Start-At (insloc 0)) c= b₁ holds
b₁ is halting

proof end;

theorem Th19: :: SCMFSA6B:19

for b₁ being State of SCM+FSA
for b₂ being parahalting Macro-Instruction st Initialized b₂ c= b₁ holds
b₁ is halting

proof end;

registration

let c₁ be parahalting Macro-Instruction;
cluster Initialized a₁ -> halting ;
coherence

proof end;

end;

theorem Th20: :: SCMFSA6B:20

for b₁ being State of SCM+FSA holds not b₁ +* (IC b₁),(goto (IC b₁)) is halting

proof end;

theorem Th21: :: SCMFSA6B:21

for b₁ being Nat
for b₂ being Macro-Instruction
for b₃, b₄ being State of SCM+FSA st b₃,b₄ equal_outside the Instruction-Locations of SCM+FSA & b₂ c= b₃ & b₂ c= b₄ & ( for b₅ being Nat st b₅ < b₁ holds
IC ((Computation b₄) . b₅) in dom b₂ ) holds
for b₅ being Nat st b₅ <= b₁ holds
(Computation b₃) . b₅,(Computation b₄) . b₅ equal_outside the Instruction-Locations of SCM+FSA

proof end;

registration

cluster parahalting -> paraclosed FinPartState of SCM+FSA ;
coherence

proof end;

cluster keeping_0 -> paraclosed FinPartState of SCM+FSA ;
coherence

proof end;

end;

theorem Th22: :: SCMFSA6B:22

for b₁ being State of SCM+FSA
for b₂ being parahalting Macro-Instruction
for b₃ being read-write Int-Location st not b₃ in UsedIntLoc b₂ holds
(IExec b₂,b₁) . b₃ = b₁ . b₃

proof end;

theorem Th23: :: SCMFSA6B:23

for b₁ being FinSeq-Location
for b₂ being State of SCM+FSA
for b₃ being parahalting Macro-Instruction st not b₁ in UsedInt*Loc b₃ holds
(IExec b₃,b₂) . b₁ = b₂ . b₁

proof end;

theorem Th24: :: SCMFSA6B:24

for b₁ being Instruction-Location of SCM+FSA
for b₂ being State of SCM+FSA st IC b₂ = b₁ & b₂ . b₁ = goto b₁ holds
not b₂ is halting

proof end;

registration

cluster parahalting -> non empty FinPartState of SCM+FSA ;
coherence

proof end;

end;

theorem Th25: :: SCMFSA6B:25

for b₁ being parahalting Macro-Instruction holds dom b₁ <> {}

proof end;

theorem Th26: :: SCMFSA6B:26

for b₁ being parahalting Macro-Instruction holds insloc 0 in dom b₁

proof end;

theorem Th27: :: SCMFSA6B:27

for b₁, b₂ being State of SCM+FSA
for b₃ being parahalting Macro-Instruction st b₃ +* (Start-At (insloc 0)) c= b₁ holds
for b₄ being Nat st ProgramPart (Relocated b₃,b₄) c= b₂ & IC b₂ = insloc b₄ & b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) holds
for b₅ being Nat holds
( (IC ((Computation b₁) . b₅)) + b₄ = IC ((Computation b₂) . b₅) & IncAddr (CurInstr ((Computation b₁) . b₅)),b₄ = CurInstr ((Computation b₂) . b₅) & ((Computation b₁) . b₅) | (Int-Locations \/ FinSeq-Locations ) = ((Computation b₂) . b₅) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th28: :: SCMFSA6B:28

for b₁, b₂ being State of SCM+FSA
for b₃ being parahalting Macro-Instruction st b₃ +* (Start-At (insloc 0)) c= b₁ & b₃ +* (Start-At (insloc 0)) c= b₂ & b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA holds
for b₄ being Nat holds
( (Computation b₁) . b₄,(Computation b₂) . b₄ equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation b₁) . b₄) = CurInstr ((Computation b₂) . b₄) )

proof end;

theorem Th29: :: SCMFSA6B:29

for b₁, b₂ being State of SCM+FSA
for b₃ being parahalting Macro-Instruction st b₃ +* (Start-At (insloc 0)) c= b₁ & b₃ +* (Start-At (insloc 0)) c= b₂ & b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA holds
( LifeSpan b₁ = LifeSpan b₂ & Result b₁, Result b₂ equal_outside the Instruction-Locations of SCM+FSA )

proof end;

theorem Th30: :: SCMFSA6B:30

for b₁ being State of SCM+FSA
for b₂ being parahalting Macro-Instruction holds IC (IExec b₂,b₁) = IC (Result (b₁ +* (Initialized b₂)))

proof end;

theorem Th31: :: SCMFSA6B:31

for b₁ being non empty Macro-Instruction holds
( insloc 0 in dom b₁ & insloc 0 in dom (Initialized b₁) & insloc 0 in dom (b₁ +* (Start-At (insloc 0))) )

proof end;

theorem Th32: :: SCMFSA6B:32

for b₁ being set
for b₂ being Instruction of SCM+FSA holds
( b₁ in dom (Macro b₂) iff ( b₁ = insloc 0 or b₁ = insloc 1 ) )

proof end;

theorem Th33: :: SCMFSA6B:33

for b₁ being Instruction of SCM+FSA holds
( (Macro b₁) . (insloc 0) = b₁ & (Macro b₁) . (insloc 1) = halt SCM+FSA & (Initialized (Macro b₁)) . (insloc 0) = b₁ & (Initialized (Macro b₁)) . (insloc 1) = halt SCM+FSA & ((Macro b₁) +* (Start-At (insloc 0))) . (insloc 0) = b₁ )

proof end;

theorem Th34: :: SCMFSA6B:34

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA st Initialized b₁ c= b₂ holds
IC b₂ = insloc 0

proof end;

Lemma31: ( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting )

proof end;

registration

cluster non empty paraclosed parahalting keeping_0 FinPartState of SCM+FSA ;
existence by Lemma31;

end;

theorem Th35: :: SCMFSA6B:35

for b₁ being State of SCM+FSA
for b₂ being parahalting keeping_0 Macro-Instruction holds (IExec b₂,b₁) . (intloc 0) = 1

proof end;

theorem Th36: :: SCMFSA6B:36

for b₁ being State of SCM+FSA
for b₂ being paraclosed Macro-Instruction
for b₃ being Macro-Instruction st b₂ +* (Start-At (insloc 0)) c= b₁ & b₁ is halting holds
for b₄ being Nat st b₄ <= LifeSpan b₁ holds
(Computation b₁) . b₄,(Computation (b₁ +* (b₂ ';' b₃))) . b₄ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th37: :: SCMFSA6B:37

for b₁ being State of SCM+FSA
for b₂ being paraclosed Macro-Instruction st b₁ +* b₂ is halting & Directed b₂ c= b₁ & Start-At (insloc 0) c= b₁ holds
IC ((Computation b₁) . ((LifeSpan (b₁ +* b₂)) + 1)) = insloc (card b₂)

proof end;

theorem Th38: :: SCMFSA6B:38

for b₁ being State of SCM+FSA
for b₂ being paraclosed Macro-Instruction st b₁ +* b₂ is halting & Directed b₂ c= b₁ & Start-At (insloc 0) c= b₁ holds
((Computation b₁) . (LifeSpan (b₁ +* b₂))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation b₁) . ((LifeSpan (b₁ +* b₂)) + 1)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th39: :: SCMFSA6B:39

for b₁ being State of SCM+FSA
for b₂ being parahalting Macro-Instruction st Initialized b₂ c= b₁ holds
for b₃ being Nat st b₃ <= LifeSpan b₁ holds
CurInstr ((Computation (b₁ +* (Directed b₂))) . b₃) <> halt SCM+FSA

proof end;

theorem Th40: :: SCMFSA6B:40

for b₁ being State of SCM+FSA
for b₂ being paraclosed Macro-Instruction st b₁ +* (b₂ +* (Start-At (insloc 0))) is halting holds
for b₃ being Macro-Instruction
for b₄ being Nat st b₄ <= LifeSpan (b₁ +* (b₂ +* (Start-At (insloc 0)))) holds
(Computation (b₁ +* (b₂ +* (Start-At (insloc 0))))) . b₄,(Computation (b₁ +* ((b₂ ';' b₃) +* (Start-At (insloc 0))))) . b₄ equal_outside the Instruction-Locations of SCM+FSA

proof end;

Lemma37: for b₁ being parahalting keeping_0 Macro-Instruction
for b₂ being parahalting Macro-Instruction
for b₃ being State of SCM+FSA st Initialized (b₁ ';' b₂) c= b₃ holds
( IC ((Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1)) = insloc (card b₁) & ((Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1)) | (Int-Locations \/ FinSeq-Locations ) = (((Computation (b₃ +* b₁)) . (LifeSpan (b₃ +* b₁))) +* (Initialized b₂)) | (Int-Locations \/ FinSeq-Locations ) & ProgramPart (Relocated b₂,(card b₁)) c= (Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1) & ((Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1)) . (intloc 0) = 1 & b₃ is halting & LifeSpan b₃ = ((LifeSpan (b₃ +* b₁)) + 1) + (LifeSpan ((Result (b₃ +* b₁)) +* (Initialized b₂))) & ( b₂ is keeping_0 implies (Result b₃) . (intloc 0) = 1 ) )

proof end;

registration

let c₁, c₂ be parahalting Macro-Instruction;
cluster a₁ ';' a₂ -> non empty paraclosed parahalting ;
coherence

proof end;

end;

theorem Th41: :: SCMFSA6B:41

for b₁ being State of SCM+FSA
for b₂ being keeping_0 Macro-Instruction st not b₁ +* (b₂ +* (Start-At (insloc 0))) is halting holds
for b₃ being Macro-Instruction
for b₄ being Nat holds (Computation (b₁ +* (b₂ +* (Start-At (insloc 0))))) . b₄,(Computation (b₁ +* ((b₂ ';' b₃) +* (Start-At (insloc 0))))) . b₄ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th42: :: SCMFSA6B:42

for b₁ being State of SCM+FSA
for b₂ being keeping_0 Macro-Instruction st b₁ +* b₂ is halting holds
for b₃ being paraclosed Macro-Instruction st (b₂ ';' b₃) +* (Start-At (insloc 0)) c= b₁ holds
for b₄ being Nat holds ((Computation ((Result (b₁ +* b₂)) +* (b₃ +* (Start-At (insloc 0))))) . b₄) +* (Start-At ((IC ((Computation ((Result (b₁ +* b₂)) +* (b₃ +* (Start-At (insloc 0))))) . b₄)) + (card b₂))),(Computation (b₁ +* (b₂ ';' b₃))) . (((LifeSpan (b₁ +* b₂)) + 1) + b₄) equal_outside the Instruction-Locations of SCM+FSA

proof end;

registration

let c₁, c₂ be keeping_0 Macro-Instruction;
cluster a₁ ';' a₂ -> paraclosed keeping_0 ;
coherence

proof end;

end;

theorem Th43: :: SCMFSA6B:43

for b₁ being State of SCM+FSA
for b₂ being parahalting keeping_0 Macro-Instruction
for b₃ being parahalting Macro-Instruction holds LifeSpan (b₁ +* (Initialized (b₂ ';' b₃))) = ((LifeSpan (b₁ +* (Initialized b₂))) + 1) + (LifeSpan ((Result (b₁ +* (Initialized b₂))) +* (Initialized b₃)))

proof end;

theorem Th44: :: SCMFSA6B:44

for b₁ being State of SCM+FSA
for b₂ being parahalting keeping_0 Macro-Instruction
for b₃ being parahalting Macro-Instruction holds IExec (b₂ ';' b₃),b₁ = (IExec b₃,(IExec b₂,b₁)) +* (Start-At ((IC (IExec b₃,(IExec b₂,b₁))) + (card b₂)))

proof end;