:: SCM_HALT semantic presentation

definition

let c₁ be Macro-Instruction;
attr a₁ is InitClosed means :Def1: :: SCM_HALT:def 1
for b₁ being State of SCM+FSA
for b₂ being Nat st Initialized a₁ c= b₁ holds
IC ((Computation b₁) . b₂) in dom a₁;
attr a₁ is InitHalting means :Def2: :: SCM_HALT:def 2
Initialized a₁ is halting;
attr a₁ is keepInt0_1 means :Def3: :: SCM_HALT:def 3
for b₁ being State of SCM+FSA st Initialized a₁ c= b₁ holds
for b₂ being Nat holds ((Computation b₁) . b₂) . (intloc 0) = 1;

end;

:: deftheorem Def1 defines InitClosed SCM_HALT:def 1 :

:: deftheorem Def2 defines InitHalting SCM_HALT:def 2 :

:: deftheorem Def3 defines keepInt0_1 SCM_HALT:def 3 :

theorem Th1: :: SCM_HALT:1

for b₁ being set
for b₂, b₃, b₄ being Nat holds
( not b₁ in dom (((intloc b₂) .--> b₃) +* (Start-At (insloc b₄))) or b₁ = intloc b₂ or b₁ = IC SCM+FSA )

proof end;

theorem Th2: :: SCM_HALT:2

for b₁ being Macro-Instruction
for b₂, b₃, b₄ being Nat holds dom b₁ misses dom (((intloc b₂) .--> b₃) +* (Start-At (insloc b₄)))

proof end;

set c₁ = ((intloc 0) .--> 1) +* (Start-At (insloc 0));

theorem Th3: :: SCM_HALT:3

for b₁ being Macro-Instruction holds Initialized b₁ = b₁ +* (((intloc 0) .--> 1) +* (Start-At (insloc 0)))

proof end;

theorem Th4: :: SCM_HALT:4

Macro (halt SCM+FSA ) is InitHalting

proof end;

registration

cluster InitHalting FinPartState of SCM+FSA ;
existence by Th4;

end;

theorem Th5: :: SCM_HALT:5

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

proof end;

theorem Th6: :: SCM_HALT:6

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

proof end;

theorem Th7: :: SCM_HALT:7

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA st Initialized b₁ c= b₂ holds
b₂ . (intloc 0) = 1

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

cluster InitHalting -> InitClosed FinPartState of SCM+FSA ;
coherence

proof end;

cluster keepInt0_1 -> InitClosed FinPartState of SCM+FSA ;
coherence

proof end;

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

proof end;

end;

theorem Th8: :: SCM_HALT:8

for b₁ being State of SCM+FSA
for b₂ being InitHalting 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 Th9: :: SCM_HALT:9

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

proof end;

registration

let c₂ be InitHalting Macro-Instruction;
cluster Initialized a₁ -> halting ;
coherence by Def2;

end;

registration

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

proof end;

end;

theorem Th10: :: SCM_HALT:10

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

proof end;

theorem Th11: :: SCM_HALT:11

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

proof end;

theorem Th12: :: SCM_HALT:12

for b₁, b₂ being State of SCM+FSA
for b₃ being InitHalting Macro-Instruction st Initialized b₃ 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 Th13: :: SCM_HALT:13

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

proof end;

theorem Th14: :: SCM_HALT:14

for b₁, b₂ being State of SCM+FSA
for b₃ being InitHalting Macro-Instruction st Initialized b₃ c= b₁ & Initialized b₃ 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 Th15: :: SCM_HALT:15

for b₁, b₂ being State of SCM+FSA
for b₃ being InitHalting Macro-Instruction st Initialized b₃ c= b₁ & Initialized b₃ 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;

registration

cluster non empty keeping_0 InitClosed InitHalting keepInt0_1 FinPartState of SCM+FSA ;
existence

proof end;

end;

registration

cluster non empty InitClosed InitHalting keepInt0_1 FinPartState of SCM+FSA ;
existence

proof end;

end;

theorem Th16: :: SCM_HALT:16

canceled;

theorem Th17: :: SCM_HALT:17

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

proof end;

theorem Th18: :: SCM_HALT:18

