:: SCMPDS_3 semantic presentation

theorem Th1: :: SCMPDS_3:1
for b1 being natural number holds
( not b1 <= 13 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 or b1 = 6 or b1 = 7 or b1 = 8 or b1 = 9 or b1 = 10 or b1 = 11 or b1 = 12 or b1 = 13 )
proof end;

theorem Th2: :: SCMPDS_3:2
for b1 being Integer
for b2, b3 being State of SCMPDS st IC b2 = IC b3 holds
ICplusConst b2,b1 = ICplusConst b3,b1
proof end;

theorem Th3: :: SCMPDS_3:3
for b1 being Integer
for b2 being Int_position
for b3, b4 being State of SCMPDS st b3 | SCM-Data-Loc = b4 | SCM-Data-Loc holds
b3 . (DataLoc (b3 . b2),b1) = b4 . (DataLoc (b4 . b2),b1)
proof end;

theorem Th4: :: SCMPDS_3:4
for b1 being Int_position
for b2, b3 being State of SCMPDS st b2 | SCM-Data-Loc = b3 | SCM-Data-Loc holds
b2 . b1 = b3 . b1
proof end;

theorem Th5: :: SCMPDS_3:5
the carrier of SCMPDS = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ the Instruction-Locations of SCMPDS by SCMPDS_2:5, SCMPDS_2:def 1;

theorem Th6: :: SCMPDS_3:6
not IC SCMPDS in SCM-Data-Loc
proof end;

theorem Th7: :: SCMPDS_3:7
for b1, b2 being State of SCMPDS st b1 | (SCM-Data-Loc \/ {(IC SCMPDS )}) = b2 | (SCM-Data-Loc \/ {(IC SCMPDS )}) holds
for b3 being Instruction of SCMPDS holds (Exec b3,b1) | (SCM-Data-Loc \/ {(IC SCMPDS )}) = (Exec b3,b2) | (SCM-Data-Loc \/ {(IC SCMPDS )})
proof end;

theorem Th8: :: SCMPDS_3:8
for b1 being Instruction of SCMPDS
for b2 being State of SCMPDS holds (Exec b1,b2) | SCM-Instr-Loc = b2 | SCM-Instr-Loc
proof end;

theorem Th9: :: SCMPDS_3:9
for b1 being FinPartState of SCMPDS holds DataPart b1 = b1 | SCM-Data-Loc
proof end;

theorem Th10: :: SCMPDS_3:10
for b1 being FinPartState of SCMPDS holds
( b1 is data-only iff dom b1 c= SCM-Data-Loc )
proof end;

theorem Th11: :: SCMPDS_3:11
for b1 being FinPartState of SCMPDS holds dom (DataPart b1) c= SCM-Data-Loc
proof end;

theorem Th12: :: SCMPDS_3:12
for b1 being FinPartState of SCMPDS holds dom (ProgramPart b1) c= the Instruction-Locations of SCMPDS by RELAT_1:87;

theorem Th13: :: SCMPDS_3:13
for b1 being Instruction of SCMPDS
for b2 being State of SCMPDS
for b3 being programmed FinPartState of SCMPDS holds Exec b1,(b2 +* b3) = (Exec b1,b2) +* b3
proof end;

theorem Th14: :: SCMPDS_3:14
for b1 being State of SCMPDS
for b2 being Instruction-Location of SCMPDS
for b3 being Int_position holds b1 . b3 = (b1 +* (Start-At b2)) . b3
proof end;

theorem Th15: :: SCMPDS_3:15
for b1, b2 being State of SCMPDS holds b1 +* (b2 | SCM-Data-Loc ) is State of SCMPDS
proof end;

definition
let c1 be Int_position ;
let c2 be Integer;
redefine func .--> as c1 .--> c2 -> FinPartState of SCMPDS ;
coherence
c1 .--> c2 is FinPartState of SCMPDS
proof end;
end;

theorem Th16: :: SCMPDS_3:16
for b1 being autonomic FinPartState of SCMPDS st DataPart b1 <> {} holds
IC SCMPDS in dom b1
proof end;

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

theorem Th17: :: SCMPDS_3:17
for b1 being autonomic non programmed FinPartState of SCMPDS holds IC SCMPDS in dom b1
proof end;

