:: SCMFSA8B semantic presentation

set A = the Instruction-Locations of SCM+FSA ;

set D = Int-Locations \/ FinSeq-Locations ;

Lm1: for l being Instruction-Location of SCM+FSA holds goto l <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:124;

Lm2: for a being Int-Location
for l being Instruction-Location of SCM+FSA holds a =0_goto l <> halt SCM+FSA
by SCMFSA_2:48, SCMFSA_2:124;

Lm3: for a being Int-Location
for l being Instruction-Location of SCM+FSA holds a >0_goto l <> halt SCM+FSA
by SCMFSA_2:49, SCMFSA_2:124;

Lm4: for I, J being Macro-Instruction holds ProgramPart (Relocated J,(card I)) c= I ';' J

proof end;

theorem Th1: :: SCMFSA8B:1

for s being State of SCM+FSA holds IC SCM+FSA in dom s

proof end;

theorem Th2: :: SCMFSA8B:2

for s being State of SCM+FSA
for l being Instruction-Location of SCM+FSA holds l in dom s

proof end;

theorem Th3: :: SCMFSA8B:3

for I being Macro-Instruction
for s being State of SCM+FSA st I is_closed_on s holds
insloc 0 in dom I

proof end;

theorem Th4: :: SCMFSA8B:4

for s being State of SCM+FSA
for l1, l2 being Instruction-Location of SCM+FSA holds (s +* (Start-At l1)) +* (Start-At l2) = s +* (Start-At l2)

proof end;

theorem Th5: :: SCMFSA8B:5

for s being State of SCM+FSA
for I being Macro-Instruction holds (Initialize s) | (Int-Locations \/ FinSeq-Locations ) = (s +* (Initialized I)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th6: :: SCMFSA8B:6

for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) & I is_closed_on s1 holds
I is_closed_on s2

proof end;

theorem Th7: :: SCMFSA8B:7

for s1, s2 being State of SCM+FSA
for I, J being Macro-Instruction st s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
s1 +* (I +* (Start-At (insloc 0))),s2 +* (J +* (Start-At (insloc 0))) equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th8: :: SCMFSA8B:8

for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) & I is_closed_on s1 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )

proof end;

theorem Th9: :: SCMFSA8B:9

for s being State of SCM+FSA
for I, J being Macro-Instruction holds
( I is_closed_on Initialize s iff I is_closed_on s +* (Initialized J) )

proof end;

theorem Th10: :: SCMFSA8B:10

for s being State of SCM+FSA
for I, J being Macro-Instruction
for l being Instruction-Location of SCM+FSA holds
( I is_closed_on s iff I is_closed_on s +* (I +* (Start-At l)) )

proof end;

theorem Th11: :: SCMFSA8B:11

