:: Development of Terminology for {\bf SCM} :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received October 8, 1993 :: Copyright (c) 1993-2012 Association of Mizar Users begin definition let i be Integer; :: original:<* redefine func<*i*> -> FinSequence of INT ; coherence <*i*> is FinSequence of INT proofend; end; registration let i1 be Integer; cluster<%i1%> -> INT -valued ; coherence <%i1%> is INT -valued ; let i2 be Integer; cluster<%i1,i2%> -> INT -valued ; coherence <%i1,i2%> is INT -valued ; let i3 be Integer; cluster<%i1,i2,i3%> -> INT -valued ; coherence <%i1,i2,i3%> is INT -valued ; let i4 be Integer; cluster<%i1,i2,i3,i4%> -> INT -valued ; coherence <%i1,i2,i3,i4%> is INT -valued ; end; definition let D be XFinSequence of INT ; mode State-consisting of D -> State of SCM means :Def1: :: SCM_1:def 1 for k being Element of NAT st k < len D holds it . (dl. k) = D . k; existence ex b1 being State of SCM st for k being Element of NAT st k < len D holds b1 . (dl. k) = D . k proofend; end; :: deftheorem Def1 defines State-consisting SCM_1:def_1_:_ for D being XFinSequence of INT for b2 being State of SCM holds ( b2 is State-consisting of D iff for k being Element of NAT st k < len D holds b2 . (dl. k) = D . k ); registration let D be XFinSequence of INT ; let il be Element of NAT ; clusterV4() Relation-like the carrier of SCM -defined Function-like the_Values_of SCM -compatible total il -started for State-consisting of D; existence ex b1 being State-consisting of D st b1 is il -started proofend; end; theorem :: SCM_1:1 for i1, i2, i3, i4 being Integer for il being Element of NAT for s being b5 -started State-consisting of <%i1,i2,i3,i4%> holds ( s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 ) proofend; theorem Th2: :: SCM_1:2 for i1, i2 being Integer for il being Element of NAT for s being b3 -started State-consisting of <%i1,i2%> holds ( s . (dl. 0) = i1 & s . (dl. 1) = i2 ) proofend; theorem Th3: :: SCM_1:3 for I1, I2 being Instruction of SCM for F being NAT -defined the InstructionsF of SCM -valued total Function st <%I1%> ^ <%I2%> c= F holds ( F . 0 = I1 & F . 1 = I2 ) proofend; Lm1: for F being NAT -defined the InstructionsF of SCM -valued total Function for k being Element of NAT for s being State of SCM holds Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) proofend; Lm2: now__::_thesis:_for_F_being_NAT_-defined_the_InstructionsF_of_SCM_-valued_total_Function for_k,_n_being_Element_of_NAT_ for_s_being_State_of_SCM for_a,_b_being_Data-Location_st_IC_(Comput_(F,s,k))_=_n_&_(_F_._n_=_a_:=_b_or_F_._n_=_AddTo_(a,b)_or_F_._n_=_SubFrom_(a,b)_or_F_._n_=_MultBy_(a,b)_or_(_a_<>_b_&_F_._n_=_Divide_(a,b)_)_)_holds_ (_Comput_(F,s,(k_+_1))_=_Exec_((F_._n),(Comput_(F,s,k)))_&_IC_(Comput_(F,s,(k_+_1)))_=_n_+_1_) let F be NAT -defined the InstructionsF of SCM -valued total Function; ::_thesis: for k, n being Element of NAT for s being State of SCM for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) let k, n be Element of NAT ; ::_thesis: for s being State of SCM for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) let s be State of SCM; ::_thesis: for a, b being Data-Location st IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) holds ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) let a, b be Data-Location; ::_thesis: ( IC (Comput (F,s,k)) = n & ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) ) assume A1: IC (Comput (F,s,k)) = n ; ::_thesis: ( ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) implies ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) ) set csk1 = Comput (F,s,(k + 1)); set csk = Comput (F,s,k); assume A2: ( F . n = a := b or F . n = AddTo (a,b) or F . n = SubFrom (a,b) or F . n = MultBy (a,b) or ( a <> b & F . n = Divide (a,b) ) ) ; ::_thesis: ( Comput (F,s,(k + 1)) = Exec ((F . n),(Comput (F,s,k))) & IC (Comput (F,s,(k + 1))) = n + 1 ) A3: dom F = NAT by PARTFUN1:def_2; thus Comput (F,s,(k + 1)) = Exec ((CurInstr (F,(Comput (F,s,k)))),(Comput (F,s,k))) by Lm1 .= Exec ((F . n),(Comput (F,s,k))) by A1, A3, PARTFUN1:def_6 ; ::_thesis: IC (Comput (F,s,(k + 1))) = n + 1 hence IC (Comput (F,s,(k + 1))) = succ (IC (Comput (F,s,k))) by A2, AMI_3:2, AMI_3:3, AMI_3:4, AMI_3:5, AMI_3:6 .= n + 1 by A1 ; ::_thesis: verum end; theorem Th4: :: SCM_1:4 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = a := b holds ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = (Comput (F,s,k)) . b & ( for d being Data-Location st d <> a holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th5: :: SCM_1:5 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = AddTo (a,b) holds ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) + ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th6: :: SCM_1:6 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = SubFrom (a,b) holds ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) - ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th7: :: SCM_1:7 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = MultBy (a,b) holds ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) * ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th8: :: SCM_1:8 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for a, b being Data-Location st IC (Comput (F,s,k)) = n & F . n = Divide (a,b) & a <> b holds ( IC (Comput (F,s,(k + 1))) = n + 1 & (Comput (F,s,(k + 1))) . a = ((Comput (F,s,k)) . a) div ((Comput (F,s,k)) . b) & (Comput (F,s,(k + 1))) . b = ((Comput (F,s,k)) . a) mod ((Comput (F,s,k)) . b) & ( for d being Data-Location st d <> a & d <> b holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th9: :: SCM_1:9 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = SCM-goto il holds ( IC (Comput (F,s,(k + 1))) = il & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th10: :: SCM_1:10 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for a being Data-Location for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a =0_goto il holds ( ( (Comput (F,s,k)) . a = 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <> 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th11: :: SCM_1:11 for F being NAT -defined the InstructionsF of SCM -valued total Function for k, n being Element of NAT for s being State of SCM for a being Data-Location for il being Element of NAT st IC (Comput (F,s,k)) = n & F . n = a >0_goto il holds ( ( (Comput (F,s,k)) . a > 0 implies IC (Comput (F,s,(k + 1))) = il ) & ( (Comput (F,s,k)) . a <= 0 implies IC (Comput (F,s,(k + 1))) = n + 1 ) & ( for d being Data-Location holds (Comput (F,s,(k + 1))) . d = (Comput (F,s,k)) . d ) ) proofend; theorem Th12: :: SCM_1:12 ( (halt SCM) `1_3 = 0 & ( for a, b being Data-Location holds (a := b) `1_3 = 1 ) & ( for a, b being Data-Location holds (AddTo (a,b)) `1_3 = 2 ) & ( for a, b being Data-Location holds (SubFrom (a,b)) `1_3 = 3 ) & ( for a, b being Data-Location holds (MultBy (a,b)) `1_3 = 4 ) & ( for a, b being Data-Location holds (Divide (a,b)) `1_3 = 5 ) & ( for i being Element of NAT holds (SCM-goto i) `1_3 = 6 ) & ( for a being Data-Location for i being Element of NAT holds (a =0_goto i) `1_3 = 7 ) & ( for a being Data-Location for i being Element of NAT holds (a >0_goto i) `1_3 = 8 ) ) by AMI_3:26, RECDEF_2:def_1; theorem :: SCM_1:13 for i1, i2, i3, i4 being Integer for s being State of SCM st s . (dl. 0) = i1 & s . (dl. 1) = i2 & s . (dl. 2) = i3 & s . (dl. 3) = i4 holds s is State-consisting of <%i1,i2,i3,i4%> proofend; :: Empty program theorem :: SCM_1:14 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(halt SCM)%> c= F holds for s being 0 -started State-consisting of <*> INT holds ( F halts_on s & LifeSpan (F,s) = 0 & Result (F,s) = s ) proofend; :: Assignment theorem :: SCM_1:15 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%((dl. 0) := (dl. 1))%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i2 & ( for d being Data-Location st d <> dl. 0 holds (Result (F,s)) . d = s . d ) ) proofend; :: Adding two integers theorem :: SCM_1:16 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(AddTo ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 + i2 & ( for d being Data-Location st d <> dl. 0 holds (Result (F,s)) . d = s . d ) ) proofend; :: Subtracting two integers theorem :: SCM_1:17 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(SubFrom ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 - i2 & ( for d being Data-Location st d <> dl. 0 holds (Result (F,s)) . d = s . d ) ) proofend; :: Multiplying two integers theorem :: SCM_1:18 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(MultBy ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 * i2 & ( for d being Data-Location st d <> dl. 0 holds (Result (F,s)) . d = s . d ) ) proofend; :: Dividing two integers theorem :: SCM_1:19 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(Divide ((dl. 0),(dl. 1)))%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & (Result (F,s)) . (dl. 0) = i1 div i2 & (Result (F,s)) . (dl. 1) = i1 mod i2 & ( for d being Data-Location st d <> dl. 0 & d <> dl. 1 holds (Result (F,s)) . d = s . d ) ) proofend; :: Unconditional jump theorem :: SCM_1:20 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%(SCM-goto 1)%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) ) proofend; :: Jump at zero theorem :: SCM_1:21 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%((dl. 0) =0_goto 1)%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) ) proofend; :: Jump at greater than zero theorem :: SCM_1:22 for F being NAT -defined the InstructionsF of SCM -valued total Function st <%((dl. 0) >0_goto 1)%> ^ <%(halt SCM)%> c= F holds for i1, i2 being Integer for s being 0 -started State-consisting of <%i1,i2%> holds ( F halts_on s & LifeSpan (F,s) = 1 & ( for d being Data-Location holds (Result (F,s)) . d = s . d ) ) proofend; theorem :: SCM_1:23 for s being State of SCM holds s is State-consisting of <*> INT proofend;