:: SCMFSA6B semantic presentation

theorem :: SCMFSA6B:1

canceled;

theorem :: SCMFSA6B:2

canceled;

theorem :: SCMFSA6B:3

for f, g being Function
for A being set st A /\ (dom f) c= A /\ (dom g) holds
(f +* (g | A)) | A = g | A

proof end;

theorem Th4: :: SCMFSA6B:4

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

proof end;

theorem Th5: :: SCMFSA6B:5

for n being Nat
for I being Macro-Instruction
for s being State of SCM+FSA st I +* (Start-At (insloc n)) c= s holds
I c= s

proof end;

theorem Th6: :: SCMFSA6B:6

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

proof end;

theorem Th7: :: SCMFSA6B:7

for n being Nat
for x being set
for I being Macro-Instruction st x in dom I holds
I . x = (I +* (Start-At (insloc n))) . x

proof end;

theorem Th8: :: SCMFSA6B:8

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

proof end;

theorem Th9: :: SCMFSA6B:9

for a being Int-Location
for l being Instruction-Location of SCM+FSA holds not a in dom (Start-At l)

proof end;

theorem Th10: :: SCMFSA6B:10

for f being FinSeq-Location
for l being Instruction-Location of SCM+FSA holds not f in dom (Start-At l)

proof end;

theorem :: SCMFSA6B:11

for l1, l being Instruction-Location of SCM+FSA holds not l1 in dom (Start-At l)

proof end;

theorem Th12: :: SCMFSA6B:12

for I being Macro-Instruction
for a being Int-Location
for l being Instruction-Location of SCM+FSA holds not a in dom (I +* (Start-At l))

proof end;

theorem Th13: :: SCMFSA6B:13

for I being Macro-Instruction
for f being FinSeq-Location
for l being Instruction-Location of SCM+FSA holds not f in dom (I +* (Start-At l))

proof end;

theorem Th14: :: SCMFSA6B:14

for I being Macro-Instruction
for s being State of SCM+FSA holds (s +* I) +* (Start-At (insloc 0)) = (s +* (Start-At (insloc 0))) +* I

proof end;

theorem :: SCMFSA6B:15

for s being State of SCM+FSA st s = Following s holds
for n being Nat holds (Computation s) . n = s

proof end;

theorem Th16: :: SCMFSA6B:16

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

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty non void IC-Ins-separated definite AMI-Struct of N;
let s be State of S;
let l be Instruction-Location of S;
let i be Instruction of S;
:: original: +*
redefine func s +* l,i -> State of S;
coherence

proof end;

end;

definition

let s be State of SCM+FSA ;
let li be Int-Location ;
let k be Integer;
:: original: +*
redefine func s +* li,k -> State of SCM+FSA ;
coherence

proof end;

end;

theorem Th17: :: SCMFSA6B:17

for N being non empty with_non-empty_elements set
for S being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for n being Nat holds s | the Instruction-Locations of S = ((Computation s) . n) | the Instruction-Locations of S

proof end;

definition

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

end;

:: deftheorem defines IExec SCMFSA6B:def 1 :

definition

let I be Macro-Instruction;
attr I is paraclosed means :Def2: :: SCMFSA6B:def 2
for s being State of SCM+FSA
for n being Nat st I +* (Start-At (insloc 0)) c= s holds
IC ((Computation s) . n) in dom I;
attr I is parahalting means :Def3: :: SCMFSA6B:def 3
I +* (Start-At (insloc 0)) is halting;
attr I is keeping_0 means :Def4: :: SCMFSA6B:def 4
for s being State of SCM+FSA st I +* (Start-At (insloc 0)) c= s holds
for k being Nat holds ((Computation s) . k) . (intloc 0) = s . (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 :

Lm1: Macro (halt SCM+FSA ) is parahalting

proof end;

registration

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

end;

theorem Th18: :: SCMFSA6B:18

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

proof end;

theorem Th19: :: SCMFSA6B:19

for s being State of SCM+FSA
for I being parahalting Macro-Instruction st Initialized I c= s holds
s is halting

proof end;

registration

let I be parahalting Macro-Instruction;
cluster Initialized I -> halting ;
coherence

proof end;

end;

theorem Th20: :: SCMFSA6B:20

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

proof end;

theorem Th21: :: SCMFSA6B:21

for n being Nat
for I being Macro-Instruction
for s1, s2 being State of SCM+FSA st s1,s2 equal_outside the Instruction-Locations of SCM+FSA & I c= s1 & I c= s2 & ( for m being Nat st m < n holds
IC ((Computation s2) . m) in dom I ) holds
for m being Nat st m <= n holds
(Computation s1) . m,(Computation s2) . m 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 :: SCMFSA6B:22

for s being State of SCM+FSA
for I being parahalting Macro-Instruction
for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec I,s) . a = s . a

