AMI_5: On the Decomposition of the States of SCM

:: On the Decomposition of the States of SCM
:: by Yasushi Tanaka
::
:: Received November 23, 1993
:: Copyright (c) 1993-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, AMI_3, SUBSET_1, AMI_2, AMI_1, STRUCT_0, XBOOLE_0, FSM_1, RELAT_1, FUNCT_1, TARSKI, FINSET_1, CARD_1, XXREAL_0, FINSEQ_1, GRAPHSP, ARYTM_3, ARYTM_1, INT_1, FUNCT_4, FUNCOP_1, CIRCUIT2, PARTFUN1, EXTPRO_1, RECDEF_2, CAT_1, AMISTD_5, COMPOS_1, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, XCMPLX_0, DOMAIN_1, RELAT_1, FUNCT_1, FUNCOP_1, PARTFUN1, FUNCT_4, NUMBERS, INT_1, NAT_1, RECDEF_2, STRUCT_0, FINSET_1, FINSEQ_1, MEMSTR_0, COMPOS_0, SCM_INST, COMPOS_1, EXTPRO_1, AMI_3, XXREAL_0, AMISTD_5;
definitions EXTPRO_1, FUNCT_1, AMISTD_5;
theorems AMI_3, GRFUNC_1, TARSKI, FUNCOP_1, FUNCT_4, MEMSTR_0, FUNCT_1, ZFMISC_1, ENUMSET1, RELAT_1, XBOOLE_0, XBOOLE_1, PBOOLE, PARTFUN1, EXTPRO_1, AMISTD_5, AMI_2, COMPOS_1;
schemes ;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, INT_1, AMI_3, FINSET_1, CARD_1, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, MEMSTR_0, COMPOS_0, XTUPLE_0, FACIRC_1;
constructors HIDDEN, DOMAIN_1, FINSEQ_4, AMI_3, PRE_POLY, AMISTD_5, FUNCT_7, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities EXTPRO_1, AMI_3, FUNCOP_1, AMI_2, MEMSTR_0, SCM_INST;
expansions ;

theorem Th1: :: AMI_5:1

for dl being Data-Location ex i being Nat st dl = dl. i

proof end;

theorem Th2: :: AMI_5:2

for dl being Data-Location holds dl <> IC by Th1, AMI_3:13;

theorem :: AMI_5:3

for il being Nat
for dl being Data-Location holds il <> dl

proof end;

theorem :: AMI_5:4

for s being State of SCM
for d being Data-Location holds d in dom s

proof end;

registration

cluster NonZero SCM -> infinite ;

coherence by AMI_3:27;

end;

Lm1: for b being Element of Data-Locations holds b is Data-Location

proof end;

theorem :: AMI_5:5

for l being Instruction of SCM holds InsCode l <= 8

proof end;

theorem :: AMI_5:6

canceled;

::$CT

theorem :: AMI_5:7

for ins being Instruction of SCM st InsCode ins = 0 holds
ins = halt SCM

proof end;

theorem :: AMI_5:8

for ins being Instruction of SCM st InsCode ins = 1 holds
ex da, db being Data-Location st ins = da := db

proof end;

theorem :: AMI_5:9

for ins being Instruction of SCM st InsCode ins = 2 holds
ex da, db being Data-Location st ins = AddTo (da,db)

proof end;

theorem :: AMI_5:10

for ins being Instruction of SCM st InsCode ins = 3 holds
ex da, db being Data-Location st ins = SubFrom (da,db)

proof end;

theorem :: AMI_5:11

for ins being Instruction of SCM st InsCode ins = 4 holds
ex da, db being Data-Location st ins = MultBy (da,db)

proof end;

theorem :: AMI_5:12

for ins being Instruction of SCM st InsCode ins = 5 holds
ex da, db being Data-Location st ins = Divide (da,db)

proof end;

theorem :: AMI_5:13

for ins being Instruction of SCM st InsCode ins = 6 holds
ex loc being Nat st ins = SCM-goto loc

proof end;

theorem :: AMI_5:14

for ins being Instruction of SCM st InsCode ins = 7 holds
ex loc being Nat ex da being Data-Location st ins = da =0_goto loc

proof end;

theorem :: AMI_5:15

for ins being Instruction of SCM st InsCode ins = 8 holds
ex loc being Nat ex da being Data-Location st ins = da >0_goto loc

proof end;

theorem :: AMI_5:16

for s being State of SCM
for iloc being Nat
for a being Data-Location holds s . a = (s +* (Start-At (iloc,SCM))) . a

proof end;

registration

cluster SCM -> IC-recognized ;

proof end;

end;

registration

cluster SCM -> CurIns-recognized ;

proof end;

end;

theorem :: AMI_5:17

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db

proof end;

theorem :: AMI_5:18

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:19

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:20

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:21

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:22

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)

proof end;

theorem :: AMI_5:23

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da being Data-Location
for loc being Nat
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )

proof end;

theorem :: AMI_5:24

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Nat
for da being Data-Location
for loc being Nat
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> (IC (Comput (P1,s1,i))) + 1 holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )

proof end;

theorem :: AMI_5:25

for s1, s2 being State of SCM st IC s1 = IC s2 & ( for a being Data-Location holds s1 . a = s2 . a ) holds
s1 = s2

proof end;