theorem Th18: :: SCMPDS_3:18
for b1, b2 being State of SCMPDS
for b3, b4, b5 being Integer st IC b1 = IC b2 & b3 <> b4 & b5 = IC b1 & (b5 - 2) + (2 * b3) >= 0 & (b5 - 2) + (2 * b4) >= 0 holds
ICplusConst b1,b3 <> ICplusConst b2,b4
proof end;

theorem Th19: :: SCMPDS_3:19
for b1, b2 being State of SCMPDS
for b3, b4 being Nat st IC b1 = IC b2 & b3 <> b4 holds
ICplusConst b1,b3 <> ICplusConst b2,b4
proof end;

theorem Th20: :: SCMPDS_3:20
for b1 being State of SCMPDS holds Next (IC b1) = ICplusConst b1,1
proof end;

theorem Th21: :: SCMPDS_3:21
for b1 being autonomic FinPartState of SCMPDS st IC SCMPDS in dom b1 holds
IC b1 in dom b1
proof end;

theorem Th22: :: SCMPDS_3:22
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2 being State of SCMPDS st b1 c= b2 holds
for b3 being Nat holds IC ((Computation b2) . b3) in dom (ProgramPart b1)
proof end;

theorem Th23: :: SCMPDS_3:23
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS 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 Th24: :: SCMPDS_3:24
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Integer
for b7, b8 being Int_position st CurInstr ((Computation b2) . b4) = b7,b5 := b8,b6 & b7 in dom b1 & DataLoc (((Computation b2) . b4) . b7),b5 in dom b1 holds
((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b8),b6) = ((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b8),b6)
proof end;

theorem Th25: :: SCMPDS_3:25
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Integer
for b7, b8 being Int_position st CurInstr ((Computation b2) . b4) = AddTo b7,b5,b8,b6 & b7 in dom b1 & DataLoc (((Computation b2) . b4) . b7),b5 in dom b1 holds
((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b8),b6) = ((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b8),b6)
proof end;

theorem Th26: :: SCMPDS_3:26
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Integer
for b7, b8 being Int_position st CurInstr ((Computation b2) . b4) = SubFrom b7,b5,b8,b6 & b7 in dom b1 & DataLoc (((Computation b2) . b4) . b7),b5 in dom b1 holds
((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b8),b6) = ((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b8),b6)
proof end;

theorem Th27: :: SCMPDS_3:27
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS st b1 c= b2 & b1 c= b3 holds
for b4 being Nat
for b5, b6 being Integer
for b7, b8 being Int_position st CurInstr ((Computation b2) . b4) = MultBy b7,b5,b8,b6 & b7 in dom b1 & DataLoc (((Computation b2) . b4) . b7),b5 in dom b1 holds
(((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b7),b5)) * (((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b8),b6)) = (((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b7),b5)) * (((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b8),b6))
proof end;

theorem Th28: :: SCMPDS_3:28
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS st b1 c= b2 & b1 c= b3 holds
for b4, b5 being Nat
for b6 being Int_position
for b7, b8 being Integer st CurInstr ((Computation b2) . b4) = b6,b7 <>0_goto b8 & b5 = IC ((Computation b2) . b4) & (b5 - 2) + (2 * b8) >= 0 & b8 <> 1 holds
( ((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b6),b7) = 0 iff ((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b6),b7) = 0 )
proof end;

theorem Th29: :: SCMPDS_3:29
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS st b1 c= b2 & b1 c= b3 holds
for b4, b5 being Nat
for b6 being Int_position
for b7, b8 being Integer st CurInstr ((Computation b2) . b4) = b6,b7 <=0_goto b8 & b5 = IC ((Computation b2) . b4) & (b5 - 2) + (2 * b8) >= 0 & b8 <> 1 holds
( ((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b6),b7) > 0 iff ((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b6),b7) > 0 )
proof end;

theorem Th30: :: SCMPDS_3:30
for b1 being autonomic non programmed FinPartState of SCMPDS
for b2, b3 being State of SCMPDS st b1 c= b2 & b1 c= b3 holds
for b4, b5 being Nat
for b6 being Int_position
for b7, b8 being Integer st CurInstr ((Computation b2) . b4) = b6,b7 >=0_goto b8 & b5 = IC ((Computation b2) . b4) & (b5 - 2) + (2 * b8) >= 0 & b8 <> 1 holds
( ((Computation b2) . b4) . (DataLoc (((Computation b2) . b4) . b6),b7) < 0 iff ((Computation b3) . b4) . (DataLoc (((Computation b3) . b4) . b6),b7) < 0 )
proof end;