for b₁ being State of SCM+FSA
for b₂ being InitClosed Macro-Instruction
for b₃ being Macro-Instruction st Initialized b₂ 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 Th19: :: SCM_HALT:19

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA
for b₃, b₄, b₅ being Nat holds (b₂ +* b₁) +* (((intloc b₃) .--> b₄) +* (Start-At (insloc b₅))) = (b₂ +* (((intloc b₃) .--> b₄) +* (Start-At (insloc b₅)))) +* b₁

proof end;

theorem Th20: :: SCM_HALT:20

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

proof end;

theorem Th21: :: SCM_HALT:21

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

proof end;

theorem Th22: :: SCM_HALT:22

for b₁ being State of SCM+FSA
for b₂ being InitClosed Macro-Instruction st b₁ +* b₂ is halting & Directed b₂ c= b₁ & ((intloc 0) .--> 1) +* (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 Th23: :: SCM_HALT:23

for b₁ being State of SCM+FSA
for b₂ being InitHalting 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 Th24: :: SCM_HALT:24

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

proof end;

theorem Th25: :: SCM_HALT:25

for b₁ being InitHalting keepInt0_1 Macro-Instruction
for b₂ being InitHalting 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₂ be InitHalting keepInt0_1 Macro-Instruction;
let c₃ be InitHalting Macro-Instruction;
cluster a₁ ';' a₂ -> non empty InitClosed InitHalting ;
coherence

proof end;

end;

theorem Th26: :: SCM_HALT:26

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

proof end;

theorem Th27: :: SCM_HALT:27

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

proof end;

theorem Th28: :: SCM_HALT:28

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

proof end;

theorem Th29: :: SCM_HALT:29

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

proof end;

registration

let c₂ be parahalting Instruction of SCM+FSA ;
cluster Macro a₁ -> InitClosed InitHalting ;
coherence ;

end;

registration

let c₂ be parahalting Instruction of SCM+FSA ;
let c₃ be parahalting Macro-Instruction;
cluster a₁ ';' a₂ -> InitClosed InitHalting ;
coherence ;

end;

registration

let c₂ be parahalting keeping_0 Instruction of SCM+FSA ;
let c₃ be InitHalting Macro-Instruction;
cluster a₁ ';' a₂ -> non empty InitClosed InitHalting ;
coherence

proof end;

end;

registration

let c₂, c₃ be keepInt0_1 Macro-Instruction;
cluster a₁ ';' a₂ -> InitClosed keepInt0_1 ;
coherence

proof end;

end;

registration

let c₂ be parahalting keeping_0 Instruction of SCM+FSA ;
let c₃ be InitHalting keepInt0_1 Macro-Instruction;
cluster a₂ ';' a₁ -> non empty InitClosed InitHalting keepInt0_1 ;
coherence

proof end;

end;

registration

let c₂ be parahalting keeping_0 Instruction of SCM+FSA ;
let c₃ be InitHalting keepInt0_1 Macro-Instruction;
cluster a₁ ';' a₂ -> non empty InitClosed InitHalting keepInt0_1 ;
coherence

proof end;

end;

registration

let c₂ be parahalting Instruction of SCM+FSA ;
let c₃ be parahalting Macro-Instruction;
cluster a₂ ';' a₁ -> InitClosed InitHalting ;
coherence ;

end;

registration

let c₂, c₃ be parahalting Instruction of SCM+FSA ;
cluster a₁ ';' a₂ -> InitClosed InitHalting ;
coherence ;

end;

theorem Th30: :: SCM_HALT:30

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being InitHalting keepInt0_1 Macro-Instruction
for b₄ being InitHalting Macro-Instruction holds (IExec (b₃ ';' b₄),b₁) . b₂ = (IExec b₄,(IExec b₃,b₁)) . b₂

proof end;

theorem Th31: :: SCM_HALT:31

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃ being InitHalting keepInt0_1 Macro-Instruction
for b₄ being InitHalting Macro-Instruction holds (IExec (b₃ ';' b₄),b₁) . b₂ = (IExec b₄,(IExec b₃,b₁)) . b₂

proof end;

theorem Th32: :: SCM_HALT:32

for b₁ being InitHalting keepInt0_1 Macro-Instruction
for b₂ being State of SCM+FSA holds (Initialize (IExec b₁,b₂)) | (Int-Locations \/ FinSeq-Locations ) = (IExec b₁,b₂) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th33: :: SCM_HALT:33

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being InitHalting keepInt0_1 Macro-Instruction
for b₄ being parahalting Instruction of SCM+FSA holds (IExec (b₃ ';' b₄),b₁) . b₂ = (Exec b₄,(IExec b₃,b₁)) . b₂

proof end;

theorem Th34: :: SCM_HALT:34

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃ being InitHalting keepInt0_1 Macro-Instruction
for b₄ being parahalting Instruction of SCM+FSA holds (IExec (b₃ ';' b₄),b₁) . b₂ = (Exec b₄,(IExec b₃,b₁)) . b₂

proof end;

definition

let c₂ be Macro-Instruction;
let c₃ be State of SCM+FSA ;
pred c₁ is_closed_onInit c₂ means :Def4: :: SCM_HALT:def 4
for b₁ being Nat holds IC ((Computation (a₂ +* (Initialized a₁))) . b₁) in dom a₁;
pred c₁ is_halting_onInit c₂ means :Def5: :: SCM_HALT:def 5
a₂ +* (Initialized a₁) is halting;

end;

:: deftheorem Def4 defines is_closed_onInit SCM_HALT:def 4 :

:: deftheorem Def5 defines is_halting_onInit SCM_HALT:def 5 :

theorem Th35: :: SCM_HALT:35

for b₁ being Macro-Instruction holds
( b₁ is InitClosed iff for b₂ being State of SCM+FSA holds b₁ is_closed_onInit b₂ )

proof end;

theorem Th36: :: SCM_HALT:36

for b₁ being Macro-Instruction holds
( b₁ is InitHalting iff for b₂ being State of SCM+FSA holds b₁ is_halting_onInit b₂ )

proof end;

theorem Th37: :: SCM_HALT:37

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being Int-Location st b₂ does_not_destroy b₃ & b₂ is_closed_onInit b₁ & Initialized b₂ c= b₁ holds
for b₄ being Nat holds ((Computation b₁) . b₄) . b₃ = b₁ . b₃

proof end;

registration

cluster non empty good InitClosed InitHalting FinPartState of SCM+FSA ;
existence

proof end;

end;

registration

cluster good InitClosed -> InitClosed keepInt0_1 FinPartState of SCM+FSA ;
correctness

proof end;

end;

registration

cluster SCM+FSA-Stop -> good InitClosed InitHalting keepInt0_1 ;
coherence ;

end;

theorem Th38: :: SCM_HALT:38

for b₁ being State of SCM+FSA
for b₂ being parahalting keeping_0 Instruction of SCM+FSA
for b₃ being InitHalting Macro-Instruction
for b₄ being Int-Location holds (IExec (b₂ ';' b₃),b₁) . b₄ = (IExec b₃,(Exec b₂,(Initialize b₁))) . b₄

proof end;

theorem Th39: :: SCM_HALT:39

for b₁ being State of SCM+FSA
for b₂ being parahalting keeping_0 Instruction of SCM+FSA
for b₃ being InitHalting Macro-Instruction
for b₄ being FinSeq-Location holds (IExec (b₂ ';' b₃),b₁) . b₄ = (IExec b₃,(Exec b₂,(Initialize b₁))) . b₄

proof end;

theorem Th40: :: SCM_HALT:40

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction holds
( b₂ is_closed_onInit b₁ iff b₂ is_closed_on Initialize b₁ )

proof end;

theorem Th41: :: SCM_HALT:41

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction holds
( b₂ is_halting_onInit b₁ iff b₂ is_halting_on Initialize b₁ )

proof end;

theorem Th42: :: SCM_HALT:42

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA holds IExec b₁,b₂ = IExec b₁,(Initialize b₂)

proof end;

theorem Th43: :: SCM_HALT:43

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ = 0 & b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
( if=0 b₄,b₂,b₃ is_closed_onInit b₁ & if=0 b₄,b₂,b₃ is_halting_onInit b₁ )

proof end;

theorem Th44: :: SCM_HALT:44

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ = 0 & b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
IExec (if=0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3)))

