:: Development of Terminology for {\bf SCM} :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received October 8, 1993 :: Copyright (c) 1993-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, INT_1, FINSEQ_1, SUBSET_1, FSM_1, AMI_3, PARTFUN1, AMI_1, EXTPRO_1, RELAT_1, FUNCT_1, CIRCUIT2, MSUALG_1, ARYTM_3, XXREAL_0, CARD_1, TARSKI, AFINSQ_1, ORDINAL4, GRAPHSP, ARYTM_1, SCM_1, STRUCT_0, RECDEF_2, FUNCT_4, CAT_1, GOBRD13, MEMSTR_0, NAT_1; notations TARSKI, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, XXREAL_0, AFINSQ_1, FUNCT_4, RECDEF_2, STRUCT_0, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_3; constructors AMI_3, RELSET_1, PRE_POLY, XTUPLE_0; registrations ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, AMI_3, AFINSQ_1, RELAT_1, PBOOLE, FINSEQ_1, STRUCT_0, VALUED_0, FUNCT_4, COMPOS_0, XTUPLE_0, MEMSTR_0; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions TARSKI, RELAT_1, FUNCT_1, MEMSTR_0; equalities AFINSQ_1, EXTPRO_1, NAT_1, AMI_3, FUNCOP_1, MEMSTR_0; theorems NAT_1, INT_1, AMI_3, AFINSQ_1, PARTFUN1, FUNCT_4, FUNCOP_1, TARSKI, EXTPRO_1, GRFUNC_1, CARD_1, MEMSTR_0; schemes PARTFUN1; begin registration let i1 be Integer; cluster <%i1%> -> INT-valued; coherence; let i2 be Integer; cluster <%i1,i2%> -> INT-valued; coherence; let i3 be Integer; cluster <%i1,i2,i3%> -> INT-valued; coherence; let i4 be Integer; cluster <%i1,i2,i3,i4%> -> INT-valued; coherence; end; definition let D be XFinSequence of INT; mode State-consisting of D -> State of SCM means :Def1: for k being Element of NAT st k < len D holds it.dl.k = D.k; existence proof defpred P[object,object] means ex k being Element of NAT st $1 = dl.k & $2 = D.k; A1: for x,y being object st x in the carrier of SCM & P[x,y] holds y in INT by INT_1:def 2; A2: for x,y1,y2 being object st x in the carrier of SCM & P[x,y1] & P[x,y2] holds y1 = y2 by AMI_3:10; consider p being PartFunc of SCM,INT such that A3: for x being object holds x in dom p iff x in the carrier of SCM & ex y being object st P[x,y] and A4: for x being object st x in dom p holds P[x,p.x] from PARTFUN1:sch 2(A1,A2); A5: p is (the carrier of SCM)-defined proof let e be object; thus thesis by A3; end; p is (the_Values_of SCM)-compatible proof let e be object; assume A6: e in dom p; then A7: ex y being object st P[e,y] by A3; reconsider o = e as Object of SCM by A6,A3; A8: Values o = INT by A7,AMI_3:11; consider k being Element of NAT such that A9: o = dl.k & p.o = D.k by A4,A6; thus p.e in (the_Values_of SCM).e by A8,A9,INT_1:def 2; end; then reconsider p as PartState of SCM by A5; take s = (the State of SCM)+*p; let k be Element of NAT; assume k < len D; ex i being Element of NAT st dl.k = dl.i & D.k = D.i; then A10: dl.k in dom p by A3; then consider i being Element of NAT such that A11: dl.k = dl.i & p.dl.k = D.i by A4; A12: k = i by A11,AMI_3:10; p c= s by FUNCT_4:25; hence s.dl.k = D.k by A12,A11,A10,GRFUNC_1:2; end; end; registration let D be XFinSequence of INT, il be Element of NAT; cluster il-started for State-consisting of D; existence proof set s = the State-consisting of D; set s1 = s +* Start-At(il,SCM); for k being Element of NAT st k < len D holds s1.dl.k = D.k proof let k be Element of NAT; assume A1: k < len D; A2: dom Start-At(il,SCM) = {IC SCM} by FUNCOP_1:13; dl.k <> IC SCM by AMI_3:13; then not dl.k in dom Start-At(il,SCM) by A2,TARSKI:def 1; hence s1.dl.k = s.dl.k by FUNCT_4:11 .= D.k by A1,Def1; end; then reconsider s1 as State-consisting of D by Def1; take s1; thus IC s1 = il by MEMSTR_0:16; end; end; theorem for i1, i2, i3, i4 being Integer, il being Element of NAT, s being il-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 proof let i1, i2, i3, i4 be Integer, il be Element of NAT, s be il-started State-consisting of <%i1,i2,i3,i4%>; set D = <%i1,i2,i3,i4%>; A1: D.2 = i3 & D.3 = i4; A2: len D = 4 & 0+0=0 by AFINSQ_1:84; D.0 = i1 & D.1 = i2; hence thesis by A1,A2,Def1; end; theorem Th2: for i1, i2 being Integer, il being Element of NAT, s being il-started State-consisting of <%i1,i2%> holds s.dl.0 = i1 & s.dl.1 = i2 proof let i1, i2 be Integer, il be Element of NAT, s be il-started State-consisting of <%i1,i2%>; set data = <%i1,i2%>; A1: len data = 2 & data.0 = i1 by AFINSQ_1:38; data.1 = i2; hence thesis by A1,Def1; end; theorem Th3: for I1, I2 being Instruction of SCM for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%I1%>^<%I2%> c= F holds F.0 = I1 & F.1 = I2 proof let I1, I2 be Instruction of SCM; let F be total NAT-defined the InstructionsF of SCM-valued Function such that A1: <%I1%>^<%I2%> c= F; set ins = <%I1%>^<%I2%>; A2: ins = <%I1, I2%>; then A3: ins.1 = I2; A4: ins.0 = I1 by A2; len ins = 2 by A2,AFINSQ_1:38; then 0 in dom ins & 1 in dom ins by CARD_1:50,TARSKI:def 2; hence thesis by A1,A3,A4,GRFUNC_1:2; end; reserve F for total NAT-defined (the InstructionsF of SCM)-valued Function; Lm1: for k being Nat, s being State of SCM holds Comput(F,s,k+1) = Exec(CurInstr(F,Comput(F,s,k)),Comput(F,s,k)) proof let k be Nat, s be State of SCM; thus Comput(F,s,k+1) = Following(F,Comput(F,s,k)) by EXTPRO_1:3 .= Exec(CurInstr(F,Comput(F,s,k)),Comput(F,s,k)); end; Lm2: now let F be total NAT-defined (the InstructionsF of SCM)-valued Function; let k, n be Element of NAT, s be State of SCM, a, b be Data-Location; assume A1: IC Comput(F,s,k) = n; 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); A3: dom F = NAT by PARTFUN1:def 2; thus csk1 = (Exec(CurInstr(F,csk), csk)) by Lm1 .= Exec(F.n, csk) by A1,A3,PARTFUN1:def 6; hence IC csk1 = IC csk + 1 by A2,AMI_3:2,3,4,5,6 .= n+1 by A1; end; theorem Th4: for k, n being Element of NAT, s being State of SCM, 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 proof let k, n be Element of NAT, s be State of SCM, a, b be Data-Location; assume A1: IC Comput(F,s,k) = n; assume F.n = a := b; then Comput(F,s,k+1) = Exec(a:=b, Comput(F,s,k)) by A1,Lm2; hence thesis by A1,AMI_3:2; end; theorem Th5: for k, n being Element of NAT, s being State of SCM, 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 proof let k, n be Element of NAT, s be State of SCM, a, b be Data-Location; assume A1: IC Comput(F,s,k) = n; assume F.n = AddTo(a,b); then Comput(F,s,k+1) = Exec(AddTo(a,b), Comput(F,s,k)) by A1,Lm2; hence thesis by A1,AMI_3:3; end; theorem Th6: for k, n being Element of NAT, s being State of SCM, 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 proof let k, n be Element of NAT, s be State of SCM, a, b be Data-Location; assume A1: IC Comput(F,s,k)= n; assume F.n = SubFrom(a,b); then Comput(F,s,k+1) = Exec(SubFrom(a,b), Comput(F,s,k)) by A1,Lm2; hence thesis by A1,AMI_3:4; end; theorem Th7: for k, n being Element of NAT, s being State of SCM, 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 proof let k, n be Element of NAT, s be State of SCM, a, b be Data-Location; assume A1: IC Comput(F,s,k) = n; assume F.n = MultBy(a,b); then Comput(F,s,k+1) = Exec(MultBy(a,b), Comput(F,s,k)) by A1,Lm2; hence thesis by A1,AMI_3:5; end; theorem Th8: for k, n being Element of NAT, s being State of SCM, 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 proof let k, n be Element of NAT, s be State of SCM, a, b be Data-Location; assume A1: IC Comput(F,s,k) = n; assume A2: F.n = Divide(a,b) & a <> b; then Comput(F,s,k+1) = Exec(Divide(a,b), Comput(F,s,k)) by A1,Lm2; hence thesis by A1,A2,AMI_3:6; end; theorem Th9: for k, n being Element of NAT, s being State of SCM, 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 proof let k, n be Element of NAT, s be State of SCM, il be Element of NAT; assume A1: IC Comput(F,s,k) = n & F.n = SCM-goto il; set csk1 = Comput(F,s,k+1); set csk = Comput(F,s,k); A2: dom F = NAT by PARTFUN1:def 2; A3: csk1 = Exec(CurInstr(F,csk), csk) by Lm1 .= Exec(SCM-goto il, csk) by A1,A2,PARTFUN1:def 6; hence IC csk1 = il by AMI_3:7; thus thesis by A3,AMI_3:7; end; theorem Th10: for k, n being Nat, s being State of SCM, a being Data-Location, 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 proof let k, n be Nat, s be State of SCM, a be Data-Location, il be Element of NAT; assume that A1: IC Comput(F,s,k) = n and A2: F.n = a =0_goto il; set csk1 = Comput(F,s,k+1); set csk = Comput(F,s,k); A3: dom F = NAT by PARTFUN1:def 2; A4: csk1 = Exec(CurInstr(F,csk), csk) by Lm1 .= Exec(a =0_goto il, csk) by A1,A2,A3,PARTFUN1:def 6; hence csk.a = 0 implies IC csk1 = il by AMI_3:8; thus thesis by A1,A4,AMI_3:8; end; theorem Th11: for k, n being Element of NAT, s being State of SCM, a being Data-Location, 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 proof let k, n be Element of NAT, s be State of SCM, a be Data-Location, il be Element of NAT; assume that A1: IC Comput(F,s,k) = n and A2: F.n = a >0_goto il; set csk1 = Comput(F,s,k+1); set csk = Comput(F,s,k); A3: dom F = NAT by PARTFUN1:def 2; csk1 = Exec(CurInstr(F,csk), csk) by Lm1 .= Exec(a >0_goto il, csk) by A1,A2,A3,PARTFUN1:def 6; hence thesis by A1,AMI_3:9; end; theorem Th12: (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, i being Element of NAT holds (a =0_goto i)`1_3 = 7) & for a being Data-Location, i being Element of NAT holds (a >0_goto i)`1_3 = 8 by AMI_3:26; theorem for i1, i2, i3, i4 being Integer, 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%> proof let i1, i2, i3, i4 be Integer, s be State of SCM such that A1: s.dl.0 = i1 & s.dl.1 = i2 & s.dl.2 = i3 & s.dl.3 = i4; set D = <%i1,i2,i3,i4%>; now let k be Element of NAT; A2: len D=4 & 4=3+1 by AFINSQ_1:84; assume k < len D; then k <= 3 by A2,NAT_1:13; then k=0 or ... or k=3; hence s.dl.k=D.k by A1; end; hence thesis by Def1; end; :: Empty program theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%halt SCM%> c= F for s being 0-started State-consisting of <*>INT holds F halts_on s & LifeSpan(F,s) = 0 & Result(F,s) = s proof let F be total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%halt SCM%> c= F; let s be 0-started State-consisting of <*>INT; 1 = len <%halt SCM%> by AFINSQ_1:34; then 0 in dom<%halt SCM%> by CARD_1:49,TARSKI:def 1; then A2: F.(0+0) = <%halt SCM%>.0 by A1,GRFUNC_1:2 .= halt SCM; A3: s = Comput(F,s,0) by EXTPRO_1:2; F.IC s = halt SCM by A2,MEMSTR_0:def 11; hence A4: F halts_on s by A3,EXTPRO_1:30; dom F = NAT by PARTFUN1:def 2; then CurInstr(F,s) = F.IC s by PARTFUN1:def 6 .= halt SCM by A2,MEMSTR_0:def 11; hence LifeSpan(F,s) = 0 by A4,A3,EXTPRO_1:def 15; IC s = 0 by MEMSTR_0:def 11; hence thesis by A2,A3,EXTPRO_1:7; end; :: Assignment theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%dl.0 := dl.1%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F be total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%dl.0 := dl.1%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s1 = Comput(F,s,0+1); A2: s.dl.1 = i2 by Th2; A3: IC s = 0 & s = Comput(F,s,0) by EXTPRO_1:2,MEMSTR_0:def 11; A4: F.0 = dl.0 := dl.1 by A1,Th3; then A5: IC s1 = 0+1 by A3,Th4; A6: F.1 = halt SCM by A1,Th3; hence F halts_on s by A5,EXTPRO_1:30; thus LifeSpan(F,s) = 1 by A6,A3,A5,EXTPRO_1:33; s1.dl.0 = s.dl.1 by A4,A3,Th4; hence (Result(F,s)).dl.0 = i2 by A6,A2,A5,EXTPRO_1:7; let d be Data-Location; assume A7: d<>dl.0; thus (Result(F,s)).d = s1.d by A6,A5,EXTPRO_1:7 .= s.d by A4,A3,A7,Th4; end; :: Adding two integers theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%AddTo(dl.0,dl.1)%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F be total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%AddTo(dl.0,dl.1)%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s0 = Comput(F,s,0); set s1 = Comput(F,s,0+1); A2: s = s0 by EXTPRO_1:2; A3: s.dl.0 = i1 & s.dl.1 = i2 by Th2; A4: IC s = 0 by MEMSTR_0:def 11; A5: F.0 = AddTo(dl.0,dl.1) by A1,Th3; then A6: IC s1 = (0+1) by A4,A2,Th5; A7: F.1 = halt SCM by A1,Th3; hence F halts_on s by A6,EXTPRO_1:30; thus LifeSpan(F,s) = 1 by A4,A7,A2,A6,EXTPRO_1:33; s1.dl.0 = s0.dl.0 + s0.dl.1 by A4,A5,A2,Th5; hence (Result(F,s)).dl.0 = i1 + i2 by A7,A3,A2,A6,EXTPRO_1:7; let d be Data-Location; assume A8: d<>dl.0; thus (Result(F,s)).d = s1.d by A7,A6,EXTPRO_1:7 .= s.d by A4,A5,A2,A8,Th5; end; :: Subtracting two integers theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%SubFrom(dl.0,dl.1)%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F being total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%SubFrom(dl.0,dl.1)%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s0 = Comput(F,s,0); set s1 = Comput(F,s,0+1); A2: s = s0 by EXTPRO_1:2; A3: s.dl.0 = i1 & s.dl.1 = i2 by Th2; A4: IC s = 0 by MEMSTR_0:def 11; A5: F.0 = SubFrom(dl.0,dl.1) by A1,Th3; then A6: IC s1 = (0+1) by A4,A2,Th6; A7: F.1 = halt SCM by A1,Th3; hence F halts_on s by A6,EXTPRO_1:30; thus LifeSpan(F,s) = 1 by A4,A7,A2,A6,EXTPRO_1:33; s1.dl.0 = s0.dl.0 - s0.dl.1 by A4,A5,A2,Th6; hence (Result(F,s)).dl.0 = i1 - i2 by A7,A3,A2,A6,EXTPRO_1:7; let d be Data-Location; assume A8: d<>dl.0; thus (Result(F,s)).d = s1.d by A7,A6,EXTPRO_1:7 .= s.d by A4,A5,A2,A8,Th6; end; :: Multiplying two integers theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%MultBy(dl.0,dl.1)%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F being total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%MultBy(dl.0,dl.1)%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s0 = Comput(F,s,0); set s1 = Comput(F,s,0+1); A2: s = s0 by EXTPRO_1:2; A3: s.dl.0 = i1 & s.dl.1 = i2 by Th2; A4: IC s = 0 by MEMSTR_0:def 11; A5: F.0 = MultBy(dl.0,dl.1) by A1,Th3; then A6: IC s1 = (0+1) by A4,A2,Th7; A7: F.1 = halt SCM by A1,Th3; hence F halts_on s by A6,EXTPRO_1:30; thus LifeSpan(F,s) = 1 by A4,A7,A2,A6,EXTPRO_1:33; s1.dl.0 = s0.dl.0 * s0.dl.1 by A4,A5,A2,Th7; hence (Result(F,s)).dl.0 = i1 * i2 by A7,A3,A2,A6,EXTPRO_1:7; let d be Data-Location; assume A8: d<>dl.0; thus (Result(F,s)).d = s1.d by A7,A6,EXTPRO_1:7 .= s.d by A4,A5,A2,A8,Th7; end; :: Dividing two integers theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%Divide(dl.0,dl.1)%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F being total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%Divide(dl.0,dl.1)%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s1 = Comput(F,s,0+1); A2: dl.0 <> dl.1 by AMI_3:10; A3: IC s = 0 & F.0 = Divide(dl.0,dl.1) by A1,Th3,MEMSTR_0:def 11; A4: s.dl.0 = i1 & s.dl.1 = i2 by Th2; A5: s = Comput(F,s,0) by EXTPRO_1:2; F.1 = halt SCM by A1,Th3; then A6: F.(IC s1) = halt SCM by A3,A2,A5,Th8; hence F halts_on s by EXTPRO_1:30; Divide(dl.0, dl.1) <> halt SCM by Th12; hence LifeSpan(F,s) = 1 by A3,A5,A6,EXTPRO_1:32; thus (Result(F,s)).dl.0 = s1.dl.0 by A6,EXTPRO_1:7 .= i1 div i2 by A3,A4,A2,A5,Th8; thus (Result(F,s)).dl.1 = s1.dl.1 by A6,EXTPRO_1:7 .= i1 mod i2 by A3,A4,A2,A5,Th8; let d be Data-Location; assume A7: d<>dl.0 & d<>dl.1; thus (Result(F,s)).d = s1.d by A6,EXTPRO_1:7 .= s.d by A3,A2,A5,A7,Th8; end; :: Unconditional jump theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%SCM-goto 1%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F being total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%SCM-goto 1%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s1 = Comput(F,s,0+1); A2: IC s = 0 & s = Comput(F,s,0) by EXTPRO_1:2,MEMSTR_0:def 11; A3: F.0 = SCM-goto 1 by A1,Th3; then A4: IC s1 = (0+1) by A2,Th9; A5: F.1 = halt SCM by A1,Th3; hence F halts_on s by A4,EXTPRO_1:30; thus LifeSpan(F,s) = 1 by A5,A2,A4,EXTPRO_1:33; let d be Data-Location; thus (Result(F,s)).d = s1.d by A5,A4,EXTPRO_1:7 .= s.d by A3,A2,Th9; end; :: Jump at zero theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%dl.0=0_goto 1%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F being total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%dl.0=0_goto 1%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s1 = Comput(F,s,0+1); A2: F.0 = dl.0 =0_goto 1 by A1,Th3; A3: F.1 = halt SCM by A1,Th3; A4: IC s = 0 & s = Comput(F,s,0) by EXTPRO_1:2,MEMSTR_0:def 11; s.dl.0 = i1 by Th2; then A5: IC s1 = (0+1) by A2,A4,Th10; hence F halts_on s by A3,EXTPRO_1:30; thus LifeSpan(F,s) = 1 by A3,A4,A5,EXTPRO_1:33; let d be Data-Location; thus (Result(F,s)).d = s1.d by A3,A5,EXTPRO_1:7 .= s.d by A2,A4,Th10; end; :: Jump at greater than zero theorem for F being total NAT-defined (the InstructionsF of SCM)-valued Function st <%dl.0>0_goto 1%>^<%halt SCM%> c= F for i1, i2 being Integer, 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 proof let F being total NAT-defined (the InstructionsF of SCM)-valued Function such that A1: <%dl.0>0_goto 1%>^<%halt SCM%> c= F; let i1, i2 be Integer, s be 0-started State-consisting of <%i1,i2%>; set s1 = Comput(F,s,0+1); A2: F.0 = dl.0 >0_goto 1 by A1,Th3; A3: F.1 = halt SCM by A1,Th3; A4: IC s = 0 & s = Comput(F,s,0) by EXTPRO_1:2,MEMSTR_0:def 11; s.dl.0 = i1 by Th2; then A5: IC s1 = (0+1) by A2,A4,Th11; hence F halts_on s by A3,EXTPRO_1:30; thus LifeSpan(F,s) = 1 by A3,A4,A5,EXTPRO_1:33; let d be Data-Location; thus (Result(F,s)).d = s1.d by A3,A5,EXTPRO_1:7 .= s.d by A2,A4,Th11; end; theorem for s being State of SCM holds s is State-consisting of <*>INT proof let s be State of SCM; let k be Element of NAT; thus thesis; end;