definition
let c1 be Nat;
canceled;
func inspos c1 -> Instruction-Location of SCMPDS equals :: SCMPDS_3:def 2
il. a1;
coherence
il. c1 is Instruction-Location of SCMPDS
by AMI_3:def 1, SCMPDS_2:def 1;
end;

:: deftheorem Def1 SCMPDS_3:def 1 :
canceled;

:: deftheorem Def2 defines inspos SCMPDS_3:def 2 :
for b1 being Nat holds inspos b1 = il. b1;

theorem Th31: :: SCMPDS_3:31
for b1, b2 being Nat st b1 <> b2 holds
inspos b1 <> inspos b2 by AMI_3:53;

theorem Th32: :: SCMPDS_3:32
for b1 being Instruction-Location of SCMPDS ex b2 being Nat st b1 = inspos b2
proof end;

definition
let c1 be Instruction-Location of SCMPDS ;
let c2 be Nat;
func c1 + c2 -> Instruction-Location of SCMPDS means :Def3: :: SCMPDS_3:def 3
ex b1 being Nat st
( a1 = inspos b1 & a3 = inspos (b1 + a2) );
existence
ex b1 being Instruction-Location of SCMPDS ex b2 being Nat st
( c1 = inspos b2 & b1 = inspos (b2 + c2) )
proof end;
uniqueness
for b1, b2 being Instruction-Location of SCMPDS st ex b3 being Nat st
( c1 = inspos b3 & b1 = inspos (b3 + c2) ) & ex b3 being Nat st
( c1 = inspos b3 & b2 = inspos (b3 + c2) ) holds
b1 = b2
by Th31;
func c1 -' c2 -> Instruction-Location of SCMPDS means :Def4: :: SCMPDS_3:def 4
ex b1 being Nat st
( a1 = inspos b1 & a3 = inspos (b1 -' a2) );
existence
ex b1 being Instruction-Location of SCMPDS ex b2 being Nat st
( c1 = inspos b2 & b1 = inspos (b2 -' c2) )
proof end;
uniqueness
for b1, b2 being Instruction-Location of SCMPDS st ex b3 being Nat st
( c1 = inspos b3 & b1 = inspos (b3 -' c2) ) & ex b3 being Nat st
( c1 = inspos b3 & b2 = inspos (b3 -' c2) ) holds
b1 = b2
by Th31;
end;

:: deftheorem Def3 defines + SCMPDS_3:def 3 :
for b1 being Instruction-Location of SCMPDS
for b2 being Nat
for b3 being Instruction-Location of SCMPDS holds
( b3 = b1 + b2 iff ex b4 being Nat st
( b1 = inspos b4 & b3 = inspos (b4 + b2) ) );

:: deftheorem Def4 defines -' SCMPDS_3:def 4 :
for b1 being Instruction-Location of SCMPDS
for b2 being Nat
for b3 being Instruction-Location of SCMPDS holds
( b3 = b1 -' b2 iff ex b4 being Nat st
( b1 = inspos b4 & b3 = inspos (b4 -' b2) ) );

theorem Th33: :: SCMPDS_3:33
for b1 being Instruction-Location of SCMPDS
for b2, b3 being Nat holds (b1 + b2) + b3 = b1 + (b2 + b3)
proof end;

theorem Th34: :: SCMPDS_3:34
for b1 being Instruction-Location of SCMPDS
for b2 being Nat holds (b1 + b2) -' b2 = b1
proof end;

theorem Th35: :: SCMPDS_3:35
for b1, b2 being Instruction-Location of SCMPDS
for b3 being Nat holds
( Start-At (b1 + b3) = Start-At (b2 + b3) iff Start-At b1 = Start-At b2 )
proof end;

theorem Th36: :: SCMPDS_3:36
for b1, b2 being Instruction-Location of SCMPDS
for b3 being Nat st Start-At b1 = Start-At b2 holds
Start-At (b1 -' b3) = Start-At (b2 -' b3)
proof end;

definition
let c1 be FinPartState of SCMPDS ;
attr a1 is initial means :: SCMPDS_3:def 5
for b1, b2 being Nat st inspos b2 in dom a1 & b1 < b2 holds
inspos b1 in dom a1;
end;

:: deftheorem Def5 defines initial SCMPDS_3:def 5 :
for b1 being FinPartState of SCMPDS holds
( b1 is initial iff for b2, b3 being Nat st inspos b3 in dom b1 & b2 < b3 holds
inspos b2 in dom b1 );

definition
func SCMPDS-Stop -> FinPartState of SCMPDS equals :: SCMPDS_3:def 6
(inspos 0) .--> (halt SCMPDS );
correctness
coherence
(inspos 0) .--> (halt SCMPDS ) is FinPartState of SCMPDS
;
;
end;

:: deftheorem Def6 defines SCMPDS-Stop SCMPDS_3:def 6 :
SCMPDS-Stop = (inspos 0) .--> (halt SCMPDS );

registration
cluster SCMPDS-Stop -> non empty programmed initial ;
coherence
( not SCMPDS-Stop is empty & SCMPDS-Stop is initial & SCMPDS-Stop is programmed )
proof end;
end;

registration
cluster non empty programmed initial FinPartState of SCMPDS ;
existence
ex b1 being FinPartState of SCMPDS st
( b1 is initial & b1 is programmed & not b1 is empty )
proof end;
end;

definition
let c1 be programmed FinPartState of SCMPDS ;
let c2 be Nat;
func Shift c1,c2 -> programmed FinPartState of SCMPDS means :Def7: :: SCMPDS_3:def 7
( dom a3 = { (inspos (b1 + a2)) where B is Nat : inspos b1 in dom a1 } & ( for b1 being Nat st inspos b1 in dom a1 holds
a3 . (inspos (b1 + a2)) = a1 . (inspos b1) ) );
existence
ex b1 being programmed FinPartState of SCMPDS st
( dom b1 = { (inspos (b2 + c2)) where B is Nat : inspos b2 in dom c1 } & ( for b2 being Nat st inspos b2 in dom c1 holds
b1 . (inspos (b2 + c2)) = c1 . (inspos b2) ) )
proof end;
uniqueness
for b1, b2 being programmed FinPartState of SCMPDS st dom b1 = { (inspos (b3 + c2)) where B is Nat : inspos b3 in dom c1 } & ( for b3 being Nat st inspos b3 in dom c1 holds
b1 . (inspos (b3 + c2)) = c1 . (inspos b3) ) & dom b2 = { (inspos (b3 + c2)) where B is Nat : inspos b3 in dom c1 } & ( for b3 being Nat st inspos b3 in dom c1 holds
b2 . (inspos (b3 + c2)) = c1 . (inspos b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Shift SCMPDS_3:def 7 :
for b1 being programmed FinPartState of SCMPDS
for b2 being Nat
for b3 being programmed FinPartState of SCMPDS holds
( b3 = Shift b1,b2 iff ( dom b3 = { (inspos (b4 + b2)) where B is Nat : inspos b4 in dom b1 } & ( for b4 being Nat st inspos b4 in dom b1 holds
b3 . (inspos (b4 + b2)) = b1 . (inspos b4) ) ) );

theorem Th37: :: SCMPDS_3:37
for b1 being Instruction-Location of SCMPDS
for b2 being Nat
for b3 being programmed FinPartState of SCMPDS st b1 in dom b3 holds
(Shift b3,b2) . (b1 + b2) = b3 . b1
proof end;

theorem Th38: :: SCMPDS_3:38
for b1 being programmed FinPartState of SCMPDS
for b2 being Nat holds dom (Shift b1,b2) = { (b3 + b2) where B is Instruction-Location of SCMPDS : b3 in dom b1 }
proof end;

theorem Th39: :: SCMPDS_3:39
for b1, b2 being Nat
for b3 being programmed FinPartState of SCMPDS holds Shift (Shift b3,b1),b2 = Shift b3,(b1 + b2)
proof end;

theorem Th40: :: SCMPDS_3:40
for b1 being programmed FinPartState of SCMPDS
for b2 being Function of the Instructions of SCMPDS ,the Instructions of SCMPDS
for b3 being Nat holds Shift (b2 * b1),b3 = b2 * (Shift b1,b3)
proof end;

theorem Th41: :: SCMPDS_3:41
for b1 being Nat
for b2, b3 being programmed FinPartState of SCMPDS holds Shift (b2 +* b3),b1 = (Shift b2,b1) +* (Shift b3,b1)
proof end;