for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I +* (Start-At (insloc 0)) c= s1 & I is_closed_on s1 holds
for n being Nat st ProgramPart (Relocated I,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 Th12: :: SCMFSA8B:12

for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being parahalting Macro-Instruction
for a being Int-Location holds (IExec (i ';' J),s) . a = (IExec J,(Exec i,(Initialize s))) . a

proof end;

theorem Th13: :: SCMFSA8B:13

for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being parahalting Macro-Instruction
for f being FinSeq-Location holds (IExec (i ';' J),s) . f = (IExec J,(Exec i,(Initialize s))) . f

proof end;

definition

let a be Int-Location ;
let I, J be Macro-Instruction;
func if=0 a,I,J -> Macro-Instruction equals :: SCMFSA8B:def 1
((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' SCM+FSA-Stop ;
coherence ;
func if>0 a,I,J -> Macro-Instruction equals :: SCMFSA8B:def 2
((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' SCM+FSA-Stop ;
coherence ;

end;

:: deftheorem defines if=0 SCMFSA8B:def 1 :

:: deftheorem defines if>0 SCMFSA8B:def 2 :

definition

let a be Int-Location ;
let I, J be Macro-Instruction;
func if<0 a,I,J -> Macro-Instruction equals :: SCMFSA8B:def 3
if=0 a,J,(if>0 a,J,I);
coherence ;

end;

:: deftheorem defines if<0 SCMFSA8B:def 3 :

Lm5: for a being Int-Location
for I, J being Macro-Instruction holds
( insloc 0 in dom (if=0 a,I,J) & insloc 1 in dom (if=0 a,I,J) & insloc 0 in dom (if>0 a,I,J) & insloc 1 in dom (if>0 a,I,J) )

proof end;

Lm6: for a being Int-Location
for I, J being Macro-Instruction holds
( (if=0 a,I,J) . (insloc 0) = a =0_goto (insloc ((card J) + 3)) & (if=0 a,I,J) . (insloc 1) = goto (insloc 2) & (if>0 a,I,J) . (insloc 0) = a >0_goto (insloc ((card J) + 3)) & (if>0 a,I,J) . (insloc 1) = goto (insloc 2) )

proof end;

theorem Th14: :: SCMFSA8B:14

for I, J being Macro-Instruction
for a being Int-Location holds card (if=0 a,I,J) = ((card I) + (card J)) + 4

proof end;

theorem Th15: :: SCMFSA8B:15

for I, J being Macro-Instruction
for a being Int-Location holds card (if>0 a,I,J) = ((card I) + (card J)) + 4

proof end;

theorem Th16: :: SCMFSA8B:16

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a = 0 & I is_closed_on s & I is_halting_on s holds
( if=0 a,I,J is_closed_on s & if=0 a,I,J is_halting_on s )

proof end;

theorem Th17: :: SCMFSA8B:17

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a = 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (if=0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th18: :: SCMFSA8B:18

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a <> 0 & J is_closed_on s & J is_halting_on s holds
( if=0 a,I,J is_closed_on s & if=0 a,I,J is_halting_on s )

proof end;

theorem Th19: :: SCMFSA8B:19

for I, J being Macro-Instruction
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <> 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if=0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th20: :: SCMFSA8B:20

for s being State of SCM+FSA
for I, J being parahalting Macro-Instruction
for a being read-write Int-Location holds
( if=0 a,I,J is parahalting & ( s . a = 0 implies IExec (if=0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & ( s . a <> 0 implies IExec (if=0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )

proof end;

theorem Th21: :: SCMFSA8B:21

for s being State of SCM+FSA
for I, J being parahalting Macro-Instruction
for a being read-write Int-Location holds
( IC (IExec (if=0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec (if=0 a,I,J),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if=0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec (if=0 a,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if=0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )

proof end;

theorem Th22: :: SCMFSA8B:22

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a > 0 & I is_closed_on s & I is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )

proof end;

theorem Th23: :: SCMFSA8B:23

for I, J being Macro-Instruction
for a being read-write Int-Location
for s being State of SCM+FSA st s . a > 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (if>0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th24: :: SCMFSA8B:24

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a <= 0 & J is_closed_on s & J is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )

proof end;

theorem Th25: :: SCMFSA8B:25

for I, J being Macro-Instruction
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <= 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th26: :: SCMFSA8B:26

for s being State of SCM+FSA
for I, J being parahalting Macro-Instruction
for a being read-write Int-Location holds
( if>0 a,I,J is parahalting & ( s . a > 0 implies IExec (if>0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & ( s . a <= 0 implies IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )

proof end;

theorem Th27: :: SCMFSA8B:27

for s being State of SCM+FSA
for I, J being parahalting Macro-Instruction
for a being read-write Int-Location holds
( IC (IExec (if>0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & ( s . a > 0 implies ( ( for d being Int-Location holds (IExec (if>0 a,I,J),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <= 0 implies ( ( for d being Int-Location holds (IExec (if>0 a,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )

proof end;

theorem :: SCMFSA8B:28

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a < 0 & I is_closed_on s & I is_halting_on s holds
( if<0 a,I,J is_closed_on s & if<0 a,I,J is_halting_on s )

proof end;

theorem Th29: :: SCMFSA8B:29

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a < 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem :: SCMFSA8B:30

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a = 0 & J is_closed_on s & J is_halting_on s holds
( if<0 a,I,J is_closed_on s & if<0 a,I,J is_halting_on s ) by Th16;

theorem Th31: :: SCMFSA8B:31

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a = 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem :: SCMFSA8B:32

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a > 0 & J is_closed_on s & J is_halting_on s holds
( if<0 a,I,J is_closed_on s & if<0 a,I,J is_halting_on s )

proof end;

theorem Th33: :: SCMFSA8B:33

for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a > 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem :: SCMFSA8B:34

for s being State of SCM+FSA
for I, J being parahalting Macro-Instruction
for a being read-write Int-Location holds
( if<0 a,I,J is parahalting & ( s . a < 0 implies IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) & ( s . a >= 0 implies IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) )

proof end;

registration

let I, J be parahalting Macro-Instruction;
let a be read-write Int-Location ;
cluster if=0 a,I,J -> parahalting ;
correctness by Th20;
cluster if>0 a,I,J -> parahalting ;
correctness by Th26;

end;

definition

let a, b be Int-Location ;
let I, J be Macro-Instruction;
func if=0 a,b,I,J -> Macro-Instruction equals :: SCMFSA8B:def 4
(SubFrom a,b) ';' (if=0 a,I,J);
coherence ;
func if>0 a,b,I,J -> Macro-Instruction equals :: SCMFSA8B:def 5
(SubFrom a,b) ';' (if>0 a,I,J);
coherence ;

end;

:: deftheorem defines if=0 SCMFSA8B:def 4 :

:: deftheorem defines if>0 SCMFSA8B:def 5 :

notation

let a, b be Int-Location ;
let I, J be Macro-Instruction;
synonym if<0 b,a,I,J for if>0 a,b,I,J;

end;

registration

let I, J be parahalting Macro-Instruction;
let a, b be read-write Int-Location ;
cluster if=0 a,b,I,J -> parahalting ;
correctness ;
cluster if>0 a,b,I,J -> parahalting ;
correctness ;

end;

theorem Th35: :: SCMFSA8B:35

for s being State of SCM+FSA
for I being Macro-Instruction holds (Result (s +* (Initialized I))) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,s) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th36: :: SCMFSA8B:36

for s being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location holds Result (s +* (Initialized I)), IExec I,s equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th37: :: SCMFSA8B:37

for s1, s2 being State of SCM+FSA
for i being Instruction of SCM+FSA
for a being Int-Location st ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & i does_not_refer a & IC s1 = IC s2 holds
( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) )

proof end;

theorem Th38: :: SCMFSA8B:38

for s1, s2 being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 holds
for k being Nat holds
( ( for b being Int-Location st a <> b holds
((Computation (s1 +* (I +* (Start-At (insloc 0))))) . k) . b = ((Computation (s2 +* (I +* (Start-At (insloc 0))))) . k) . b ) & ( for f being FinSeq-Location holds ((Computation (s1 +* (I +* (Start-At (insloc 0))))) . k) . f = ((Computation (s2 +* (I +* (Start-At (insloc 0))))) . k) . f ) & IC ((Computation (s1 +* (I +* (Start-At (insloc 0))))) . k) = IC ((Computation (s2 +* (I +* (Start-At (insloc 0))))) . k) & CurInstr ((Computation (s1 +* (I +* (Start-At (insloc 0))))) . k) = CurInstr ((Computation (s2 +* (I +* (Start-At (insloc 0))))) . k) )

proof end;

theorem Th39: :: SCMFSA8B:39

for s being State of SCM+FSA
for I, J being Macro-Instruction
for l being Instruction-Location of SCM+FSA holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on s +* (I +* (Start-At l)) & I is_halting_on s +* (I +* (Start-At l)) ) )

proof end;

theorem Th40: :: SCMFSA8B:40

proof end;

theorem Th41: :: SCMFSA8B:41

for s1, s2 being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location st ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I does_not_refer a & I is_closed_on Initialize s1 & I is_halting_on Initialize s1 holds
( ( for d being Int-Location st a <> d holds
(IExec I,s1) . d = (IExec I,s2) . d ) & ( for f being FinSeq-Location holds (IExec I,s1) . f = (IExec I,s2) . f ) & IC (IExec I,s1) = IC (IExec I,s2) )

proof end;

theorem :: SCMFSA8B:42

for s being State of SCM+FSA
for I, J being parahalting Macro-Instruction
for a, b being read-write Int-Location st I does_not_refer a & J does_not_refer a holds
( IC (IExec (if=0 a,b,I,J),s) = insloc (((card I) + (card J)) + 5) & ( s . a = s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if=0 a,b,I,J),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if=0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <> s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if=0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if=0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )

proof end;

theorem :: SCMFSA8B:43

for s being State of SCM+FSA
for I, J being parahalting Macro-Instruction
for a, b being read-write Int-Location st I does_not_refer a & J does_not_refer a holds
( IC (IExec (if>0 a,b,I,J),s) = insloc (((card I) + (card J)) + 5) & ( s . a > s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )

proof end;