proof end;

theorem Th45: :: SCM_HALT:45

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ <> 0 & b₃ is_closed_onInit b₁ & b₃ is_halting_onInit b₁ holds
( if=0 b₄,b₂,b₃ is_closed_onInit b₁ & if=0 b₄,b₂,b₃ is_halting_onInit b₁ )

proof end;

theorem Th46: :: SCM_HALT:46

for b₁, b₂ being Macro-Instruction
for b₃ being read-write Int-Location
for b₄ being State of SCM+FSA st b₄ . b₃ <> 0 & b₂ is_closed_onInit b₄ & b₂ is_halting_onInit b₄ holds
IExec (if=0 b₃,b₁,b₂),b₄ = (IExec b₂,b₄) +* (Start-At (insloc (((card b₁) + (card b₂)) + 3)))

proof end;

theorem Th47: :: SCM_HALT:47

for b₁ being State of SCM+FSA
for b₂, b₃ being InitHalting Macro-Instruction
for b₄ being read-write Int-Location holds
( if=0 b₄,b₂,b₃ is InitHalting & ( b₁ . b₄ = 0 implies IExec (if=0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) & ( b₁ . b₄ <> 0 implies IExec (if=0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) )

proof end;

theorem Th48: :: SCM_HALT:48

for b₁ being State of SCM+FSA
for b₂, b₃ being InitHalting Macro-Instruction
for b₄ being read-write Int-Location holds
( IC (IExec (if=0 b₄,b₂,b₃),b₁) = insloc (((card b₂) + (card b₃)) + 3) & ( b₁ . b₄ = 0 implies ( ( for b₅ being Int-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) ) ) & ( b₁ . b₄ <> 0 implies ( ( for b₅ being Int-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) ) ) )

proof end;

theorem Th49: :: SCM_HALT:49

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ > 0 & b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
( if>0 b₄,b₂,b₃ is_closed_onInit b₁ & if>0 b₄,b₂,b₃ is_halting_onInit b₁ )

proof end;

theorem Th50: :: SCM_HALT:50

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ > 0 & b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
IExec (if>0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3)))

