:: On the Decomposition of the States of SCM :: by Yasushi Tanaka :: :: Received November 23, 1993 :: Copyright (c) 1993 Association of Mizar Users environ vocabularies BOOLE, NAT_1, ARYTM_1, FUNCT_1, RELAT_1, FUNCT_4, AMI_3, AMI_1, AMI_2, GR_CY_1, FINSEQ_1, FINSET_1, TARSKI, CAT_1, FUNCOP_1, MCART_1, ORDINAL2, QC_LANG1, AMI_4, AMI_5, INT_1, ARYTM; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, XCMPLX_0, ZFMISC_1, MCART_1, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_4, INT_1, NAT_1, STRUCT_0, FINSET_1, FINSEQ_1, AMI_1, SCMNORM, AMI_2, AMI_3, AMI_4, XXREAL_0; constructors DOMAIN_1, XXREAL_0, NAT_1, FINSEQ_4, AMI_4, SCMNORM; registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FRAENKEL, NUMBERS, XREAL_0, INT_1, FINSEQ_1, CARD_3, AMI_1, AMI_2, AMI_3, FINSET_1, CARD_1; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; definitions AMI_1, TARSKI, AMI_3, FUNCOP_1, CARD_1, AMI_2, SCMNORM; theorems AMI_1, AMI_2, AMI_3, GRFUNC_1, NAT_1, CQC_LANG, TARSKI, FUNCOP_1, FUNCT_4, FUNCT_1, MCART_1, GR_CY_1, FUNCT_2, CARD_3, FINSET_1, ZFMISC_1, AMI_4, ENUMSET1, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, SYSREL, SCMNORM; begin canceled 17; reserve x,y for set; theorem Th18: for dl being Data-Location ex i being Element of NAT st dl = dl.i proof let dl be Data-Location; dl in SCM-Data-Loc by AMI_3:def 2; then consider x,y such that A1: x in {1} and A2: y in NAT and A3: dl = [x,y] by ZFMISC_1:103; reconsider k = y as Element of NAT by A2; take k; thus dl = dl.k by A1,A3,TARSKI:def 1; end; canceled; theorem Th20: for dl being Data-Location holds dl <> IC SCM proof let dl be Data-Location; consider i being Element of NAT such that A1: dl = dl.i by Th18; thus thesis by A1,AMI_3:57; end; canceled; theorem Th22: for il being Instruction-Location of SCM, dl being Data-Location holds il <> dl proof let il be Instruction-Location of SCM, dl be Data-Location; consider j being Element of NAT such that A2: dl = dl.j by Th18; thus il <> dl by A2,AMI_3:56; end; reserve i, j, k for Element of NAT; theorem the carrier of SCM = {IC SCM} \/ SCM-Data-Loc \/ NAT by AMI_3:4; theorem for s being State of SCM, d being Data-Location, l being Instruction-Location of SCM holds d in dom s & l in dom s proof let s be State of SCM, d be Data-Location, l be Instruction-Location of SCM; d in SCM-Data-Loc by AMI_3:def 2; then d in {IC SCM} \/ SCM-Data-Loc by XBOOLE_0:def 2; then d in {IC SCM} \/ SCM-Data-Loc \/ NAT by XBOOLE_0:def 2; hence d in dom s by AMI_1:79,AMI_3:4; l in NAT by AMI_1:def 4; then l in {IC SCM} \/ SCM-Data-Loc \/ NAT by XBOOLE_0:def 2; hence l in dom s by AMI_1:79,AMI_3:4; end; canceled; theorem for s1,s2 being State of SCM st IC(s1) = IC(s2) & (for a being Data-Location holds s1.a = s2.a) & (for i being Instruction-Location of SCM holds s1.i = s2.i) holds s1 = s2 proof let s1,s2 be State of SCM such that A1: IC(s1) = IC(s2) and A2: (for a being Data-Location holds s1.a = s2.a) and A3: (for i being Instruction-Location of SCM holds s1.i = s2.i); consider g1 being Function such that A4: s1 = g1 & dom g1 = dom SCM-OK & for x being set st x in dom SCM-OK holds g1.x in SCM-OK.x by CARD_3:def 5; consider g2 being Function such that A5: s2 = g2 & dom g2 = dom SCM-OK & for x being set st x in dom SCM-OK holds g2.x in SCM-OK.x by CARD_3:def 5; A6: SCM-Memory = dom g1 & SCM-Memory = dom g2 by A4,A5,FUNCT_2:def 1; now let x be set such that A7: x in SCM-Memory; A8: x in {IC SCM} \/ SCM-Data-Loc or x in NAT by A7,AMI_3:4,XBOOLE_0:def 2; per cases by A8,XBOOLE_0:def 2; suppose x in {IC SCM}; then x = IC SCM by TARSKI:def 1; hence g1.x = g2.x by A1,A4,A5; end; suppose x in SCM-Data-Loc; then x is Data-Location by AMI_3:def 2; hence g1.x = g2.x by A2,A4,A5; end; suppose x in NAT; then reconsider l = x as Instruction-Location of SCM by AMI_1:def 4; g1.l = g2.l by A3,A4,A5; hence g1.x = g2.x; end; end; hence s1 = s2 by A4,A5,A6,FUNCT_1:9; end; theorem for s being State of SCM holds SCM-Data-Loc c= dom s by SCMNORM:13,AMI_3:72; theorem Th28: for s being State of SCM holds NAT c= dom s proof let s be State of SCM; NAT c= {IC SCM} \/ SCM-Data-Loc \/ NAT by XBOOLE_1:10; hence NAT c= dom s by AMI_1:79,AMI_3:4; end; canceled; theorem for s being State of SCM holds dom (s|NAT) = NAT proof let s be State of SCM; NAT c= dom s by Th28; hence dom (s|NAT) = NAT by RELAT_1:91; end; theorem SCM-Data-Loc is not finite; theorem NAT is not finite; registration cluster SCM-Data-Loc -> infinite; coherence; end; registration let I be Instruction of SCM; cluster InsCode I -> natural; coherence proof dom [: NAT, (union {INT} \/ SCM-Memory)* :] = NAT by SYSREL:12; then A1: dom the Instructions of SCM c= NAT by RELAT_1:25; InsCode I in dom the Instructions of SCM; hence thesis by A1; end; end; definition canceled; let I be Instruction of SCM; func @I -> Element of SCM-Instr equals I; coherence; end; definition let loc be Element of NAT; func loc@ -> Instruction-Location of SCM equals loc; coherence by AMI_1:def 4; end; definition let loc be Element of SCM-Data-Loc; func loc@ -> Data-Location equals loc; coherence by AMI_3:def 2; end; reserve I,J,K for Element of Segm 9, a,a1 for Element of NAT, b,b1,c for Element of SCM-Data-Loc; canceled 3; theorem Th36: for l being Instruction of SCM holds InsCode(l) <= 8 proof let l be Instruction of SCM; l in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } or l in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then A1: l in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } or l in { [K,<*a1,b1*>] : K in { 7,8 } } or l in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; per cases by A1,XBOOLE_0:def 2; suppose l in { [SCM-Halt,{}] }; then l = [SCM-Halt,{}] by TARSKI:def 1; then l`1 = 0 by MCART_1:7; hence InsCode(l) <= 8; end; suppose l in { [J,<*a*>] : J = 6 }; then ex J,a st l = [J,<*a*>] & J = 6; then l`1 = 6 by MCART_1:7; hence InsCode(l) <= 8; end; suppose l in { [K,<*a1,b1*>] : K in { 7,8 } }; then ex K,a1,b1 st l = [K,<*a1,b1*>] & K in { 7,8 }; then l`1 in { 7,8 } by MCART_1:7; then l`1 = 7 or l`1 = 8 by TARSKI:def 2; hence InsCode(l) <= 8; end; suppose l in { [I,<*b,c*>] : I in { 1,2,3,4,5} }; then ex I,b,c st l = [I,<*b,c*>] & I in { 1,2,3,4,5}; then l`1 in { 1,2,3,4,5} by MCART_1:7; then l`1 = 1 or l`1 = 2 or l`1 = 3 or l`1 = 4 or l`1 = 5 by ENUMSET1:def 3; hence InsCode(l) <= 8; end; end; reserve a, b for Data-Location, loc for Instruction-Location of SCM; theorem Th37: InsCode (halt SCM) = 0 by AMI_3:71,MCART_1:7; reserve I,J,K for Element of Segm 9, a,a1 for Element of NAT, b,b1,c for Element of SCM-Data-Loc, da,db for Data-Location, loc for Instruction-Location of SCM; canceled 8; theorem Th46: for ins being Instruction of SCM st InsCode ins = 0 holds ins = halt SCM proof let ins be Instruction of SCM such that A1: InsCode ins = 0; A2: now assume ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} }; then consider I,b,c such that A3: ins = [I,<*b,c*>] and A4: I in { 1,2,3,4,5}; InsCode ins = I by A3,MCART_1:7; hence contradiction by A1,A4; end; A5: now assume ins in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A6: ins = [K,<*a1,b1*>] and A7: K in { 7,8 }; InsCode ins = K by A6,MCART_1:7; hence contradiction by A1,A7; end; A8: now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A9: ins = [J,<*a*>] and A10: J = 6; thus contradiction by A1,A9,A10, MCART_1:7; end; ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A2,XBOOLE_0:def 2; then ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A5,XBOOLE_0:def 2; then ins in {[SCM-Halt,{}]} by A8,XBOOLE_0:def 2; hence ins = halt SCM by AMI_3:71,TARSKI:def 1; end; theorem Th47: for ins being Instruction of SCM st InsCode ins = 1 holds ex da,db st ins = da:=db proof let ins be Instruction of SCM such that A1: InsCode ins = 1; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A4: ins = [K,<*a1,b1*>] and A5: K in { 7,8 }; InsCode ins = K by A4,MCART_1:7; hence contradiction by A1,A5,TARSKI:def 2; end; now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A6: ins = [J,<*a*>] and A7: J = 6; thus contradiction by A1,A6,A7, MCART_1:7; end; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A2,XBOOLE_0:def 2; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 2; then ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then consider I,b,c such that A8: ins = [I,<*b,c*>] and I in { 1,2,3,4,5}; reconsider da = b@ ,db = c@ as Data-Location; take da,db; thus ins = da:=db by A1,A8,MCART_1:7; end; theorem Th48: for ins being Instruction of SCM st InsCode ins = 2 holds ex da,db st ins = AddTo(da,db) proof let ins be Instruction of SCM such that A1: InsCode ins = 2; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A4: ins = [K,<*a1,b1*>] and A5: K in { 7,8 }; InsCode ins = K by A4,MCART_1:7; hence contradiction by A1,A5,TARSKI:def 2; end; now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A6: ins = [J,<*a*>] and A7: J = 6; thus contradiction by A1,A6,A7, MCART_1:7; end; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A2,XBOOLE_0:def 2; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 2; then ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then consider I,b,c such that A8: ins = [I,<*b,c*>] and I in { 1,2,3,4,5}; reconsider da = b@ ,db = c@ as Data-Location; take da,db; thus ins = AddTo(da,db) by A1,A8,MCART_1:7; end; theorem Th49: for ins being Instruction of SCM st InsCode ins = 3 holds ex da,db st ins = SubFrom(da,db) proof let ins be Instruction of SCM such that A1: InsCode ins = 3; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A4: ins = [K,<*a1,b1*>] and A5: K in { 7,8 }; InsCode ins = K by A4,MCART_1:7; hence contradiction by A1,A5,TARSKI:def 2; end; now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A6: ins = [J,<*a*>] and A7: J = 6; thus contradiction by A1,A6,A7, MCART_1:7; end; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A2,XBOOLE_0:def 2; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 2; then ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then consider I,b,c such that A8: ins = [I,<*b,c*>] and I in { 1,2,3,4,5}; reconsider da = b@ ,db = c@ as Data-Location; take da,db; thus ins = SubFrom(da,db) by A1,A8,MCART_1:7; end; theorem Th50: for ins being Instruction of SCM st InsCode ins = 4 holds ex da,db st ins = MultBy(da,db) proof let ins be Instruction of SCM such that A1: InsCode ins = 4; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A4: ins = [K,<*a1,b1*>] and A5: K in { 7,8 }; InsCode ins = K by A4,MCART_1:7; hence contradiction by A1,A5,TARSKI:def 2; end; now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A6: ins = [J,<*a*>] and A7: J = 6; thus contradiction by A1,A6,A7, MCART_1:7; end; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A2,XBOOLE_0:def 2; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 2; then ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then consider I,b,c such that A8: ins = [I,<*b,c*>] and I in { 1,2,3,4,5}; reconsider da = b@ ,db = c@ as Data-Location; take da,db; thus ins = MultBy(da,db) by A1,A8,MCART_1:7; end; theorem Th51: for ins being Instruction of SCM st InsCode ins = 5 holds ex da,db st ins = Divide(da,db) proof let ins be Instruction of SCM such that A1: InsCode ins = 5; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A4: ins = [K,<*a1,b1*>] and A5: K in { 7,8 }; InsCode ins = K by A4,MCART_1:7; hence contradiction by A1,A5,TARSKI:def 2; end; now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A6: ins = [J,<*a*>] and A7: J = 6; thus contradiction by A1,A6,A7, MCART_1:7; end; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A2,XBOOLE_0:def 2; then not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 2; then ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} } by XBOOLE_0:def 2; then consider I,b,c such that A8: ins = [I,<*b,c*>] and I in { 1,2,3,4,5}; reconsider da = b@ ,db = c@ as Data-Location; take da,db; thus ins = Divide (da,db) by A1,A8,MCART_1:7; end; theorem Th52: for ins being Instruction of SCM st InsCode ins = 6 holds ex loc st ins = goto loc proof let ins be Instruction of SCM such that A1: InsCode ins = 6; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [K,<*a1,b1*>] : K in { 7,8 } }; then consider K,a1,b1 such that A4: ins = [K,<*a1,b1*>] and A5: K in { 7,8 }; InsCode ins = K by A4,MCART_1:7; hence contradiction by A1,A5,TARSKI:def 2; end; now assume ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} }; then consider I,b,c such that A6: ins = [I,<*b,c*>] and A7: I in { 1,2,3,4,5}; InsCode ins = I by A6,MCART_1:7; hence contradiction by A1,A7,ENUMSET1:def 3; end; then ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by XBOOLE_0:def 2; then ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A3,XBOOLE_0:def 2; then ins in { [J,<*a*>] : J = 6 } by A2,XBOOLE_0:def 2; then consider J,a such that A8: ins = [J,<*a*>] and A9: J = 6; reconsider loc = a@ as Instruction-Location of SCM; take loc; thus ins = goto loc by A8,A9; end; theorem Th53: for ins being Instruction of SCM st InsCode ins = 7 holds ex loc,da st ins = da=0_goto loc proof let ins be Instruction of SCM such that A1: InsCode ins = 7; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A4: ins = [J,<*a*>] and A5: J = 6; thus contradiction by A1,A4,A5, MCART_1:7; end; A6: now assume ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} }; then consider I,b,c such that A7: ins = [I,<*b,c*>] and A8: I in { 1,2,3,4,5}; InsCode ins = I by A7,MCART_1:7; hence contradiction by A1,A8,ENUMSET1:def 3; end; A9: not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A2,A3,XBOOLE_0:def 2; ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A6,XBOOLE_0:def 2; then ins in { [K,<*a1,b1*>] : K in { 7,8 } } by A9,XBOOLE_0:def 2; then consider K,a1,b1 such that A10: ins = [K,<*a1,b1*>] and K in { 7,8 }; reconsider loc = a1@ as Instruction-Location of SCM; reconsider da = b1@ as Data-Location; take loc,da; thus ins = da=0_goto loc by A1,A10,MCART_1:7; end; theorem Th54: for ins being Instruction of SCM st InsCode ins = 8 holds ex loc,da st ins = da>0_goto loc proof let ins be Instruction of SCM such that A1: InsCode ins = 8; A2: not ins in { [SCM-Halt,{}] } by A1,Th37,AMI_3:71,TARSKI:def 1; A3: now assume ins in { [J,<*a*>] : J = 6 }; then consider J,a such that A4: ins = [J,<*a*>] and A5: J = 6; thus contradiction by A1,A4,A5, MCART_1:7; end; A6: now assume ins in { [I,<*b,c*>] : I in { 1,2,3,4,5} }; then consider I,b,c such that A7: ins = [I,<*b,c*>] and A8: I in { 1,2,3,4,5}; InsCode ins = I by A7,MCART_1:7; hence contradiction by A1,A8,ENUMSET1:def 3; end; A9: not ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } by A2,A3,XBOOLE_0:def 2; ins in { [SCM-Halt,{}] } \/ { [J,<*a*>] : J = 6 } \/ { [K,<*a1,b1*>] : K in { 7,8 } } by A6,XBOOLE_0:def 2; then ins in { [K,<*a1,b1*>] : K in { 7,8 } } by A9,XBOOLE_0:def 2; then consider K,a1,b1 such that A10: ins = [K,<*a1,b1*>] and K in { 7,8 }; reconsider loc = a1@ as Instruction-Location of SCM; reconsider da = b1@ as Data-Location; take loc,da; thus ins = da>0_goto loc by A1,A10,MCART_1:7; end; theorem for loc being Instruction-Location of SCM holds (@(goto loc)) jump_address = loc proof let loc be Instruction-Location of SCM; reconsider roku=6 as Element of Segm 9 by GR_CY_1:10; reconsider mk=loc as Element of NAT by AMI_1:def 4; @(goto loc) = [ roku, <*mk*>]; hence (@(goto loc)) jump_address = loc by AMI_2:24; end; theorem for loc being Instruction-Location of SCM, a being Data-Location holds (@(a=0_goto loc)) cjump_address = loc & (@(a=0_goto loc)) cond_address = a proof let loc be Instruction-Location of SCM, a be Data-Location; reconsider nana=7 as Element of Segm 9 by GR_CY_1:10; reconsider mk=loc as Element of NAT by AMI_1:def 4; reconsider aa=a as Element of SCM-Data-Loc by AMI_3:def 2; @(a=0_goto loc) = [ nana, <*mk,aa*>]; hence (@(a=0_goto loc)) cjump_address = loc & (@(a=0_goto loc)) cond_address = a by AMI_2:25; end; theorem for loc being Instruction-Location of SCM, a being Data-Location holds (@(a>0_goto loc)) cjump_address = loc & (@(a>0_goto loc)) cond_address = a proof let loc be Instruction-Location of SCM, a be Data-Location; reconsider hachi=8 as Element of Segm 9 by GR_CY_1:10; reconsider mk=loc as Element of NAT by AMI_1:def 4; reconsider aa=a as Element of SCM-Data-Loc by AMI_3:def 2; @(a>0_goto loc) = [ hachi, <*mk,aa*>]; hence (@(a>0_goto loc)) cjump_address = loc & (@(a>0_goto loc)) cond_address = a by AMI_2:25; end; theorem Th58: for s1,s2 being State of SCM st (s1 | (SCM-Data-Loc \/ {IC SCM})) = (s2 | (SCM-Data-Loc \/ {IC SCM})) for l being Instruction of SCM holds Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) proof let s1,s2 be State of SCM such that A1: (s1 | (SCM-Data-Loc \/ {IC SCM})) = (s2 | (SCM-Data-Loc \/ {IC SCM})); IC SCM in {IC SCM} by TARSKI:def 1; then A2: IC SCM in (SCM-Data-Loc \/ {IC SCM}) by XBOOLE_0:def 2; A3: (SCM-Data-Loc \/ {IC SCM}) c= the carrier of SCM by AMI_3:4,XBOOLE_1: 7; then (SCM-Data-Loc \/ {IC SCM}) c= dom s1 by AMI_1:79; then A4: IC SCM in dom (s1 | (SCM-Data-Loc \/ {IC SCM})) by A2,RELAT_1:91; (SCM-Data-Loc \/ {IC SCM}) c= dom s2 by A3,AMI_1:79; then A5: IC SCM in dom (s2 | (SCM-Data-Loc \/ {IC SCM})) by A2,RELAT_1:91; A6: IC s1 = (s2 | (SCM-Data-Loc \/ {IC SCM})).IC SCM by A1,A4,FUNCT_1:70 .= IC s2 by A5,FUNCT_1:70; let l be Instruction of SCM; A7: dom Exec(l,s1) = the carrier of SCM by AMI_1:79; A8: dom Exec(l,s2) = the carrier of SCM by AMI_1:79; A9: SCM-Data-Loc c= (SCM-Data-Loc \/ {IC SCM}) by XBOOLE_1:7; per cases by Th36,NAT_1:33; suppose InsCode (l) = 0; then A10: l = halt SCM by Th46; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = s2 | (SCM-Data-Loc \/ {IC SCM}) by A1,AMI_1:def 8 .= Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A10,AMI_1:def 8; end; suppose InsCode (l) = 1; then consider da,db such that A11: l = da:=db by Th47; da in SCM-Data-Loc by AMI_3:def 2; then A12: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46 .= (SCM-Data-Loc \ {da} ) \/ {da} by XBOOLE_1:39; A13: dom ((Exec (l,s1)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A7,RELAT_1:91; A14: dom ((Exec (l,s2)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A8,RELAT_1:91; for x being set st x in ((SCM-Data-Loc) \ {da}) holds (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s2) | (SCM-Data-Loc \ {da})).x proof let x be set; assume A15: x in ((SCM-Data-Loc) \ {da}); then A16: x in SCM-Data-Loc by XBOOLE_0:def 4; A17: not x in {da} by A15,XBOOLE_0:def 4; reconsider a = x as Data-Location by A16,AMI_3:def 2; A18: a <> da by A17,TARSKI:def 1; A19: a in (SCM-Data-Loc \/ {IC SCM}) by A16,XBOOLE_0:def 2; thus (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s1)).a by A15,FUNCT_1:72 .= s1.a by A11,A18,AMI_3:8 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A19,FUNCT_1:72 .= s2.a by A1,A19,FUNCT_1:72 .= (Exec (l,s2)).a by A11,A18,AMI_3:8 .= (Exec (l,s2) | (SCM-Data-Loc \ {da})).x by A15,FUNCT_1:72; end; then A20: Exec (l,s1) | (SCM-Data-Loc \ {da} ) = Exec (l,s2) | (SCM-Data-Loc \ {da} ) by A13,A14,FUNCT_1:9; A21: db in SCM-Data-Loc by AMI_3:def 2; Exec (l,s1).da = s1.db by A11,AMI_3:8 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).db by A9,A21,FUNCT_1:72 .= s2.db by A1,A9,A21,FUNCT_1:72 .= Exec (l,s2).da by A11,AMI_3:8; then Exec (l,s1) | {da} = Exec(l,s2) | {da} by A7,A8,GRFUNC_1:90; then A22: DataPart Exec (l,s1) = DataPart Exec (l,s2) by A12,A20,RELAT_1:185,AMI_3:72; Exec (l,s1).IC SCM = Next IC s1 by A11,AMI_3:8 .= Exec (l,s2).IC SCM by A6,A11,AMI_3:8; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A22,RELAT_1:185,AMI_3:72; end; suppose InsCode (l) = 2; then consider da,db such that A23: l = AddTo(da,db) by Th48; da in SCM-Data-Loc by AMI_3:def 2; then A24: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46 .= (SCM-Data-Loc \ {da} ) \/ {da} by XBOOLE_1:39; A25: dom ((Exec (l,s1)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A7,RELAT_1:91; A26: dom ((Exec (l,s2)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A8,RELAT_1:91; for x being set st x in ((SCM-Data-Loc) \ {da}) holds (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s2) | (SCM-Data-Loc \ {da})).x proof let x be set; assume A27: x in ((SCM-Data-Loc) \ {da}); then A28: x in SCM-Data-Loc by XBOOLE_0:def 4; A29: not x in {da} by A27,XBOOLE_0:def 4; reconsider a = x as Data-Location by A28,AMI_3:def 2; A30: a <> da by A29,TARSKI:def 1; A31: a in (SCM-Data-Loc \/ {IC SCM}) by A28,XBOOLE_0:def 2; thus (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s1)).a by A27,FUNCT_1:72 .= s1.a by A23,A30,AMI_3:9 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A31,FUNCT_1:72 .= s2.a by A1,A31,FUNCT_1:72 .= (Exec (l,s2)).a by A23,A30,AMI_3:9 .= (Exec (l,s2) | (SCM-Data-Loc \ {da})).x by A27,FUNCT_1:72; end; then A32: Exec (l,s1) | (SCM-Data-Loc \ {da} ) = Exec (l,s2) | (SCM-Data-Loc \ {da} ) by A25,A26,FUNCT_1:9; A33: db in SCM-Data-Loc by AMI_3:def 2; A34: da in SCM-Data-Loc by AMI_3:def 2; then A35: s1.da = (s1 | (SCM-Data-Loc \/ {IC SCM})).da by A9,FUNCT_1:72 .= s2.da by A1,A9,A34,FUNCT_1:72; A36: s1.db = (s1 | (SCM-Data-Loc \/ {IC SCM})).db by A9,A33,FUNCT_1:72 .= s2.db by A1,A9,A33,FUNCT_1:72; Exec (l,s1).da = s1.da + s1.db by A23,AMI_3:9 .= Exec (l,s2).da by A23,A35,A36,AMI_3:9; then Exec (l,s1) | {da} = Exec(l,s2) | {da} by A7,A8,GRFUNC_1:90; then A37: DataPart Exec (l,s1) = DataPart Exec (l,s2) by A24,A32,RELAT_1:185,AMI_3:72; Exec (l,s1).IC SCM = Next IC s1 by A23,AMI_3:9 .= Exec (l,s2).IC SCM by A6,A23,AMI_3:9; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A37,RELAT_1:185,AMI_3:72; end; suppose InsCode (l) = 3; then consider da,db such that A38: l = SubFrom(da,db) by Th49; da in SCM-Data-Loc by AMI_3:def 2; then A39: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46 .= (SCM-Data-Loc \ {da} ) \/ {da} by XBOOLE_1:39; A40: dom ((Exec (l,s1)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A7,RELAT_1:91; A41: dom ((Exec (l,s2)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A8,RELAT_1:91; for x being set st x in ((SCM-Data-Loc) \ {da}) holds (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s2) | (SCM-Data-Loc \ {da})).x proof let x be set; assume A42: x in ((SCM-Data-Loc) \ {da}); then A43: x in SCM-Data-Loc by XBOOLE_0:def 4; A44: not x in {da} by A42,XBOOLE_0:def 4; reconsider a = x as Data-Location by A43,AMI_3:def 2; A45: a <> da by A44,TARSKI:def 1; A46: a in (SCM-Data-Loc \/ {IC SCM}) by A43,XBOOLE_0:def 2; thus (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s1)).a by A42,FUNCT_1:72 .= s1.a by A38,A45,AMI_3:10 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A46,FUNCT_1:72 .= s2.a by A1,A46,FUNCT_1:72 .= (Exec (l,s2)).a by A38,A45,AMI_3:10 .= (Exec (l,s2) | (SCM-Data-Loc \ {da})).x by A42,FUNCT_1:72; end; then A47: Exec (l,s1) | (SCM-Data-Loc \ {da} ) = Exec (l,s2) | (SCM-Data-Loc \ {da} ) by A40,A41,FUNCT_1:9; A48: db in SCM-Data-Loc by AMI_3:def 2; A49: da in SCM-Data-Loc by AMI_3:def 2; then A50: s1.da = (s1 | (SCM-Data-Loc \/ {IC SCM})).da by A9,FUNCT_1:72 .= s2.da by A1,A9,A49,FUNCT_1:72; A51: s1.db = (s1 | (SCM-Data-Loc \/ {IC SCM})).db by A9,A48,FUNCT_1:72 .= s2.db by A1,A9,A48,FUNCT_1:72; Exec (l,s1).da = s1.da - s1.db by A38,AMI_3:10 .= Exec (l,s2).da by A38,A50,A51,AMI_3:10; then Exec (l,s1) | {da} = Exec(l,s2) | {da} by A7,A8,GRFUNC_1:90; then A52: DataPart Exec (l,s1) = DataPart Exec (l,s2) by A39,A47,RELAT_1:185,AMI_3:72; Exec (l,s1).IC SCM = Next IC s1 by A38,AMI_3:10 .= Exec (l,s2).IC SCM by A6,A38,AMI_3:10; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A52,RELAT_1:185,AMI_3:72; end; suppose InsCode (l) = 4; then consider da,db such that A53: l = MultBy(da,db) by Th50; da in SCM-Data-Loc by AMI_3:def 2; then A54: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46 .= (SCM-Data-Loc \ {da} ) \/ {da} by XBOOLE_1:39; A55: dom ((Exec (l,s1)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A7,RELAT_1:91; A56: dom ((Exec (l,s2)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A8,RELAT_1:91; for x being set st x in ((SCM-Data-Loc) \ {da}) holds (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s2) | (SCM-Data-Loc \ {da})).x proof let x be set; assume A57: x in ((SCM-Data-Loc) \ {da}); then A58: x in SCM-Data-Loc by XBOOLE_0:def 4; A59: not x in {da} by A57,XBOOLE_0:def 4; reconsider a = x as Data-Location by A58,AMI_3:def 2; A60: a <> da by A59,TARSKI:def 1; A61: a in (SCM-Data-Loc \/ {IC SCM}) by A58,XBOOLE_0:def 2; thus (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s1)).a by A57,FUNCT_1:72 .= s1.a by A53,A60,AMI_3:11 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A61,FUNCT_1:72 .= s2.a by A1,A61,FUNCT_1:72 .= (Exec (l,s2)).a by A53,A60,AMI_3:11 .= (Exec (l,s2) | (SCM-Data-Loc \ {da})).x by A57,FUNCT_1:72; end; then A62: Exec (l,s1) | (SCM-Data-Loc \ {da} ) = Exec (l,s2) | (SCM-Data-Loc \ {da} ) by A55,A56,FUNCT_1:9; A63: db in SCM-Data-Loc by AMI_3:def 2; A64: da in SCM-Data-Loc by AMI_3:def 2; then A65: s1.da = (s1 | (SCM-Data-Loc \/ {IC SCM})).da by A9,FUNCT_1:72 .= s2.da by A1,A9,A64,FUNCT_1:72; A66: s1.db = (s1 | (SCM-Data-Loc \/ {IC SCM})).db by A9,A63,FUNCT_1:72 .= s2.db by A1,A9,A63,FUNCT_1:72; Exec (l,s1).da = s1.da * s1.db by A53,AMI_3:11 .= Exec (l,s2).da by A53,A65,A66,AMI_3:11; then Exec (l,s1) | {da} = Exec(l,s2) | {da} by A7,A8,GRFUNC_1:90; then A67: DataPart Exec (l,s1) = DataPart Exec (l,s2) by A54,A62,RELAT_1:185,AMI_3:72; Exec (l,s1).IC SCM = Next IC s1 by A53,AMI_3:11 .= Exec (l,s2).IC SCM by A6,A53,AMI_3:11; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A67,RELAT_1:185,AMI_3:72; end; suppose InsCode (l) = 5; then consider da,db such that A68: l = Divide(da,db) by Th51; thus thesis proof per cases; suppose A69: da=db; da in SCM-Data-Loc by AMI_3:def 2; then A70: SCM-Data-Loc = SCM-Data-Loc \/ {da} by ZFMISC_1:46 .= (SCM-Data-Loc \ {da} ) \/ {da} by XBOOLE_1:39; A71: dom ((Exec (l,s1)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A7,RELAT_1:91; A72: dom ((Exec (l,s2)) | (SCM-Data-Loc \ {da})) = (SCM-Data-Loc \ {da}) by A8,RELAT_1:91; for x being set st x in ((SCM-Data-Loc) \ {da}) holds (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s2) | (SCM-Data-Loc \ {da})).x proof let x be set; assume A73: x in ((SCM-Data-Loc) \ {da}); then A74: x in SCM-Data-Loc by XBOOLE_0:def 4; A75: not x in {da} by A73,XBOOLE_0:def 4; reconsider a = x as Data-Location by A74,AMI_3:def 2; A76: a <> da by A75,TARSKI:def 1; A77: a in (SCM-Data-Loc \/ {IC SCM}) by A74,XBOOLE_0:def 2; thus (Exec (l,s1) | (SCM-Data-Loc \ {da})).x = (Exec (l,s1)).a by A73,FUNCT_1:72 .= s1.a by A68,A69,A76,AMI_3:12 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A77,FUNCT_1:72 .= s2.a by A1,A77,FUNCT_1:72 .= (Exec (l,s2)).a by A68,A69,A76,AMI_3:12 .= (Exec (l,s2) | (SCM-Data-Loc \ {da})).x by A73,FUNCT_1:72; end; then A78: Exec (l,s1) | (SCM-Data-Loc \ {da} ) = Exec (l,s2) | (SCM-Data-Loc \ {da} ) by A71,A72,FUNCT_1:9; A79: da in SCM-Data-Loc by AMI_3:def 2; then A80: s1.da = (s1 | (SCM-Data-Loc \/ {IC SCM})).da by A9,FUNCT_1 :72 .= s2.da by A1,A9,A79,FUNCT_1:72; Exec (l,s1).da = s1.da mod s1.da by A68,A69,AMI_3:12 .= Exec (l,s2).da by A68,A69,A80,AMI_3:12; then Exec (l,s1) | {da} = Exec(l,s2) | {da} by A7,A8,GRFUNC_1:90; then A81: DataPart Exec (l,s1) = DataPart Exec (l,s2) by A70,A78,RELAT_1:185,AMI_3:72; Exec (l,s1).IC SCM = Next IC s1 by A68,AMI_3:12 .= Exec (l,s2).IC SCM by A6,A68,AMI_3:12; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A81,RELAT_1:185,AMI_3:72; end; suppose A82: da <> db; A83: da in SCM-Data-Loc by AMI_3:def 2; db in SCM-Data-Loc by AMI_3:def 2; then A84: SCM-Data-Loc = SCM-Data-Loc \/ {da,db} by A83,ZFMISC_1:48 .= (SCM-Data-Loc \ {da,db} ) \/ {da,db} by XBOOLE_1:39; A85: dom ((Exec (l,s1)) | (SCM-Data-Loc \ {da,db})) = (SCM-Data-Loc \ {da ,db}) by A7,RELAT_1:91; A86: dom ((Exec (l,s2)) | (SCM-Data-Loc \ {da,db})) = (SCM-Data-Loc \ {da ,db}) by A8,RELAT_1:91; for x being set st x in ((SCM-Data-Loc) \ {da,db}) holds (Exec (l,s1) | (SCM-Data-Loc \ {da,db})).x = (Exec (l,s2) | (SCM-Data-Loc \ {da,db})).x proof let x be set; assume A87: x in ((SCM-Data-Loc) \ {da,db}); then A88: x in SCM-Data-Loc by XBOOLE_0:def 4; A89: not x in {da,db} by A87,XBOOLE_0:def 4; reconsider a = x as Data-Location by A88,AMI_3:def 2; A90: a <> da & a <> db by A89,TARSKI:def 2; A91: a in (SCM-Data-Loc \/ {IC SCM}) by A88,XBOOLE_0:def 2; thus (Exec (l,s1) | (SCM-Data-Loc \ {da,db})).x = (Exec (l,s1)).a by A87,FUNCT_1:72 .= s1.a by A68,A90,AMI_3:12 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A91,FUNCT_1:72 .= s2.a by A1,A91,FUNCT_1:72 .= (Exec (l,s2)).a by A68,A90,AMI_3:12 .= (Exec (l,s2) | (SCM-Data-Loc \ {da,db})).x by A87,FUNCT_1:72; end; then A92: Exec (l,s1) | (SCM-Data-Loc \ {da,db} ) = Exec (l,s2) | (SCM-Data-Loc \ {da,db} ) by A85,A86,FUNCT_1:9; A93: db in SCM-Data-Loc by AMI_3:def 2; A94: da in SCM-Data-Loc by AMI_3:def 2; then A95: s1.da = (s1 | (SCM-Data-Loc \/ {IC SCM})).da by A9,FUNCT_1 :72 .= s2.da by A1,A9,A94,FUNCT_1:72; A96: s1.db = (s1 | (SCM-Data-Loc \/ {IC SCM})).db by A9,A93,FUNCT_1:72 .= s2.db by A1,A9,A93,FUNCT_1:72; A97: Exec (l,s1).da = s1.da div s1.db by A68,A82,AMI_3:12 .= Exec (l,s2).da by A68,A82,A95,A96,AMI_3:12; Exec (l,s1).db = s1.da mod s1.db by A68,AMI_3:12 .= Exec (l,s2).db by A68,A95,A96,AMI_3:12; then Exec (l,s1) | {da,db} = Exec(l,s2) | {da,db} by A7,A8,A97,GRFUNC_1:91; then A98: DataPart Exec (l,s1) = DataPart Exec (l,s2) by A84,A92,RELAT_1:185,AMI_3:72; Exec (l,s1).IC SCM = Next IC s1 by A68,AMI_3:12 .= Exec (l,s2).IC SCM by A6,A68,AMI_3:12; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A98,RELAT_1:185,AMI_3:72; end; end; end; suppose InsCode (l) = 6; then consider loc such that A99: l = goto loc by Th52; A100: dom DataPart Exec(l,s1) = SCM-Data-Loc by A7,RELAT_1:91,AMI_3:72; A101: dom DataPart Exec (l,s2) = SCM-Data-Loc by A8,RELAT_1:91,AMI_3:72; for x being set st x in SCM-Data-Loc holds (DataPart Exec (l,s1)).x = (DataPart Exec (l,s2)).x proof let x be set; assume A102: x in SCM-Data-Loc; then reconsider a = x as Data-Location by AMI_3:def 2; A103: a in (SCM-Data-Loc \/ {IC SCM}) by A102,XBOOLE_0:def 2; thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A102,FUNCT_1:72,AMI_3:72 .= s1.a by A99,AMI_3:13 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A103,FUNCT_1:72 .= s2.a by A1,A103,FUNCT_1:72 .= (Exec (l,s2)).a by A99,AMI_3:13 .= (DataPart Exec (l,s2)).x by A102,FUNCT_1:72,AMI_3:72; end; then A104: Exec (l,s1) | (SCM-Data-Loc ) = Exec (l,s2) | (SCM-Data-Loc ) by A100,A101,FUNCT_1:9,AMI_3:72; Exec (l,s1).IC SCM = loc by A99,AMI_3:13 .= Exec (l,s2).IC SCM by A99,AMI_3:13; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A104,RELAT_1:185; end; suppose InsCode (l) = 7; then consider loc,da such that A105: l = da=0_goto loc by Th53; A106: dom (DataPart (Exec (l,s1))) = SCM-Data-Loc by A7,RELAT_1:91,AMI_3:72; A107: dom ((DataPart Exec (l,s2))) = SCM-Data-Loc by A8,RELAT_1:91,AMI_3:72; for x being set st x in SCM-Data-Loc holds (DataPart Exec (l,s1)).x = (DataPart Exec (l,s2)).x proof let x be set; assume A108: x in SCM-Data-Loc; then reconsider a = x as Data-Location by AMI_3:def 2; A109: a in (SCM-Data-Loc \/ {IC SCM}) by A108,XBOOLE_0:def 2; thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A108,FUNCT_1:72,AMI_3:72 .= s1.a by A105,AMI_3:14 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A109,FUNCT_1:72 .= s2.a by A1,A109,FUNCT_1:72 .= (Exec (l,s2)).a by A105,AMI_3:14 .= (DataPart Exec (l,s2)).x by A108,FUNCT_1:72,AMI_3:72; end; then A110: Exec (l,s1) | (SCM-Data-Loc ) = Exec (l,s2) | (SCM-Data-Loc ) by A106,A107,FUNCT_1:9,AMI_3:72; Exec (l,s1).IC SCM = Exec (l,s2).IC SCM proof A111: da in SCM-Data-Loc by AMI_3:def 2; then A112: s1.da = (s1 | (SCM-Data-Loc \/ {IC SCM})).da by A9,FUNCT_1:72 .= s2.da by A1,A9,A111,FUNCT_1:72; per cases; suppose A113: s1.da = 0; hence Exec (l,s1).IC SCM = loc by A105,AMI_3:14 .= Exec (l,s2).IC SCM by A105,A112,A113, AMI_3:14; end; suppose A114: s1.da <> 0; hence Exec (l,s1).IC SCM = Next IC s1 by A105,AMI_3:14 .= Exec (l,s2).IC SCM by A6,A105,A112,A114, AMI_3:14; end; end; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A110,RELAT_1:185; end; suppose InsCode (l) = 8; then consider loc,da such that A115: l = da>0_goto loc by Th54; A116: dom (DataPart Exec (l,s1)) = SCM-Data-Loc by A7,RELAT_1:91,AMI_3:72; A117: dom (DataPart Exec (l,s2)) = SCM-Data-Loc by A8,RELAT_1:91,AMI_3:72; for x being set st x in SCM-Data-Loc holds (DataPart Exec (l,s1)).x = (DataPart Exec (l,s2)).x proof let x be set; assume A118: x in SCM-Data-Loc; then reconsider a = x as Data-Location by AMI_3:def 2; A119: a in (SCM-Data-Loc \/ {IC SCM}) by A118,XBOOLE_0:def 2; thus (DataPart Exec (l,s1)).x = (Exec (l,s1)).a by A118,FUNCT_1:72,AMI_3:72 .= s1.a by A115,AMI_3:15 .= (s1 | (SCM-Data-Loc \/ {IC SCM})).a by A119,FUNCT_1:72 .= s2.a by A1,A119,FUNCT_1:72 .= (Exec (l,s2)).a by A115,AMI_3:15 .= (DataPart Exec (l,s2)).x by A118,FUNCT_1:72,AMI_3:72; end; then A120: Exec (l,s1) | (SCM-Data-Loc ) = Exec (l,s2) | (SCM-Data-Loc ) by A116,A117,FUNCT_1:9,AMI_3:72; Exec (l,s1).IC SCM = Exec (l,s2).IC SCM proof A121: da in SCM-Data-Loc by AMI_3:def 2; then A122: s1.da = (s1 | (SCM-Data-Loc \/ {IC SCM})).da by A9,FUNCT_1:72 .= s2.da by A1,A9,A121,FUNCT_1:72; per cases; suppose A123: s1.da > 0; hence Exec (l,s1).IC SCM = loc by A115,AMI_3:15 .= Exec (l,s2).IC SCM by A115,A122,A123, AMI_3:15; end; suppose A124: s1.da <= 0; hence Exec (l,s1).IC SCM = Next IC s1 by A115,AMI_3:15 .= Exec (l,s2).IC SCM by A6,A115,A122,A124, AMI_3:15; end; end; then Exec (l,s1) | {IC SCM} = Exec (l,s2) | {IC SCM} by A7,A8,GRFUNC_1:90; hence Exec (l,s1) | (SCM-Data-Loc \/ {IC SCM}) = Exec (l,s2) | (SCM-Data-Loc \/ {IC SCM}) by A120,RELAT_1:185; end; end; theorem Th59: for i being Instruction of SCM, s being State of SCM holds Exec (i, s) | NAT = s | NAT proof let i be Instruction of SCM, s be State of SCM; dom (Exec (i,s)) = the carrier of SCM by AMI_1:79; then A1: dom (Exec (i, s) | NAT) = NAT by RELAT_1:91; dom s = the carrier of SCM by AMI_1:79; then A2: dom (s | NAT) = NAT by RELAT_1:91; for x being set st x in NAT holds (Exec (i, s) | NAT).x = (s | NAT).x proof let x be set; assume x in NAT; then reconsider l = x as Instruction-Location of SCM by AMI_1:def 4; A3: l in NAT by AMI_1:def 4; hence (Exec (i, s) | NAT).x = (Exec (i, s)).l by FUNCT_1:72 .= s.l by AMI_1:def 13 .= (s | NAT).x by A3,FUNCT_1:72; end; hence Exec (i, s) | NAT = s | NAT by A1,A2,FUNCT_1:9; end; begin :: Finite partial states of SCM canceled 17; theorem for i being Instruction of SCM, s being State of SCM, p being programmed FinPartState of SCM holds Exec (i, s +* p) = Exec (i,s) +* p proof let i be Instruction of SCM, s be State of SCM, p be programmed FinPartState of SCM; A1: dom p c= NAT by AMI_1:def 40; now assume {IC SCM} meets NAT; then consider x being set such that A2: x in {IC SCM} and A3: x in NAT by XBOOLE_0:3; reconsider l = x as Instruction-Location of SCM by A3,AMI_1:def 4; l = IC SCM by A2,TARSKI:def 1; hence contradiction by AMI_1:48; end; then SCM-Data-Loc \/ {IC SCM} misses NAT by AMI_2:29,XBOOLE_1:70; then A4: SCM-Data-Loc \/ {IC SCM} misses dom p by A1,XBOOLE_1:63; then A5: s|(SCM-Data-Loc \/ {IC SCM}) = (s +* p) | (SCM-Data-Loc \/ {IC SCM}) by FUNCT_4:76; A6: (Exec(i,s) +* p)|(SCM-Data-Loc \/ {IC SCM}) = Exec(i,s)|(SCM-Data-Loc \/ {IC SCM}) by A4,FUNCT_4:76 .= Exec(i,s +* p) | (SCM-Data-Loc \/ {IC SCM}) by A5,Th58; A7: Exec (i, s +* p)|NAT = (s +* p)|NAT by Th59 .= s |NAT +* p|NAT by FUNCT_4:75 .= Exec (i,s) |NAT +* p|NAT by Th59 .= (Exec (i, s) +* p)|NAT by FUNCT_4:75; thus Exec (i, s +* p) = Exec (i, s +* p)| dom(Exec (i, s +* p)) by RELAT_1:97 .= Exec (i, s +* p)| ({IC SCM} \/ SCM-Data-Loc \/ NAT) by AMI_1:79,AMI_3:4 .= (Exec (i, s) +* p)| ({IC SCM} \/ SCM-Data-Loc) +* (Exec (i, s) +* p)|NAT by A6,A7,FUNCT_4:83 .= (Exec (i,s) +* p)| the carrier of SCM by AMI_3:4,FUNCT_4:83 .= (Exec (i,s) +* p)| dom(Exec (i, s) +* p) by AMI_1:79 .= Exec (i,s) +* p by RELAT_1:97; end; canceled 2; theorem for s being State of SCM, iloc being Instruction-Location of SCM, a being Data-Location holds s.a = (s +* Start-At iloc).a proof let s be State of SCM, iloc be Instruction-Location of SCM, a be Data-Location; A1: dom (Start-At iloc) = {IC SCM} by FUNCOP_1:19; a in the carrier of SCM; then a in dom s by AMI_1:79; then A2: a in dom s \/ dom (Start-At iloc) by XBOOLE_0:def 2; a <> IC SCM by Th20; then not a in {IC SCM} by TARSKI:def 1; hence s.a = (s +* Start-At iloc).a by A1,A2,FUNCT_4:def 1; end; begin :: Autonomic finite partial states of SCM canceled 2; theorem Th83: for p being autonomic FinPartState of SCM st DataPart p <> {} holds IC SCM in dom p proof let p be autonomic FinPartState of SCM; assume DataPart p <> {}; then A1: dom DataPart p <> {}; assume A2: not IC SCM in dom p; p is not autonomic proof consider d1 being Element of dom DataPart p; A3: d1 in dom DataPart p by A1; dom DataPart p c= the carrier of SCM by AMI_1:80; then reconsider d1 as Element of SCM by A3; dom DataPart p c= SCM-Data-Loc by RELAT_1:87,AMI_3:72; then reconsider d1 as Data-Location by A3,AMI_3:def 2; consider d2 being Element of SCM-Data-Loc \ dom p; not SCM-Data-Loc c= dom p; then A4: SCM-Data-Loc \ dom p <> {} by XBOOLE_1:37; then d2 in SCM-Data-Loc by XBOOLE_0:def 4; then reconsider d2 as Data-Location by AMI_3:def 2; consider il being Element of (NAT) \ dom p; not NAT c= dom p; then A5: (NAT) \ dom p <> {} by XBOOLE_1:37; then il is Element of NAT by XBOOLE_0:def 4; then reconsider il as Instruction-Location of SCM by AMI_1:def 4; set p1 = p +* ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il); set p2 = p +* ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il); consider s1 being State of SCM such that A6: p1 c= s1 by CARD_3:97; consider s2 being State of SCM such that A7: p2 c= s2 by CARD_3:97; take s1,s2; A8: not d2 in dom p by A4,XBOOLE_0:def 4; A9: not il in dom p by A5,XBOOLE_0:def 4; dom p misses {IC SCM} by A2,ZFMISC_1:56; then A10: dom p /\ {IC SCM} = {} by XBOOLE_0:def 7; dom p misses {d2} by A8,ZFMISC_1:56; then A11: dom p /\ {d2} = {} by XBOOLE_0:def 7; A12: dom p misses {il} by A9,ZFMISC_1:56; dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) = dom((il .--> (d1:=d2)) +* ( d2.--> 0)) \/ dom(Start-At il) by FUNCT_4:def 1 .= dom((il .--> (d1:=d2)) +* ( d2.--> 0)) \/ {IC SCM} by FUNCOP_1:19 .= dom(il .--> (d1:=d2)) \/ dom ( d2.--> 0) \/ {IC SCM} by FUNCT_4:def 1 .= {il} \/ dom ( d2.--> 0) \/ {IC SCM} by FUNCOP_1:19 .= {il} \/ {d2} \/ {IC SCM} by FUNCOP_1:19; then dom p /\ dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) = dom p /\ ({il} \/ {d2}) \/ {} by A10,XBOOLE_1:23 .= dom p /\ {il} \/ {} by A11,XBOOLE_1:23 .= {} by A12,XBOOLE_0:def 7; then dom p misses dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) by XBOOLE_0:def 7; then p c= p1 by FUNCT_4:33; hence p c= s1 by A6,XBOOLE_1:1; dom p misses {IC SCM} by A2,ZFMISC_1:56; then A13: dom p /\ {IC SCM} = {} by XBOOLE_0:def 7; dom p misses {d2} by A8,ZFMISC_1:56; then A14: dom p /\ {d2} = {} by XBOOLE_0:def 7; A15: dom p misses {il} by A9,ZFMISC_1:56; dom ((il .--> (d1:=d2)) +* (d2.--> 1) +* Start-At il) = dom((il .--> (d1:=d2)) +* ( d2.--> 1)) \/ dom(Start-At il) by FUNCT_4:def 1 .= dom((il .--> (d1:=d2)) +* ( d2.--> 1)) \/ {IC SCM} by FUNCOP_1:19 .= dom(il .--> (d1:=d2)) \/ dom ( d2.--> 1) \/ {IC SCM} by FUNCT_4:def 1 .= {il} \/ dom ( d2.--> 1) \/ {IC SCM} by FUNCOP_1:19 .= {il} \/ {d2} \/ {IC SCM} by FUNCOP_1:19; then dom p /\ dom ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il) = dom p /\ ({il} \/ {d2}) \/ {} by A13,XBOOLE_1:23 .= dom p /\ {il} \/ {} by A14,XBOOLE_1:23 .= {} by A15,XBOOLE_0:def 7; then dom p misses dom ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il) by XBOOLE_0:def 7; then p c= p2 by FUNCT_4:33; hence p c= s2 by A7,XBOOLE_1:1; take 1; DataPart p c= p by RELAT_1:88; then A16: dom DataPart p c= dom p by RELAT_1:25; dom ( Computation(s1,1)) = the carrier of SCM by AMI_1:79; then A17: dom ( Computation(s1,1)|dom p) = dom p by AMI_1:80,RELAT_1:91; A18: dom(Start-At il) = {IC SCM} by FUNCOP_1:19; then A19: IC SCM in dom (Start-At il) by TARSKI:def 1; A20: dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) = dom ((il .--> (d1:=d2)) +* ( d2.--> 0)) \/ dom(Start-At il) by FUNCT_4:def 1; then A21: IC SCM in dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) by A19,XBOOLE_0:def 2; A22: dom p1 = dom p \/ dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) by FUNCT_4:def 1; then IC SCM in dom p1 by A21,XBOOLE_0:def 2; then A23: IC s1 = p1.IC SCM by A6,GRFUNC_1:8 .= ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il).IC SCM by A21,FUNCT_4:14 .= (Start-At il).IC SCM by A19,FUNCT_4:14 .= il by FUNCOP_1:87; dom (il .--> (d1:=d2)) = {il} by FUNCOP_1:19; then A24: il in dom (il .--> (d1:=d2)) by TARSKI:def 1; A25: dom (d2 .--> 0) = {d2} by FUNCOP_1:19; il <> d2 by Th22; then A26: not il in dom (d2 .--> 0) by A25,TARSKI:def 1; A27: dom ((il .--> (d1:=d2)) +* ( d2.--> 0)) = dom (il .--> (d1:=d2)) \/ dom ( d2.--> 0) by FUNCT_4:def 1; then A28: il in dom ((il .--> (d1:=d2)) +* ( d2.--> 0)) by A24,XBOOLE_0:def 2; il <> IC SCM by AMI_1:48; then A29: not il in dom (Start-At il) by A18,TARSKI:def 1; A30: il in dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) by A20,A28,XBOOLE_0:def 2; then il in dom p1 by A22,XBOOLE_0:def 2; then A31: s1.il = p1.il by A6,GRFUNC_1:8 .= ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il).il by A30,FUNCT_4:14 .= ((il .--> (d1:=d2)) +* ( d2.--> 0)).il by A29,FUNCT_4:12 .= (il .--> (d1:=d2)).il by A26,FUNCT_4:12 .=(d1:=d2) by FUNCOP_1:87; A32: d2 in dom (d2 .--> 0) by A25,TARSKI:def 1; then A33: d2 in dom ((il .--> (d1:=d2)) +* ( d2.--> 0)) by A27,XBOOLE_0:def 2; d2 <> IC SCM by Th20; then A34: not d2 in dom (Start-At il) by A18,TARSKI:def 1; A35: d2 in dom ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il) by A20,A33,XBOOLE_0:def 2; then d2 in dom p1 by A22,XBOOLE_0:def 2; then A36: s1.d2 = p1.d2 by A6,GRFUNC_1:8 .= ((il .--> (d1:=d2)) +* ( d2.--> 0) +* Start-At il).d2 by A35,FUNCT_4:14 .= ((il .--> (d1:=d2)) +* ( d2.--> 0)).d2 by A34,FUNCT_4:12 .= (d2.--> 0).d2 by A32,FUNCT_4:14 .= 0 by FUNCOP_1:87; Computation(s1,0+1).d1 = (Following Computation(s1,0)).d1 by AMI_1:14 .= (Following s1).d1 by AMI_1:13 .= 0 by A23,A31,A36,AMI_3:8; then A37: ( Computation(s1,1)|dom p).d1 = 0 by A3,A16,A17,FUNCT_1:70; dom ( Computation(s2,1)) = the carrier of SCM by AMI_1:79; then A38: dom ( Computation(s2,1)|dom p) = dom p by AMI_1:80,RELAT_1:91; A39: dom(Start-At il) = {IC SCM} by FUNCOP_1:19; then A40: IC SCM in dom (Start-At il) by TARSKI:def 1; A41: dom ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il) = dom ((il .--> (d1:=d2)) +* ( d2.--> 1)) \/ dom(Start-At il) by FUNCT_4:def 1; then A42: IC SCM in dom ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il) by A40,XBOOLE_0:def 2; A43: dom p2 = dom p \/ dom ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il) by FUNCT_4:def 1; then IC SCM in dom p2 by A42,XBOOLE_0:def 2; then A44: IC s2 = p2.IC SCM by A7,GRFUNC_1:8 .= ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il).IC SCM by A42,FUNCT_4:14 .= (Start-At il).IC SCM by A40,FUNCT_4:14 .= il by FUNCOP_1:87; dom (il .--> (d1:=d2)) = {il} by FUNCOP_1:19; then A45: il in dom (il .--> (d1:=d2)) by TARSKI:def 1; A46: dom (d2 .--> 1) = {d2} by FUNCOP_1:19; il <> d2 by Th22; then A47: not il in dom (d2 .--> 1) by A46,TARSKI:def 1; A48: dom ((il .--> (d1:=d2)) +* ( d2.--> 1)) = dom (il .--> (d1:=d2)) \/ dom ( d2.--> 1) by FUNCT_4:def 1; then A49: il in dom ((il .--> (d1:=d2)) +* ( d2.--> 1)) by A45,XBOOLE_0:def 2; il <> IC SCM by AMI_1:48; then A50: not il in dom (Start-At il) by A39,TARSKI:def 1; A51: il in dom ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il) by A41,A49,XBOOLE_0:def 2; then il in dom p2 by A43,XBOOLE_0:def 2; then A52: s2.il = p2.il by A7,GRFUNC_1:8 .= ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il).il by A51,FUNCT_4:14 .= ((il .--> (d1:=d2)) +* ( d2.--> 1)).il by A50,FUNCT_4:12 .= (il .--> (d1:=d2)).il by A47,FUNCT_4:12 .=(d1:=d2) by FUNCOP_1:87; A53: d2 in dom (d2 .--> 1) by A46,TARSKI:def 1; then A54: d2 in dom ((il .--> (d1:=d2)) +* ( d2.--> 1)) by A48,XBOOLE_0:def 2; d2 <> IC SCM by Th20; then A55: not d2 in dom (Start-At il) by A39,TARSKI:def 1; A56: d2 in dom ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il) by A41,A54,XBOOLE_0:def 2; then d2 in dom p2 by A43,XBOOLE_0:def 2; then A57: s2.d2 = p2.d2 by A7,GRFUNC_1:8 .= ((il .--> (d1:=d2)) +* ( d2.--> 1) +* Start-At il).d2 by A56,FUNCT_4:14 .= ((il .--> (d1:=d2)) +* ( d2.--> 1)).d2 by A55,FUNCT_4:12 .= (d2.--> 1).d2 by A53,FUNCT_4:14 .= 1 by FUNCOP_1:87; Computation(s2,0+1).d1 = (Following Computation(s2,0)).d1 by AMI_1:14 .= (Following s2).d1 by AMI_1:13 .= 1 by A44,A52,A57,AMI_3:8; hence Computation(s1,1)|dom p <> Computation(s2,1)|dom p by A3,A16,A37 ,A38,FUNCT_1:70; end; hence contradiction; end; registration cluster autonomic non programmed FinPartState of SCM; existence proof take p = (Start-At il.0) +* Euclide-Algorithm +* (dl.0,dl.1) --> (1,1); (dl.0,dl.1) --> (1,1) in dom Euclide-Function by AMI_4:11; then consider s being FinPartState of SCM such that A1: (dl.0,dl.1) --> (1,1) = s and A2: (Start-At il.0) +* Euclide-Algorithm +* s is pre-program of SCM and Euclide-Function.s c= Result((Start-At il.0) +* Euclide-Algorithm +* s ) by AMI_1:def 29,AMI_4:13; thus p is autonomic by A1,A2; take IC SCM; A3: dom p = dom ((Start-At il.0) +* Euclide-Algorithm) \/ dom((dl.0,dl.1) --> (1,1)) by FUNCT_4:def 1; A4: dom ((Start-At il.0) +* Euclide-Algorithm) = dom (Start-At il.0) \/ dom (Euclide-Algorithm) by FUNCT_4:def 1; dom (Start-At il.0) = {IC SCM} by FUNCOP_1:19; then IC SCM in dom (Start-At il.0) by TARSKI:def 1; then IC SCM in dom ((Start-At il.0) +* Euclide-Algorithm) by A4, XBOOLE_0:def 2; hence IC SCM in dom p by A3,XBOOLE_0:def 2; assume IC SCM in NAT; hence contradiction by AMI_3:4; end; end; theorem Th84: for p being autonomic non programmed FinPartState of SCM holds IC SCM in dom p proof let p be autonomic non programmed FinPartState of SCM; A1: not dom p c= NAT by AMI_1:def 40; dom p = dom p /\ the carrier of SCM by AMI_1:80,XBOOLE_1:28 .= dom p /\ ({IC SCM} \/ SCM-Data-Loc) \/ dom p /\ NAT by AMI_3:4,XBOOLE_1:23; then dom p /\ ({IC SCM} \/ SCM-Data-Loc) <> {} by A1,XBOOLE_1:17; then A2: dom p /\ {IC SCM} \/ dom p /\ SCM-Data-Loc <> {} by XBOOLE_1:23; per cases by A2; suppose dom p /\ {IC SCM} <> {}; then dom p meets {IC SCM} by XBOOLE_0:def 7; hence IC SCM in dom p by ZFMISC_1:56; end; suppose A3: dom p /\ SCM-Data-Loc <> {}; DataPart p <> {} by A3,RELAT_1:60,90,AMI_3:72; hence IC SCM in dom p by Th83; end; end; theorem for p being autonomic FinPartState of SCM st IC SCM in dom p holds IC p in dom p proof let p be autonomic FinPartState of SCM; assume A1: IC SCM in dom p; assume A2: not IC p in dom p; set il = IC p; set p1 = p +* ((il .--> goto il.0)); set p2 = p +* ((il .--> goto il.1)); consider s1 being State of SCM such that A3: p1 c= s1 by CARD_3:97; consider s2 being State of SCM such that A4: p2 c= s2 by CARD_3:97; p is not autonomic proof A5: dom (il .--> (goto il.1)) = {il} by FUNCOP_1:19; A6: dom (il .--> (goto il.0)) = {il} by FUNCOP_1:19; take s1,s2; dom p misses {il} by A2,ZFMISC_1:56; then A7: p c= p1 & p c= p2 by A5,A6,FUNCT_4:33; hence p c= s1 & p c= s2 by A3,A4,XBOOLE_1:1; take 1; A8: il in dom (il .--> (goto il.1)) by A5,TARSKI:def 1; A9: il in dom (il .--> (goto il.0)) by A6,TARSKI:def 1; dom p1 = dom p \/ dom ((il .--> goto il.0)) by FUNCT_4:def 1; then il in dom p1 by A9,XBOOLE_0:def 2; then A10: s1.il = p1.il by A3,GRFUNC_1:8 .= ((il .--> goto il.0)).il by A9,FUNCT_4:14 .= goto il.0 by FUNCOP_1:87; dom p2 = dom p \/ dom ((il .--> goto il.1)) by FUNCT_4:def 1; then il in dom p2 by A8,XBOOLE_0:def 2; then A11: s2.il = p2.il by A4,GRFUNC_1:8 .= ((il .--> goto il.1)).il by A8,FUNCT_4:14 .= goto il.1 by FUNCOP_1:87; A12: (Following s1).IC SCM = Exec (goto il.0,s1).IC SCM by A1,A3,A7,A10,AMI_1:97,XBOOLE_1:1 .= il.0 by AMI_3:13; A13: (Following s2).IC SCM = Exec (goto il.1,s2).IC SCM by A1,A4,A7,A11,AMI_1:97,XBOOLE_1:1 .= il.1 by AMI_3:13; assume A14: Computation(s1,1)|dom p = Computation(s2,1)|dom p; A15: (Following(s1))|dom p = (Following ( Computation(s1,0)))|dom p by AMI_1:13 .= Computation(s1,0+1)|dom p by AMI_1:14 .= (Following ( Computation(s2,0)))|dom p by A14, AMI_1:14 .= (Following(s2))|dom p by AMI_1:13; il.0 = ((Following(s1))|dom p).IC SCM by A1,A12,FUNCT_1:72 .= il.1 by A1,A13,A15,FUNCT_1:72; hence contradiction; end; hence contradiction; end; theorem Th86: for p being autonomic non programmed FinPartState of SCM, s being State of SCM st p c= s for i being Element of NAT holds IC Computation(s,i) in dom ProgramPart(p) proof let p be autonomic non programmed FinPartState of SCM, s be State of SCM such that A1: p c= s; let i be Element of NAT; set Csi = Computation(s,i); set loc = IC Csi; reconsider ll = loc as Element of NAT by ORDINAL1:def 13; set loc1 = il.(ll+1); assume A3: not IC Computation(s,i) in dom ProgramPart(p); A4: loc in NAT by AMI_1:def 4; loc in dom ProgramPart p iff loc in dom p /\ NAT by FUNCT_1:68; then A5: not loc in dom p by A3,A4,XBOOLE_0:def 3; set p1 = p +* (loc .--> goto loc); set p2 = p +* (loc .--> goto loc1); A6: dom p1 = dom p \/ dom (loc .--> goto loc) & dom p2 = dom p \/ dom (loc .--> goto loc1) by FUNCT_4:def 1; A7: dom (loc .--> goto loc) = {loc} & dom (loc .--> goto loc1) = {loc} by FUNCOP_1:19; then A8: loc in dom (loc .--> goto loc) & loc in dom (loc .--> goto loc1) by TARSKI:def 1; then A9: loc in dom p1 & loc in dom p2 by A6,XBOOLE_0:def 2; consider s1 being State of SCM such that A10: p1 c= s1 by CARD_3:97; consider s2 being State of SCM such that A11: p2 c= s2 by CARD_3:97; set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); p is not autonomic proof take s1, s2; dom s1 = the carrier of SCM & dom s2 = the carrier of SCM by AMI_1:79; then A12: dom p c= dom s1 & dom p c= dom s2 by AMI_1:80; now let x be set; assume A13: x in dom p; then dom p misses dom (loc .--> goto loc) & x in dom p1 by A5,A6,A7,XBOOLE_0:def 2,ZFMISC_1:56; then p.x = p1.x & p1.x = s1.x by A10,A13,FUNCT_4:17,GRFUNC_1:8; hence p.x = s1.x; end; hence A14: p c= s1 by A12,GRFUNC_1:8; now let x be set; assume A15: x in dom p; then dom p misses dom (loc .--> goto loc1) & x in dom p2 by A5,A6,A7,XBOOLE_0:def 2,ZFMISC_1:56; then p.x = p2.x & p2.x = s2.x by A11,A15,FUNCT_4:17,GRFUNC_1:8; hence p.x = s2.x; end; hence A16: p c= s2 by A12,GRFUNC_1:8; (loc .--> goto loc).loc = goto loc & (loc .--> goto loc1).loc = goto loc1 by FUNCOP_1:87; then p1.loc = goto loc & p2.loc = goto loc1 by A8,FUNCT_4:14; then A17: s1.loc = goto loc & s2.loc = goto loc1 by A9,A10,A11,GRFUNC_1:8; take k = i+1; set Cs1k = Computation(s1,k); set Cs2k = Computation(s2,k); A18: Cs1k = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A19: Cs2k = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A20: Cs1i.loc = goto loc & Cs2i.loc = goto loc1 by A17,AMI_1:54; A21: (Cs1i|dom p) = (Csi|dom p) by A1,A14,AMI_1:def 25; A22: Cs1i.IC SCM = (Cs1i|dom p).IC SCM & Csi.IC SCM = (Csi|dom p).IC SCM by Th84,FUNCT_1:72; (Cs1i|dom p) = (Cs2i|dom p) by A14,A16,AMI_1:def 25; then Cs1i.IC SCM = loc & Cs2i.IC SCM = loc by A21,A22,Th84,FUNCT_1:72; then A23: Cs1k.IC SCM = loc & Cs2k.IC SCM = loc1 by A18,A19,A20,AMI_3:13; (Cs1k|dom p).IC SCM = Cs1k.IC SCM & (Cs2k|dom p).IC SCM = Cs2k.IC SCM by Th84,FUNCT_1:72; hence Cs1k|dom p <> Cs2k|dom p by A23; end; hence contradiction; end; theorem Th87: for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds IC Computation(s1,i) = IC Computation(s2,i) & I = CurInstr ( Computation(s2,i)) proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); thus A3: IC Cs1i = IC Cs2i proof assume A4: IC Computation(s1,i) <> IC Computation(s2,i); (Cs1i|dom p).IC SCM = Cs1i.IC SCM & (Cs2i|dom p).IC SCM = Cs2i.IC SCM by Th84,FUNCT_1:72; hence contradiction by A1,A4,AMI_1:def 25; end; thus I = CurInstr ( Computation(s2,i)) proof assume A5: I <> CurInstr ( Computation(s2,i)); A6: IC Cs1i in dom ProgramPart p & IC Cs2i in dom ProgramPart p by A1,Th86; ProgramPart p c= p by RELAT_1:88; then dom ProgramPart p c= dom p by GRFUNC_1:8; then (Cs1i|dom p).IC Cs1i = Cs1i.IC Cs1i & (Cs2i|dom p).IC Cs2i = Cs2i.IC Cs2i by A6,FUNCT_1:72; hence contradiction by A1,A2,A3,A5,AMI_1:def 25; end; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da, db being Data-Location, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = da := db & da in dom p implies Computation(s1,i).db = Computation(s2,i).db proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da, db be Data-Location, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A4: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A5: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A6: da in dom p implies (Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da = Cs2i1.da by FUNCT_1:72; assume A7: I = da := db & da in dom p & Computation(s1,i).db <> Computation(s2,i).db; then Cs1i1.da = Cs1i.db & Cs2i1.da = Cs2i.db by A2,A3,A4,A5,AMI_3:8; hence contradiction by A1,A6,A7,AMI_1:def 25; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da, db being Data-Location, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = AddTo(da, db) & da in dom p implies Computation(s1,i).da + Computation(s1,i).db = Computation(s2,i).da + Computation(s2,i).db proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da, db be Data-Location, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A4: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A5: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A6: da in dom p implies (Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da = Cs2i1.da by FUNCT_1:72; assume A7: I = AddTo(da, db) & da in dom p & Computation(s1,i).da + Computation(s1,i).db <> Computation(s2,i).da + Computation(s2,i).db; then Cs1i1.da = Cs1i.da + Cs1i.db & Cs2i1.da = Cs2i.da + Cs2i.db by A2,A3,A4,A5,AMI_3:9; hence contradiction by A1,A6,A7,AMI_1:def 25; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da, db being Data-Location, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = SubFrom(da, db) & da in dom p implies Computation(s1,i).da - Computation(s1,i).db = Computation(s2,i).da - Computation(s2,i).db proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da, db be Data-Location, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A4: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A5: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A6: da in dom p implies (Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da = Cs2i1.da by FUNCT_1:72; assume A7: I = SubFrom(da, db) & da in dom p & Computation(s1,i).da - Computation(s1,i).db <> Computation(s2,i).da - Computation(s2,i).db; then Cs1i1.da = Cs1i.da - Cs1i.db & Cs2i1.da = Cs2i.da - Cs2i.db by A2,A3,A4,A5,AMI_3:10; hence contradiction by A1,A6,A7,AMI_1:def 25; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da, db being Data-Location, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = MultBy(da, db) & da in dom p implies Computation(s1,i).da * Computation(s1,i).db = Computation(s2,i).da * Computation(s2,i).db proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da, db be Data-Location, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A4: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A5: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A6: da in dom p implies (Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da = Cs2i1.da by FUNCT_1:72; assume A7: I = MultBy(da, db) & da in dom p & Computation(s1,i).da * Computation(s1,i).db <> Computation(s2,i).da * Computation(s2,i).db; then Cs1i1.da = Cs1i.da * Cs1i.db & Cs2i1.da = Cs2i.da * Cs2i.db by A2,A3,A4,A5,AMI_3:11; hence contradiction by A1,A6,A7,AMI_1:def 25; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da, db being Data-Location, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = Divide(da, db) & da in dom p & da <> db implies Computation(s1,i).da div Computation(s1,i).db = Computation(s2,i).da div Computation(s2,i).db proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da, db be Data-Location, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A4: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A5: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A6: da in dom p implies (Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da = Cs2i1.da by FUNCT_1:72; assume A7: I = Divide(da, db) & da in dom p & da <> db & Computation(s1,i).da div Computation(s1,i).db <> Computation(s2,i).da div Computation(s2,i).db; then Cs1i1.da = Cs1i.da div Cs1i.db & Cs2i1.da = Cs2i.da div Cs2i.db by A2,A3,A4,A5,AMI_3:12; hence contradiction by A1,A6,A7,AMI_1:def 25; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da, db being Data-Location, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = Divide(da, db) & db in dom p & da <> db implies Computation(s1,i).da mod Computation(s1,i).db = Computation(s2,i).da mod Computation(s2,i).db proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da, db be Data-Location, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A4: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A5: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); assume A6: I = Divide(da, db) & db in dom p & da <> db & Computation(s1,i).da mod Computation(s1,i).db <> Computation(s2,i).da mod Computation(s2,i).db; then A7: (Cs1i1|dom p).db = Cs1i1.db & (Cs2i1|dom p).db = Cs2i1.db by FUNCT_1 :72; Cs1i1.db = Cs1i.da mod Cs1i.db & Cs2i1.db = Cs2i.da mod Cs2i.db by A2,A3,A4,A5,A6,AMI_3:12; hence contradiction by A1,A6,A7,AMI_1:def 25; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da being Data-Location, loc being Instruction-Location of SCM, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = da=0_goto loc & loc <> Next (IC Computation(s1,i)) implies ( Computation(s1,i).da = 0 iff Computation(s2,i).da = 0) proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da be Data-Location, loc be Instruction-Location of SCM, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A4: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A5: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A6: (Cs1i1|dom p).IC SCM = Cs1i1.IC SCM & (Cs2i1|dom p).IC SCM = Cs2i1.IC SCM by Th84,FUNCT_1:72; A7: (Cs1i1|dom p) = (Cs2i1|dom p) by A1,AMI_1:def 25; assume A8: I = da=0_goto loc & loc <> Next (IC Computation(s1,i)); A9: now assume Computation(s1,i).da = 0 & Computation(s2,i).da <> 0; then Cs1i1.IC SCM = loc & Cs2i1.IC SCM = Next IC Cs2i by A2,A3,A4,A5,A8,AMI_3:14; hence contradiction by A1,A2,A6,A7,A8,Th87; end; now assume Computation(s2,i).da = 0 & Computation(s1,i).da <> 0; then Cs2i1.IC SCM = loc & Cs1i1.IC SCM = Next IC Cs1i by A2,A3,A4,A5,A8,AMI_3:14; hence contradiction by A1,A6,A8,AMI_1:def 25; end; hence Computation(s1,i).da = 0 iff Computation(s2,i).da = 0 by A9; end; theorem for p being autonomic non programmed FinPartState of SCM, s1, s2 being State of SCM st p c= s1 & p c= s2 for i being Element of NAT, da being Data-Location, loc being Instruction-Location of SCM, I being Instruction of SCM st I = CurInstr ( Computation(s1,i)) holds I = da>0_goto loc & loc <> Next (IC Computation(s1,i)) implies ( Computation(s1,i).da > 0 iff Computation(s2,i).da > 0) proof let p be autonomic non programmed FinPartState of SCM, s1, s2 be State of SCM such that A1: p c= s1 & p c= s2; let i be Element of NAT, da be Data-Location, loc be Instruction-Location of SCM, I be Instruction of SCM such that A2: I = CurInstr ( Computation(s1,i)); set Cs1i = Computation(s1,i); set Cs2i = Computation(s2,i); A3: IC Cs1i = IC Cs2i by A1,A2,Th87; A4: I = CurInstr ( Computation(s2,i)) by A1,A2,Th87; set Cs1i1 = Computation(s1,i+1); set Cs2i1 = Computation(s2,i+1); A5: Cs1i1 = Following Cs1i by AMI_1:14 .= Exec (CurInstr Cs1i, Cs1i); A6: Cs2i1 = Following Cs2i by AMI_1:14 .= Exec (CurInstr Cs2i, Cs2i); A7: (Cs1i1|dom p).IC SCM = Cs1i1.IC SCM & (Cs2i1|dom p).IC SCM = Cs2i1.IC SCM by Th84,FUNCT_1:72; A8: (Cs1i1|dom p) = (Cs2i1|dom p) by A1,AMI_1:def 25; assume A9: I = da>0_goto loc & loc <> Next (IC Computation(s1,i)); A10: now assume A11: Computation(s1,i).da > 0 & Computation(s2,i).da <= 0; then Cs1i1.IC SCM = loc by A2,A5,A9,AMI_3:15; hence contradiction by A3,A4,A6,A7,A8,A9,A11,AMI_3:15; end; now assume A12: Computation(s2,i).da > 0 & Computation(s1,i).da <= 0; then Cs2i1.IC SCM = loc by A4,A6,A9,AMI_3:15; hence contradiction by A2,A5,A7,A8,A9,A12,AMI_3:15; end; hence Computation(s1,i).da > 0 iff Computation(s2,i).da > 0 by A10; end;