:: On the Instructions of { \bf SCM } :: by Artur Korni{\l}owicz :: :: Received May 8, 2001 :: Copyright (c) 2001 Association of Mizar Users environ vocabularies AMI_3, AMI_1, ORDINAL2, ARYTM, AMI_2, CAT_1, BOOLE, FUNCT_7, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, FINSEQ_1, GR_CY_1, AMISTD_2, AMI_5, AMISTD_1, SETFAM_1, REALSET1, TARSKI, SGRAPH1, GOBOARD5, FRECHET, ARYTM_1, NAT_1, INT_1, UNIALG_1, CARD_5, CARD_3, RELOC; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, REALSET1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_1, FUNCOP_1, FINSEQ_1, FUNCT_4, STRUCT_0, CARD_3, FUNCT_7, AMI_1, AMI_2, AMI_3, AMISTD_1, AMISTD_2, XXREAL_0; constructors XXREAL_0, NAT_1, NAT_D, REALSET1, FUNCT_7, PRALG_2, AMI_5, AMISTD_2; registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, ARYTM_3, FRAENKEL, NUMBERS, XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_3, TEX_2, AMI_1, AMI_2, AMI_3, AMI_5, SCMRING1, AMISTD_2; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions TARSKI, FUNCT_1, FUNCT_2, FUNCT_7, AMISTD_1, AMISTD_2, XBOOLE_0, AMI_3, FUNCOP_1, AMI_2, AMI_1; theorems TARSKI, NAT_1, AMI_1, AMI_3, FUNCT_4, AMI_5, FUNCT_1, FUNCT_2, RELSET_1, FUNCOP_1, SETFAM_1, AMI_2, AMISTD_1, MCART_1, FINSEQ_1, FINSEQ_3, AMISTD_2, FUNCT_7, CARD_3, ORDINAL1, XBOOLE_0, XBOOLE_1, YELLOW_8, NAT_D, RELAT_1; schemes FUNCT_2; begin reserve a, b, d1, d2 for Data-Location, il, i1, i2 for Instruction-Location of SCM, I for Instruction of SCM, s, s1, s2 for State of SCM, T for InsType of SCM, k for natural number; theorem Th1: not a in the Instruction-Locations of SCM proof a in SCM-Data-Loc by AMI_3:def 2; hence thesis by AMI_2:29,XBOOLE_0:3; end; theorem Th2: SCM-Data-Loc <> the Instruction-Locations of SCM proof assume A1: not thesis; consider a being Element of SCM-Instr-Loc; thus thesis by A1,AMI_2:12; end; theorem Th3: for o being Object of SCM holds o = IC SCM or o in the Instruction-Locations of SCM or o is Data-Location proof let o be Object of SCM; o in {IC SCM} \/ SCM-Data-Loc or o in SCM-Instr-Loc by AMI_5:23,XBOOLE_0:def 2; then o in {IC SCM} or o in SCM-Data-Loc or o in SCM-Instr-Loc by XBOOLE_0:def 2; hence thesis by AMI_3:def 2,TARSKI:def 1; end; theorem Th4: i1 <> i2 implies Next i1 <> Next i2 proof assume A1: i1 <> i2 & Next i1 = Next i2; consider m1 being Element of SCM-Instr-Loc such that A2: m1 = i1 & Next i1 = Next m1 by AMI_3:def 11; consider m2 being Element of SCM-Instr-Loc such that A3: m2 = i2 & Next i2 = Next m2 by AMI_3:def 11; thus contradiction by A1,A2,A3; end; theorem Th5: s1,s2 equal_outside the Instruction-Locations of SCM implies s1.a = s2.a proof set IL = the Instruction-Locations of SCM; assume A1: s1,s2 equal_outside IL; A2: dom s1 = the carrier of SCM by AMI_1:79; A3: dom s2 = the carrier of SCM by AMI_1:79; A4: not a in IL by Th1; then a in dom s1 \ IL by A2,XBOOLE_0:def 4; then A5: a in dom s1 /\ (dom s1 \ IL) by XBOOLE_0:def 3; a in dom s2 \ IL by A3,A4,XBOOLE_0:def 4; then A6: a in dom s2 /\ (dom s2 \ IL) by XBOOLE_0:def 3; thus s1.a = (s1|(dom s1 \ IL)).a by A5,FUNCT_1:71 .= (s2|(dom s2 \ IL)).a by A1,FUNCT_7:def 2 .= s2.a by A6,FUNCT_1:71; end; theorem Th6: for N being with_non-empty_elements set, S being realistic IC-Ins-separated definite (non empty non void AMI-Struct over N), t, u being State of S, il being Instruction-Location of S, e being Element of ObjectKind IC S, I being Element of ObjectKind il st e = il & u = t+*((IC S, il)-->(e, I)) holds u.il = I & IC u = il & IC Following u = Exec(u.IC u, u).IC S proof let N be with_non-empty_elements set, S be realistic IC-Ins-separated definite (non empty non void AMI-Struct over N), t, u be State of S, il be Instruction-Location of S, e be Element of ObjectKind IC S, I be Element of ObjectKind il such that A1: e = il and A2: u = t+*((IC S, il)-->(e, I)); A3: dom ((IC S, il)-->(e, I)) = {IC S, il} by FUNCT_4:65; then A4: IC S in dom ((IC S, il)-->(e, I)) by TARSKI:def 2; A5: IC S <> il by AMI_1:48; il in dom ((IC S, il)-->(e, I)) by A3,TARSKI:def 2; hence u.il = ((IC S, il)-->(e, I)).il by A2,FUNCT_4:14 .= I by FUNCT_4:66; thus IC u = ((IC S, il)-->(e, I)).IC S by A2,A4,FUNCT_4:14 .= il by A1,A5,FUNCT_4:66; thus IC Following u = Exec(u.IC u, u).IC S; end; Lm1: for x, y being set st x in dom <*y*> holds x = 1 proof let x, y be set; assume x in dom <*y*>; then x in Seg 1 by FINSEQ_1:def 8; hence thesis by FINSEQ_1:4,TARSKI:def 1; end; Lm2: for x, y, z being set st x in dom <*y,z*> holds x = 1 or x = 2 proof let x, y, z be set; assume x in dom <*y,z*>; then x in Seg 2 by FINSEQ_3:29; hence thesis by FINSEQ_1:4,TARSKI:def 2; end; Lm3: T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 proof consider y being set such that A1: [T,y] in the Instructions of SCM by RELAT_1:def 4; reconsider I = [T,y] as Instruction of SCM by A1; A2: T = InsCode I by MCART_1:7; InsCode I <= 8 by AMI_5:36; hence thesis by NAT_1:33,A2; end; theorem Th7: AddressPart halt SCM = {} by AMI_3:71,MCART_1:def 2; canceled 8; theorem Th16: T = 0 implies AddressParts T = {0} proof assume A1: T = 0; hereby let a be set; assume a in AddressParts T; then consider I such that A2: a = AddressPart I and A3: InsCode I = T; I = halt SCM by A1,A3,AMI_5:46; hence a in {0} by A2,Th7,TARSKI:def 1; end; let a be set; assume a in {0}; then a = 0 by TARSKI:def 1; hence thesis by A1,Th7,AMI_5:37; end; registration let T; cluster AddressParts T -> non empty; coherence proof consider a, b, i1; A1: T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 by Lm3; InsCode halt SCM = 0 & InsCode (a:=b) = 1 & InsCode AddTo(a,b) = 2 & InsCode SubFrom(a,b) = 3 & InsCode MultBy(a,b) = 4 & InsCode Divide(a,b) = 5 & InsCode goto i1 = 6 & InsCode (a =0_goto i1) = 7 & InsCode (a >0_goto i1) = 8 by AMI_5:37,MCART_1:7; then AddressPart halt SCM in AddressParts T or AddressPart (a:=b) in AddressParts T or AddressPart AddTo(a,b) in AddressParts T or AddressPart SubFrom(a,b) in AddressParts T or AddressPart MultBy(a,b) in AddressParts T or AddressPart Divide(a,b) in AddressParts T or AddressPart goto i1 in AddressParts T or AddressPart (a =0_goto i1) in AddressParts T or AddressPart (a >0_goto i1) in AddressParts T by A1; hence thesis; end; end; theorem Th17: T = 1 implies dom product" AddressParts T = {1,2} proof assume A1: T = 1; consider a, b; A2: AddressPart (a:=b) = <*a,b*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode (a:=b) = 1 by MCART_1:7; then AddressPart (a:=b) in AddressParts T by A1; then x in dom AddressPart (a:=b) by A3,AMISTD_2:def 1; hence x in {1,2} by A2,FINSEQ_1:4,FINSEQ_3:29; end; let x be set; assume A4: x in {1,2}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider d1, d2 such that A7: I = d1:=d2 by A1,A6,AMI_5:47; f = <*d1,d2*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,FINSEQ_3:29; end; hence thesis by AMISTD_2:def 1; end; theorem Th18: T = 2 implies dom product" AddressParts T = {1,2} proof assume A1: T = 2; consider a, b; A2: AddressPart AddTo(a,b) = <*a,b*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode AddTo(a,b) = 2 by MCART_1:7; then AddressPart AddTo(a,b) in AddressParts T by A1; then x in dom AddressPart AddTo(a,b) by A3,AMISTD_2:def 1; hence x in {1,2} by A2,FINSEQ_1:4,FINSEQ_3:29; end; let x be set; assume A4: x in {1,2}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider d1, d2 such that A7: I = AddTo(d1,d2) by A1,A6,AMI_5:48; f = <*d1,d2*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,FINSEQ_3:29; end; hence thesis by AMISTD_2:def 1; end; theorem Th19: T = 3 implies dom product" AddressParts T = {1,2} proof assume A1: T = 3; consider a, b; A2: AddressPart SubFrom(a,b) = <*a,b*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode SubFrom(a,b) = 3 by MCART_1:7; then AddressPart SubFrom(a,b) in AddressParts T by A1; then x in dom AddressPart SubFrom(a,b) by A3,AMISTD_2:def 1; hence x in {1,2} by A2,FINSEQ_1:4,FINSEQ_3:29; end; let x be set; assume A4: x in {1,2}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider d1, d2 such that A7: I = SubFrom(d1,d2) by A1,A6,AMI_5:49; f = <*d1,d2*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,FINSEQ_3:29; end; hence thesis by AMISTD_2:def 1; end; theorem Th20: T = 4 implies dom product" AddressParts T = {1,2} proof assume A1: T = 4; consider a, b; A2: AddressPart MultBy(a,b) = <*a,b*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode MultBy(a,b) = 4 by MCART_1:7; then AddressPart MultBy(a,b) in AddressParts T by A1; then x in dom AddressPart MultBy(a,b) by A3,AMISTD_2:def 1; hence x in {1,2} by A2,FINSEQ_1:4,FINSEQ_3:29; end; let x be set; assume A4: x in {1,2}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider d1, d2 such that A7: I = MultBy(d1,d2) by A1,A6,AMI_5:50; f = <*d1,d2*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,FINSEQ_3:29; end; hence thesis by AMISTD_2:def 1; end; theorem Th21: T = 5 implies dom product" AddressParts T = {1,2} proof assume A1: T = 5; consider a, b; A2: AddressPart Divide(a,b) = <*a,b*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode Divide(a,b) = 5 by MCART_1:7; then AddressPart Divide(a,b) in AddressParts T by A1; then x in dom AddressPart Divide(a,b) by A3,AMISTD_2:def 1; hence x in {1,2} by A2,FINSEQ_1:4,FINSEQ_3:29; end; let x be set; assume A4: x in {1,2}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider d1, d2 such that A7: I = Divide(d1,d2) by A1,A6,AMI_5:51; f = <*d1,d2*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,FINSEQ_3:29; end; hence thesis by AMISTD_2:def 1; end; theorem Th22: T = 6 implies dom product" AddressParts T = {1} proof assume A1: T = 6; consider i1; A2: AddressPart goto i1 = <*i1*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode goto i1 = 6 by MCART_1:7; then AddressPart goto i1 in AddressParts T by A1; then x in dom AddressPart goto i1 by A3,AMISTD_2:def 1; hence x in {1} by A2,FINSEQ_1:4,def 8; end; let x be set; assume A4: x in {1}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider i1 such that A7: I = goto i1 by A1,A6,AMI_5:52; f = <*i1*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,def 8; end; hence thesis by AMISTD_2:def 1; end; theorem Th23: T = 7 implies dom product" AddressParts T = {1,2} proof assume A1: T = 7; consider i1, a; A2: AddressPart (a =0_goto i1) = <*i1,a*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode (a =0_goto i1) = 7 by MCART_1:7; then AddressPart (a =0_goto i1) in AddressParts T by A1; then x in dom AddressPart (a =0_goto i1) by A3,AMISTD_2:def 1; hence x in {1,2} by A2,FINSEQ_1:4,FINSEQ_3:29; end; let x be set; assume A4: x in {1,2}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider i1, a such that A7: I = a =0_goto i1 by A1,A6,AMI_5:53; f = <*i1,a*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,FINSEQ_3:29; end; hence thesis by AMISTD_2:def 1; end; theorem Th24: T = 8 implies dom product" AddressParts T = {1,2} proof assume A1: T = 8; consider i1, a; A2: AddressPart (a >0_goto i1) = <*i1,a*> by MCART_1:def 2; hereby let x be set; assume A3: x in dom product" AddressParts T; InsCode (a >0_goto i1) = 8 by MCART_1:7; then AddressPart (a >0_goto i1) in AddressParts T by A1; then x in dom AddressPart (a >0_goto i1) by A3,AMISTD_2:def 1; hence x in {1,2} by A2,FINSEQ_1:4,FINSEQ_3:29; end; let x be set; assume A4: x in {1,2}; for f being Function st f in AddressParts T holds x in dom f proof let f be Function; assume f in AddressParts T; then consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = T; consider i1, a such that A7: I = a >0_goto i1 by A1,A6,AMI_5:54; f = <*i1,a*> by A5,A7,MCART_1:def 2; hence x in dom f by A4,FINSEQ_1:4,FINSEQ_3:29; end; hence thesis by AMISTD_2:def 1; end; theorem Th25: (product" AddressParts InsCode (a:=b)).1 = SCM-Data-Loc proof A1: InsCode (a:=b) = 1 by MCART_1:7; then dom product" AddressParts InsCode (a:=b) = {1,2} by Th17; then A2: 1 in dom product" AddressParts InsCode (a:=b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode (a:=b)).1; then x in pi(AddressParts InsCode (a:=b),1) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode (a:=b) and A4: f.1 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode (a:=b) by A3; InsCode I = 1 by A6,MCART_1:7; then consider d1, d2 such that A7: I = d1:=d2 by AMI_5:47; x = <*d1,d2*>.1 by A4,A5,A7,MCART_1:def 2 .= d1 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode (x:=b) = 1 by MCART_1:7; then AddressPart (x:=b) in AddressParts InsCode (a:=b) by A1; then A8: (AddressPart (x:=b)).1 in pi (AddressParts InsCode (a:=b),1) by CARD_3:def 6; (AddressPart (x:=b)).1 = <*x,b*>.1 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th26: (product" AddressParts InsCode (a:=b)).2 = SCM-Data-Loc proof A1: InsCode (a:=b) = 1 by MCART_1:7; then dom product" AddressParts InsCode (a:=b) = {1,2} by Th17; then A2: 2 in dom product" AddressParts InsCode (a:=b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode (a:=b)).2; then x in pi(AddressParts InsCode (a:=b),2) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode (a:=b) and A4: f.2 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode (a:=b) by A3; InsCode I = 1 by A6,MCART_1:7; then consider d1, d2 such that A7: I = d1:=d2 by AMI_5:47; x = <*d1,d2*>.2 by A4,A5,A7,MCART_1:def 2 .= d2 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode (a:=x) = 1 by MCART_1:7; then AddressPart (a:=x) in AddressParts InsCode (a:=b) by A1; then A8: (AddressPart (a:=x)).2 in pi (AddressParts InsCode (a:=b),2) by CARD_3:def 6; (AddressPart (a:=x)).2 = <*a,x*>.2 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th27: (product" AddressParts InsCode AddTo(a,b)).1 = SCM-Data-Loc proof A1: InsCode AddTo(a,b) = 2 by MCART_1:7; then dom product" AddressParts InsCode AddTo(a,b) = {1,2} by Th18; then A2: 1 in dom product" AddressParts InsCode AddTo(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode AddTo(a,b)).1; then x in pi(AddressParts InsCode AddTo(a,b),1) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode AddTo(a,b) and A4: f.1 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode AddTo(a,b) by A3; InsCode I = 2 by A6,MCART_1:7; then consider d1, d2 such that A7: I = AddTo(d1,d2) by AMI_5:48; x = <*d1,d2*>.1 by A4,A5,A7,MCART_1:def 2 .= d1 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode AddTo(x,b) = 2 by MCART_1:7; then AddressPart AddTo(x,b) in AddressParts InsCode AddTo(a,b) by A1; then A8: (AddressPart AddTo(x,b)).1 in pi(AddressParts InsCode AddTo(a,b),1) by CARD_3:def 6; (AddressPart AddTo(x,b)).1 = <*x,b*>.1 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th28: (product" AddressParts InsCode AddTo(a,b)).2 = SCM-Data-Loc proof A1: InsCode AddTo(a,b) = 2 by MCART_1:7; then dom product" AddressParts InsCode AddTo(a,b) = {1,2} by Th18; then A2: 2 in dom product" AddressParts InsCode AddTo(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode AddTo(a,b)).2; then x in pi(AddressParts InsCode AddTo(a,b),2) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode AddTo(a,b) and A4: f.2 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode AddTo(a,b) by A3; InsCode I = 2 by A6,MCART_1:7; then consider d1, d2 such that A7: I = AddTo(d1,d2) by AMI_5:48; x = <*d1,d2*>.2 by A4,A5,A7,MCART_1:def 2 .= d2 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode AddTo(a,x) = 2 by MCART_1:7; then AddressPart AddTo(a,x) in AddressParts InsCode AddTo(a,b) by A1; then A8: (AddressPart AddTo(a,x)).2 in pi(AddressParts InsCode AddTo(a,b),2) by CARD_3:def 6; (AddressPart AddTo(a,x)).2 = <*a,x*>.2 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th29: (product" AddressParts InsCode SubFrom(a,b)).1 = SCM-Data-Loc proof A1: InsCode SubFrom(a,b) = 3 by MCART_1:7; then dom product" AddressParts InsCode SubFrom(a,b) = {1,2} by Th19; then A2: 1 in dom product" AddressParts InsCode SubFrom(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode SubFrom(a,b)).1; then x in pi(AddressParts InsCode SubFrom(a,b),1) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode SubFrom(a,b) and A4: f.1 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode SubFrom(a,b) by A3; InsCode I = 3 by A6,MCART_1:7; then consider d1, d2 such that A7: I = SubFrom(d1,d2) by AMI_5:49; x = <*d1,d2*>.1 by A4,A5,A7,MCART_1:def 2 .= d1 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode SubFrom(x,b) = 3 by MCART_1:7; then AddressPart SubFrom(x,b) in AddressParts InsCode SubFrom(a,b) by A1; then A8: (AddressPart SubFrom(x,b)).1 in pi(AddressParts InsCode SubFrom( a,b),1) by CARD_3:def 6; (AddressPart SubFrom(x,b)).1 = <*x,b*>.1 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th30: (product" AddressParts InsCode SubFrom(a,b)).2 = SCM-Data-Loc proof A1: InsCode SubFrom(a,b) = 3 by MCART_1:7; then dom product" AddressParts InsCode SubFrom(a,b) = {1,2} by Th19; then A2: 2 in dom product" AddressParts InsCode SubFrom(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode SubFrom(a,b)).2; then x in pi(AddressParts InsCode SubFrom(a,b),2) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode SubFrom(a,b) and A4: f.2 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode SubFrom(a,b) by A3; InsCode I = 3 by A6,MCART_1:7; then consider d1, d2 such that A7: I = SubFrom(d1,d2) by AMI_5:49; x = <*d1,d2*>.2 by A4,A5,A7,MCART_1:def 2 .= d2 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode SubFrom(a,x) = 3 by MCART_1:7; then AddressPart SubFrom(a,x) in AddressParts InsCode SubFrom(a,b) by A1; then A8: (AddressPart SubFrom(a,x)).2 in pi(AddressParts InsCode SubFrom( a,b),2) by CARD_3:def 6; (AddressPart SubFrom(a,x)).2 = <*a,x*>.2 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th31: (product" AddressParts InsCode MultBy(a,b)).1 = SCM-Data-Loc proof A1: InsCode MultBy(a,b) = 4 by MCART_1:7; then dom product" AddressParts InsCode MultBy(a,b) = {1,2} by Th20; then A2: 1 in dom product" AddressParts InsCode MultBy(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode MultBy(a,b)).1; then x in pi(AddressParts InsCode MultBy(a,b),1) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode MultBy(a,b) and A4: f.1 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode MultBy(a,b) by A3; InsCode I = 4 by A6,MCART_1:7; then consider d1, d2 such that A7: I = MultBy(d1,d2) by AMI_5:50; x = <*d1,d2*>.1 by A4,A5,A7,MCART_1:def 2 .= d1 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode MultBy(x,b) = 4 by MCART_1:7; then AddressPart MultBy(x,b) in AddressParts InsCode MultBy(a,b) by A1; then A8: (AddressPart MultBy(x,b)).1 in pi(AddressParts InsCode MultBy(a, b),1) by CARD_3:def 6; (AddressPart MultBy(x,b)).1 = <*x,b*>.1 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th32: (product" AddressParts InsCode MultBy(a,b)).2 = SCM-Data-Loc proof A1: InsCode MultBy(a,b) = 4 by MCART_1:7; then dom product" AddressParts InsCode MultBy(a,b) = {1,2} by Th20; then A2: 2 in dom product" AddressParts InsCode MultBy(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode MultBy(a,b)).2; then x in pi(AddressParts InsCode MultBy(a,b),2) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode MultBy(a,b) and A4: f.2 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode MultBy(a,b) by A3; InsCode I = 4 by A6,MCART_1:7; then consider d1, d2 such that A7: I = MultBy(d1,d2) by AMI_5:50; x = <*d1,d2*>.2 by A4,A5,A7,MCART_1:def 2 .= d2 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode MultBy(a,x) = 4 by MCART_1:7; then AddressPart MultBy(a,x) in AddressParts InsCode MultBy(a,b) by A1; then A8: (AddressPart MultBy(a,x)).2 in pi(AddressParts InsCode MultBy(a, b),2) by CARD_3:def 6; (AddressPart MultBy(a,x)).2 = <*a,x*>.2 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th33: (product" AddressParts InsCode Divide(a,b)).1 = SCM-Data-Loc proof A1: InsCode Divide(a,b) = 5 by MCART_1:7; then dom product" AddressParts InsCode Divide(a,b) = {1,2} by Th21; then A2: 1 in dom product" AddressParts InsCode Divide(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode Divide(a,b)).1; then x in pi(AddressParts InsCode Divide(a,b),1) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode Divide(a,b) and A4: f.1 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode Divide(a,b) by A3; InsCode I = 5 by A6,MCART_1:7; then consider d1, d2 such that A7: I = Divide(d1,d2) by AMI_5:51; x = <*d1,d2*>.1 by A4,A5,A7,MCART_1:def 2 .= d1 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode Divide(x,b) = 5 by MCART_1:7; then AddressPart Divide(x,b) in AddressParts InsCode Divide(a,b) by A1; then A8: (AddressPart Divide(x,b)).1 in pi(AddressParts InsCode Divide(a, b),1) by CARD_3:def 6; (AddressPart Divide(x,b)).1 = <*x,b*>.1 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th34: (product" AddressParts InsCode Divide(a,b)).2 = SCM-Data-Loc proof A1: InsCode Divide(a,b) = 5 by MCART_1:7; then dom product" AddressParts InsCode Divide(a,b) = {1,2} by Th21; then A2: 2 in dom product" AddressParts InsCode Divide(a,b) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode Divide(a,b)).2; then x in pi(AddressParts InsCode Divide(a,b),2) by A2,AMISTD_2:def 1; then consider f being Function such that A3: f in AddressParts InsCode Divide(a,b) and A4: f.2 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode Divide(a,b) by A3; InsCode I = 5 by A6,MCART_1:7; then consider d1, d2 such that A7: I = Divide(d1,d2) by AMI_5:51; x = <*d1,d2*>.2 by A4,A5,A7,MCART_1:def 2 .= d2 by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode Divide(a,x) = 5 by MCART_1:7; then AddressPart Divide(a,x) in AddressParts InsCode Divide(a,b) by A1; then A8: (AddressPart Divide(a,x)).2 in pi(AddressParts InsCode Divide(a, b),2) by CARD_3:def 6; (AddressPart Divide(a,x)).2 = <*a,x*>.2 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th35: (product" AddressParts InsCode goto i1).1 = the Instruction-Locations of SCM proof InsCode goto i1 = 6 by MCART_1:7; then dom product" AddressParts InsCode goto i1 = {1} by Th22; then A1: 1 in dom product" AddressParts InsCode goto i1 by TARSKI:def 1; A2: InsCode goto i1 = 6 by MCART_1:7; hereby let x be set; assume x in (product" AddressParts InsCode goto i1).1; then x in pi(AddressParts InsCode goto i1,1) by A1,AMISTD_2:8; then consider g being Function such that A3: g in AddressParts InsCode goto i1 and A4: x = g.1 by CARD_3:def 6; consider I being Instruction of SCM such that A5: g = AddressPart I and A6: InsCode I = InsCode goto i1 by A3; consider i2 such that A7: I = goto i2 by A2,A6,AMI_5:52; g = <*i2*> by A5,A7,MCART_1:def 2; then x = i2 by A4,FINSEQ_1:def 8; hence x in the Instruction-Locations of SCM; end; let x be set; assume x in the Instruction-Locations of SCM; then reconsider x as Instruction-Location of SCM by AMI_1:def 4; A8: AddressPart goto x = <*x*> by MCART_1:def 2; InsCode goto i1 = InsCode goto x by A2,MCART_1:7; then A9: <*x*> in AddressParts InsCode goto i1 by A8; <*x*>.1 = x by FINSEQ_1:def 8; then x in pi(AddressParts InsCode goto i1,1) by A9,CARD_3:def 6; hence thesis by A1,AMISTD_2:8; end; theorem Th36: (product" AddressParts InsCode (a =0_goto i1)).1 = the Instruction-Locations of SCM proof InsCode (a =0_goto i1) = 7 by MCART_1:7; then dom product" AddressParts InsCode (a =0_goto i1) = {1,2} by Th23; then A1: 1 in dom product" AddressParts InsCode (a =0_goto i1) by TARSKI:def 2; A2: InsCode (a =0_goto i1) = 7 by MCART_1:7; hereby let x be set; assume x in (product" AddressParts InsCode (a =0_goto i1)).1; then x in pi(AddressParts InsCode (a =0_goto i1),1) by A1,AMISTD_2:8; then consider g being Function such that A3: g in AddressParts InsCode (a =0_goto i1) and A4: x = g.1 by CARD_3:def 6; consider I being Instruction of SCM such that A5: g = AddressPart I and A6: InsCode I = InsCode (a =0_goto i1) by A3; consider i2, b such that A7: I = b =0_goto i2 by A2,A6,AMI_5:53; g = <*i2,b*> by A5,A7,MCART_1:def 2; then x = i2 by A4,FINSEQ_1:61; hence x in the Instruction-Locations of SCM; end; let x be set; assume x in the Instruction-Locations of SCM; then reconsider x as Instruction-Location of SCM by AMI_1:def 4; A8: AddressPart (a =0_goto x) = <*x,a*> by MCART_1:def 2; InsCode (a =0_goto i1) = InsCode (a =0_goto x) by A2,MCART_1:7; then A9: <*x,a*> in AddressParts InsCode (a =0_goto i1) by A8; <*x,a*>.1 = x by FINSEQ_1:61; then x in pi(AddressParts InsCode (a =0_goto i1),1) by A9,CARD_3:def 6; hence thesis by A1,AMISTD_2:8; end; theorem Th37: (product" AddressParts InsCode (a =0_goto i1)).2 = SCM-Data-Loc proof A1: InsCode (a =0_goto i1) = 7 by MCART_1:7; then dom product" AddressParts InsCode (a =0_goto i1) = {1,2} by Th23; then A2: 2 in dom product" AddressParts InsCode (a =0_goto i1) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode (a =0_goto i1)).2; then x in pi(AddressParts InsCode (a =0_goto i1),2) by A2,AMISTD_2:def 1 ; then consider f being Function such that A3: f in AddressParts InsCode (a =0_goto i1) and A4: f.2 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode (a =0_goto i1) by A3; InsCode I = 7 by A6,MCART_1:7; then consider i2, b such that A7: I = b =0_goto i2 by AMI_5:53; x = <*i2,b*>.2 by A4,A5,A7,MCART_1:def 2 .= b by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode (x =0_goto i1) = 7 by MCART_1:7; then AddressPart (x =0_goto i1) in AddressParts InsCode (a =0_goto i1) by A1; then A8: (AddressPart (x =0_goto i1)).2 in pi(AddressParts InsCode (a =0_goto i1),2) by CARD_3:def 6; (AddressPart (x =0_goto i1)).2 = <*i1,x*>.2 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; theorem Th38: (product" AddressParts InsCode (a >0_goto i1)).1 = the Instruction-Locations of SCM proof InsCode (a >0_goto i1) = 8 by MCART_1:7; then dom product" AddressParts InsCode (a >0_goto i1) = {1,2} by Th24; then A1: 1 in dom product" AddressParts InsCode (a >0_goto i1) by TARSKI:def 2; A2: InsCode (a >0_goto i1) = 8 by MCART_1:7; hereby let x be set; assume x in (product" AddressParts InsCode (a >0_goto i1)).1; then x in pi(AddressParts InsCode (a >0_goto i1),1) by A1,AMISTD_2:8; then consider g being Function such that A3: g in AddressParts InsCode (a >0_goto i1) and A4: x = g.1 by CARD_3:def 6; consider I being Instruction of SCM such that A5: g = AddressPart I and A6: InsCode I = InsCode (a >0_goto i1) by A3; consider i2, b such that A7: I = b >0_goto i2 by A2,A6,AMI_5:54; g = <*i2,b*> by A5,A7,MCART_1:def 2; then x = i2 by A4,FINSEQ_1:61; hence x in the Instruction-Locations of SCM; end; let x be set; assume x in the Instruction-Locations of SCM; then reconsider x as Instruction-Location of SCM by AMI_1:def 4; A8: AddressPart (a >0_goto x) = <*x,a*> by MCART_1:def 2; InsCode (a >0_goto i1) = InsCode (a >0_goto x) by A2,MCART_1:7; then A9: <*x,a*> in AddressParts InsCode (a >0_goto i1) by A8; <*x,a*>.1 = x by FINSEQ_1:61; then x in pi(AddressParts InsCode (a >0_goto i1),1) by A9,CARD_3:def 6; hence thesis by A1,AMISTD_2:8; end; theorem Th39: (product" AddressParts InsCode (a >0_goto i1)).2 = SCM-Data-Loc proof A1: InsCode (a >0_goto i1) = 8 by MCART_1:7; then dom product" AddressParts InsCode (a >0_goto i1) = {1,2} by Th24; then A2: 2 in dom product" AddressParts InsCode (a >0_goto i1) by TARSKI:def 2; hereby let x be set; assume x in (product" AddressParts InsCode (a >0_goto i1)).2; then x in pi(AddressParts InsCode (a >0_goto i1),2) by A2,AMISTD_2:def 1 ; then consider f being Function such that A3: f in AddressParts InsCode (a >0_goto i1) and A4: f.2 = x by CARD_3:def 6; consider I being Instruction of SCM such that A5: f = AddressPart I and A6: InsCode I = InsCode (a >0_goto i1) by A3; InsCode I = 8 by A6,MCART_1:7; then consider i2, b such that A7: I = b >0_goto i2 by AMI_5:54; x = <*i2,b*>.2 by A4,A5,A7,MCART_1:def 2 .= b by FINSEQ_1:61; hence x in SCM-Data-Loc by AMI_3:def 2; end; let x be set; assume x in SCM-Data-Loc; then reconsider x as Data-Location by AMI_3:def 2; InsCode (x >0_goto i1) = 8 by MCART_1:7; then AddressPart (x >0_goto i1) in AddressParts InsCode (a >0_goto i1) by A1; then A8: (AddressPart (x >0_goto i1)).2 in pi(AddressParts InsCode (a >0_goto i1),2) by CARD_3:def 6; (AddressPart (x >0_goto i1)).2 = <*i1,x*>.2 by MCART_1:def 2 .= x by FINSEQ_1:61; hence thesis by A2,A8,AMISTD_2:def 1; end; Lm4: for l being Instruction-Location of SCM, i being Instruction of SCM holds (for s being State of SCM st IC s = l & s.l = i holds Exec(i,s).IC SCM = Next IC s) implies NIC(i, l) = {Next l} proof let l be Instruction-Location of SCM, i be Instruction of SCM; assume A1: for s being State of SCM st IC s = l & s.l = i holds Exec(i, s).IC SCM = Next IC s; set X = {IC Following s where s is State of SCM: IC s = l & s.l = i}; hereby let x be set; assume x in NIC(i,l); then consider s being State of SCM such that A2: x = IC Following s & IC s = l & s.l = i; x = Next l by A2,A1; hence x in {Next l} by TARSKI:def 1; end; let x be set; assume x in {Next l}; then A3: x = Next l by TARSKI:def 1; consider t being State of SCM; reconsider il1 = l as Element of ObjectKind IC SCM by AMI_1:def 11; reconsider I = i as Element of ObjectKind l by AMI_1:def 14; set u = t+*((IC SCM, l)-->(il1, I)); A4: IC u = l by Th6; A5: u.l = i by Th6; then IC Following u = Next l by A1,A4; hence thesis by A3,A4,A5; end; Lm5: for i being Instruction of SCM holds (for l being Instruction-Location of SCM holds NIC(i,l)={Next l}) implies JUMP i is empty proof let i be Instruction of SCM; assume A1: for l being Instruction-Location of SCM holds NIC(i,l)={Next l}; consider p, q being Element of the Instruction-Locations of SCM such that A2: p <> q by YELLOW_8:def 1; reconsider p, q as Instruction-Location of SCM by AMI_1:def 4; set X = { NIC(i,f) where f is Instruction-Location of SCM: not contradiction }; assume not thesis; then consider x being set such that A3: x in meet X by XBOOLE_0:def 1; NIC(i,p) = {Next p} & NIC(i,q) = {Next q} by A1; then {Next p} in X & {Next q} in X; then x in {Next p} & x in {Next q} by A3,SETFAM_1:def 1; then x = Next p & x = Next q by TARSKI:def 1; hence contradiction by A2,Th4; end; theorem Th40: NIC(halt SCM, il) = {il} proof now let x be set; A1: now assume A2: x = il; consider t being State of SCM; reconsider il1 = il as Element of ObjectKind IC SCM by AMI_1:def 11; reconsider I = halt SCM as Element of ObjectKind il by AMI_1:def 14; set u = t+*((IC SCM, il)-->(il1, I)); dom ((IC SCM, il)-->(il1, I)) = {IC SCM, il} by FUNCT_4:65; then A3: IC SCM in dom ((IC SCM, il)-->(il1, I)) by TARSKI:def 2; A4: IC SCM <> il by AMI_1:48; A5: u.il = halt SCM by Th6; A6: IC u = il by Th6; then IC Following u = u.IC SCM by A5,AMI_1:def 8 .= ((IC SCM, il)-->(il1, I)).IC SCM by A3,FUNCT_4:14 .= il by A4,FUNCT_4:66; hence x in {IC Following s : IC s = il & s.il=halt SCM} by A2,A5,A6; end; now assume x in {IC Following s : IC s = il & s.il=halt SCM}; then consider s being State of SCM such that A7: x = IC Following s & IC s = il & s.il = halt SCM; thus x = il by A7,AMI_1:def 8; end; hence x in {il} iff x in {IC Following s : IC s = il & s.il=halt SCM} by A1,TARSKI:def 1; end; hence thesis by TARSKI:2; end; registration cluster JUMP halt SCM -> empty; coherence proof set X = { NIC(halt SCM, il) : not contradiction }; assume not thesis; then consider x being set such that A1: x in meet X by XBOOLE_0:def 1; set i1 = il.1, i2 = il.2; NIC(halt SCM, i1) in X & NIC(halt SCM, i2) in X; then {i1} in X & {i2} in X by Th40; then x in {i1} & x in {i2} by A1,SETFAM_1:def 1; then x = i1 & x = i2 by TARSKI:def 1; hence contradiction; end; end; theorem Th41: NIC(a := b, il) = {Next il} proof set i = a:=b; for s being State of SCM st IC s = il & s.il = i holds Exec(i,s).IC SCM = Next IC s by AMI_3:8; hence thesis by Lm4; end; registration let a, b; cluster JUMP (a := b) -> empty; coherence proof for l being Instruction-Location of SCM holds NIC(a:=b,l)={Next l} by Th41; hence thesis by Lm5; end; end; theorem Th42: NIC(AddTo(a,b), il) = {Next il} proof set i = AddTo(a,b); for s being State of SCM st IC s = il & s.il = i holds Exec(i,s).IC SCM = Next IC s by AMI_3:9; hence thesis by Lm4; end; registration let a, b; cluster JUMP AddTo(a, b) -> empty; coherence proof for l being Instruction-Location of SCM holds NIC(AddTo(a,b),l)={Next l} by Th42; hence thesis by Lm5; end; end; theorem Th43: NIC(SubFrom(a,b), il) = {Next il} proof set i = SubFrom(a,b); for s being State of SCM st IC s = il & s.il = i holds Exec(i,s).IC SCM = Next IC s by AMI_3:10; hence thesis by Lm4; end; registration let a, b; cluster JUMP SubFrom(a, b) -> empty; coherence proof for l being Instruction-Location of SCM holds NIC(SubFrom(a,b),l)={Next l} by Th43; hence thesis by Lm5; end; end; theorem Th44: NIC(MultBy(a,b), il) = {Next il} proof set i = MultBy(a,b); for s being State of SCM st IC s = il & s.il = i holds Exec(i,s).IC SCM = Next IC s by AMI_3:11; hence thesis by Lm4; end; registration let a, b; cluster JUMP MultBy(a,b) -> empty; coherence proof for l being Instruction-Location of SCM holds NIC(MultBy(a,b),l)={Next l} by Th44; hence thesis by Lm5; end; end; theorem Th45: NIC(Divide(a,b), il) = {Next il} proof set i = Divide(a,b); for s being State of SCM st IC s = il & s.il = i holds Exec(i,s).IC SCM = Next IC s by AMI_3:12; hence thesis by Lm4; end; registration let a, b; cluster JUMP Divide(a,b) -> empty; coherence proof for l being Instruction-Location of SCM holds NIC(Divide(a,b),l)={Next l} by Th45; hence thesis by Lm5; end; end; theorem Th46: NIC(goto i1, il) = {i1} proof now let x be set; A1: now assume A2: x = i1; consider t being State of SCM; reconsider il1 = il as Element of ObjectKind IC SCM by AMI_1:def 11; reconsider I = goto i1 as Element of ObjectKind il by AMI_1:def 14; set u = t+*((IC SCM, il)-->(il1, I)); A3: IC u = il by Th6; A4: u.il = goto i1 by Th6; then IC Following u = i1 by A3,AMI_3:13; hence x in {IC Following s : IC s = il & s.il=goto i1} by A2,A3,A4; end; now assume x in {IC Following s : IC s = il & s.il=goto i1}; then consider s being State of SCM such that A5: x = IC Following s & IC s = il & s.il = goto i1; thus x = i1 by A5,AMI_3:13; end; hence x in {i1} iff x in {IC Following s : IC s = il & s.il=goto i1} by A1,TARSKI:def 1; end; hence thesis by TARSKI:2; end; theorem Th47: JUMP goto i1 = {i1} proof set X = { NIC(goto i1, il) : not contradiction }; now let x be set; hereby assume A1: x in meet X; set il1 = il.1; NIC(goto i1, il1) in X; then x in NIC(goto i1, il1) by A1,SETFAM_1:def 1; hence x in {i1} by Th46; end; assume x in {i1}; then A2: x = i1 by TARSKI:def 1; A3: NIC(goto i1, i1) in X; now let Y be set; assume Y in X; then consider il being Instruction-Location of SCM such that A4: Y = NIC(goto i1, il); NIC(goto i1, il) = {i1} by Th46; hence i1 in Y by A4,TARSKI:def 1; end; hence x in meet X by A2,A3,SETFAM_1:def 1; end; hence JUMP goto i1 = {i1} by TARSKI:2; end; registration let i1; cluster JUMP goto i1 -> non empty trivial; coherence proof JUMP goto i1 = {i1} by Th47; hence thesis; end; end; theorem Th48: NIC(a=0_goto i1, il) = {i1, Next il} proof set F = {IC Following s : IC s = il & s.il= a=0_goto i1}; hereby let x be set; assume x in NIC(a=0_goto i1, il); then consider s being State of SCM such that A1: x = IC Following s & IC s = il & s.il = a=0_goto i1; per cases; suppose s.a = 0; then x = i1 by A1,AMI_3:14; hence x in {i1, Next il} by TARSKI:def 2; end; suppose s.a <> 0; then x = Next il by A1,AMI_3:14; hence x in {i1, Next il} by TARSKI:def 2; end; end; let x be set; assume A2: x in {i1,Next il}; consider t being State of SCM; reconsider il1 = il as Element of ObjectKind IC SCM by AMI_1:def 11; reconsider I = a=0_goto i1 as Element of ObjectKind il by AMI_1:def 14; set u = t+*((IC SCM, il)-->(il1, I)); A3: a <> il by Th1; A4: IC SCM <> a by AMI_5:20; per cases by A2,TARSKI:def 2; suppose A5: x = i1; set v = u+*(a .--> 0); A6: dom (a .--> 0) = {a} by FUNCOP_1:19; then not IC SCM in dom (a .--> 0) by A4,TARSKI:def 1; then A7: IC v = IC u by FUNCT_4:12 .= il1 by Th6; not il in dom (a .--> 0) by A3,A6,TARSKI:def 1; then A8: v.il = u.il by FUNCT_4:12 .= I by Th6; a in dom (a .--> 0) by A6,TARSKI:def 1; then v.a = (a .--> 0).a by FUNCT_4:14 .= 0 by FUNCOP_1:87; then IC Following v = i1 by A7,A8,AMI_3:14; hence thesis by A5,A7,A8; end; suppose A9: x = Next il; set v = u+*(a .--> 1); A10: dom (a .--> 1) = {a} by FUNCOP_1:19; then not IC SCM in dom (a .--> 1) by A4,TARSKI:def 1; then A11: IC v = IC u by FUNCT_4:12 .= il1 by Th6; not il in dom (a .--> 1) by A3,A10,TARSKI:def 1; then A12: v.il = u.il by FUNCT_4:12 .= I by Th6; a in dom (a .--> 1) by A10,TARSKI:def 1; then v.a = (a .--> 1).a by FUNCT_4:14 .= 1 by FUNCOP_1:87; then IC Following v = Next il by A11,A12,AMI_3:14; hence thesis by A9,A11,A12; end; end; theorem Th49: JUMP (a=0_goto i1) = {i1} proof set X = { NIC(a=0_goto i1, il) : not contradiction }; now let x be set; hereby assume A1: x in meet X; set il1 = il.1, il2 = il.2; NIC(a=0_goto i1, il1) in X & NIC(a=0_goto i1, il2) in X; then A2: x in NIC(a=0_goto i1, il1) & x in NIC(a=0_goto i1, il2) by A1,SETFAM_1:def 1; NIC(a=0_goto i1, il1) = {i1, Next il1} & NIC(a=0_goto i1, il2) = {i1, Next il2} by Th48; then (x = i1 or x = Next il1) & (x = i1 or x = Next il2) by A2, TARSKI:def 2; hence x in {i1} by Th4,TARSKI:def 1; end; assume x in {i1}; then A3: x = i1 by TARSKI:def 1; A4: NIC(a=0_goto i1, i1) in X; now let Y be set; assume Y in X; then consider il being Instruction-Location of SCM such that A5: Y = NIC(a=0_goto i1, il); NIC(a=0_goto i1, il) = {i1, Next il} by Th48; hence i1 in Y by A5,TARSKI:def 2; end; hence x in meet X by A3,A4,SETFAM_1:def 1; end; hence JUMP (a=0_goto i1) = {i1} by TARSKI:2; end; registration let a, i1; cluster JUMP (a =0_goto i1) -> non empty trivial; coherence proof JUMP (a =0_goto i1) = {i1} by Th49; hence thesis; end; end; theorem Th50: NIC(a>0_goto i1, il) = {i1, Next il} proof set F = {IC Following s : IC s = il & s.il= a>0_goto i1}; hereby let x be set; assume x in NIC(a>0_goto i1, il); then consider s being State of SCM such that A1: x = IC Following s & IC s = il & s.il = a>0_goto i1; per cases; suppose s.a > 0; then x = i1 by A1,AMI_3:15; hence x in {i1, Next il} by TARSKI:def 2; end; suppose s.a <= 0; then x = Next il by A1,AMI_3:15; hence x in {i1, Next il} by TARSKI:def 2; end; end; let x be set; assume A2: x in {i1,Next il}; consider t being State of SCM; reconsider il1 = il as Element of ObjectKind IC SCM by AMI_1:def 11; reconsider I = a>0_goto i1 as Element of ObjectKind il by AMI_1:def 14; set u = t+*((IC SCM, il)-->(il1, I)); A3: a <> il by Th1; A4: IC SCM <> a by AMI_5:20; per cases by A2,TARSKI:def 2; suppose A5: x = i1; set v = u+*(a .--> 1); A6: dom (a .--> 1) = {a} by FUNCOP_1:19; then not IC SCM in dom (a .--> 1) by A4,TARSKI:def 1; then A7: IC v = IC u by FUNCT_4:12 .= il1 by Th6; not il in dom (a .--> 1) by A3,A6,TARSKI:def 1; then A8: v.il = u.il by FUNCT_4:12 .= I by Th6; a in dom (a .--> 1) by A6,TARSKI:def 1; then v.a = (a .--> 1).a by FUNCT_4:14 .= 1 by FUNCOP_1:87; then IC Following v = i1 by A7,A8,AMI_3:15; hence thesis by A5,A7,A8; end; suppose A9: x = Next il; set v = u+*(a .--> 0); A10: dom (a .--> 0) = {a} by FUNCOP_1:19; then not IC SCM in dom (a .--> 0) by A4,TARSKI:def 1; then A11: IC v = IC u by FUNCT_4:12 .= il1 by Th6; not il in dom (a .--> 0) by A3,A10,TARSKI:def 1; then A12: v.il = u.il by FUNCT_4:12 .= I by Th6; a in dom (a .--> 0) by A10,TARSKI:def 1; then v.a = (a .--> 0).a by FUNCT_4:14 .= 0 by FUNCOP_1:87; then IC Following v = Next il by A11,A12,AMI_3:15; hence thesis by A9,A11,A12; end; end; theorem Th51: JUMP (a>0_goto i1) = {i1} proof set X = { NIC(a>0_goto i1, il) : not contradiction }; now let x be set; hereby assume A1: x in meet X; set il1 = il.1, il2 = il.2; NIC(a>0_goto i1, il1) in X & NIC(a>0_goto i1, il2) in X; then A2: x in NIC(a>0_goto i1, il1) & x in NIC(a>0_goto i1, il2) by A1,SETFAM_1:def 1; NIC(a>0_goto i1, il1) = {i1, Next il1} & NIC(a>0_goto i1, il2) = {i1, Next il2} by Th50; then (x = i1 or x = Next il1) & (x = i1 or x = Next il2) by A2, TARSKI:def 2; hence x in {i1} by Th4,TARSKI:def 1; end; assume x in {i1}; then A3: x = i1 by TARSKI:def 1; A4: NIC(a>0_goto i1, i1) in X; now let Y be set; assume Y in X; then consider il being Instruction-Location of SCM such that A5: Y = NIC(a>0_goto i1, il); NIC(a>0_goto i1, il) = {i1, Next il} by Th50; hence i1 in Y by A5,TARSKI:def 2; end; hence x in meet X by A3,A4,SETFAM_1:def 1; end; hence JUMP (a>0_goto i1) = {i1} by TARSKI:2; end; registration let a, i1; cluster JUMP (a >0_goto i1) -> non empty trivial; coherence proof JUMP (a >0_goto i1) = {i1} by Th51; hence thesis; end; end; theorem Th52: SUCC il = {il, Next il} proof set X = { NIC(I, il) \ JUMP I where I is Element of the Instructions of SCM: not contradiction }; set N = {il, Next il}; now let x be set; hereby assume x in union X; then consider Y being set such that A1: x in Y & Y in X by TARSKI:def 4; consider i being Element of the Instructions of SCM such that A2: Y = NIC(i, il) \ JUMP i by A1; per cases by AMI_3:69; suppose i = [0,{}]; then x in {il} \ JUMP halt SCM by A1,A2,Th40,AMI_3:71; then x = il by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = a:=b; then consider a, b such that A3: i = a:=b; x in {Next il} \ JUMP (a:=b) by A1,A2,A3,Th41; then x = Next il by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = AddTo(a,b); then consider a, b such that A4: i = AddTo(a,b); x in {Next il} \ JUMP AddTo(a,b) by A1,A2,A4,Th42; then x = Next il by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = SubFrom(a,b); then consider a, b such that A5: i = SubFrom(a,b); x in {Next il} \ JUMP SubFrom(a,b) by A1,A2,A5,Th43; then x = Next il by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = MultBy(a,b); then consider a, b such that A6: i = MultBy(a,b); x in {Next il} \ JUMP MultBy(a,b) by A1,A2,A6,Th44; then x = Next il by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex a,b st i = Divide(a,b); then consider a, b such that A7: i = Divide(a,b); x in {Next il} \ JUMP Divide(a,b) by A1,A2,A7,Th45; then x = Next il by TARSKI:def 1; hence x in N by TARSKI:def 2; end; suppose ex i1 st i = goto i1; then consider i1 such that A8: i = goto i1; x in {i1} \ JUMP i by A1,A2,A8,Th46; then x in {i1} \ {i1} by A8,Th47; hence x in N by XBOOLE_1:37; end; suppose ex a,i1 st i = a=0_goto i1; then consider a, i1 such that A9: i = a=0_goto i1; x in NIC(i, il) \ {i1} by A1,A2,A9,Th49; then A10: x in NIC(i, il) & not x in {i1} by XBOOLE_0:def 4; NIC(i, il) = {i1, Next il} by A9,Th48; then x = i1 or x = Next il by A10,TARSKI:def 2; hence x in N by A10,TARSKI:def 1,def 2; end; suppose ex a,i1 st i = a>0_goto i1; then consider a, i1 such that A11: i = a>0_goto i1; x in NIC(i, il) \ {i1} by A1,A2,A11,Th51; then A12: x in NIC(i, il) & not x in {i1} by XBOOLE_0:def 4; NIC(i, il) = {i1, Next il} by A11,Th50; then x = i1 or x = Next il by A12,TARSKI:def 2; hence x in N by A12,TARSKI:def 1,def 2; end; end; assume A13: x in {il, Next il}; per cases by A13,TARSKI:def 2; suppose A14: x = il; set i = halt SCM; NIC(i, il) \ JUMP i = {il} by Th40; then x in {il} & {il} in X by A14,TARSKI:def 1; hence x in union X by TARSKI:def 4; end; suppose A15: x = Next il; consider a, b being Data-Location; set i = AddTo(a,b); NIC(i, il) \ JUMP i = {Next il} by Th42; then x in {Next il} & {Next il} in X by A15,TARSKI:def 1; hence x in union X by TARSKI:def 4; end; end; hence SUCC il = {il, Next il} by TARSKI:2; end; theorem Th53: for f being IL-Function of NAT, SCM st for k being Element of NAT holds f.k = il.k holds f is bijective & for k being Element of NAT holds f.(k+1) in SUCC (f.k) & for j being Element of NAT st f.j in SUCC (f.k) holds k <= j proof let f be IL-Function of NAT, SCM such that A1: for k being Element of NAT holds f.k = il.k; thus A2: f is bijective proof thus f is one-to-one proof let x1, x2 be set such that A3: x1 in dom f & x2 in dom f and A4: f.x1 = f.x2; reconsider k1 = x1, k2 = x2 as Element of NAT by A3,FUNCT_2:def 1; f.k1 = il.k1 & f.k2 = il.k2 by A1; hence x1 = x2 by A4; end; thus f is onto proof thus rng f c= the Instruction-Locations of SCM by RELSET_1:12; thus the Instruction-Locations of SCM c= rng f proof let x be set; assume x in the Instruction-Locations of SCM; then x is Instruction-Location of SCM by AMI_1:def 4; then consider i being Element of NAT such that A5: x = il.i by AMI_5:19; dom f = NAT by FUNCT_2:def 1; then il.i = f.i & i in dom f by A1; hence x in rng f by A5,FUNCT_1:def 5; end; end; end; let k be Element of NAT; A6: SUCC (f.k) = {f.k, Next (f.k)} by Th52; A7: f.(k+1) = il.(k+1) & f.k = il.k by A1; A8: f.(k+1) = il.(k+1) by A1 .= Next il.k by AMI_3:54; hence f.(k+1) in SUCC (f.k) by A6,A7,TARSKI:def 2; let j be Element of NAT; assume A9: f.j in SUCC (f.k); A10: f is one-to-one by A2,FUNCT_2:def 4; A11: dom f = NAT by FUNCT_2:def 1; per cases by A6,A9,TARSKI:def 2; suppose f.j = f.k; hence k <= j by A10,A11,FUNCT_1:def 8; end; suppose f.j = Next (f.k); then j = k+1 by A7,A8,A10,A11,FUNCT_1:def 8; hence k <= j by NAT_1:11; end; end; registration cluster SCM -> standard; coherence proof deffunc F(Element of NAT) = il.$1; consider f being Function of NAT, the Instruction-Locations of SCM such that A1: for k being Element of NAT holds f.k = F(k) from FUNCT_2:sch 4; reconsider f as IL-Function of NAT, SCM by AMI_1:def 36; f is bijective & for k being Element of NAT holds f.(k+1) in SUCC (f.k) & for j being Element of NAT st f.j in SUCC (f.k) holds k <= j by A1,Th53; hence SCM is standard by AMISTD_1:19; end; end; theorem Th54: il.(SCM,k) = il.k proof deffunc F(Element of NAT) = il.$1; consider f being Function of NAT, the Instruction-Locations of SCM such that A1: for k being Element of NAT holds f.k = F(k) from FUNCT_2:sch 4; reconsider f as IL-Function of NAT, SCM by AMI_1:def 36; A2: f is bijective by A1,Th53; A3: for k being Element of NAT holds f.(k+1) in SUCC (f.k) & for j being Element of NAT st f.j in SUCC (f.k) holds k <= j by A1,Th53; ex f being IL-Function of NAT, SCM st f is bijective & (for m, n being Element of NAT holds m <= n iff f.m <= f.n) & il.k = f.k proof take f; thus f is bijective by A1,Th53; thus for m, n being Element of NAT holds m <= n iff f.m <= f.n by A2,A3,AMISTD_1:18; thus thesis by A1; end; hence thesis by AMISTD_1:def 12; end; theorem Th55: Next il.(SCM,k) = il.(SCM,k+1) proof thus Next il.(SCM,k) = Next il.k by Th54 .= il.(k+1) by AMI_3:54 .= il.(SCM,k+1) by Th54; end; theorem Th56: Next il = NextLoc il proof Next il = il.(SCM,locnum il + 1) proof Next il.(SCM,locnum il) = il.(SCM,locnum il+1) by Th55; hence thesis by AMISTD_1:def 13; end; hence thesis; end; registration cluster InsCode halt SCM -> jump-only InsType of SCM; coherence proof now let s be State of SCM, o be Object of SCM, I be Instruction of SCM; assume that A1: InsCode I = InsCode halt SCM and o <> IC SCM; I = halt SCM by A1,AMI_5:37,46; hence Exec(I, s).o = s.o by AMI_1:def 8; end; hence thesis by AMISTD_1:def 3; end; end; registration cluster halt SCM -> jump-only; coherence proof thus InsCode halt SCM is jump-only; end; end; registration let i1; cluster InsCode goto i1 -> jump-only InsType of SCM; coherence proof set S = SCM; now let s be State of S, o be Object of S, I be Instruction of S; assume that A1: InsCode I = InsCode goto i1 and A2: o <> IC S; InsCode goto i1 = 6 by MCART_1:7; then consider i2 such that A3: I = goto i2 by A1,AMI_5:52; per cases by A2,Th3; suppose o in the Instruction-Locations of S; then reconsider l=o as Instruction-Location of S by AMI_1:def 4; l=o; hence Exec(I, s).o = s.o by AMI_1:def 13; end; suppose o is Data-Location; hence Exec(I, s).o = s.o by A3,AMI_3:13; end; end; hence thesis by AMISTD_1:def 3; end; end; registration let i1; cluster goto i1 -> jump-only non sequential non ins-loc-free; coherence proof thus InsCode goto i1 is jump-only; thus goto i1 is non sequential proof JUMP goto i1 <> {}; hence thesis by AMISTD_1:43; end; take 1; dom AddressPart goto i1 = dom <*i1*> by MCART_1:def 2 .= {1} by FINSEQ_1:4,def 8; hence 1 in dom AddressPart goto i1 by TARSKI:def 1; thus thesis by Th35; end; end; registration let a, i1; cluster InsCode (a =0_goto i1) -> jump-only InsType of SCM; coherence proof set S = SCM; now let s be State of S, o be Object of S, I be Instruction of S; assume that A1: InsCode I = InsCode (a =0_goto i1) and A2: o <> IC S; InsCode (a =0_goto i1) = 7 by MCART_1:7; then consider i2, b such that A3: I = (b =0_goto i2) by A1,AMI_5:53; per cases by A2,Th3; suppose o in the Instruction-Locations of S; then reconsider l=o as Instruction-Location of S by AMI_1:def 4; l=o; hence Exec(I, s).o = s.o by AMI_1:def 13; end; suppose o is Data-Location; hence Exec(I, s).o = s.o by A3,AMI_3:14; end; end; hence thesis by AMISTD_1:def 3; end; cluster InsCode (a >0_goto i1) -> jump-only InsType of SCM; coherence proof set S = SCM; now let s be State of S, o be Object of S, I be Instruction of S; assume that A4: InsCode I = InsCode (a >0_goto i1) and A5: o <> IC S; InsCode (a >0_goto i1) = 8 by MCART_1:7; then consider i2, b such that A6: I = (b >0_goto i2) by A4,AMI_5:54; per cases by A5,Th3; suppose o in the Instruction-Locations of S; then reconsider l=o as Instruction-Location of S by AMI_1:def 4; l=o; hence Exec(I, s).o = s.o by AMI_1:def 13; end; suppose o is Data-Location; hence Exec(I, s).o = s.o by A6,AMI_3:15; end; end; hence thesis by AMISTD_1:def 3; end; end; registration let a, i1; cluster a =0_goto i1 -> jump-only non sequential non ins-loc-free; coherence proof thus InsCode (a =0_goto i1) is jump-only; thus a =0_goto i1 is non sequential proof JUMP (a =0_goto i1) <> {}; hence thesis by AMISTD_1:43; end; take 1; dom AddressPart (a =0_goto i1) = dom <*i1,a*> by MCART_1:def 2 .= {1,2} by FINSEQ_1:4,FINSEQ_3:29; hence 1 in dom AddressPart (a =0_goto i1) by TARSKI:def 2; thus thesis by Th36; end; cluster a >0_goto i1 -> jump-only non sequential non ins-loc-free; coherence proof thus InsCode (a >0_goto i1) is jump-only; thus a >0_goto i1 is non sequential proof JUMP (a >0_goto i1) <> {}; hence thesis by AMISTD_1:43; end; take 1; dom AddressPart (a >0_goto i1) = dom <*i1,a*> by MCART_1:def 2 .= {1,2} by FINSEQ_1:4,FINSEQ_3:29; hence 1 in dom AddressPart (a >0_goto i1) by TARSKI:def 2; thus thesis by Th38; end; end; X: dl.0 <> dl.1 by AMI_3:52; registration let a, b; cluster InsCode (a:=b) -> non jump-only InsType of SCM; coherence proof consider w being State of SCM; set t = w+*((dl.0, dl.1)-->(0,1)); A1: InsCode (a:=b) = 1 by MCART_1:7 .= InsCode (dl.0:=dl.1) by MCART_1:7; A2: dl.0 <> IC SCM by AMI_3:57; dom ((dl.0, dl.1)-->(0,1)) = {dl.0, dl.1} by FUNCT_4:65; then A3: dl.0 in dom ((dl.0, dl.1)-->(0,1)) & dl.1 in dom ((dl.0, dl.1)-->(0,1)) by TARSKI:def 2; then A4: t.dl.0 = (dl.0, dl.1)-->(0,1).dl.0 by FUNCT_4:14 .= 0 by FUNCT_4:66,X; Exec((dl.0:=dl.1), t).dl.0 = t.dl.1 by AMI_3:8 .= (dl.0, dl.1)-->(0,1).dl.1 by A3,FUNCT_4:14 .= 1 by FUNCT_4:66; hence thesis by A1,A2,A4,AMISTD_1:def 3; end; cluster InsCode AddTo(a,b) -> non jump-only InsType of SCM; coherence proof consider w being State of SCM; set t = w+*((dl.0, dl.1)-->(0,1)); A5: InsCode AddTo(a,b) = 2 by MCART_1:7 .= InsCode AddTo(dl.0, dl.1) by MCART_1:7; A6: dl.0 <> IC SCM by AMI_3:57; dom ((dl.0, dl.1)-->(0,1)) = {dl.0, dl.1} by FUNCT_4:65; then A7: dl.0 in dom ((dl.0, dl.1)-->(0,1)) & dl.1 in dom ((dl.0, dl.1)-->(0,1)) by TARSKI:def 2; then A8: t.dl.0 = (dl.0, dl.1)-->(0,1).dl.0 by FUNCT_4:14 .= 0 by FUNCT_4:66,X; t.dl.1 = (dl.0, dl.1)-->(0,1).dl.1 by A7,FUNCT_4:14 .= 1 by FUNCT_4:66; then Exec(AddTo(dl.0, dl.1), t).dl.0 = 0+1 by AMI_3:9,A8; hence thesis by A5,A6,A8,AMISTD_1:def 3; end; cluster InsCode SubFrom(a,b) -> non jump-only InsType of SCM; coherence proof consider w being State of SCM; set t = w+*((dl.0, dl.1)-->(0,1)); A9: InsCode SubFrom(a,b) = 3 by MCART_1:7 .= InsCode SubFrom(dl.0, dl.1) by MCART_1:7; A10: dl.0 <> IC SCM by AMI_3:57; dom ((dl.0, dl.1)-->(0,1)) = {dl.0, dl.1} by FUNCT_4:65; then A11: dl.0 in dom ((dl.0, dl.1)-->(0,1)) & dl.1 in dom ((dl.0, dl.1)-->(0,1)) by TARSKI:def 2; then A12: t.dl.0 = (dl.0, dl.1)-->(0,1).dl.0 by FUNCT_4:14 .= 0 by FUNCT_4:66,X; A13: t.dl.1 = (dl.0, dl.1)-->(0,1).dl.1 by A11,FUNCT_4:14 .= 1 by FUNCT_4:66; Exec(SubFrom(dl.0, dl.1), t).dl.0 = t.dl.0 - t.dl.1 by AMI_3:10 .= -1 by A12,A13; hence thesis by A9,A10,A12,AMISTD_1:def 3; end; cluster InsCode MultBy(a,b) -> non jump-only InsType of SCM; coherence proof consider w being State of SCM; set t = w+*((dl.0, dl.1)-->(1,0)); A14: InsCode MultBy(a,b) = 4 by MCART_1:7 .= InsCode MultBy(dl.0, dl.1) by MCART_1:7; A15: dl.0 <> IC SCM by AMI_3:57; dom ((dl.0, dl.1)-->(1,0)) = {dl.0, dl.1} by FUNCT_4:65; then A16: dl.0 in dom ((dl.0, dl.1)-->(1,0)) & dl.1 in dom ((dl.0, dl.1)-->(1,0)) by TARSKI:def 2; then A17: t.dl.0 = (dl.0, dl.1)-->(1,0).dl.0 by FUNCT_4:14 .= 1 by FUNCT_4:66,X; A18: t.dl.1 = (dl.0, dl.1)-->(1,0).dl.1 by A16,FUNCT_4:14 .= 0 by FUNCT_4:66; Exec(MultBy(dl.0, dl.1), t).dl.0 = t.dl.0 * t.dl.1 by AMI_3:11 .= 0 by A18; hence thesis by A14,A15,A17,AMISTD_1:def 3; end; cluster InsCode Divide(a,b) -> non jump-only InsType of SCM; coherence proof consider w being State of SCM; set t = w+*((dl.0, dl.1)-->(7,3)); A19: InsCode Divide(a,b) = 5 by MCART_1:7 .= InsCode Divide(dl.0, dl.1) by MCART_1:7; A20: dl.0 <> IC SCM by AMI_3:57; dom ((dl.0, dl.1)-->(7,3)) = {dl.0, dl.1} by FUNCT_4:65; then A21: dl.0 in dom ((dl.0, dl.1)-->(7,3)) & dl.1 in dom ((dl.0, dl.1)-->(7,3)) by TARSKI:def 2; then A22: t.dl.0 = (dl.0, dl.1)-->(7,3).dl.0 by FUNCT_4:14 .= 7 by FUNCT_4:66,X; A23: t.dl.1 = (dl.0, dl.1)-->(7,3).dl.1 by A21,FUNCT_4:14 .= 3 by FUNCT_4:66; A24: 7 = 2 * 3 + 1; Exec(Divide(dl.0, dl.1), t).dl.0 = 7 div (3 qua Element of NAT) by A22,A23,AMI_3:12,X .= 2 by A24,NAT_D:def 1; hence thesis by A19,A20,A22,AMISTD_1:def 3; end; end; registration let a, b; cluster a:=b -> non jump-only sequential; coherence proof thus InsCode (a:=b) is not jump-only; let s be State of SCM; Next IC s = NextLoc IC s by Th56; hence thesis by AMI_3:8; end; cluster AddTo(a,b) -> non jump-only sequential; coherence proof thus InsCode AddTo(a,b) is not jump-only; let s be State of SCM; Next IC s = NextLoc IC s by Th56; hence thesis by AMI_3:9; end; cluster SubFrom(a,b) -> non jump-only sequential; coherence proof thus InsCode SubFrom(a,b) is not jump-only; let s be State of SCM; Next IC s = NextLoc IC s by Th56; hence thesis by AMI_3:10; end; cluster MultBy(a,b) -> non jump-only sequential; coherence proof thus InsCode MultBy(a,b) is not jump-only; let s be State of SCM; Next IC s = NextLoc IC s by Th56; hence thesis by AMI_3:11; end; cluster Divide(a,b) -> non jump-only sequential; coherence proof thus InsCode Divide(a,b) is not jump-only; let s be State of SCM; Next IC s = NextLoc IC s by Th56; hence thesis by AMI_3:12; end; end; registration cluster SCM -> homogeneous with_explicit_jumps without_implicit_jumps; coherence proof thus SCM is homogeneous proof let I, J be Instruction of SCM such that A1: InsCode I = InsCode J; A2: J = [0,{}] or (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex a,b st J = Divide(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1) or (ex a,i1 st J = a>0_goto i1) by AMI_3:69; per cases by AMI_3:69; suppose I = [0,{}]; hence thesis by A1,A2,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex a,b st I = a:=b; then consider a, b such that A3: I = a:=b; A4: InsCode I = 1 by A3,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A3,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex a,b st J = a:=b; then consider d1, d2 such that A5: J = d1:=d2; thus dom AddressPart I = dom <*a,b*> by A3,MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*d1,d2*> by FINSEQ_3:29 .= dom AddressPart J by A5,MCART_1:def 2; end; suppose (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex a,b st J = Divide(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1) or (ex a,i1 st J = a>0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A4,MCART_1:7; end; end; hence thesis; end; suppose ex a,b st I = AddTo(a,b); then consider a, b such that A6: I = AddTo(a,b); A7: InsCode I = 2 by A6,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A6,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex a,b st J = AddTo(a,b); then consider d1, d2 such that A8: J = AddTo(d1,d2); thus dom AddressPart I = dom <*a,b*> by A6,MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*d1,d2*> by FINSEQ_3:29 .= dom AddressPart J by A8,MCART_1:def 2; end; suppose (ex a,b st J = a:=b) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex a,b st J = Divide(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1) or (ex a,i1 st J = a>0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A7,MCART_1:7; end; end; hence thesis; end; suppose ex a,b st I = SubFrom(a,b); then consider a, b such that A9: I = SubFrom(a,b); A10: InsCode I = 3 by A9,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A9,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex a,b st J = SubFrom(a,b); then consider d1, d2 such that A11: J = SubFrom(d1,d2); thus dom AddressPart I = dom <*a,b*> by A9,MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*d1,d2*> by FINSEQ_3:29 .= dom AddressPart J by A11,MCART_1:def 2; end; suppose (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex a,b st J = Divide(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1) or (ex a,i1 st J = a>0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A10,MCART_1:7; end; end; hence thesis; end; suppose ex a,b st I = MultBy(a,b); then consider a, b such that A12: I = MultBy(a,b); A13: InsCode I = 4 by A12,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A12,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex a,b st J = MultBy(a,b); then consider d1, d2 such that A14: J = MultBy(d1,d2); thus dom AddressPart I = dom <*a,b*> by A12,MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*d1,d2*> by FINSEQ_3:29 .= dom AddressPart J by A14,MCART_1:def 2; end; suppose (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = Divide(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1) or (ex a,i1 st J = a>0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A13,MCART_1:7; end; end; hence thesis; end; suppose ex a,b st I = Divide(a,b); then consider a, b such that A15: I = Divide(a,b); A16: InsCode I = 5 by A15,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A15,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex a,b st J = Divide(a,b); then consider d1, d2 such that A17: J = Divide(d1,d2); thus dom AddressPart I = dom <*a,b*> by A15,MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*d1,d2*> by FINSEQ_3:29 .= dom AddressPart J by A17,MCART_1:def 2; end; suppose (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1) or (ex a,i1 st J = a>0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A16,MCART_1:7; end; end; hence thesis; end; suppose ex i1 st I = goto i1; then consider i1 such that A18: I = goto i1; A19: InsCode I = 6 by A18,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A18,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex i2 st J = goto i2; then consider i2 such that A20: J = goto i2; thus dom AddressPart I = dom <*i1*> by A18,MCART_1:def 2 .= Seg 1 by FINSEQ_1:def 8 .= dom <*i2*> by FINSEQ_1:def 8 .= dom AddressPart J by A20,MCART_1:def 2; end; suppose (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex a,b st J = Divide(a,b)) or (ex a,i1 st J = a=0_goto i1) or (ex a,i1 st J = a>0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A19,MCART_1:7; end; end; hence thesis; end; suppose ex a,i1 st I = a=0_goto i1; then consider a, i1 such that A21: I = a=0_goto i1; A22: InsCode I = 7 by A21,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A21,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex d1,i2 st J = d1 =0_goto i2; then consider d1, i2 such that A23: J = d1 =0_goto i2; thus dom AddressPart I = dom <*i1,a*> by A21,MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*i2,d1*> by FINSEQ_3:29 .= dom AddressPart J by A23,MCART_1:def 2; end; suppose (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex a,b st J = Divide(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a>0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A22,MCART_1:7; end; end; hence thesis; end; suppose ex a,i1 st I = a>0_goto i1; then consider a, i1 such that A24: I = a>0_goto i1; A25: InsCode I = 8 by A24,MCART_1:7; now per cases by AMI_3:69; suppose J = [0,{}]; hence dom AddressPart I = dom AddressPart J by A1,A24,AMI_3:71,AMI_5:37,MCART_1:7; end; suppose ex d1,i2 st J = d1 >0_goto i2; then consider d1, i2 such that A26: J = d1 >0_goto i2; thus dom AddressPart I = dom <*i1,a*> by A24,MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*i2,d1*> by FINSEQ_3:29 .= dom AddressPart J by A26,MCART_1:def 2; end; suppose (ex a,b st J = a:=b) or (ex a,b st J = AddTo(a,b)) or (ex a,b st J = SubFrom(a,b)) or (ex a,b st J = MultBy(a,b)) or (ex a,b st J = Divide(a,b)) or (ex i1 st J = goto i1) or (ex a,i1 st J = a=0_goto i1); hence dom AddressPart I = dom AddressPart J by A1,A25,MCART_1:7; end; end; hence thesis; end; end; thus SCM is with_explicit_jumps proof let I be Instruction of SCM; let f be set such that A27: f in JUMP I; per cases by AMI_3:69; suppose A28: I = [0,{}]; JUMP halt SCM is empty; hence thesis by A27,A28,AMI_3:71; end; suppose ex a,b st I = a:=b; then consider a, b such that A29: I = a:=b; JUMP (a:=b) is empty; hence thesis by A27,A29; end; suppose ex a,b st I = AddTo(a,b); then consider a, b such that A30: I = AddTo(a,b); JUMP AddTo(a,b) is empty; hence thesis by A27,A30; end; suppose ex a,b st I = SubFrom(a,b); then consider a, b such that A31: I = SubFrom(a,b); JUMP SubFrom(a,b) is empty; hence thesis by A27,A31; end; suppose ex a,b st I = MultBy(a,b); then consider a, b such that A32: I = MultBy(a,b); JUMP MultBy(a,b) is empty; hence thesis by A27,A32; end; suppose ex a,b st I = Divide(a,b); then consider a, b such that A33: I = Divide(a,b); JUMP Divide(a,b) is empty; hence thesis by A27,A33; end; suppose ex i1 st I = goto i1; then consider i1 such that A34: I = goto i1; JUMP goto i1 = {i1} by Th47; then A35: f = i1 by A27,A34,TARSKI:def 1; take 1; A36: AddressPart goto i1 = <*i1*> by MCART_1:def 2; dom <*i1*> = Seg 1 by FINSEQ_1:def 8; hence 1 in dom AddressPart I by A34,A36,FINSEQ_1:4,TARSKI:def 1; thus f = (AddressPart I).1 & (product" AddressParts InsCode I).1 = the Instruction-Locations of SCM by A34,A35,A36,Th35,FINSEQ_1:def 8; end; suppose ex a,i1 st I = a=0_goto i1; then consider a, i1 such that A37: I = a=0_goto i1; JUMP (a=0_goto i1) = {i1} by Th49; then A38: f = i1 by A27,A37,TARSKI:def 1; take 1; A39: AddressPart (a=0_goto i1) = <*i1,a*> by MCART_1:def 2; dom <*i1,a*> = Seg 2 by FINSEQ_3:29; hence 1 in dom AddressPart I by A37,A39,FINSEQ_1:4,TARSKI:def 2; thus f = (AddressPart I).1 & (product" AddressParts InsCode I).1 = the Instruction-Locations of SCM by A37,A38,A39,Th36,FINSEQ_1:61; end; suppose ex a,i1 st I = a>0_goto i1; then consider a, i1 such that A40: I = a>0_goto i1; JUMP (a>0_goto i1) = {i1} by Th51; then A41: f = i1 by A27,A40,TARSKI:def 1; take 1; A42: AddressPart (a>0_goto i1) = <*i1,a*> by MCART_1:def 2; dom <*i1,a*> = Seg 2 by FINSEQ_3:29; hence 1 in dom AddressPart I by A40,A42,FINSEQ_1:4,TARSKI:def 2; thus f = (AddressPart I).1 & (product" AddressParts InsCode I).1 = the Instruction-Locations of SCM by A40,A41,A42,Th38,FINSEQ_1:61; end; end; let I be Instruction of SCM; let f be set; given k being set such that A43: k in dom AddressPart I and A44: f = (AddressPart I).k and A45: (product" AddressParts InsCode I).k = the Instruction-Locations of SCM; per cases by AMI_3:69; suppose I = [0,{}]; then dom AddressPart I = dom {} by MCART_1:def 2; hence thesis by A43; end; suppose ex a,b st I = a:=b; then consider a, b such that A46: I = a:=b; k in dom <*a,b*> by A43,A46,MCART_1:def 2; then k = 1 or k = 2 by Lm2; hence thesis by A45,A46,Th2,Th25,Th26; end; suppose ex a,b st I = AddTo(a,b); then consider a, b such that A47: I = AddTo(a,b); k in dom <*a,b*> by A43,A47,MCART_1:def 2; then k = 1 or k = 2 by Lm2; hence thesis by A45,A47,Th2,Th27,Th28; end; suppose ex a,b st I = SubFrom(a,b); then consider a, b such that A48: I = SubFrom(a,b); k in dom <*a,b*> by A43,A48,MCART_1:def 2; then k = 1 or k = 2 by Lm2; hence thesis by A45,A48,Th2,Th29,Th30; end; suppose ex a,b st I = MultBy(a,b); then consider a, b such that A49: I = MultBy(a,b); k in dom <*a,b*> by A43,A49,MCART_1:def 2; then k = 1 or k = 2 by Lm2; hence thesis by A45,A49,Th2,Th31,Th32; end; suppose ex a,b st I = Divide(a,b); then consider a, b such that A50: I = Divide(a,b); k in dom <*a,b*> by A43,A50,MCART_1:def 2; then k = 1 or k = 2 by Lm2; hence thesis by A45,A50,Th2,Th33,Th34; end; suppose ex i1 st I = goto i1; then consider i1 such that A51: I = goto i1; A52: AddressPart I = <*i1*> by A51,MCART_1:def 2; then k = 1 by A43,Lm1; then A53: f = i1 by A44,A52,FINSEQ_1:def 8; JUMP I = {i1} by A51,Th47; hence thesis by A53,TARSKI:def 1; end; suppose ex a,i1 st I = a=0_goto i1; then consider a, i1 such that A54: I = a=0_goto i1; A55: AddressPart I = <*i1,a*> by A54,MCART_1:def 2; then k = 1 or k = 2 by A43,Lm2; then A56: f = i1 by A44,A45,A54,A55,Th2,Th37,FINSEQ_1:61; JUMP I = {i1} by A54,Th49; hence thesis by A56,TARSKI:def 1; end; suppose ex a,i1 st I = a>0_goto i1; then consider a, i1 such that A57: I = a>0_goto i1; A58: AddressPart I = <*i1,a*> by A57,MCART_1:def 2; then k = 1 or k = 2 by A43,Lm2; then A59: f = i1 by A44,A45,A57,A58,Th2,Th39,FINSEQ_1:61; JUMP I = {i1} by A57,Th51; hence thesis by A59,TARSKI:def 1; end; end; end; registration cluster SCM -> regular; coherence proof let T be InsType of SCM; per cases by Lm3; suppose A1: T = 0; reconsider f = {} as Function; take f; thus thesis by A1,Th16,CARD_3:19; end; suppose A2: T = 1; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A3: x = f and A4: dom f = dom product" AddressParts T and A5: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A6: dom product" AddressParts T = {1,2} by A2,Th17; then A7: 1 in dom product" AddressParts T by TARSKI:def 2; then f.1 in (product" AddressParts T).1 by A5; then f.1 in pi(AddressParts T,1) by A7,AMISTD_2:def 1; then consider g being Function such that A8: g in AddressParts T and A9: g.1 = f.1 by CARD_3:def 6; A10: 2 in dom product" AddressParts T by A6,TARSKI:def 2; then f.2 in (product" AddressParts T).2 by A5; then f.2 in pi(AddressParts T,2) by A10,AMISTD_2:def 1; then consider h being Function such that A11: h in AddressParts T and A12: h.2 = f.2 by CARD_3:def 6; consider I being Instruction of SCM such that A13: g = AddressPart I and A14: InsCode I = T by A8; consider d1, b such that A15: I = d1:=b by A2,A14,AMI_5:47; A16: g = <*d1,b*> by A13,A15,MCART_1:def 2; consider J being Instruction of SCM such that A17: h = AddressPart J and A18: InsCode J = T by A11; consider a, d2 such that A19: J = a:=d2 by A2,A18,AMI_5:47; A20: h = <*a,d2*> by A17,A19,MCART_1:def 2; A21: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for k being set st k in {1,2} holds <*d1,d2*>.k = f.k proof let k be set; assume A22: k in {1,2}; per cases by A22,TARSKI:def 2; suppose A23: k = 1; <*d1,d2*>.1 = d1 by FINSEQ_1:61 .= f.1 by A9,A16,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A23; end; suppose A24: k = 2; <*d1,d2*>.2 = d2 by FINSEQ_1:61 .= f.2 by A12,A20,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A24; end; end; then A25: <*d1,d2*> = f by A4,A6,A21,FUNCT_1:9; InsCode (d1:=d2) = 1 & AddressPart (d1:=d2) = <*d1,d2*> by MCART_1:7 ; hence thesis by A2,A3,A25; end; suppose A26: T = 2; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A27: x = f and A28: dom f = dom product" AddressParts T and A29: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A30: dom product" AddressParts T = {1,2} by A26,Th18; then A31: 1 in dom product" AddressParts T by TARSKI:def 2; then f.1 in (product" AddressParts T).1 by A29; then f.1 in pi(AddressParts T,1) by A31,AMISTD_2:def 1; then consider g being Function such that A32: g in AddressParts T and A33: g.1 = f.1 by CARD_3:def 6; A34: 2 in dom product" AddressParts T by A30,TARSKI:def 2; then f.2 in (product" AddressParts T).2 by A29; then f.2 in pi(AddressParts T,2) by A34,AMISTD_2:def 1; then consider h being Function such that A35: h in AddressParts T and A36: h.2 = f.2 by CARD_3:def 6; consider I being Instruction of SCM such that A37: g = AddressPart I and A38: InsCode I = T by A32; consider d1, b such that A39: I = AddTo(d1,b) by A26,A38,AMI_5:48; A40: g = <*d1,b*> by A37,A39,MCART_1:def 2; consider J being Instruction of SCM such that A41: h = AddressPart J and A42: InsCode J = T by A35; consider a, d2 such that A43: J = AddTo(a,d2) by A26,A42,AMI_5:48; A44: h = <*a,d2*> by A41,A43,MCART_1:def 2; A45: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for k being set st k in {1,2} holds <*d1,d2*>.k = f.k proof let k be set; assume A46: k in {1,2}; per cases by A46,TARSKI:def 2; suppose A47: k = 1; <*d1,d2*>.1 = d1 by FINSEQ_1:61 .= f.1 by A33,A40,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A47; end; suppose A48: k = 2; <*d1,d2*>.2 = d2 by FINSEQ_1:61 .= f.2 by A36,A44,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A48; end; end; then A49: <*d1,d2*> = f by A28,A30,A45,FUNCT_1:9; InsCode AddTo(d1,d2) = 2 & AddressPart AddTo(d1,d2) = <*d1,d2*> by MCART_1:7; hence thesis by A26,A27,A49; end; suppose A50: T = 3; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A51: x = f and A52: dom f = dom product" AddressParts T and A53: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A54: dom product" AddressParts T = {1,2} by A50,Th19; then A55: 1 in dom product" AddressParts T by TARSKI:def 2; then f.1 in (product" AddressParts T).1 by A53; then f.1 in pi(AddressParts T,1) by A55,AMISTD_2:def 1; then consider g being Function such that A56: g in AddressParts T and A57: g.1 = f.1 by CARD_3:def 6; A58: 2 in dom product" AddressParts T by A54,TARSKI:def 2; then f.2 in (product" AddressParts T).2 by A53; then f.2 in pi(AddressParts T,2) by A58,AMISTD_2:def 1; then consider h being Function such that A59: h in AddressParts T and A60: h.2 = f.2 by CARD_3:def 6; consider I being Instruction of SCM such that A61: g = AddressPart I and A62: InsCode I = T by A56; consider d1, b such that A63: I = SubFrom(d1,b) by A50,A62,AMI_5:49; A64: g = <*d1,b*> by A61,A63,MCART_1:def 2; consider J being Instruction of SCM such that A65: h = AddressPart J and A66: InsCode J = T by A59; consider a, d2 such that A67: J = SubFrom(a,d2) by A50,A66,AMI_5:49; A68: h = <*a,d2*> by A65,A67,MCART_1:def 2; A69: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for k being set st k in {1,2} holds <*d1,d2*>.k = f.k proof let k be set; assume A70: k in {1,2}; per cases by A70,TARSKI:def 2; suppose A71: k = 1; <*d1,d2*>.1 = d1 by FINSEQ_1:61 .= f.1 by A57,A64,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A71; end; suppose A72: k = 2; <*d1,d2*>.2 = d2 by FINSEQ_1:61 .= f.2 by A60,A68,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A72; end; end; then A73: <*d1,d2*> = f by A52,A54,A69,FUNCT_1:9; InsCode SubFrom(d1,d2) = 3 & AddressPart SubFrom(d1,d2) = <*d1,d2*> by MCART_1:7; hence thesis by A50,A51,A73; end; suppose A74: T = 4; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A75: x = f and A76: dom f = dom product" AddressParts T and A77: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A78: dom product" AddressParts T = {1,2} by A74,Th20; then A79: 1 in dom product" AddressParts T by TARSKI:def 2; then f.1 in (product" AddressParts T).1 by A77; then f.1 in pi(AddressParts T,1) by A79,AMISTD_2:def 1; then consider g being Function such that A80: g in AddressParts T and A81: g.1 = f.1 by CARD_3:def 6; A82: 2 in dom product" AddressParts T by A78,TARSKI:def 2; then f.2 in (product" AddressParts T).2 by A77; then f.2 in pi(AddressParts T,2) by A82,AMISTD_2:def 1; then consider h being Function such that A83: h in AddressParts T and A84: h.2 = f.2 by CARD_3:def 6; consider I being Instruction of SCM such that A85: g = AddressPart I and A86: InsCode I = T by A80; consider d1, b such that A87: I = MultBy(d1,b) by A74,A86,AMI_5:50; A88: g = <*d1,b*> by A85,A87,MCART_1:def 2; consider J being Instruction of SCM such that A89: h = AddressPart J and A90: InsCode J = T by A83; consider a, d2 such that A91: J = MultBy(a,d2) by A74,A90,AMI_5:50; A92: h = <*a,d2*> by A89,A91,MCART_1:def 2; A93: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for k being set st k in {1,2} holds <*d1,d2*>.k = f.k proof let k be set; assume A94: k in {1,2}; per cases by A94,TARSKI:def 2; suppose A95: k = 1; <*d1,d2*>.1 = d1 by FINSEQ_1:61 .= f.1 by A81,A88,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A95; end; suppose A96: k = 2; <*d1,d2*>.2 = d2 by FINSEQ_1:61 .= f.2 by A84,A92,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A96; end; end; then A97: <*d1,d2*> = f by A76,A78,A93,FUNCT_1:9; InsCode MultBy(d1,d2) = 4 & AddressPart MultBy(d1,d2) = <*d1,d2*> by MCART_1:7; hence thesis by A74,A75,A97; end; suppose A98: T = 5; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A99: x = f and A100: dom f = dom product" AddressParts T and A101: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A102: dom product" AddressParts T = {1,2} by A98,Th21; then A103: 1 in dom product" AddressParts T by TARSKI:def 2; then f.1 in (product" AddressParts T).1 by A101; then f.1 in pi(AddressParts T,1) by A103,AMISTD_2:def 1; then consider g being Function such that A104: g in AddressParts T and A105: g.1 = f.1 by CARD_3:def 6; A106: 2 in dom product" AddressParts T by A102,TARSKI:def 2; then f.2 in (product" AddressParts T).2 by A101; then f.2 in pi(AddressParts T,2) by A106,AMISTD_2:def 1; then consider h being Function such that A107: h in AddressParts T and A108: h.2 = f.2 by CARD_3:def 6; consider I being Instruction of SCM such that A109: g = AddressPart I and A110: InsCode I = T by A104; consider d1, b such that A111: I = Divide(d1,b) by A98,A110,AMI_5:51; A112: g = <*d1,b*> by A109,A111,MCART_1:def 2; consider J being Instruction of SCM such that A113: h = AddressPart J and A114: InsCode J = T by A107; consider a, d2 such that A115: J = Divide(a,d2) by A98,A114,AMI_5:51; A116: h = <*a,d2*> by A113,A115,MCART_1:def 2; A117: dom <*d1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for k being set st k in {1,2} holds <*d1,d2*>.k = f.k proof let k be set; assume A118: k in {1,2}; per cases by A118,TARSKI:def 2; suppose A119: k = 1; <*d1,d2*>.1 = d1 by FINSEQ_1:61 .= f.1 by A105,A112,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A119; end; suppose A120: k = 2; <*d1,d2*>.2 = d2 by FINSEQ_1:61 .= f.2 by A108,A116,FINSEQ_1:61; hence <*d1,d2*>.k = f.k by A120; end; end; then A121: <*d1,d2*> = f by A100,A102,A117,FUNCT_1:9; InsCode Divide(d1,d2) = 5 & AddressPart Divide(d1,d2) = <*d1,d2*> by MCART_1:7; hence thesis by A98,A99,A121; end; suppose A122: T = 6; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A123: x = f and A124: dom f = dom product" AddressParts T and A125: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A126: dom product" AddressParts T = {1} by A122,Th22; then A127: 1 in dom product" AddressParts T by TARSKI:def 1; then f.1 in (product" AddressParts T).1 by A125; then f.1 in pi(AddressParts T,1) by A127,AMISTD_2:def 1; then consider g being Function such that A128: g in AddressParts T and A129: g.1 = f.1 by CARD_3:def 6; consider I being Instruction of SCM such that A130: g = AddressPart I and A131: InsCode I = T by A128; consider i1 such that A132: I = goto i1 by A122,A131,AMI_5:52; A133: dom <*i1*> = {1} by FINSEQ_1:4,def 8; for k being set st k in {1} holds <*i1*>.k = f.k proof let k be set; assume k in {1}; then k = 1 by TARSKI:def 1; hence <*i1*>.k = f.k by A129,A130,A132,MCART_1:def 2; end; then A134: <*i1*> = f by A124,A126,A133,FUNCT_1:9; InsCode goto i1 = 6 & AddressPart goto i1 = <*i1*> by MCART_1:7; hence thesis by A122,A123,A134; end; suppose A135: T = 7; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A136: x = f and A137: dom f = dom product" AddressParts T and A138: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A139: dom product" AddressParts T = {1,2} by A135,Th23; then A140: 1 in dom product" AddressParts T by TARSKI:def 2; then f.1 in (product" AddressParts T).1 by A138; then f.1 in pi(AddressParts T,1) by A140,AMISTD_2:def 1; then consider g being Function such that A141: g in AddressParts T and A142: g.1 = f.1 by CARD_3:def 6; A143: 2 in dom product" AddressParts T by A139,TARSKI:def 2; then f.2 in (product" AddressParts T).2 by A138; then f.2 in pi(AddressParts T,2) by A143,AMISTD_2:def 1; then consider h being Function such that A144: h in AddressParts T and A145: h.2 = f.2 by CARD_3:def 6; consider I being Instruction of SCM such that A146: g = AddressPart I and A147: InsCode I = T by A141; consider i1, d1 such that A148: I = d1 =0_goto i1 by A135,A147,AMI_5:53; A149: g = <*i1,d1*> by A146,A148,MCART_1:def 2; consider J being Instruction of SCM such that A150: h = AddressPart J and A151: InsCode J = T by A144; consider i2, d2 such that A152: J = d2 =0_goto i2 by A135,A151,AMI_5:53; A153: h = <*i2,d2*> by A150,A152,MCART_1:def 2; A154: dom <*i1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for k being set st k in {1,2} holds <*i1,d2*>.k = f.k proof let k be set; assume A155: k in {1,2}; per cases by A155,TARSKI:def 2; suppose A156: k = 1; <*i1,d2*>.1 = i1 by FINSEQ_1:61 .= f.1 by A142,A149,FINSEQ_1:61; hence <*i1,d2*>.k = f.k by A156; end; suppose A157: k = 2; <*i1,d2*>.2 = d2 by FINSEQ_1:61 .= f.2 by A145,A153,FINSEQ_1:61; hence <*i1,d2*>.k = f.k by A157; end; end; then A158: <*i1,d2*> = f by A137,A139,A154,FUNCT_1:9; InsCode (d2 =0_goto i1) = 7 & AddressPart (d2 =0_goto i1) = <*i1,d2*> by MCART_1:7; hence thesis by A135,A136,A158; end; suppose A159: T = 8; take product" AddressParts T; thus AddressParts T c= product product" AddressParts T by AMISTD_2:9; let x be set; assume x in product product" AddressParts T; then consider f being Function such that A160: x = f and A161: dom f = dom product" AddressParts T and A162: for k being set st k in dom product" AddressParts T holds f.k in (product" AddressParts T).k by CARD_3:def 5; A163: dom product" AddressParts T = {1,2} by A159,Th24; then A164: 1 in dom product" AddressParts T by TARSKI:def 2; then f.1 in (product" AddressParts T).1 by A162; then f.1 in pi(AddressParts T,1) by A164,AMISTD_2:def 1; then consider g being Function such that A165: g in AddressParts T and A166: g.1 = f.1 by CARD_3:def 6; A167: 2 in dom product" AddressParts T by A163,TARSKI:def 2; then f.2 in (product" AddressParts T).2 by A162; then f.2 in pi(AddressParts T,2) by A167,AMISTD_2:def 1; then consider h being Function such that A168: h in AddressParts T and A169: h.2 = f.2 by CARD_3:def 6; consider I being Instruction of SCM such that A170: g = AddressPart I and A171: InsCode I = T by A165; consider i1, d1 such that A172: I = d1 >0_goto i1 by A159,A171,AMI_5:54; A173: g = <*i1,d1*> by A170,A172,MCART_1:def 2; consider J being Instruction of SCM such that A174: h = AddressPart J and A175: InsCode J = T by A168; consider i2, d2 such that A176: J = d2 >0_goto i2 by A159,A175,AMI_5:54; A177: h = <*i2,d2*> by A174,A176,MCART_1:def 2; A178: dom <*i1,d2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for k being set st k in {1,2} holds <*i1,d2*>.k = f.k proof let k be set; assume A179: k in {1,2}; per cases by A179,TARSKI:def 2; suppose A180: k = 1; <*i1,d2*>.1 = i1 by FINSEQ_1:61 .= f.1 by A166,A173,FINSEQ_1:61; hence <*i1,d2*>.k = f.k by A180; end; suppose A181: k = 2; <*i1,d2*>.2 = d2 by FINSEQ_1:61 .= f.2 by A169,A177,FINSEQ_1:61; hence <*i1,d2*>.k = f.k by A181; end; end; then A182: <*i1,d2*> = f by A161,A163,A178,FUNCT_1:9; InsCode (d2 >0_goto i1) = 8 & AddressPart (d2 >0_goto i1) = <*i1,d2*> by MCART_1:7; hence thesis by A159,A160,A182; end; end; end; theorem Th57: IncAddr(goto i1,k) = goto il.(SCM, locnum i1 + k) proof A1: InsCode IncAddr(goto i1,k) = InsCode goto i1 by AMISTD_2:def 14 .= 6 by MCART_1:7 .= InsCode goto il.(SCM, locnum i1 + k) by MCART_1:7; A2: dom AddressPart IncAddr(goto i1,k) = dom AddressPart goto i1 by AMISTD_2:def 14; A3: dom AddressPart goto il.(SCM, locnum i1 + k) = dom <*il.(SCM, locnum i1 + k)*> by MCART_1:def 2 .= Seg 1 by FINSEQ_1:def 8 .= dom <*i1*> by FINSEQ_1:def 8 .= dom AddressPart goto i1 by MCART_1:def 2; for x being set st x in dom AddressPart goto i1 holds (AddressPart IncAddr(goto i1,k)).x = (AddressPart goto il.(SCM, locnum i1 + k)).x proof let x be set; assume A4: x in dom AddressPart goto i1; then x in dom <*i1*> by MCART_1:def 2; then A5: x = 1 by Lm1; then (product" AddressParts InsCode goto i1).x = the Instruction-Locations of SCM by Th35; then consider f being Instruction-Location of SCM such that A6: f = (AddressPart goto i1).x and A7: (AddressPart IncAddr(goto i1,k)).x = il.(SCM,k + locnum f) by A4,AMISTD_2:def 14; f = <*i1*>.x by A6,MCART_1:def 2 .= i1 by A5,FINSEQ_1:def 8; hence (AddressPart IncAddr(goto i1,k)).x = <*il.(SCM, locnum i1 + k)*>.x by A5,A7,FINSEQ_1:def 8 .= (AddressPart goto il.(SCM, locnum i1 + k)).x by MCART_1:def 2; end; then AddressPart IncAddr(goto i1,k) = AddressPart goto il.(SCM, locnum i1 + k) by A2,A3,FUNCT_1:9; hence IncAddr(goto i1,k) = goto il.(SCM, locnum i1 + k) by A1,AMISTD_2:16; end; theorem Th58: IncAddr(a=0_goto i1,k) = a=0_goto il.(SCM, locnum i1 + k) proof A1: InsCode IncAddr(a=0_goto i1,k) = InsCode (a=0_goto i1) by AMISTD_2:def 14 .= 7 by MCART_1:7 .= InsCode (a=0_goto il.(SCM, locnum i1 + k)) by MCART_1:7; A2: dom AddressPart IncAddr(a=0_goto i1,k) = dom AddressPart (a=0_goto i1) by AMISTD_2:def 14; A3: dom AddressPart (a=0_goto il.(SCM, locnum i1 + k)) = dom <*il.(SCM, locnum i1 + k), a*> by MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*i1,a*> by FINSEQ_3:29 .= dom AddressPart (a=0_goto i1) by MCART_1:def 2; for x being set st x in dom AddressPart (a=0_goto i1) holds (AddressPart IncAddr(a=0_goto i1,k)).x = (AddressPart (a=0_goto il.(SCM, locnum i1 + k))).x proof let x be set; assume A4: x in dom AddressPart (a=0_goto i1); then A5: x in dom <*i1,a*> by MCART_1:def 2; per cases by A5,Lm2; suppose A6: x = 1; then (product" AddressParts InsCode (a=0_goto i1)).x = the Instruction-Locations of SCM by Th36; then consider f being Instruction-Location of SCM such that A7: f = (AddressPart (a=0_goto i1)).x and A8: (AddressPart IncAddr(a=0_goto i1,k)).x = il.(SCM,k + locnum f) by A4,AMISTD_2:def 14; f = <*i1,a*>.x by A7,MCART_1:def 2 .= i1 by A6,FINSEQ_1:61; hence (AddressPart IncAddr(a=0_goto i1,k)).x = <*il.(SCM, locnum i1 + k),a*>.x by A6,A8,FINSEQ_1:61 .= (AddressPart (a=0_goto il.(SCM, locnum i1 + k))).x by MCART_1:def 2; end; suppose A9: x = 2; then (product" AddressParts InsCode (a=0_goto i1)).x <> the Instruction-Locations of SCM by Th2,Th37; hence (AddressPart IncAddr(a=0_goto i1,k)).x = (AddressPart (a=0_goto i1)).x by A4,AMISTD_2:def 14 .= <*i1,a*>.x by MCART_1:def 2 .= a by A9,FINSEQ_1:61 .= <*il.(SCM, locnum i1 + k),a*>.x by A9,FINSEQ_1:61 .= (AddressPart (a=0_goto il.(SCM, locnum i1 + k))).x by MCART_1:def 2; end; end; then AddressPart IncAddr(a=0_goto i1,k) = AddressPart (a=0_goto il.(SCM, locnum i1 + k)) by A2,A3,FUNCT_1:9; hence IncAddr(a=0_goto i1,k) = a=0_goto il.(SCM, locnum i1 + k) by A1,AMISTD_2:16; end; theorem Th59: IncAddr(a>0_goto i1,k) = a>0_goto il.(SCM, locnum i1 + k) proof A1: InsCode IncAddr(a>0_goto i1,k) = InsCode (a>0_goto i1) by AMISTD_2:def 14 .= 8 by MCART_1:7 .= InsCode (a>0_goto il.(SCM, locnum i1 + k)) by MCART_1:7; A2: dom AddressPart IncAddr(a>0_goto i1,k) = dom AddressPart (a>0_goto i1) by AMISTD_2:def 14; A3: dom AddressPart (a>0_goto il.(SCM, locnum i1 + k)) = dom <*il.(SCM, locnum i1 + k), a*> by MCART_1:def 2 .= Seg 2 by FINSEQ_3:29 .= dom <*i1,a*> by FINSEQ_3:29 .= dom AddressPart (a>0_goto i1) by MCART_1:def 2; for x being set st x in dom AddressPart (a>0_goto i1) holds (AddressPart IncAddr(a>0_goto i1,k)).x = (AddressPart (a>0_goto il.(SCM, locnum i1 + k))).x proof let x be set; assume A4: x in dom AddressPart (a>0_goto i1); then A5: x in dom <*i1,a*> by MCART_1:def 2; per cases by A5,Lm2; suppose A6: x = 1; then (product" AddressParts InsCode (a>0_goto i1)).x = the Instruction-Locations of SCM by Th38; then consider f being Instruction-Location of SCM such that A7: f = (AddressPart (a>0_goto i1)).x and A8: (AddressPart IncAddr(a>0_goto i1,k)).x = il.(SCM,k + locnum f) by A4,AMISTD_2:def 14; f = <*i1,a*>.x by A7,MCART_1:def 2 .= i1 by A6,FINSEQ_1:61; hence (AddressPart IncAddr(a>0_goto i1,k)).x = <*il.(SCM, locnum i1 + k),a*>.x by A6,A8,FINSEQ_1:61 .= (AddressPart (a>0_goto il.(SCM, locnum i1 + k))).x by MCART_1:def 2; end; suppose A9: x = 2; then (product" AddressParts InsCode (a>0_goto i1)).x <> the Instruction-Locations of SCM by Th2,Th39; hence (AddressPart IncAddr(a>0_goto i1,k)).x = (AddressPart (a>0_goto i1)).x by A4,AMISTD_2:def 14 .= <*i1,a*>.x by MCART_1:def 2 .= a by A9,FINSEQ_1:61 .= <*il.(SCM, locnum i1 + k),a*>.x by A9,FINSEQ_1:61 .= (AddressPart (a>0_goto il.(SCM, locnum i1 + k))).x by MCART_1:def 2; end; end; then AddressPart IncAddr(a>0_goto i1,k) = AddressPart (a>0_goto il.(SCM, locnum i1 + k)) by A2,A3,FUNCT_1:9; hence IncAddr(a>0_goto i1,k) = a>0_goto il.(SCM, locnum i1 + k) by A1,AMISTD_2:16; end; registration cluster SCM -> IC-good Exec-preserving; coherence proof thus SCM is IC-good proof let I be Instruction of SCM; per cases by AMI_3:69; suppose I = [0,{}]; hence thesis by AMI_3:71; end; suppose ex a,b st I = a:=b; then consider a, b such that A1: I = a:=b; thus thesis by A1; end; suppose ex a,b st I = AddTo(a,b); then consider a, b such that A2: I = AddTo(a,b); thus thesis by A2; end; suppose ex a,b st I = SubFrom(a,b); then consider a, b such that A3: I = SubFrom(a,b); thus thesis by A3; end; suppose ex a,b st I = MultBy(a,b); then consider a, b such that A4: I = MultBy(a,b); thus thesis by A4; end; suppose ex a,b st I = Divide(a,b); then consider a, b such that A5: I = Divide(a,b); thus thesis by A5; end; suppose ex i1 st I = goto i1; then consider i1 such that A6: I = goto i1; let k be natural number, s1, s2 be State of SCM such that s2 = s1 +* (IC SCM .--> (IC s1 + k)); IC Exec(I,s1) = i1 by A6,AMI_3:13; hence IC Exec(I,s1) + k = IC Exec(goto il.(SCM, locnum i1 + k),s2) by AMI_3:13 .= IC Exec(IncAddr(I,k), s2) by A6,Th57; end; suppose ex a,i1 st I = a=0_goto i1; then consider a, i1 such that A7: I = a=0_goto i1; let k be natural number, s1, s2 be State of SCM such that A8: s2 = s1 +* (IC SCM .--> (IC s1 + k)); A9: a <> IC SCM by AMI_5:20; dom (IC SCM .--> (IC s1 + k)) = {IC SCM} by FUNCOP_1:19; then not a in dom (IC SCM .--> (IC s1 + k)) by A9,TARSKI:def 1; then A10: s1.a = s2.a by A8,FUNCT_4:12; now per cases; suppose A11: s1.a = 0; then IC Exec(I,s1) = i1 by A7,AMI_3:14; hence IC Exec(I,s1) + k = IC Exec(a=0_goto il.(SCM, locnum i1 + k),s2) by A10,A11,AMI_3: 14 .= IC Exec(IncAddr(I,k), s2) by A7,Th58; end; suppose A12: s1.a <> 0; dom (IC SCM .--> (IC s1 + k)) = {IC SCM} by FUNCOP_1:19; then IC SCM in dom (IC SCM .--> (IC s1 + k)) by TARSKI:def 1; then A13: IC s2 = (IC SCM .--> (IC s1 + k)).IC SCM by A8,FUNCT_4:14 .= il.(SCM,locnum IC s1 + k) by FUNCOP_1:87; A14: IC Exec(I, s2) = Next IC s2 by A7,A10,A12,AMI_3:14 .= NextLoc IC s2 by Th56 .= il.(SCM,locnum IC s1 + k + 1) by A13,AMISTD_1:def 13 .= il.(SCM,locnum IC s1 + 1 + k); IC Exec(I,s1) = Next IC s1 by A7,A12,AMI_3:14 .= NextLoc IC s1 by Th56 .= il.(SCM,locnum IC s1 + 1); hence IC Exec(I,s1) + k = Exec(I,s2).IC SCM by A14,AMISTD_1:def 13 .= Next IC s2 by A7,A10,A12,AMI_3:14 .= IC Exec(a=0_goto il.(SCM, locnum i1 + k),s2) by A10,A12,AMI_3:14 .= IC Exec(IncAddr(I,k), s2) by A7,Th58; end; end; hence thesis; end; suppose ex a,i1 st I = a>0_goto i1; then consider a, i1 such that A15: I = a>0_goto i1; let k be natural number, s1, s2 be State of SCM such that A16: s2 = s1 +* (IC SCM .--> (IC s1 + k)); A17: a <> IC SCM by AMI_5:20; dom (IC SCM .--> (IC s1 + k)) = {IC SCM} by FUNCOP_1:19; then not a in dom (IC SCM .--> (IC s1 + k)) by A17,TARSKI:def 1; then A18: s1.a = s2.a by A16,FUNCT_4:12; now per cases; suppose A19: s1.a > 0; then IC Exec(I,s1) = i1 by A15,AMI_3:15; hence IC Exec(I,s1) + k = IC Exec(a>0_goto il.(SCM, locnum i1 + k),s2) by A18,A19,AMI_3: 15 .= IC Exec(IncAddr(I,k), s2) by A15,Th59; end; suppose A20: s1.a <= 0; dom (IC SCM .--> (IC s1 + k)) = {IC SCM} by FUNCOP_1:19; then IC SCM in dom (IC SCM .--> (IC s1 + k)) by TARSKI:def 1; then A21: IC s2 = (IC SCM .--> (IC s1 + k)).IC SCM by A16,FUNCT_4:14 .= il.(SCM,locnum IC s1 + k) by FUNCOP_1:87; A22: IC Exec(I, s2) = Next IC s2 by A15,A18,A20,AMI_3:15 .= NextLoc IC s2 by Th56 .= il.(SCM,locnum IC s1 + k + 1) by A21,AMISTD_1:def 13 .= il.(SCM,locnum IC s1 + 1 + k); IC Exec(I,s1) = Next IC s1 by A15,A20,AMI_3:15 .= NextLoc IC s1 by Th56 .= il.(SCM,locnum IC s1 + 1); hence IC Exec(I,s1) + k = Exec(I,s2).IC SCM by A22,AMISTD_1:def 13 .= Next IC s2 by A15,A18,A20,AMI_3:15 .= IC Exec(a>0_goto il.(SCM, locnum i1 + k),s2) by A18,A20,AMI_3:15 .= IC Exec(IncAddr(I,k), s2) by A15,Th59; end; end; hence thesis; end; end; let I be Instruction of SCM; let s1, s2 be State of SCM such that A23: s1, s2 equal_outside the Instruction-Locations of SCM; A24: dom Exec(I,s1) = dom the Object-Kind of SCM by CARD_3:18; then A25: dom Exec(I,s1) = dom Exec(I,s2) by CARD_3:18; A26: dom the Object-Kind of SCM = the carrier of SCM by FUNCT_2:def 1; A27: IC s1 = IC s2 by A23,AMI_1:121; per cases by AMI_3:69; suppose I = [0,{}]; hence thesis by A23,AMISTD_2:def 19,AMI_3:71; end; suppose ex a,b st I = a:=b; then consider a, b such that A28: I = a:=b; for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A29: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A30: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; per cases by A24,A26,A29,A30,Th3; suppose A31: x = IC SCM; hence Exec(I,s1).x = Next IC s1 by A28,AMI_3:8 .= Exec(I,s2).x by A27,A28,A31,AMI_3:8; end; suppose A32: x = a; hence Exec(I,s1).x = s1.b by A28,AMI_3:8 .= s2.b by A23,Th5 .= Exec(I,s2).x by A28,A32,AMI_3:8; end; suppose that A33: x is Data-Location and A34: x <> a; thus Exec(I,s1).x = s1.x by A28,A33,A34,AMI_3:8 .= s2.x by A23,A33,Th5 .= Exec(I,s2).x by A28,A33,A34,AMI_3:8; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; suppose ex a,b st I = AddTo(a,b); then consider a, b such that A35: I = AddTo(a,b); for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A36: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A37: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; per cases by A24,A26,A36,A37,Th3; suppose A38: x = IC SCM; hence Exec(I,s1).x = Next IC s1 by A35,AMI_3:9 .= Exec(I,s2).x by A27,A35,A38,AMI_3:9; end; suppose A39: x = a; hence Exec(I,s1).x = s1.a + s1.b by A35,AMI_3:9 .= s1.a + s2.b by A23,Th5 .= s2.a + s2.b by A23,Th5 .= Exec(I,s2).x by A35,A39,AMI_3:9; end; suppose that A40: x is Data-Location and A41: x <> a; thus Exec(I,s1).x = s1.x by A35,A40,A41,AMI_3:9 .= s2.x by A23,A40,Th5 .= Exec(I,s2).x by A35,A40,A41,AMI_3:9; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; suppose ex a,b st I = SubFrom(a,b); then consider a, b such that A42: I = SubFrom(a,b); for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A43: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A44: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; per cases by A24,A26,A43,A44,Th3; suppose A45: x = IC SCM; hence Exec(I,s1).x = Next IC s1 by A42,AMI_3:10 .= Exec(I,s2).x by A27,A42,A45,AMI_3:10; end; suppose A46: x = a; hence Exec(I,s1).x = s1.a - s1.b by A42,AMI_3:10 .= s1.a - s2.b by A23,Th5 .= s2.a - s2.b by A23,Th5 .= Exec(I,s2).x by A42,A46,AMI_3:10; end; suppose that A47: x is Data-Location and A48: x <> a; thus Exec(I,s1).x = s1.x by A42,A47,A48,AMI_3:10 .= s2.x by A23,A47,Th5 .= Exec(I,s2).x by A42,A47,A48,AMI_3:10; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; suppose ex a,b st I = MultBy(a,b); then consider a, b such that A49: I = MultBy(a,b); for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A50: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A51: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; per cases by A24,A26,A50,A51,Th3; suppose A52: x = IC SCM; hence Exec(I,s1).x = Next IC s1 by A49,AMI_3:11 .= Exec(I,s2).x by A27,A49,A52,AMI_3:11; end; suppose A53: x = a; hence Exec(I,s1).x = s1.a * s1.b by A49,AMI_3:11 .= s1.a * s2.b by A23,Th5 .= s2.a * s2.b by A23,Th5 .= Exec(I,s2).x by A49,A53,AMI_3:11; end; suppose that A54: x is Data-Location and A55: x <> a; thus Exec(I,s1).x = s1.x by A49,A54,A55,AMI_3:11 .= s2.x by A23,A54,Th5 .= Exec(I,s2).x by A49,A54,A55,AMI_3:11; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; suppose ex a,b st I = Divide(a,b); then consider a, b such that A56: I = Divide(a,b); for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A57: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A58: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; per cases by A24,A26,A57,A58,Th3; suppose A59: x = IC SCM; hence Exec(I,s1).x = Next IC s1 by A56,AMI_3:12 .= Exec(I,s2).x by A27,A56,A59,AMI_3:12; end; suppose A60: x is Data-Location; A61: s1.a = s2.a & s1.b = s2.b by A23,Th5; now let c be Data-Location; per cases; suppose A62: c = b; hence Exec(I,s1).c = s2.a mod s2.b by A56,A61,AMI_3:12 .= Exec(I,s2).c by A56,A62,AMI_3:12; end; suppose A63: c = a & c <> b; hence Exec(I,s1).c = s2.a div s2.b by A56,A61,AMI_3:12 .= Exec(I,s2).c by A56,A63,AMI_3:12; end; suppose A64: c <> a & c <> b; hence Exec(I,s1).c = s1.c by A56,AMI_3:12 .= s2.c by A23,Th5 .= Exec(I,s2).c by A56,A64,AMI_3:12; end; end; hence thesis by A60; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; suppose ex i1 st I = goto i1; then consider i1 such that A65: I = goto i1; for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A66: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A67: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; per cases by A24,A26,A66,A67,Th3; suppose A68: x = IC SCM; hence Exec(I,s1).x = i1 by A65,AMI_3:13 .= Exec(I,s2).x by A65,A68,AMI_3:13; end; suppose A69: x is Data-Location; hence Exec(I,s1).x = s1.x by A65,AMI_3:13 .= s2.x by A23,A69,Th5 .= Exec(I,s2).x by A65,A69,AMI_3:13; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; suppose ex a,i1 st I = a=0_goto i1; then consider a, i1 such that A70: I = a=0_goto i1; for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A71: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A72: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; A73: s1.a = s2.a by A23,Th5; per cases by A24,A26,A71,A72,Th3; suppose that A74: x = IC SCM and A75: s1.a = 0; thus Exec(I,s1).x = i1 by A70,A74,A75,AMI_3:14 .= Exec(I,s2).x by A70,A73,A74,A75,AMI_3:14; end; suppose that A76: x = IC SCM and A77: s1.a <> 0; thus Exec(I,s1).x = Next IC s1 by A70,A76,A77,AMI_3:14 .= Exec(I,s2).x by A27,A70,A73,A76,A77,AMI_3:14; end; suppose A78: x is Data-Location; hence Exec(I,s1).x = s1.x by A70,AMI_3:14 .= s2.x by A23,A78,Th5 .= Exec(I,s2).x by A70,A78,AMI_3:14; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; suppose ex a,i1 st I = a>0_goto i1; then consider a, i1 such that A79: I = a>0_goto i1; for x being set st x in dom Exec(I,s1) \ the Instruction-Locations of SCM holds Exec(I,s1).x = Exec(I,s2).x proof let x be set; assume A80: x in dom Exec(I,s1) \ the Instruction-Locations of SCM; then A81: not x in the Instruction-Locations of SCM by XBOOLE_0:def 4; A82: s1.a = s2.a by A23,Th5; per cases by A24,A26,A80,A81,Th3; suppose that A83: x = IC SCM and A84: s1.a > 0; thus Exec(I,s1).x = i1 by A79,A83,A84,AMI_3:15 .= Exec(I,s2).x by A79,A82,A83,A84,AMI_3:15; end; suppose that A85: x = IC SCM and A86: s1.a <= 0; thus Exec(I,s1).x = Next IC s1 by A79,A85,A86,AMI_3:15 .= Exec(I,s2).x by A27,A79,A82,A85,A86,AMI_3:15; end; suppose A87: x is Data-Location; hence Exec(I,s1).x = s1.x by A79,AMI_3:15 .= s2.x by A23,A87,Th5 .= Exec(I,s2).x by A79,A87,AMI_3:15; end; end; hence Exec(I,s1)|(dom Exec(I,s1) \ the Instruction-Locations of SCM) = Exec(I,s2)|(dom Exec(I,s2) \ the Instruction-Locations of SCM) by A25,FUNCT_1:165; end; end; end;