proof end;

theorem Th51: :: SCM_HALT:51

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ <= 0 & b₃ is_closed_onInit b₁ & b₃ is_halting_onInit b₁ holds
( if>0 b₄,b₂,b₃ is_closed_onInit b₁ & if>0 b₄,b₂,b₃ is_halting_onInit b₁ )

proof end;

theorem Th52: :: SCM_HALT:52

for b₁, b₂ being Macro-Instruction
for b₃ being read-write Int-Location
for b₄ being State of SCM+FSA st b₄ . b₃ <= 0 & b₂ is_closed_onInit b₄ & b₂ is_halting_onInit b₄ holds
IExec (if>0 b₃,b₁,b₂),b₄ = (IExec b₂,b₄) +* (Start-At (insloc (((card b₁) + (card b₂)) + 3)))

proof end;

theorem Th53: :: SCM_HALT:53

for b₁ being State of SCM+FSA
for b₂, b₃ being InitHalting Macro-Instruction
for b₄ being read-write Int-Location holds
( if>0 b₄,b₂,b₃ is InitHalting & ( b₁ . b₄ > 0 implies IExec (if>0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) & ( b₁ . b₄ <= 0 implies IExec (if>0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) )

proof end;

theorem Th54: :: SCM_HALT:54

for b₁ being State of SCM+FSA
for b₂, b₃ being InitHalting Macro-Instruction
for b₄ being read-write Int-Location holds
( IC (IExec (if>0 b₄,b₂,b₃),b₁) = insloc (((card b₂) + (card b₃)) + 3) & ( b₁ . b₄ > 0 implies ( ( for b₅ being Int-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) ) ) & ( b₁ . b₄ <= 0 implies ( ( for b₅ being Int-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) ) ) )

proof end;

theorem Th55: :: SCM_HALT:55

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ < 0 & b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7)))

proof end;

theorem Th56: :: SCM_HALT:56

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ = 0 & b₃ is_closed_onInit b₁ & b₃ is_halting_onInit b₁ holds
IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7)))