proof end;

theorem :: SCMFSA6B:23

for f being FinSeq-Location
for s being State of SCM+FSA
for I being parahalting Macro-Instruction st not f in UsedInt*Loc I holds
(IExec I,s) . f = s . f

proof end;

theorem Th24: :: SCMFSA6B:24

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

proof end;

registration

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

proof end;

end;

theorem Th25: :: SCMFSA6B:25

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

proof end;

theorem Th26: :: SCMFSA6B:26

for I being parahalting Macro-Instruction holds insloc 0 in dom I

proof end;

theorem Th27: :: SCMFSA6B:27

for s1, s2 being State of SCM+FSA
for J being parahalting Macro-Instruction st J +* (Start-At (insloc 0)) c= s1 holds
for n being Nat st ProgramPart (Relocated J,n) c= s2 & IC s2 = insloc n & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
for i being Nat holds
( (IC ((Computation s1) . i)) + n = IC ((Computation s2) . i) & IncAddr (CurInstr ((Computation s1) . i)),n = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | (Int-Locations \/ FinSeq-Locations ) = ((Computation s2) . i) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th28: :: SCMFSA6B:28

for s1, s2 being State of SCM+FSA
for I being parahalting Macro-Instruction st I +* (Start-At (insloc 0)) c= s1 & I +* (Start-At (insloc 0)) c= s2 & s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
for k being Nat holds
( (Computation s1) . k,(Computation s2) . k equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation s1) . k) = CurInstr ((Computation s2) . k) )

proof end;

theorem Th29: :: SCMFSA6B:29

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

proof end;

theorem Th30: :: SCMFSA6B:30

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

proof end;

theorem Th31: :: SCMFSA6B:31

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

proof end;

theorem Th32: :: SCMFSA6B:32

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

proof end;

theorem Th33: :: SCMFSA6B:33

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

proof end;

theorem :: SCMFSA6B:34

for I being Macro-Instruction
for s being State of SCM+FSA st Initialized I c= s holds
IC s = insloc 0

proof end;

Lm2: ( 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 Lm2;

end;

theorem :: SCMFSA6B:35

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

proof end;

theorem Th36: :: SCMFSA6B:36

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

proof end;

theorem Th37: :: SCMFSA6B:37

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

proof end;

theorem Th38: :: SCMFSA6B:38

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

proof end;

theorem Th39: :: SCMFSA6B:39

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

proof end;

theorem Th40: :: SCMFSA6B:40

for s being State of SCM+FSA
for I being paraclosed Macro-Instruction st s +* (I +* (Start-At (insloc 0))) is halting holds
for J being Macro-Instruction
for k being Nat st k <= LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
(Computation (s +* (I +* (Start-At (insloc 0))))) . k,(Computation (s +* ((I ';' J) +* (Start-At (insloc 0))))) . k equal_outside the Instruction-Locations of SCM+FSA

proof end;

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

proof end;

registration

let I, J be parahalting Macro-Instruction;
cluster I ';' J -> non empty paraclosed parahalting ;
coherence

proof end;

end;

theorem Th41: :: SCMFSA6B:41

for s being State of SCM+FSA
for I being keeping_0 Macro-Instruction st not s +* (I +* (Start-At (insloc 0))) is halting holds
for J being Macro-Instruction
for k being Nat holds (Computation (s +* (I +* (Start-At (insloc 0))))) . k,(Computation (s +* ((I ';' J) +* (Start-At (insloc 0))))) . k equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th42: :: SCMFSA6B:42

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

proof end;

registration

let I, J be keeping_0 Macro-Instruction;
cluster I ';' J -> paraclosed keeping_0 ;
coherence

proof end;

end;

theorem Th43: :: SCMFSA6B:43

for s being State of SCM+FSA
for I being parahalting keeping_0 Macro-Instruction
for J being parahalting Macro-Instruction holds LifeSpan (s +* (Initialized (I ';' J))) = ((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Result (s +* (Initialized I))) +* (Initialized J)))

proof end;

theorem :: SCMFSA6B:44

for s being State of SCM+FSA
for I being parahalting keeping_0 Macro-Instruction
for J being parahalting Macro-Instruction holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))

proof end;