:: SCMFSA_3 semantic presentation

theorem Th1: :: SCMFSA_3:1
not IC SCM+FSA in Int-Locations
proof end;

theorem Th2: :: SCMFSA_3:2
not IC SCM+FSA in FinSeq-Locations
proof end;

theorem Th3: :: SCMFSA_3:3
for b1 being Instruction of SCM+FSA
for b2 being Instruction of SCM st b1 = b2 holds
for b3 being State of SCM+FSA
for b4 being State of SCM st b4 = (b3 | the carrier of SCM ) +* (the Instruction-Locations of SCM --> b2) holds
Exec b1,b3 = (b3 +* (Exec b2,b4)) +* (b3 | the Instruction-Locations of SCM+FSA ) by AMI_3:def 1, SCMFSA_2:75, SCMFSA_2:def 1;

theorem Th4: :: SCMFSA_3:4
for b1, b2 being State of SCM+FSA st b1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = b2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) holds
for b3 being Instruction of SCM+FSA holds (Exec b3,b1) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = (Exec b3,b2) | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )})
proof end;

theorem Th5: :: SCMFSA_3:5
for b1 being with_non-empty_elements set
for b2 being non empty non void steady-programmed AMI-Struct of b1
for b3 being Instruction of b2
for b4 being State of b2 holds (Exec b3,b4) | the Instruction-Locations of b2 = b4 | the Instruction-Locations of b2
proof end;