proof end;

theorem Th57: :: SCM_HALT:57

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ > 0 & b₃ is_closed_onInit b₁ & b₃ is_halting_onInit b₁ holds
IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7)))

proof end;

theorem Th58: :: SCM_HALT:58

for b₁ being State of SCM+FSA
for b₂, b₃ being InitHalting Macro-Instruction
for b₄ being read-write Int-Location holds
( if<0 b₄,b₂,b₃ is InitHalting & ( b₁ . b₄ < 0 implies IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7))) ) & ( b₁ . b₄ >= 0 implies IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7))) ) )

proof end;

registration

let c₂, c₃ be InitHalting Macro-Instruction;
let c₄ be read-write Int-Location ;
cluster if=0 a₃,a₁,a₂ -> non empty InitClosed InitHalting ;
correctness by Th47;
cluster if>0 a₃,a₁,a₂ -> non empty InitClosed InitHalting ;
correctness by Th53;
cluster if<0 a₃,a₁,a₂ -> non empty InitClosed InitHalting ;
correctness by Th58;

end;

theorem Th59: :: SCM_HALT:59

for b₁ being Macro-Instruction holds
( b₁ is InitHalting iff for b₂ being State of SCM+FSA holds b₁ is_halting_on Initialize b₂ )

proof end;

theorem Th60: :: SCM_HALT:60

for b₁ being Macro-Instruction holds
( b₁ is InitClosed iff for b₂ being State of SCM+FSA holds b₁ is_closed_on Initialize b₂ )

proof end;

theorem Th61: :: SCM_HALT:61

for b₁ being State of SCM+FSA
for b₂ being InitHalting Macro-Instruction
for b₃ being read-write Int-Location holds (IExec b₂,b₁) . b₃ = ((Computation ((Initialize b₁) +* (b₂ +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize b₁) +* (b₂ +* (Start-At (insloc 0)))))) . b₃

proof end;

theorem Th62: :: SCM_HALT:62

for b₁ being State of SCM+FSA
for b₂ being InitHalting Macro-Instruction
for b₃ being Int-Location
for b₄ being Nat st b₂ does_not_destroy b₃ holds
(IExec b₂,b₁) . b₃ = ((Computation ((Initialize b₁) +* (b₂ +* (Start-At (insloc 0))))) . b₄) . b₃

proof end;

set c₂ = the Instruction-Locations of SCM+FSA ;

set c₃ = Int-Locations \/ FinSeq-Locations ;

theorem Th63: :: SCM_HALT:63

for b₁ being State of SCM+FSA
for b₂ being InitHalting Macro-Instruction
for b₃ being Int-Location st b₂ does_not_destroy b₃ holds
(IExec b₂,b₁) . b₃ = (Initialize b₁) . b₃

proof end;

theorem Th64: :: SCM_HALT:64

for b₁ being State of SCM+FSA
for b₂ being InitHalting keepInt0_1 Macro-Instruction
for b₃ being read-write Int-Location st b₂ does_not_destroy b₃ holds
((Computation ((Initialize b₁) +* ((b₂ ';' (SubFrom b₃,(intloc 0))) +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize b₁) +* ((b₂ ';' (SubFrom b₃,(intloc 0))) +* (Start-At (insloc 0)))))) . b₃ = (b₁ . b₃) - 1

proof end;

theorem Th65: :: SCM_HALT:65

for b₁ being State of SCM+FSA
for b₂ being InitClosed Macro-Instruction st Initialized b₂ c= b₁ & b₁ is halting holds
for b₃ being Nat st b₃ <= LifeSpan b₁ holds
(Computation b₁) . b₃,(Computation (b₁ +* (loop b₂))) . b₃ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th66: :: SCM_HALT:66

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

proof end;

theorem Th67: :: SCM_HALT:67

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

proof end;

theorem Th68: :: SCM_HALT:68

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction st b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
for b₃ being Nat st b₃ <= LifeSpan (b₁ +* (Initialized b₂)) holds
(Computation (b₁ +* (Initialized b₂))) . b₃,(Computation (b₁ +* (Initialized (loop b₂)))) . b₃ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th69: :: SCM_HALT:69

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction st b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
for b₃ being Nat st b₃ < LifeSpan (b₁ +* (Initialized b₂)) holds
CurInstr ((Computation (b₁ +* (Initialized b₂))) . b₃) = CurInstr ((Computation (b₁ +* (Initialized (loop b₂)))) . b₃)

proof end;

theorem Th70: :: SCM_HALT:70

for b₁ being Instruction-Location of SCM+FSA holds not b₁ in dom (((intloc 0) .--> 1) +* (Start-At (insloc 0)))

proof end;

theorem Th71: :: SCM_HALT:71

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction st b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
( CurInstr ((Computation (b₁ +* (Initialized (loop b₂)))) . (LifeSpan (b₁ +* (Initialized b₂)))) = goto (insloc 0) & ( for b₃ being Nat st b₃ <= LifeSpan (b₁ +* (Initialized b₂)) holds
CurInstr ((Computation (b₁ +* (Initialized (loop b₂)))) . b₃) <> halt SCM+FSA ) )

proof end;

theorem Th72: :: SCM_HALT:72

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction st b₂ is_closed_onInit b₁ & b₂ is_halting_onInit b₁ holds
CurInstr ((Computation (b₁ +* (Initialized (loop b₂)))) . (LifeSpan (b₁ +* (Initialized b₂)))) = goto (insloc 0) by Th71;

theorem Th73: :: SCM_HALT:73

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being read-write Int-Location st b₂ does_not_destroy b₃ & b₁ . (intloc 0) = 1 & b₁ . b₃ > 0 holds
loop (if=0 b₃,(Goto (insloc 2)),(b₂ ';' (SubFrom b₃,(intloc 0)))) is_pseudo-closed_on b₁

proof end;

theorem Th74: :: SCM_HALT:74

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being read-write Int-Location st b₂ does_not_destroy b₃ & b₁ . b₃ > 0 holds
Initialized (loop (if=0 b₃,(Goto (insloc 2)),(b₂ ';' (SubFrom b₃,(intloc 0))))) is_pseudo-closed_on b₁

proof end;

theorem Th75: :: SCM_HALT:75

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being read-write Int-Location st b₂ does_not_destroy b₃ & b₁ . (intloc 0) = 1 holds
( Times b₃,b₂ is_closed_on b₁ & Times b₃,b₂ is_halting_on b₁ )

proof end;

theorem Th76: :: SCM_HALT:76

for b₁ being good InitHalting Macro-Instruction
for b₂ being read-write Int-Location st b₁ does_not_destroy b₂ holds
Initialized (Times b₂,b₁) is halting

proof end;

registration

let c₄ be read-write Int-Location ;
let c₅ be good Macro-Instruction;
cluster Times a₁,a₂ -> good ;
coherence

proof end;

end;

theorem Th77: :: SCM_HALT:77

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being read-write Int-Location st b₂ does_not_destroy b₃ & b₁ . b₃ > 0 holds
ex b₄ being State of SCM+FSA ex b₅ being Nat st
( b₄ = b₁ +* (Initialized (loop (if=0 b₃,(Goto (insloc 2)),(b₂ ';' (SubFrom b₃,(intloc 0)))))) & b₅ = (LifeSpan (b₁ +* (Initialized (if=0 b₃,(Goto (insloc 2)),(b₂ ';' (SubFrom b₃,(intloc 0))))))) + 1 & ((Computation b₄) . b₅) . b₃ = (b₁ . b₃) - 1 & ((Computation b₄) . b₅) . (intloc 0) = 1 & ( for b₆ being read-write Int-Location st b₆ <> b₃ holds
((Computation b₄) . b₅) . b₆ = (IExec b₂,b₁) . b₆ ) & ( for b₆ being FinSeq-Location holds ((Computation b₄) . b₅) . b₆ = (IExec b₂,b₁) . b₆ ) & IC ((Computation b₄) . b₅) = insloc 0 & ( for b₆ being Nat st b₆ <= b₅ holds
IC ((Computation b₄) . b₆) in dom (loop (if=0 b₃,(Goto (insloc 2)),(b₂ ';' (SubFrom b₃,(intloc 0))))) ) )

proof end;