theorem Th6: :: SCMFSA_3:6
for b1 being FinPartState of SCM+FSA holds DataPart b1 = b1 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th7: :: SCMFSA_3:7
for b1 being FinPartState of SCM+FSA holds
( b1 is data-only iff dom b1 c= Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th8: :: SCMFSA_3:8
for b1 being FinPartState of SCM+FSA holds dom (DataPart b1) c= Int-Locations \/ FinSeq-Locations
proof end;

theorem Th9: :: SCMFSA_3:9
canceled;

theorem Th10: :: SCMFSA_3:10
for b1 being Instruction of SCM+FSA
for b2 being State of SCM+FSA
for b3 being programmed FinPartState of SCM+FSA holds Exec b1,(b2 +* b3) = (Exec b1,b2) +* b3
proof end;

theorem Th11: :: SCMFSA_3:11
for b1 being State of SCM+FSA
for b2 being Instruction-Location of SCM+FSA
for b3 being Int-Location holds b1 . b3 = (b1 +* (Start-At b2)) . b3
proof end;

theorem Th12: :: SCMFSA_3:12
for b1 being State of SCM+FSA
for b2 being Instruction-Location of SCM+FSA
for b3 being FinSeq-Location holds b1 . b3 = (b1 +* (Start-At b2)) . b3
proof end;

theorem Th13: :: SCMFSA_3:13
for b1, b2 being State of SCM+FSA holds b1 +* (b2 | (Int-Locations \/ FinSeq-Locations )) is State of SCM+FSA
proof end;

definition
let c1 be Int-Location ;
let c2 be Integer;
redefine func .--> as c1 .--> c2 -> FinPartState of SCM+FSA ;
coherence
c1 .--> c2 is FinPartState of SCM+FSA
proof end;
end;

theorem Th14: :: SCMFSA_3:14
for b1 being autonomic FinPartState of SCM+FSA st DataPart b1 <> {} holds
IC SCM+FSA in dom b1
proof end;

registration
cluster autonomic non programmed FinPartState of SCM+FSA ;
existence
ex b1 being FinPartState of SCM+FSA st
( b1 is autonomic & not b1 is programmed )
proof end;
end;

theorem Th15: :: SCMFSA_3:15
for b1 being autonomic non programmed FinPartState of SCM+FSA holds IC SCM+FSA in dom b1
proof end;

theorem Th16: :: SCMFSA_3:16
for b1 being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom b1 holds
IC b1 in dom b1
proof end;

theorem Th17: :: SCMFSA_3:17
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2 being State of SCM+FSA st b1 c= b2 holds
for b3 being Nat holds IC ((Computation b2) . b3) in dom (ProgramPart b1)
proof end;

theorem Th18: :: SCMFSA_3:18
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat holds
( IC ((Computation b2) . b4) = IC ((Computation b3) . b4) & CurInstr ((Computation b2) . b4) = CurInstr ((Computation b3) . b4) )
proof end;

theorem Th19: :: SCMFSA_3:19
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location st CurInstr ((Computation b2) . b4) = b5 := b6 & b5 in dom b1 holds
((Computation b2) . b4) . b6 = ((Computation b3) . b4) . b6
proof end;

theorem Th20: :: SCMFSA_3:20
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location st CurInstr ((Computation b2) . b4) = AddTo b5,b6 & b5 in dom b1 holds
(((Computation b2) . b4) . b5) + (((Computation b2) . b4) . b6) = (((Computation b3) . b4) . b5) + (((Computation b3) . b4) . b6)
proof end;

theorem Th21: :: SCMFSA_3:21
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location st CurInstr ((Computation b2) . b4) = SubFrom b5,b6 & b5 in dom b1 holds
(((Computation b2) . b4) . b5) - (((Computation b2) . b4) . b6) = (((Computation b3) . b4) . b5) - (((Computation b3) . b4) . b6)
proof end;

theorem Th22: :: SCMFSA_3:22
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location st CurInstr ((Computation b2) . b4) = MultBy b5,b6 & b5 in dom b1 holds
(((Computation b2) . b4) . b5) * (((Computation b2) . b4) . b6) = (((Computation b3) . b4) . b5) * (((Computation b3) . b4) . b6)
proof end;

theorem Th23: :: SCMFSA_3:23
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location st CurInstr ((Computation b2) . b4) = Divide b5,b6 & b5 in dom b1 & b5 <> b6 holds
(((Computation b2) . b4) . b5) div (((Computation b2) . b4) . b6) = (((Computation b3) . b4) . b5) div (((Computation b3) . b4) . b6)
proof end;

theorem Th24: :: SCMFSA_3:24
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location st CurInstr ((Computation b2) . b4) = Divide b5,b6 & b6 in dom b1 & b5 <> b6 holds
(((Computation b2) . b4) . b5) mod (((Computation b2) . b4) . b6) = (((Computation b3) . b4) . b5) mod (((Computation b3) . b4) . b6)
proof end;

theorem Th25: :: SCMFSA_3:25
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5 being Int-Location
for b6 being Instruction-Location of SCM+FSA st CurInstr ((Computation b2) . b4) = b5 =0_goto b6 & b6 <> Next (IC ((Computation b2) . b4)) holds
( ((Computation b2) . b4) . b5 = 0 iff ((Computation b3) . b4) . b5 = 0 )
proof end;

theorem Th26: :: SCMFSA_3:26
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5 being Int-Location
for b6 being Instruction-Location of SCM+FSA st CurInstr ((Computation b2) . b4) = b5 >0_goto b6 & b6 <> Next (IC ((Computation b2) . b4)) holds
( ((Computation b2) . b4) . b5 > 0 iff ((Computation b3) . b4) . b5 > 0 )
proof end;

theorem Th27: :: SCMFSA_3:27
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location
for b7 being FinSeq-Location st CurInstr ((Computation b2) . b4) = b5 := b7,b6 & b5 in dom b1 holds
for b8, b9 being Nat st b8 = abs (((Computation b2) . b4) . b6) & b9 = abs (((Computation b3) . b4) . b6) holds
(((Computation b2) . b4) . b7) /. b8 = (((Computation b3) . b4) . b7) /. b9
proof end;

theorem Th28: :: SCMFSA_3:28
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Int-Location
for b7 being FinSeq-Location st CurInstr ((Computation b2) . b4) = b7,b6 := b5 & b7 in dom b1 holds
for b8, b9 being Nat st b8 = abs (((Computation b2) . b4) . b6) & b9 = abs (((Computation b3) . b4) . b6) holds
(((Computation b2) . b4) . b7) +* b8,(((Computation b2) . b4) . b5) = (((Computation b3) . b4) . b7) +* b9,(((Computation b3) . b4) . b5)
proof end;

theorem Th29: :: SCMFSA_3:29
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5 being Int-Location
for b6 being FinSeq-Location st CurInstr ((Computation b2) . b4) = b5 :=len b6 & b5 in dom b1 holds
len (((Computation b2) . b4) . b6) = len (((Computation b3) . b4) . b6)
proof end;

theorem Th30: :: SCMFSA_3:30
for b1 being autonomic non programmed FinPartState of SCM+FSA
for b2, b3 being State of SCM+FSA st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5 being Int-Location
for b6 being FinSeq-Location st CurInstr ((Computation b2) . b4) = b6 :=<0,...,0> b5 & b6 in dom b1 holds
for b7, b8 being Nat st b7 = abs (((Computation b2) . b4) . b5) & b8 = abs (((Computation b3) . b4) . b5) holds
b7 |-> 0 = b8 |-> 0
proof end;