theorem Th78: :: SCM_HALT:78

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being read-write Int-Location st b₁ . (intloc 0) = 1 & b₁ . b₃ <= 0 holds
(IExec (Times b₃,b₂),b₁) | (Int-Locations \/ FinSeq-Locations ) = b₁ | (Int-Locations \/ FinSeq-Locations )

proof end;

Lemma71: for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA
for b₃ being Instruction of SCM+FSA st ( b₃ = b₁ =0_goto b₂ or b₃ = goto b₂ ) holds
b₃ <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:124;

theorem Th79: :: SCM_HALT:79

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being read-write Int-Location st b₂ does_not_destroy b₃ & b₁ . b₃ > 0 holds
( (IExec (b₂ ';' (SubFrom b₃,(intloc 0))),b₁) . b₃ = (b₁ . b₃) - 1 & (IExec (Times b₃,b₂),b₁) | (Int-Locations \/ FinSeq-Locations ) = (IExec (Times b₃,b₂),(IExec (b₂ ';' (SubFrom b₃,(intloc 0))),b₁)) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th80: :: SCM_HALT:80

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being FinSeq-Location
for b₄ being read-write Int-Location st b₁ . b₄ <= 0 holds
(IExec (Times b₄,b₂),b₁) . b₃ = b₁ . b₃

proof end;

theorem Th81: :: SCM_HALT:81

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being Int-Location
for b₄ being read-write Int-Location st b₁ . b₄ <= 0 holds
(IExec (Times b₄,b₂),b₁) . b₃ = (Initialize b₁) . b₃

proof end;

theorem Th82: :: SCM_HALT:82

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being FinSeq-Location
for b₄ being read-write Int-Location st b₂ does_not_destroy b₄ & b₁ . b₄ > 0 holds
(IExec (Times b₄,b₂),b₁) . b₃ = (IExec (Times b₄,b₂),(IExec (b₂ ';' (SubFrom b₄,(intloc 0))),b₁)) . b₃

proof end;

theorem Th83: :: SCM_HALT:83

for b₁ being State of SCM+FSA
for b₂ being good InitHalting Macro-Instruction
for b₃ being Int-Location
for b₄ being read-write Int-Location st b₂ does_not_destroy b₄ & b₁ . b₄ > 0 holds
(IExec (Times b₄,b₂),b₁) . b₃ = (IExec (Times b₄,b₂),(IExec (b₂ ';' (SubFrom b₄,(intloc 0))),b₁)) . b₃

proof end;

definition

let c₄ be Instruction of SCM+FSA ;
attr a₁ is good means :Def6: :: SCM_HALT:def 6
a₁ does_not_destroy intloc 0;

end;

:: deftheorem Def6 defines good SCM_HALT:def 6 :

registration

cluster parahalting good M3(the Instructions of SCM+FSA );
existence

proof end;

end;

registration

let c₄ be good Instruction of SCM+FSA ;
let c₅ be good Macro-Instruction;
cluster a₁ ';' a₂ -> good ;
coherence

proof end;

cluster a₂ ';' a₁ -> good ;
coherence

proof end;

end;

registration

let c₄, c₅ be good Instruction of SCM+FSA ;
cluster a₁ ';' a₂ -> good ;
coherence

proof end;

end;

registration

let c₄ be read-write Int-Location ;
let c₅ be Int-Location ;
cluster a₁ := a₂ -> good ;
coherence

proof end;

cluster SubFrom a₁,a₂ -> good ;
coherence

proof end;

end;

registration

let c₄ be read-write Int-Location ;
let c₅ be Int-Location ;
let c₆ be FinSeq-Location ;
cluster a₁ := a₃,a₂ -> good ;
coherence

proof end;

end;

registration

let c₄, c₅ be Int-Location ;
let c₆ be FinSeq-Location ;
cluster a₃,a₁ := a₂ -> good ;
coherence

proof end;

end;

registration

let c₄ be read-write Int-Location ;
let c₅ be FinSeq-Location ;
cluster a₁ :=len a₂ -> good ;
coherence

proof end;

end;

registration

let c₄ be Nat;
cluster intloc (a₁ + 1) -> read-write ;
coherence

proof end;

end;