Copyright (c) 1996 Association of Mizar Users
environ vocabulary FUNCT_1, RELAT_1, FUNCT_4, BOOLE, FINSET_1, FINSUB_1, PROB_1, AMI_1, AMI_3, SCMFSA_2, FINSEQ_1, AMI_5, TARSKI, SCMFSA6A, RELOC, CAT_1, CARD_1, FUNCOP_1, SQUARE_1, AMI_2, ARYTM_1, NAT_1, ABSVALUE, FINSEQ_2, SF_MASTR, CARD_3, FINSEQ_4; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, FINSET_1, FINSUB_1, NAT_1, INT_1, STRUCT_0, GROUP_1, SETWISEO, CQC_LANG, CQC_SIM1, CARD_1, PROB_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_7, AMI_1, AMI_3, AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A; constructors FUNCT_7, SETWISEO, NAT_1, CQC_SIM1, AMI_5, SCMFSA_5, SCMFSA6A, FINSEQ_4, PROB_1, MEMBERED; clusters FINSET_1, FINSUB_1, RELSET_1, FUNCT_1, AMI_1, SCMFSA_2, SCMFSA_4, INT_1, CQC_LANG, AMI_3, FRAENKEL, MEMBERED, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, XBOOLE_0; theorems TARSKI, ENUMSET1, ZFMISC_1, FINSEQ_1, FINSUB_1, SETWISEO, NAT_1, FINSET_1, RELAT_1, GRFUNC_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_7, CQC_LANG, CQC_SIM1, CQC_THE1, CARD_3, CARD_4, AMI_1, AMI_3, AMI_5, SCMFSA_2, PROB_1, SCMFSA_4, SCMFSA_5, SCMFSA6A, RELSET_1, XBOOLE_0, XBOOLE_1; schemes NAT_1, DOMAIN_1, FUNCT_2; begin :: Preliminaries theorem Th1: for x, y, a being set, f being Function st f.x = f.y holds f.a = (f*((id dom f)+*(x,y))).a proof let x, y, a be set, f be Function; assume A1: f.x = f.y; A2: dom id dom f = dom f by RELAT_1:71; set g1 = (id dom f)+*(x,y); per cases; suppose not x in dom f; then id dom f = g1 by A2,FUNCT_7:def 3; hence f.a = (f*((id dom f)+*(x,y))).a by RELAT_1:78; suppose A3: x in dom f; then A4: g1.x = y by A2,FUNCT_7:33; A5: dom g1 = dom f by A2,FUNCT_7:32; thus f.a = (f*((id dom f)+*(x,y))).a proof per cases; suppose A6: a in dom f; now assume a <> x; then g1.a = (id dom f).a by FUNCT_7:34 .= a by A6,FUNCT_1:35; hence thesis by A5,A6,FUNCT_1:23; end; hence thesis by A1,A3,A4,A5,FUNCT_1:23; suppose A7: not a in dom f; dom (f*g1) c= dom g1 by RELAT_1:44; then not a in dom (f*g1) by A5,A7; then (f*g1).a = {} & f.a = {} by A7,FUNCT_1:def 4; hence thesis; end; end; theorem Th2: for x, y being set, f being Function st x in dom f implies y in dom f & f.x = f.y holds f = f*((id dom f)+*(x,y)) proof let x, y be set, f be Function; assume A1: x in dom f implies y in dom f & f.x = f.y; set g1 = (id dom f)+*(x,y); set g = f*g1; A2: dom id dom f = dom f by RELAT_1:71; per cases; suppose not x in dom f; then id dom f = g1 by A2,FUNCT_7:def 3; hence f = f*g1 by RELAT_1:78; suppose A3: x in dom f; A4: dom g1 = dom f by A2,FUNCT_7:32; now rng g1 c= dom f proof let b be set; assume b in rng g1; then consider a being set such that A5: a in dom g1 & b = g1.a by FUNCT_1:def 5; per cases; suppose a = x; hence b in dom f by A1,A2,A3,A5,FUNCT_7:33; suppose a <> x; then (id dom f).a = g1.a by FUNCT_7:34; hence b in dom f by A4,A5,FUNCT_1:35; end; hence dom f = dom g by A4,RELAT_1:46; let a be set; assume a in dom f; thus f.a = g.a by A1,A3,Th1; end; hence f = f*((id dom f)+*(x,y)) by FUNCT_1:9; end; definition let A be finite set, B be set; cluster -> finite Function of A, B; coherence proof let f be Function of A, B; dom f c= A by RELSET_1:12; then dom f is finite by FINSET_1:13; hence thesis by AMI_1:21; end; end; definition let A be finite set, B be set, f be Function of A, Fin B; cluster Union f -> finite; coherence proof now thus dom f is finite by AMI_1:21; let x be set; assume A1: x in dom f; then reconsider A as non empty set by FUNCT_2:def 1; reconsider x' = x as Element of A by A1,FUNCT_2:def 1; reconsider f' = f as Function of A, Fin B; f'.x' is finite; hence f.x is finite; end; hence Union f is finite by CARD_4:63; end; end; definition cluster Int-Locations -> non empty; coherence by SCMFSA_2:9; end; definition cluster FinSeq-Locations -> non empty; coherence by SCMFSA_2:10; end; begin :: Uniqueness of instruction components reserve a, b, c, a1, a2, b1, b2 for Int-Location, l, l1, l2 for Instruction-Location of SCM+FSA, f, g, f1, f2 for FinSeq-Location, i, j for Instruction of SCM+FSA; canceled 2; theorem Th5: a1:=b1 = a2:=b2 implies a1 = a2 & b1 = b2 proof assume A1: a1:=b1 = a2:=b2; consider A1, B1 being Data-Location such that A2: a1 = A1 & b1 = B1 & a1:=b1 = A1:=B1 by SCMFSA_2:def 11; consider A2, B2 being Data-Location such that A3: a2 = A2 & b2 = B2 & a2:=b2 = A2:=B2 by SCMFSA_2:def 11; A4: A1:=B1 = [ 1, <*A1, B1*>] by AMI_3:def 3; A5: A2:=B2 = [ 1, <*A2, B2*>] by AMI_3:def 3; <*A1,B1*>.1 = A1 & <*A1,B1*>.2 = B1 & <*A2,B2*>.1 = A2 & <*A2,B2*>.2 = B2 by FINSEQ_1:61; hence a1 = a2 & b1 = b2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem Th6: AddTo(a1,b1) = AddTo(a2,b2) implies a1 = a2 & b1 = b2 proof assume A1: AddTo(a1,b1) = AddTo(a2,b2); consider A1, B1 being Data-Location such that A2: a1 = A1 & b1 = B1 & AddTo(a1,b1) = AddTo(A1,B1) by SCMFSA_2:def 12; consider A2, B2 being Data-Location such that A3: a2 = A2 & b2 = B2 & AddTo(a2,b2) = AddTo(A2,B2) by SCMFSA_2:def 12; A4: AddTo(A1,B1) = [ 2, <*A1, B1*>] by AMI_3:def 4; A5: AddTo(A2,B2) = [ 2, <*A2, B2*>] by AMI_3:def 4; <*A1,B1*>.1 = A1 & <*A1,B1*>.2 = B1 & <*A2,B2*>.1 = A2 & <*A2,B2*>.2 = B2 by FINSEQ_1:61; hence a1 = a2 & b1 = b2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem Th7: SubFrom(a1,b1) = SubFrom(a2,b2) implies a1 = a2 & b1 = b2 proof assume A1: SubFrom(a1,b1) = SubFrom(a2,b2); consider A1, B1 being Data-Location such that A2: a1 = A1 & b1 = B1 & SubFrom(a1,b1) = SubFrom(A1,B1) by SCMFSA_2:def 13; consider A2, B2 being Data-Location such that A3: a2 = A2 & b2 = B2 & SubFrom(a2,b2) = SubFrom(A2,B2) by SCMFSA_2:def 13; A4: SubFrom(A1,B1) = [ 3, <*A1, B1*>] by AMI_3:def 5; A5: SubFrom(A2,B2) = [ 3, <*A2, B2*>] by AMI_3:def 5; <*A1,B1*>.1 = A1 & <*A1,B1*>.2 = B1 & <*A2,B2*>.1 = A2 & <*A2,B2*>.2 = B2 by FINSEQ_1:61; hence a1 = a2 & b1 = b2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem Th8: MultBy(a1,b1) = MultBy(a2,b2) implies a1 = a2 & b1 = b2 proof assume A1: MultBy(a1,b1) = MultBy(a2,b2); consider A1, B1 being Data-Location such that A2: a1 = A1 & b1 = B1 & MultBy(a1,b1) = MultBy(A1,B1) by SCMFSA_2:def 14; consider A2, B2 being Data-Location such that A3: a2 = A2 & b2 = B2 & MultBy(a2,b2) = MultBy(A2,B2) by SCMFSA_2:def 14; A4: MultBy(A1,B1) = [ 4, <*A1, B1*>] by AMI_3:def 6; A5: MultBy(A2,B2) = [ 4, <*A2, B2*>] by AMI_3:def 6; <*A1,B1*>.1 = A1 & <*A1,B1*>.2 = B1 & <*A2,B2*>.1 = A2 & <*A2,B2*>.2 = B2 by FINSEQ_1:61; hence a1 = a2 & b1 = b2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem Th9: Divide(a1,b1) = Divide(a2,b2) implies a1 = a2 & b1 = b2 proof assume A1: Divide(a1,b1) = Divide(a2,b2); consider A1, B1 being Data-Location such that A2: a1 = A1 & b1 = B1 & Divide(a1,b1) = Divide(A1,B1) by SCMFSA_2:def 15; consider A2, B2 being Data-Location such that A3: a2 = A2 & b2 = B2 & Divide(a2,b2) = Divide(A2,B2) by SCMFSA_2:def 15; A4: Divide(A1,B1) = [ 5, <*A1, B1*>] by AMI_3:def 7; A5: Divide(A2,B2) = [ 5, <*A2, B2*>] by AMI_3:def 7; <*A1,B1*>.1 = A1 & <*A1,B1*>.2 = B1 & <*A2,B2*>.1 = A2 & <*A2,B2*>.2 = B2 by FINSEQ_1:61; hence a1 = a2 & b1 = b2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem :: Lgoto6: goto l1 = goto l2 implies l1 = l2 proof assume A1: goto l1 = goto l2; consider L1 being Instruction-Location of SCM such that A2: l1 = L1 & goto l1 = goto L1 by SCMFSA_2:def 16; consider L2 being Instruction-Location of SCM such that A3: l2 = L2 & goto l2 = goto L2 by SCMFSA_2:def 16; A4: goto L1 = [ 6, <*L1*>] by AMI_3:def 8; A5: goto L2 = [ 6, <*L2*>] by AMI_3:def 8; <*L1*>.1 = L1 & <*L2*>.1 = L2 by FINSEQ_1:57; hence l1 = l2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem Th11: a1=0_goto l1 = a2=0_goto l2 implies a1 = a2 & l1 = l2 proof assume A1: a1=0_goto l1 = a2=0_goto l2; consider A1 being Data-Location, L1 being Instruction-Location of SCM such that A2: a1 = A1 & l1 = L1 & a1=0_goto l1 = A1=0_goto L1 by SCMFSA_2:def 17; consider A2 being Data-Location, L2 being Instruction-Location of SCM such that A3: a2 = A2 & l2 = L2 & a2=0_goto l2 = A2=0_goto L2 by SCMFSA_2:def 17; A4: A1=0_goto L1 = [ 7, <*L1, A1*>] by AMI_3:def 9; A5: A2=0_goto L2 = [ 7, <*L2, A2*>] by AMI_3:def 9; <*L1,A1*>.1 = L1 & <*L1,A1*>.2 = A1 & <*L2,A2*>.1 = L2 & <*L2,A2*>.2 = A2 by FINSEQ_1:61; hence a1 = a2 & l1 = l2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem Th12: a1>0_goto l1 = a2>0_goto l2 implies a1 = a2 & l1 = l2 proof assume A1: a1>0_goto l1 = a2>0_goto l2; consider A1 being Data-Location, L1 being Instruction-Location of SCM such that A2: a1 = A1 & l1 = L1 & a1>0_goto l1 = A1>0_goto L1 by SCMFSA_2:def 18; consider A2 being Data-Location, L2 being Instruction-Location of SCM such that A3: a2 = A2 & l2 = L2 & a2>0_goto l2 = A2>0_goto L2 by SCMFSA_2:def 18; A4: A1>0_goto L1 = [ 8, <*L1, A1*>] by AMI_3:def 10; A5: A2>0_goto L2 = [ 8, <*L2, A2*>] by AMI_3:def 10; <*L1,A1*>.1 = L1 & <*L1,A1*>.2 = A1 & <*L2,A2*>.1 = L2 & <*L2,A2*>.2 = A2 by FINSEQ_1:61; hence a1 = a2 & l1 = l2 by A1,A2,A3,A4,A5,ZFMISC_1:33; end; theorem Th13: b1:=(f1, a1) = b2:=(f2, a2) implies a1 = a2 & b1 = b2 & f1 = f2 proof assume A1: b1:=(f1, a1) = b2:=(f2, a2); A2: b1:=(f1, a1) = [9,<*b1,f1,a1*>] & b2:=(f2, a2) = [9,<*b2,f2,a2*>] by SCMFSA_2:def 19; <*b1,f1,a1*>.1 = b1 & <*b1,f1,a1*>.2 = f1 & <*b1,f1,a1*>.3 = a1 & <*b2,f2,a2*>.1 = b2 & <*b2,f2,a2*>.2 = f2 & <*b2,f2,a2*>.3 = a2 by FINSEQ_1:62; hence a1 = a2 & b1 = b2 & f1 = f2 by A1,A2,ZFMISC_1:33; end; theorem Th14: (f1, a1):=b1 = (f2, a2):=b2 implies a1 = a2 & b1 = b2 & f1 = f2 proof assume A1: (f1, a1):=b1 = (f2, a2):=b2; A2: (f1, a1):=b1 = [10,<*b1,f1,a1*>] & (f2, a2):=b2 = [10,<*b2,f2,a2*>] by SCMFSA_2:def 20; <*b1,f1,a1*>.1 = b1 & <*b1,f1,a1*>.2 = f1 & <*b1,f1,a1*>.3 = a1 & <*b2,f2,a2*>.1 = b2 & <*b2,f2,a2*>.2 = f2 & <*b2,f2,a2*>.3 = a2 by FINSEQ_1:62; hence a1 = a2 & b1 = b2 & f1 = f2 by A1,A2,ZFMISC_1:33; end; theorem Th15: a1:=len f1 = a2:=len f2 implies a1 = a2 & f1 = f2 proof assume A1: a1:=len f1 = a2:=len f2; A2: a1:=len f1 = [11,<*a1,f1*>] & a2:=len f2 = [11,<*a2,f2*>] by SCMFSA_2:def 21; <*a1,f1*>.1 = a1 & <*a1,f1*>.2 = f1 & <*a2,f2*>.1 = a2 & <*a2,f2*>.2 = f2 by FINSEQ_1:61; hence a1 = a2 & f1 = f2 by A1,A2,ZFMISC_1:33; end; theorem Th16: f1:=<0,...,0>a1 = f2:=<0,...,0>a2 implies a1 = a2 & f1 = f2 proof assume A1: f1:=<0,...,0>a1 = f2:=<0,...,0>a2; A2: f1:=<0,...,0>a1 = [12,<*a1,f1*>] & f2:=<0,...,0>a2 = [12,<*a2,f2*>] by SCMFSA_2:def 22; <*a1,f1*>.1 = a1 & <*a1,f1*>.2 = f1 & <*a2,f2*>.1 = a2 & <*a2,f2*>.2 = f2 by FINSEQ_1:61; hence a1 = a2 & f1 = f2 by A1,A2,ZFMISC_1:33; end; begin :: Integer locations used in a macro instruction definition let i be Instruction of SCM+FSA; func UsedIntLoc i -> Element of Fin Int-Locations means :Def1: ex a, b being Int-Location st (i = (a := b) or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b)) & it = {a, b} if InsCode i in {1, 2, 3, 4, 5}, ex a being Int-Location, l being Instruction-Location of SCM+FSA st (i = a=0_goto l or i = a>0_goto l) & it = {a} if InsCode i = 7 or InsCode i = 8, ex a, b being Int-Location, f being FinSeq-Location st (i = b := (f, a) or i = (f, a) := b) & it = {a, b} if InsCode i = 9 or InsCode i = 10, ex a being Int-Location, f being FinSeq-Location st (i = a :=len f or i = f :=<0,...,0>a) & it = {a} if InsCode i = 11 or InsCode i = 12 otherwise it = {}; existence proof hereby assume InsCode i in {1, 2, 3, 4, 5}; then InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 by ENUMSET1:23; then consider a, b being Int-Location such that A1: i = (a := b) or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b) by SCMFSA_2:54,55,56,57,58; reconsider a' = a, b' = b as Element of Int-Locations by SCMFSA_2:9; reconsider IT = {a', b'} as Element of Fin Int-Locations; take IT; take a, b; thus (i = (a := b) or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b)) & IT = {a, b} by A1; end; hereby assume InsCode i = 7 or InsCode i = 8; then consider l being Instruction-Location of SCM+FSA, a being Int-Location such that A2: i = a=0_goto l or i = a>0_goto l by SCMFSA_2:60,61; reconsider a' = a as Element of Int-Locations by SCMFSA_2:9; reconsider IT = {a'} as Element of Fin Int-Locations; take IT; take a, l; thus (i = a=0_goto l or i = a>0_goto l) & IT = {a} by A2; end; hereby assume InsCode i = 9 or InsCode i = 10; then consider a, b being Int-Location, f being FinSeq-Location such that A3: i = b := (f, a) or i = (f, a) := b by SCMFSA_2:62,63; reconsider a' = a, b' = b as Element of Int-Locations by SCMFSA_2:9; reconsider IT = {a', b'} as Element of Fin Int-Locations; take IT; take a, b, f; thus (i = b := (f, a) or i = (f, a) := b) & IT = {a, b} by A3; end; hereby assume InsCode i = 11 or InsCode i = 12; then consider a being Int-Location, f being FinSeq-Location such that A4: i = a :=len f or i = f :=<0,...,0>a by SCMFSA_2:64,65; reconsider a' = a as Element of Int-Locations by SCMFSA_2:9; reconsider IT = {a'} as Element of Fin Int-Locations; take IT; take a, f; thus (i = a :=len f or i = f :=<0,...,0>a) & IT = {a} by A4; end; {} in Fin Int-Locations by FINSUB_1:18; hence thesis; end; uniqueness proof let it1, it2 be Element of Fin Int-Locations; hereby assume InsCode i in {1, 2, 3, 4, 5}; given a1, b1 being Int-Location such that A5: (i = (a1 := b1) or i = AddTo(a1, b1) or i = SubFrom(a1, b1) or i = MultBy(a1, b1) or i = Divide(a1, b1)) & it1 = {a1, b1}; given a2, b2 being Int-Location such that A6: (i = (a2 := b2) or i = AddTo(a2, b2) or i = SubFrom(a2, b2) or i = MultBy(a2, b2) or i = Divide(a2, b2)) & it2 = {a2, b2}; A7: i = AddTo(a1, b1) or i = AddTo(a2, b2) implies InsCode i = 2 by SCMFSA_2:43; A8: i = SubFrom(a1, b1) or i = SubFrom(a2, b2) implies InsCode i = 3 by SCMFSA_2:44; A9: i = MultBy(a1, b1) or i = MultBy(a2, b2) implies InsCode i = 4 by SCMFSA_2:45; A10: i = Divide(a1, b1) or i = Divide(a2, b2) implies InsCode i = 5 by SCMFSA_2:46; per cases by A5,A6,A7,A8,A9,A10,SCMFSA_2:42; suppose i = (a1 := b1) & i = (a2 := b2); then a1 = a2 & b1 = b2 by Th5; hence it1 = it2 by A5,A6; suppose i = AddTo(a1, b1) & i = AddTo(a2, b2); then a1 = a2 & b1 = b2 by Th6; hence it1 = it2 by A5,A6; suppose i = SubFrom(a1, b1) & i = SubFrom(a2, b2); then a1 = a2 & b1 = b2 by Th7; hence it1 = it2 by A5,A6; suppose i = MultBy(a1, b1) & i = MultBy(a2, b2); then a1 = a2 & b1 = b2 by Th8; hence it1 = it2 by A5,A6; suppose i = Divide(a1, b1) & i = Divide(a2, b2); then a1 = a2 & b1 = b2 by Th9; hence it1 = it2 by A5,A6; end; hereby assume InsCode i = 7 or InsCode i = 8; given a1 being Int-Location, l1 being Instruction-Location of SCM+FSA such that A11: (i = a1=0_goto l1 or i = a1>0_goto l1) & it1 = {a1}; given a2 being Int-Location, l2 being Instruction-Location of SCM+FSA such that A12: (i = a2=0_goto l2 or i = a2>0_goto l2) & it2 = {a2}; A13: i = a1>0_goto l1 or i = a2>0_goto l2 implies InsCode i = 8 by SCMFSA_2:49; per cases by A11,A12,A13,SCMFSA_2:48; suppose i = a1=0_goto l1 & i = a2=0_goto l2; hence it1 = it2 by A11,A12, Th11; suppose i = a1>0_goto l1 & i = a2>0_goto l2; hence it1 = it2 by A11,A12, Th12; end; hereby assume InsCode i = 9 or InsCode i = 10; given a1, b1 being Int-Location, f1 being FinSeq-Location such that A14: (i = b1 := (f1, a1) or i = (f1, a1) := b1) & it1 = {a1, b1}; given a2, b2 being Int-Location, f2 being FinSeq-Location such that A15: (i = b2 := (f2, a2) or i = (f2, a2) := b2) & it2 = {a2, b2}; A16: i = (f1, a1) := b1 or i = (f2, a2) := b2 implies InsCode i = 10 by SCMFSA_2:51; per cases by A14,A15,A16,SCMFSA_2:50; suppose i = b1 := (f1, a1) & i = b2 := (f2, a2); then a1 = a2 & b1 = b2 by Th13; hence it1 = it2 by A14,A15; suppose i = (f1, a1) := b1 & i = (f2, a2) := b2; then a1 = a2 & b1 = b2 by Th14; hence it1 = it2 by A14,A15; end; hereby assume InsCode i = 11 or InsCode i = 12; given a1 being Int-Location, f1 being FinSeq-Location such that A17: (i = a1 :=len f1 or i = f1 :=<0,...,0>a1) & it1 = {a1}; given a2 being Int-Location, f2 being FinSeq-Location such that A18: (i = a2 :=len f2 or i = f2 :=<0,...,0>a2) & it2 = {a2}; A19: i = f1 :=<0,...,0>a1 or i = f2 :=<0,...,0>a2 implies InsCode i = 12 by SCMFSA_2:53; per cases by A17,A18,A19,SCMFSA_2:52; suppose i = a1 :=len f1 & i = a2 :=len f2; hence it1 = it2 by A17,A18,Th15 ; suppose i = f1 :=<0,...,0>a1 & i = f2 :=<0,...,0>a2; hence it1 = it2 by A17,A18,Th16; end; thus thesis; end; consistency by ENUMSET1:23; end; theorem Th17: UsedIntLoc halt SCM+FSA = {} proof not 0 in {1, 2, 3, 4, 5} by ENUMSET1:23; hence UsedIntLoc halt SCM+FSA = {} by Def1,SCMFSA_2:124; end; theorem Th18: i = a:=b or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b) implies UsedIntLoc i = {a, b} proof assume A1: i = a:=b or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b); a in Int-Locations & b in Int-Locations by SCMFSA_2:9; then {a, b} c= Int-Locations by ZFMISC_1:38; then reconsider ab = {a, b} as Element of Fin Int-Locations by FINSUB_1:def 5; InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 by A1,SCMFSA_2:42,43,44,45,46; then InsCode i in {1, 2, 3, 4, 5} by ENUMSET1:24; then UsedIntLoc i = ab by A1,Def1; hence UsedIntLoc i = {a, b}; end; theorem Th19: UsedIntLoc goto l = {} proof A1: InsCode goto l = 6 by SCMFSA_2:47; not 6 in {1, 2, 3, 4, 5} by ENUMSET1:23; hence UsedIntLoc goto l = {} by A1,Def1; end; theorem Th20: i = a=0_goto l or i = a>0_goto l implies UsedIntLoc i = {a} proof assume A1: i = a=0_goto l or i = a>0_goto l; a in Int-Locations by SCMFSA_2:9; then {a} c= Int-Locations by ZFMISC_1:37; then reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def 5; InsCode i = 7 or InsCode i = 8 by A1,SCMFSA_2:48,49; then UsedIntLoc i = ab by A1,Def1; hence UsedIntLoc i = {a}; end; theorem Th21: i = b := (f, a) or i = (f, a) := b implies UsedIntLoc i = {a, b} proof assume A1: i = b := (f, a) or i = (f, a) := b; a in Int-Locations & b in Int-Locations by SCMFSA_2:9; then {a, b} c= Int-Locations by ZFMISC_1:38; then reconsider ab = {a, b} as Element of Fin Int-Locations by FINSUB_1:def 5; InsCode i = 9 or InsCode i = 10 by A1,SCMFSA_2:50,51; then UsedIntLoc i = ab by A1,Def1; hence UsedIntLoc i = {a, b}; end; theorem Th22: i = a :=len f or i = f :=<0,...,0>a implies UsedIntLoc i = {a} proof assume A1: i = a :=len f or i = f :=<0,...,0>a; a in Int-Locations by SCMFSA_2:9; then {a} c= Int-Locations by ZFMISC_1:37; then reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def 5; InsCode i = 11 or InsCode i = 12 by A1,SCMFSA_2:52,53; then UsedIntLoc i = ab by A1,Def1; hence UsedIntLoc i = {a}; end; definition let p be programmed FinPartState of SCM+FSA; func UsedIntLoc p -> Subset of Int-Locations means :Def2: ex UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations st (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & it = Union (UIL * p); existence proof defpred P[set,set] means ex I being Instruction of SCM+FSA st $1 = I & $2 = UsedIntLoc I; A1: for e being Element of the Instructions of SCM+FSA ex u being Element of Fin Int-Locations st P[e,u] proof let e be Element of the Instructions of SCM+FSA; reconsider f = e as Instruction of SCM+FSA ; reconsider u = UsedIntLoc f as Element of Fin Int-Locations; take u, f; thus thesis; end; consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A2: for i being Element of the Instructions of SCM+FSA holds P[i,UIL.i] from FuncExD(A1); set IT = Union (UIL * p); reconsider dp = dom p as finite set by AMI_1:21; rng p c= the Instructions of SCM+FSA by SCMFSA_4:1; then reconsider p' = p as Function of dp, the Instructions of SCM+FSA by FUNCT_2:4; reconsider Up = UIL * p' as Function of dp, Fin Int-Locations; A3: IT = union rng Up by PROB_1:def 3; A4: rng Up c= Fin Int-Locations by RELSET_1:12; Fin Int-Locations c= bool Int-Locations by FINSUB_1:26; then rng Up c= bool Int-Locations by A4,XBOOLE_1:1; then A5: union rng Up c= union bool Int-Locations by ZFMISC_1:95; take IT; thus IT is Subset of Int-Locations by A3,A5,ZFMISC_1:99; take UIL; hereby let i be Instruction of SCM+FSA; P[i,UIL.i] by A2; hence UIL.i = UsedIntLoc i; end; thus thesis; end; uniqueness proof let IT1, IT2 be Subset of Int-Locations; given UIL1 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A6: (for i being Instruction of SCM+FSA holds UIL1.i = UsedIntLoc i) & IT1 = Union (UIL1 * p); given UIL2 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A7: (for i being Instruction of SCM+FSA holds UIL2.i = UsedIntLoc i) & IT2 = Union (UIL2 * p); for c be Element of the Instructions of SCM+FSA holds UIL1.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL1.c = UsedIntLoc d by A6 .= UIL2.c by A7; end; hence IT1 = IT2 by A6,A7,FUNCT_2:113; end; end; definition let p be programmed FinPartState of SCM+FSA; cluster UsedIntLoc p -> finite; coherence proof consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc p = Union (UIL * p) by Def2; reconsider dp = dom p as finite set by AMI_1:21; rng p c= the Instructions of SCM+FSA by SCMFSA_4:1; then reconsider p' = p as Function of dp, the Instructions of SCM+FSA by FUNCT_2:4; reconsider Up = UIL * p' as Function of dp, Fin Int-Locations; Union Up is finite; hence thesis by A1; end; end; reserve p, r for programmed FinPartState of SCM+FSA, I, J for Macro-Instruction, k, m, n for Nat; theorem Th23: i in rng p implies UsedIntLoc i c= UsedIntLoc p proof assume i in rng p; then consider x being set such that A1: x in dom p & i = p.x by FUNCT_1:def 5; consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc p = Union (UIL * p) by Def2; A3: (UIL * p).x = UIL.i by A1,FUNCT_1:23 .= UsedIntLoc i by A2; dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then x in dom (UIL * p) by A1,FUNCT_1:21; then A4: (UIL * p).x in rng (UIL * p) by FUNCT_1:def 5; UsedIntLoc p = union rng (UIL * p) by A2,PROB_1:def 3; hence UsedIntLoc i c= UsedIntLoc p by A3,A4,ZFMISC_1:92; end; theorem :: UFP1: UsedIntLoc (p +* r) c= (UsedIntLoc p) \/ (UsedIntLoc r) proof consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc (p +* r) = Union (UIL * (p +* r)) by Def2; consider UIL1 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL1.i = UsedIntLoc i) & UsedIntLoc p = Union (UIL1 * p) by Def2; consider UIL2 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A3: (for i being Instruction of SCM+FSA holds UIL2.i = UsedIntLoc i) & UsedIntLoc r = Union (UIL2 * r) by Def2; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL1.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedIntLoc d by A1 .= UIL1.c by A2; end; then A4: UIL=UIL1 by FUNCT_2:113; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedIntLoc d by A1 .= UIL2.c by A3; end; then A5: UIL=UIL2 by FUNCT_2:113; A6: Union (UIL * (p +* r)) = union rng (UIL * (p +* r)) by PROB_1:def 3; A7: Union (UIL * p) = union rng (UIL * p) by PROB_1:def 3; A8: Union (UIL * r) = union rng (UIL * r) by PROB_1:def 3; dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then rng p c= dom UIL & rng r c= dom UIL by SCMFSA_4:1; then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:10; then rng (UIL * (p +* r)) c= rng (UIL * p) \/ rng (UIL * r) by FUNCT_4:18; then union rng (UIL * (p +* r)) c= union (rng (UIL * p) \/ rng (UIL * r)) by ZFMISC_1:95; hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,ZFMISC_1:96; end; theorem Th25: dom p misses dom r implies UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r) proof consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc (p +* r) = Union (UIL * (p +* r)) by Def2; consider UIL1 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL1.i = UsedIntLoc i) & UsedIntLoc p = Union (UIL1 * p) by Def2; consider UIL2 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A3: (for i being Instruction of SCM+FSA holds UIL2.i = UsedIntLoc i) & UsedIntLoc r = Union (UIL2 * r) by Def2; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL1.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedIntLoc d by A1 .= UIL1.c by A2; end; then A4: UIL=UIL1 by FUNCT_2:113; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedIntLoc d by A1 .= UIL2.c by A3; end; then A5: UIL=UIL2 by FUNCT_2:113; A6: Union (UIL * (p +* r)) = union rng (UIL * (p +* r)) by PROB_1:def 3; A7: Union (UIL * p) = union rng (UIL * p) by PROB_1:def 3; A8: Union (UIL * r) = union rng (UIL * r) by PROB_1:def 3; dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then rng p c= dom UIL & rng r c= dom UIL by SCMFSA_4:1; then A9: UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:10; assume A10: dom p misses dom r; A11: dom (UIL * p) c= dom p & dom (UIL * r) c= dom r by RELAT_1:44; then dom p misses dom (UIL * r) by A10,XBOOLE_1:63; then dom (UIL * p) misses dom (UIL * r) by A11,XBOOLE_1:63; then (UIL * p) +* (UIL * r) = (UIL * p) \/ (UIL * r) by FUNCT_4:32; then union rng (UIL * (p +* r)) = union (rng (UIL * p) \/ rng (UIL * r)) by A9,RELAT_1:26; hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,ZFMISC_1:96; end; theorem Th26: UsedIntLoc p = UsedIntLoc Shift(p, k) proof consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc p = Union (UIL * p) by Def2; consider UIL2 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL2.i = UsedIntLoc i) & UsedIntLoc Shift (p, k) = Union (UIL2 * Shift (p, k)) by Def2; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedIntLoc d by A1 .= UIL2.c by A2; end; then A3: UIL=UIL2 by FUNCT_2:113; set Sp = Shift (p, k); A4: Union (UIL * Sp) = union rng (UIL * Sp) by PROB_1:def 3; A5: dom Sp = { insloc(m+k) where m is Nat : insloc m in dom p } by SCMFSA_4:def 7; now let y be set; hereby assume y in rng Sp; then consider x being set such that A6: x in dom Sp & y = Sp.x by FUNCT_1:def 5; consider m being Nat such that A7: x = insloc (m+k) & insloc m in dom p by A5,A6; Sp.x = p.insloc m by A7,SCMFSA_4:def 7; hence y in rng p by A6,A7,FUNCT_1:def 5; end; assume y in rng p; then consider x being set such that A8: x in dom p & y = p.x by FUNCT_1:def 5; dom p c= the Instruction-Locations of SCM+FSA by AMI_3:def 13; then reconsider x' = x as Instruction-Location of SCM+FSA by A8; consider m being Nat such that A9: x' = insloc m by SCMFSA_2:21; A10: insloc (m+k) in dom Sp by A5,A8,A9; Sp.insloc (m+k) = p.insloc m by A8,A9,SCMFSA_4:def 7; hence y in rng Sp by A8,A9,A10,FUNCT_1:def 5; end; then A11: rng Sp = rng p by TARSKI:2; rng (UIL * Sp) = UIL.:rng Sp by RELAT_1:160 .= rng (UIL * p) by A11,RELAT_1:160; hence thesis by A1,A2,A3,A4,PROB_1:def 3; end; theorem Th27: UsedIntLoc i = UsedIntLoc IncAddr(i, k) proof A1: InsCode i <= 11+1 by SCMFSA_2:35; A2: InsCode i <= 10+1 implies InsCode i <= 10 or InsCode i = 11 by NAT_1:26; A3: InsCode i <= 9+1 implies InsCode i <= 8+1 or InsCode i = 10 by NAT_1:26; A4: InsCode i <= 8+1 implies InsCode i <= 7+1 or InsCode i = 9 by NAT_1:26; per cases by A1,A2,A3,A4,CQC_THE1:9,NAT_1:26; suppose InsCode i = 0; then i = halt SCM+FSA by SCMFSA_2:122; hence UsedIntLoc IncAddr(i, k) = UsedIntLoc i by SCMFSA_4:8; suppose InsCode i = 1; then consider a, b such that A5: i = a:=b by SCMFSA_2:54; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A5,SCMFSA_4:9; suppose InsCode i = 2; then consider a, b such that A6: i = AddTo(a,b) by SCMFSA_2:55; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A6,SCMFSA_4:10; suppose InsCode i = 3; then consider a, b such that A7: i = SubFrom(a, b) by SCMFSA_2:56; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A7,SCMFSA_4:11; suppose InsCode i = 4; then consider a, b such that A8: i = MultBy(a, b) by SCMFSA_2:57; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A8,SCMFSA_4:12; suppose InsCode i = 5; then consider a, b such that A9: i = Divide(a, b) by SCMFSA_2:58; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A9,SCMFSA_4:13; suppose InsCode i = 6; then consider l such that A10: i = goto l by SCMFSA_2:59; IncAddr(i, k) = goto (l+k) by A10,SCMFSA_4:14 ; hence UsedIntLoc IncAddr(i, k) = {} by Th19 .= UsedIntLoc i by A10,Th19; suppose InsCode i = 7; then consider l, a such that A11: i = a=0_goto l by SCMFSA_2:60; IncAddr(i, k) = a=0_goto (l+k) by A11,SCMFSA_4:15; hence UsedIntLoc IncAddr(i, k) = {a} by Th20 .= UsedIntLoc i by A11,Th20; suppose InsCode i = 8; then consider l, a such that A12: i = a>0_goto l by SCMFSA_2:61; IncAddr(i, k) = a>0_goto (l+k) by A12,SCMFSA_4:16; hence UsedIntLoc IncAddr(i, k) = {a} by Th20 .= UsedIntLoc i by A12,Th20; suppose InsCode i = 9; then consider a, b, f such that A13: i = b:=(f,a) by SCMFSA_2:62; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A13,SCMFSA_4:17; suppose InsCode i = 10; then consider a, b, f such that A14: i = (f,a):=b by SCMFSA_2:63; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A14,SCMFSA_4:18; suppose InsCode i = 11; then consider a, f such that A15: i = a:=len f by SCMFSA_2:64; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A15,SCMFSA_4:19; suppose InsCode i = 12; then consider a,f such that A16: i = f:=<0,...,0>a by SCMFSA_2:65; thus UsedIntLoc IncAddr(i, k) = UsedIntLoc i by A16,SCMFSA_4:20; end; theorem Th28: UsedIntLoc p = UsedIntLoc IncAddr(p, k) proof consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc p = Union (UIL * p) by Def2; consider UIL2 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL2.i = UsedIntLoc i) & UsedIntLoc IncAddr (p, k) = Union (UIL2 * IncAddr (p, k)) by Def2; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedIntLoc d by A1 .= UIL2.c by A2; end; then A3: UIL=UIL2 by FUNCT_2:113; set Ip = IncAddr (p, k); set f = UIL * Ip; set g = UIL * p; now A4: dom Ip = dom p by SCMFSA_4:def 6; A5: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then A6: rng p c= dom UIL & rng Ip c= dom UIL by SCMFSA_4:1; then A7: dom f = dom Ip by RELAT_1:46; hence dom f = dom g by A4,A6,RELAT_1:46; let x be set; assume A8: x in dom f; then Ip.x in rng Ip by A7,FUNCT_1:def 5; then reconsider Ipx = Ip.x as Instruction of SCM+FSA by A5,A6; p.x in rng p by A4,A7,A8,FUNCT_1:def 5; then reconsider px = p.x as Instruction of SCM+FSA by A5,A6; dom p c= the Instruction-Locations of SCM+FSA by AMI_3:def 13; then reconsider x' = x as Instruction-Location of SCM+FSA by A4,A7,A8; consider m being Nat such that A9: x' = insloc m by SCMFSA_2:21; A10: Ip.x = IncAddr(pi(p,x'),k) by A4,A7,A8,A9,SCMFSA_4:def 6 .= IncAddr(px, k) by A4,A7,A8,AMI_5:def 5; thus f.x = UIL.Ipx by A8,FUNCT_1:22 .= UsedIntLoc Ipx by A1 .= UsedIntLoc px by A10,Th27 .= UIL.px by A2,A3 .= g.x by A4,A7,A8,FUNCT_1:23; end; hence thesis by A1,A2,A3,FUNCT_1:9; end; theorem Th29: UsedIntLoc I = UsedIntLoc ProgramPart Relocated (I, k) proof UsedIntLoc ProgramPart Relocated (I, k) = UsedIntLoc IncAddr(Shift(ProgramPart(I),k),k) by SCMFSA_5:2 .= UsedIntLoc Shift (ProgramPart I, k) by Th28 .= UsedIntLoc ProgramPart I by Th26; hence thesis by AMI_5:72; end; theorem Th30: UsedIntLoc I = UsedIntLoc Directed I proof consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc I = Union (UIL * I) by Def2; consider UIL2 being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL2.i = UsedIntLoc i) & UsedIntLoc Directed I = Union (UIL2 * Directed I) by Def2; A3: for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedIntLoc d by A1 .= UIL2.c by A2; end; A4: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; dom id the Instructions of SCM+FSA = the Instructions of SCM+FSA by RELAT_1:71; then A5: (id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc card I) = (id the Instructions of SCM+FSA)+* (halt SCM+FSA, goto insloc card I) by FUNCT_7:def 3; A6: UIL.halt SCM+FSA = {} by A1,Th17; A7: UIL.goto insloc card I = UsedIntLoc goto insloc card I by A1 .= {} by Th19; UIL * Directed I = UIL * (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc card I))*I) by SCMFSA6A:def 1 .= UIL * ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc card I)) * I by RELAT_1:55 .= UIL * I by A4,A5,A6,A7,Th2; hence thesis by A1,A2,A3,FUNCT_2:113; end; theorem Th31: UsedIntLoc (I ';' J) = (UsedIntLoc I) \/ (UsedIntLoc J) proof dom I = dom Directed I by SCMFSA6A:14; then A1: dom (Directed I) misses dom (ProgramPart Relocated(J, card I)) by SCMFSA6A:16; thus UsedIntLoc (I ';' J) = UsedIntLoc (Directed I +* ProgramPart Relocated(J, card I)) by SCMFSA6A:def 4 .= UsedIntLoc (Directed I) \/ UsedIntLoc ProgramPart Relocated(J, card I) by A1,Th25 .= (UsedIntLoc I) \/ UsedIntLoc ProgramPart Relocated(J, card I) by Th30 .= (UsedIntLoc I) \/ (UsedIntLoc J) by Th29; end; theorem Th32: UsedIntLoc Macro i = UsedIntLoc i proof consider UIL being Function of the Instructions of SCM+FSA, Fin Int-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) & UsedIntLoc Macro i = Union (UIL * Macro i) by Def2; A2: insloc 0 <> insloc 1 by SCMFSA_2:18; A3: rng (Macro i) = rng ((insloc 0,insloc 1) --> (i,halt SCM+FSA)) by SCMFSA6A:def 2 .= {i, halt SCM+FSA} by A2,FUNCT_4:67; A4: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; thus UsedIntLoc Macro i = union rng (UIL * Macro i) by A1,PROB_1:def 3 .= union (UIL.:rng Macro i) by RELAT_1:160 .= union {UIL.i,UIL.halt SCM+FSA} by A3,A4,FUNCT_1:118 .= UIL.i \/ UIL.halt SCM+FSA by ZFMISC_1:93 .= (UsedIntLoc i) \/ UIL.halt SCM+FSA by A1 .= (UsedIntLoc i) \/ (UsedIntLoc halt SCM+FSA) by A1 .= UsedIntLoc i by Th17; end; theorem :: MiJ: UsedIntLoc (i ';' J) = (UsedIntLoc i) \/ UsedIntLoc J proof thus UsedIntLoc (i ';' J) = UsedIntLoc (Macro i ';' J) by SCMFSA6A:def 5 .= (UsedIntLoc Macro i) \/ UsedIntLoc J by Th31 .= (UsedIntLoc i) \/ UsedIntLoc J by Th32; end; theorem :: MIj: UsedIntLoc (I ';' j) = (UsedIntLoc I) \/ UsedIntLoc j proof thus UsedIntLoc (I ';' j) = UsedIntLoc (I ';' Macro j) by SCMFSA6A:def 6 .= (UsedIntLoc I) \/ UsedIntLoc Macro j by Th31 .= (UsedIntLoc I) \/ UsedIntLoc j by Th32; end; theorem :: Mij: UsedIntLoc (i ';' j) = (UsedIntLoc i) \/ UsedIntLoc j proof thus UsedIntLoc (i ';' j) = UsedIntLoc (Macro i ';' Macro j) by SCMFSA6A:def 7 .= (UsedIntLoc Macro i) \/ UsedIntLoc Macro j by Th31 .= (UsedIntLoc Macro i) \/ UsedIntLoc j by Th32 .= (UsedIntLoc i) \/ UsedIntLoc j by Th32; end; begin :: Finite sequence locations used in macro instructions definition let i be Instruction of SCM+FSA; func UsedInt*Loc i -> Element of Fin FinSeq-Locations means :Def3: ex a, b being Int-Location, f being FinSeq-Location st (i = b := (f, a) or i = (f, a) := b) & it = {f} if InsCode i = 9 or InsCode i = 10, ex a being Int-Location, f being FinSeq-Location st (i = a :=len f or i = f :=<0,...,0>a) & it = {f} if InsCode i = 11 or InsCode i = 12 otherwise it = {}; existence proof hereby assume InsCode i = 9 or InsCode i = 10; then consider a, b being Int-Location, f being FinSeq-Location such that A1: i = b := (f, a) or i = (f, a) := b by SCMFSA_2:62,63; reconsider f' = f as Element of FinSeq-Locations by SCMFSA_2:10; reconsider IT = {f'} as Element of Fin FinSeq-Locations; take IT; take a, b, f; thus (i = b := (f, a) or i = (f, a) := b) & IT = {f} by A1; end; hereby assume InsCode i = 11 or InsCode i = 12; then consider a being Int-Location, f being FinSeq-Location such that A2: i = a :=len f or i = f :=<0,...,0>a by SCMFSA_2:64,65; reconsider f' = f as Element of FinSeq-Locations by SCMFSA_2:10; reconsider IT = {f'} as Element of Fin FinSeq-Locations; take IT; take a, f; thus (i = a :=len f or i = f :=<0,...,0>a) & IT = {f} by A2; end; {} in Fin FinSeq-Locations by FINSUB_1:18; hence thesis; end; uniqueness proof let it1, it2 be Element of Fin FinSeq-Locations; hereby assume InsCode i = 9 or InsCode i = 10; given a1, b1 being Int-Location, f1 being FinSeq-Location such that A3: (i = b1 := (f1, a1) or i = (f1, a1) := b1) & it1 = {f1}; given a2, b2 being Int-Location, f2 being FinSeq-Location such that A4: (i = b2 := (f2, a2) or i = (f2, a2) := b2) & it2 = {f2}; A5: i = (f1, a1) := b1 or i = (f2, a2) := b2 implies InsCode i = 10 by SCMFSA_2:51; per cases by A3,A4,A5,SCMFSA_2:50; suppose i = b1 := (f1, a1) & i = b2 := (f2, a2); hence it1 = it2 by A3,A4, Th13; suppose i = (f1, a1) := b1 & i = (f2, a2) := b2; hence it1 = it2 by A3,A4, Th14; end; hereby assume InsCode i = 11 or InsCode i = 12; given a1 being Int-Location, f1 being FinSeq-Location such that A6: (i = a1 :=len f1 or i = f1 :=<0,...,0>a1) & it1 = {f1}; given a2 being Int-Location, f2 being FinSeq-Location such that A7: (i = a2 :=len f2 or i = f2 :=<0,...,0>a2) & it2 = {f2}; A8: i = f1 :=<0,...,0>a1 or i = f2 :=<0,...,0>a2 implies InsCode i = 12 by SCMFSA_2:53; per cases by A6,A7,A8,SCMFSA_2:52; suppose i = a1 :=len f1 & i = a2 :=len f2; hence it1 = it2 by A6,A7,Th15 ; suppose i = f1 :=<0,...,0>a1 & i = f2 :=<0,...,0>a2; hence it1 = it2 by A6 ,A7,Th16; end; thus thesis; end; consistency; end; theorem Th36: i = halt SCM+FSA or i = a:=b or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b) or i = goto l or i = a=0_goto l or i = a>0_goto l implies UsedInt*Loc i = {} proof assume i = halt SCM+FSA or i = a:=b or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b) or i = goto l or i = a=0_goto l or i = a>0_goto l; then InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 by SCMFSA_2:42,43,44,45,46,47,48,49,124; hence UsedInt*Loc i = {} by Def3; end; theorem Th37: i = b := (f, a) or i = (f, a) := b implies UsedInt*Loc i = {f} proof assume A1: i = b := (f, a) or i = (f, a) := b; f in FinSeq-Locations by SCMFSA_2:10; then {f} c= FinSeq-Locations by ZFMISC_1:37; then reconsider ab = {f} as Element of Fin FinSeq-Locations by FINSUB_1:def 5; InsCode i = 9 or InsCode i = 10 by A1,SCMFSA_2:50,51; then UsedInt*Loc i = ab by A1,Def3; hence UsedInt*Loc i = {f}; end; theorem Th38: i = a :=len f or i = f :=<0,...,0>a implies UsedInt*Loc i = {f} proof assume A1: i = a :=len f or i = f :=<0,...,0>a; f in FinSeq-Locations by SCMFSA_2:10; then {f} c= FinSeq-Locations by ZFMISC_1:37; then reconsider ab = {f} as Element of Fin FinSeq-Locations by FINSUB_1:def 5; InsCode i = 11 or InsCode i = 12 by A1,SCMFSA_2:52,53; then UsedInt*Loc i = ab by A1,Def3; hence UsedInt*Loc i = {f}; end; definition let p be programmed FinPartState of SCM+FSA; func UsedInt*Loc p -> Subset of FinSeq-Locations means :Def4: ex UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations st (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & it = Union (UIL * p); existence proof defpred P[set,set] means ex I being Instruction of SCM+FSA st $1 = I & $2 = UsedInt*Loc I; A1: for e being Element of the Instructions of SCM+FSA ex u being Element of Fin FinSeq-Locations st P[e,u] proof let e be Element of the Instructions of SCM+FSA; reconsider f = e as Instruction of SCM+FSA ; reconsider u = UsedInt*Loc f as Element of Fin FinSeq-Locations; take u, f; thus thesis; end; consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A2: for i being Element of the Instructions of SCM+FSA holds P[i,UIL.i] from FuncExD(A1); set IT = Union (UIL * p); reconsider dp = dom p as finite set by AMI_1:21; rng p c= the Instructions of SCM+FSA by SCMFSA_4:1; then reconsider p' = p as Function of dp, the Instructions of SCM+FSA by FUNCT_2:4; reconsider Up = UIL * p' as Function of dp, Fin FinSeq-Locations; A3: IT = union rng Up by PROB_1:def 3; A4: rng Up c= Fin FinSeq-Locations by RELSET_1:12; Fin FinSeq-Locations c= bool FinSeq-Locations by FINSUB_1:26; then rng Up c= bool FinSeq-Locations by A4,XBOOLE_1:1; then A5: union rng Up c= union bool FinSeq-Locations by ZFMISC_1:95; take IT; thus IT is Subset of FinSeq-Locations by A3,A5,ZFMISC_1:99; take UIL; hereby let i be Instruction of SCM+FSA; P[i,UIL.i] by A2; hence UIL.i = UsedInt*Loc i; end; thus thesis; end; uniqueness proof let IT1, IT2 be Subset of FinSeq-Locations; given UIL1 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A6: (for i being Instruction of SCM+FSA holds UIL1.i = UsedInt*Loc i) & IT1 = Union (UIL1 * p); given UIL2 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A7: (for i being Instruction of SCM+FSA holds UIL2.i = UsedInt*Loc i) & IT2 = Union (UIL2 * p); for c be Element of the Instructions of SCM+FSA holds UIL1.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL1.c = UsedInt*Loc d by A6 .= UIL2.c by A7; end; hence IT1 = IT2 by A6,A7,FUNCT_2:113; end; end; definition let p be programmed FinPartState of SCM+FSA; cluster UsedInt*Loc p -> finite; coherence proof consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc p = Union (UIL * p) by Def4; reconsider dp = dom p as finite set by AMI_1:21; rng p c= the Instructions of SCM+FSA by SCMFSA_4:1; then reconsider p' = p as Function of dp, the Instructions of SCM+FSA by FUNCT_2:4; reconsider Up = UIL * p' as Function of dp, Fin FinSeq-Locations; Union Up is finite; hence thesis by A1; end; end; theorem Th39: i in rng p implies UsedInt*Loc i c= UsedInt*Loc p proof assume i in rng p; then consider x being set such that A1: x in dom p & i = p.x by FUNCT_1:def 5; consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc p = Union (UIL * p) by Def4; A3: (UIL * p).x = UIL.i by A1,FUNCT_1:23 .= UsedInt*Loc i by A2; dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then x in dom (UIL * p) by A1,FUNCT_1:21; then A4: (UIL * p).x in rng (UIL * p) by FUNCT_1:def 5; UsedInt*Loc p = union rng (UIL * p) by A2,PROB_1:def 3; hence UsedInt*Loc i c= UsedInt*Loc p by A3,A4,ZFMISC_1:92; end; theorem :: FUFP1: UsedInt*Loc (p +* r) c= (UsedInt*Loc p) \/ (UsedInt*Loc r) proof consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc (p +* r) = Union (UIL * (p +* r)) by Def4; consider UIL1 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL1.i = UsedInt*Loc i) & UsedInt*Loc p = Union (UIL1 * p) by Def4; consider UIL2 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A3: (for i being Instruction of SCM+FSA holds UIL2.i = UsedInt*Loc i) & UsedInt*Loc r = Union (UIL2 * r) by Def4; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL1.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedInt*Loc d by A1 .= UIL1.c by A2; end; then A4: UIL=UIL1 by FUNCT_2:113; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedInt*Loc d by A1 .= UIL2.c by A3; end; then A5: UIL=UIL2 by FUNCT_2:113; A6: Union (UIL * (p +* r)) = union rng (UIL * (p +* r)) by PROB_1:def 3; A7: Union (UIL * p) = union rng (UIL * p) by PROB_1:def 3; A8: Union (UIL * r) = union rng (UIL * r) by PROB_1:def 3; dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then rng p c= dom UIL & rng r c= dom UIL by SCMFSA_4:1; then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:10; then rng (UIL * (p +* r)) c= rng (UIL * p) \/ rng (UIL * r) by FUNCT_4:18; then union rng (UIL * (p +* r)) c= union (rng (UIL * p) \/ rng (UIL * r)) by ZFMISC_1:95; hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,ZFMISC_1:96; end; theorem Th41: dom p misses dom r implies UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r) proof consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc (p +* r) = Union (UIL * (p +* r)) by Def4; consider UIL1 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL1.i = UsedInt*Loc i) & UsedInt*Loc p = Union (UIL1 * p) by Def4; consider UIL2 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A3: (for i being Instruction of SCM+FSA holds UIL2.i = UsedInt*Loc i) & UsedInt*Loc r = Union (UIL2 * r) by Def4; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL1.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedInt*Loc d by A1 .= UIL1.c by A2; end; then A4: UIL=UIL1 by FUNCT_2:113; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedInt*Loc d by A1 .= UIL2.c by A3; end; then A5: UIL=UIL2 by FUNCT_2:113; A6: Union (UIL * (p +* r)) = union rng (UIL * (p +* r)) by PROB_1:def 3; A7: Union (UIL * p) = union rng (UIL * p) by PROB_1:def 3; A8: Union (UIL * r) = union rng (UIL * r) by PROB_1:def 3; dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then rng p c= dom UIL & rng r c= dom UIL by SCMFSA_4:1; then A9: UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:10; assume A10: dom p misses dom r; A11: dom (UIL * p) c= dom p & dom (UIL * r) c= dom r by RELAT_1:44; then dom p misses dom (UIL * r) by A10,XBOOLE_1:63; then dom (UIL * p) misses dom (UIL * r) by A11,XBOOLE_1:63; then (UIL * p) +* (UIL * r) = (UIL * p) \/ (UIL * r) by FUNCT_4:32; then union rng (UIL * (p +* r)) = union (rng (UIL * p) \/ rng (UIL * r)) by A9,RELAT_1:26; hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,ZFMISC_1:96; end; theorem Th42: UsedInt*Loc p = UsedInt*Loc Shift(p, k) proof consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc p = Union (UIL * p) by Def4; consider UIL2 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL2.i = UsedInt*Loc i) & UsedInt*Loc Shift (p, k) = Union (UIL2 * Shift (p, k)) by Def4; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedInt*Loc d by A1 .= UIL2.c by A2; end; then A3: UIL=UIL2 by FUNCT_2:113; set Sp = Shift (p, k); A4: Union (UIL * Sp) = union rng (UIL * Sp) by PROB_1:def 3; A5: dom Sp = { insloc(m+k) where m is Nat : insloc m in dom p } by SCMFSA_4:def 7; now let y be set; hereby assume y in rng Sp; then consider x being set such that A6: x in dom Sp & y = Sp.x by FUNCT_1:def 5; consider m being Nat such that A7: x = insloc (m+k) & insloc m in dom p by A5,A6; Sp.x = p.insloc m by A7,SCMFSA_4:def 7; hence y in rng p by A6,A7,FUNCT_1:def 5; end; assume y in rng p; then consider x being set such that A8: x in dom p & y = p.x by FUNCT_1:def 5; dom p c= the Instruction-Locations of SCM+FSA by AMI_3:def 13; then reconsider x' = x as Instruction-Location of SCM+FSA by A8; consider m being Nat such that A9: x' = insloc m by SCMFSA_2:21; A10: insloc (m+k) in dom Sp by A5,A8,A9; Sp.insloc (m+k) = p.insloc m by A8,A9,SCMFSA_4:def 7; hence y in rng Sp by A8,A9,A10,FUNCT_1:def 5; end; then A11: rng Sp = rng p by TARSKI:2; rng (UIL * Sp) = UIL.:rng Sp by RELAT_1:160 .= rng (UIL * p) by A11,RELAT_1:160; hence thesis by A1,A2,A3,A4,PROB_1:def 3; end; theorem Th43: UsedInt*Loc i = UsedInt*Loc IncAddr(i, k) proof A1: InsCode i <= 11+1 by SCMFSA_2:35; A2: InsCode i <= 10+1 implies InsCode i <= 10 or InsCode i = 11 by NAT_1:26; A3: InsCode i <= 9+1 implies InsCode i <= 8+1 or InsCode i = 10 by NAT_1:26; A4: InsCode i <= 8+1 implies InsCode i <= 7+1 or InsCode i = 9 by NAT_1:26; per cases by A1,A2,A3,A4,CQC_THE1:9,NAT_1:26; suppose InsCode i = 0; then i = halt SCM+FSA by SCMFSA_2:122; hence UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by SCMFSA_4:8; suppose InsCode i = 1; then consider a, b such that A5: i = a:=b by SCMFSA_2:54; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A5,SCMFSA_4:9; suppose InsCode i = 2; then consider a, b such that A6: i = AddTo(a,b) by SCMFSA_2:55; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A6,SCMFSA_4:10; suppose InsCode i = 3; then consider a, b such that A7: i = SubFrom(a, b) by SCMFSA_2:56; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A7,SCMFSA_4:11; suppose InsCode i = 4; then consider a, b such that A8: i = MultBy(a, b) by SCMFSA_2:57; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A8,SCMFSA_4:12; suppose InsCode i = 5; then consider a, b such that A9: i = Divide(a, b) by SCMFSA_2:58; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A9,SCMFSA_4:13; suppose InsCode i = 6; then consider l such that A10: i = goto l by SCMFSA_2:59; IncAddr(i, k) = goto (l+k) by A10,SCMFSA_4:14 ; hence UsedInt*Loc IncAddr(i, k) = {} by Th36 .= UsedInt*Loc i by A10,Th36; suppose InsCode i = 7; then consider l, a such that A11: i = a=0_goto l by SCMFSA_2:60; IncAddr(i, k) = a=0_goto (l+k) by A11,SCMFSA_4:15; hence UsedInt*Loc IncAddr(i, k) = {} by Th36 .= UsedInt*Loc i by A11,Th36; suppose InsCode i = 8; then consider l, a such that A12: i = a>0_goto l by SCMFSA_2:61; IncAddr(i, k) = a>0_goto (l+k) by A12,SCMFSA_4:16; hence UsedInt*Loc IncAddr(i, k) = {} by Th36 .= UsedInt*Loc i by A12,Th36; suppose InsCode i = 9; then consider a, b, f such that A13: i = b:=(f,a) by SCMFSA_2:62; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A13,SCMFSA_4:17; suppose InsCode i = 10; then consider a, b, f such that A14: i = (f,a):=b by SCMFSA_2:63; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A14,SCMFSA_4:18; suppose InsCode i = 11; then consider a, f such that A15: i = a:=len f by SCMFSA_2:64; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A15,SCMFSA_4:19; suppose InsCode i = 12; then consider a,f such that A16: i = f:=<0,...,0>a by SCMFSA_2:65; thus UsedInt*Loc IncAddr(i, k) = UsedInt*Loc i by A16,SCMFSA_4:20; end; theorem Th44: UsedInt*Loc p = UsedInt*Loc IncAddr(p, k) proof consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc p = Union (UIL * p) by Def4; consider UIL2 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL2.i = UsedInt*Loc i) & UsedInt*Loc IncAddr (p, k) = Union (UIL2 * IncAddr (p, k)) by Def4; for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedInt*Loc d by A1 .= UIL2.c by A2; end; then A3: UIL=UIL2 by FUNCT_2:113; set Ip = IncAddr (p, k); set f = UIL * Ip; set g = UIL * p; now A4: dom Ip = dom p by SCMFSA_4:def 6; A5: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; then A6: rng p c= dom UIL & rng Ip c= dom UIL by SCMFSA_4:1; then A7: dom f = dom Ip by RELAT_1:46; hence dom f = dom g by A4,A6,RELAT_1:46; let x be set; assume A8: x in dom f; then Ip.x in rng Ip by A7,FUNCT_1:def 5; then reconsider Ipx = Ip.x as Instruction of SCM+FSA by A5,A6; p.x in rng p by A4,A7,A8,FUNCT_1:def 5; then reconsider px = p.x as Instruction of SCM+FSA by A5,A6; dom p c= the Instruction-Locations of SCM+FSA by AMI_3:def 13; then reconsider x' = x as Instruction-Location of SCM+FSA by A4,A7,A8; consider m being Nat such that A9: x' = insloc m by SCMFSA_2:21; A10: Ip.x = IncAddr(pi(p,x'),k) by A4,A7,A8,A9,SCMFSA_4:def 6 .= IncAddr(px, k) by A4,A7,A8,AMI_5:def 5; thus f.x = UIL.Ipx by A8,FUNCT_1:22 .= UsedInt*Loc Ipx by A1 .= UsedInt*Loc px by A10,Th43 .= UIL.px by A2,A3 .= g.x by A4,A7,A8,FUNCT_1:23; end; hence thesis by A1,A2,A3,FUNCT_1:9; end; theorem Th45: UsedInt*Loc I = UsedInt*Loc ProgramPart Relocated (I, k) proof UsedInt*Loc ProgramPart Relocated (I, k) = UsedInt*Loc IncAddr(Shift(ProgramPart(I),k),k) by SCMFSA_5:2 .= UsedInt*Loc Shift (ProgramPart I, k) by Th44 .= UsedInt*Loc ProgramPart I by Th42; hence thesis by AMI_5:72; end; theorem Th46: UsedInt*Loc I = UsedInt*Loc Directed I proof consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc I = Union (UIL * I) by Def4; consider UIL2 being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A2: (for i being Instruction of SCM+FSA holds UIL2.i = UsedInt*Loc i) & UsedInt*Loc Directed I = Union (UIL2 * Directed I) by Def4; A3: for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c proof let c be Element of the Instructions of SCM+FSA; reconsider d = c as Instruction of SCM+FSA ; thus UIL.c = UsedInt*Loc d by A1 .= UIL2.c by A2; end; A4: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; dom id the Instructions of SCM+FSA = the Instructions of SCM+FSA by RELAT_1:71; then A5: (id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc card I) = (id the Instructions of SCM+FSA)+* (halt SCM+FSA, goto insloc card I) by FUNCT_7:def 3; A6: UIL.halt SCM+FSA = UsedInt*Loc halt SCM+FSA by A1 .= {} by Th36; A7: UIL.goto insloc card I = UsedInt*Loc goto insloc card I by A1 .= {} by Th36; UIL * Directed I = UIL * (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc card I))*I) by SCMFSA6A:def 1 .= UIL * ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto insloc card I)) * I by RELAT_1:55 .= UIL * I by A4,A5,A6,A7,Th2; hence thesis by A1,A2,A3,FUNCT_2:113; end; theorem Th47: UsedInt*Loc (I ';' J) = (UsedInt*Loc I) \/ (UsedInt*Loc J) proof dom I = dom Directed I by SCMFSA6A:14; then A1: dom (Directed I) misses dom (ProgramPart Relocated(J, card I)) by SCMFSA6A:16; thus UsedInt*Loc (I ';' J) = UsedInt*Loc (Directed I +* ProgramPart Relocated(J, card I)) by SCMFSA6A:def 4 .= UsedInt*Loc (Directed I) \/ UsedInt*Loc ProgramPart Relocated(J, card I) by A1,Th41 .= (UsedInt*Loc I) \/ UsedInt*Loc ProgramPart Relocated(J, card I) by Th46 .= (UsedInt*Loc I) \/ (UsedInt*Loc J) by Th45; end; theorem Th48: UsedInt*Loc Macro i = UsedInt*Loc i proof consider UIL being Function of the Instructions of SCM+FSA, Fin FinSeq-Locations such that A1: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) & UsedInt*Loc Macro i = Union (UIL * Macro i) by Def4; A2: insloc 0 <> insloc 1 by SCMFSA_2:18; A3: rng (Macro i) = rng ((insloc 0,insloc 1) --> (i,halt SCM+FSA)) by SCMFSA6A:def 2 .= {i, halt SCM+FSA} by A2,FUNCT_4:67; A4: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1; thus UsedInt*Loc Macro i = union rng (UIL * Macro i) by A1,PROB_1:def 3 .= union (UIL.:rng Macro i) by RELAT_1:160 .= union {UIL.i,UIL.halt SCM+FSA} by A3,A4,FUNCT_1:118 .= UIL.i \/ UIL.halt SCM+FSA by ZFMISC_1:93 .= (UsedInt*Loc i) \/ UIL.halt SCM+FSA by A1 .= (UsedInt*Loc i) \/ (UsedInt*Loc halt SCM+FSA) by A1 .= UsedInt*Loc i \/ {} by Th36 .= UsedInt*Loc i; end; theorem :: FMiJ: UsedInt*Loc (i ';' J) = (UsedInt*Loc i) \/ UsedInt*Loc J proof thus UsedInt*Loc (i ';' J) = UsedInt*Loc (Macro i ';' J) by SCMFSA6A:def 5 .= (UsedInt*Loc Macro i) \/ UsedInt*Loc J by Th47 .= (UsedInt*Loc i) \/ UsedInt*Loc J by Th48; end; theorem :: FMIj: UsedInt*Loc (I ';' j) = (UsedInt*Loc I) \/ UsedInt*Loc j proof thus UsedInt*Loc (I ';' j) = UsedInt*Loc (I ';' Macro j) by SCMFSA6A:def 6 .= (UsedInt*Loc I) \/ UsedInt*Loc Macro j by Th47 .= (UsedInt*Loc I) \/ UsedInt*Loc j by Th48; end; theorem :: FMij: UsedInt*Loc (i ';' j) = (UsedInt*Loc i) \/ UsedInt*Loc j proof thus UsedInt*Loc (i ';' j) = UsedInt*Loc (Macro i ';' Macro j) by SCMFSA6A:def 7 .= (UsedInt*Loc Macro i) \/ UsedInt*Loc Macro j by Th47 .= (UsedInt*Loc Macro i) \/ UsedInt*Loc j by Th48 .= (UsedInt*Loc i) \/ UsedInt*Loc j by Th48; end; begin :: Choosing integer location not used in a macro instruction definition let IT be Int-Location; attr IT is read-only means :Def5: IT = intloc 0; antonym IT is read-write; end; definition cluster intloc 0 -> read-only; coherence by Def5; end; definition cluster read-write Int-Location; existence proof take intloc 1; intloc 0 <> intloc 1 by SCMFSA_2:16; hence thesis by Def5; end; end; reserve L for finite Subset of Int-Locations; definition let L be finite Subset of Int-Locations; func FirstNotIn L -> Int-Location means :Def6: ex sn being non empty Subset of NAT st it = intloc min sn & sn = {k where k is Nat : not intloc k in L}; existence proof defpred X[Nat] means not intloc $1 in L; set sn = {k where k is Nat : X[k]}; A1: sn is Subset of NAT from SubsetD; not Int-Locations c= L by SCMFSA_2:22,XBOOLE_0:def 10; then consider x being set such that A2: x in Int-Locations & not x in L by TARSKI:def 3; reconsider x as Int-Location by A2,SCMFSA_2:11; consider k being Nat such that A3: x = intloc k by SCMFSA_2:19; k in sn by A2,A3; then reconsider sn as non empty Subset of NAT by A1; take intloc min sn, sn; thus thesis; end; uniqueness; end; theorem Th52: not FirstNotIn L in L proof set FNI = FirstNotIn L; consider sn being non empty Subset of NAT such that A1: FNI = intloc min sn and A2: sn = {k where k is Nat : not intloc k in L} by Def6; min sn in sn by CQC_SIM1:def 8; then consider k being Nat such that A3: k = min sn & not intloc k in L by A2; thus not FNI in L by A1,A3; end; theorem :: FNI2: FirstNotIn L = intloc m & not intloc n in L implies m <= n proof assume A1: FirstNotIn L = intloc m & not intloc n in L; consider sn being non empty Subset of NAT such that A2: FirstNotIn L = intloc min sn and A3: sn = {k where k is Nat : not intloc k in L} by Def6; A4: m = min sn by A1,A2,SCMFSA_2:16; n in sn by A1,A3; hence m <= n by A4,CQC_SIM1:def 8; end; definition let p be programmed FinPartState of SCM+FSA; func FirstNotUsed p -> Int-Location means :Def7: ex sil being finite Subset of Int-Locations st sil = UsedIntLoc p \/ {intloc 0} & it = FirstNotIn sil; existence proof intloc 0 in Int-Locations by SCMFSA_2:9; then reconsider i0 = {intloc 0} as finite Subset of Int-Locations by ZFMISC_1 :37; reconsider sil = UsedIntLoc p \/ i0 as finite Subset of Int-Locations; take FirstNotIn sil, sil; thus thesis; end; uniqueness; end; definition let p be programmed FinPartState of SCM+FSA; cluster FirstNotUsed p -> read-write; coherence proof consider sil being finite Subset of Int-Locations such that A1: sil = UsedIntLoc p \/ {intloc 0} & FirstNotUsed p = FirstNotIn sil by Def7; now assume FirstNotIn sil = intloc 0; then not intloc 0 in sil by Th52; hence contradiction by A1,SETWISEO:6; end; hence thesis by A1,Def5; end; end; theorem Th54: not FirstNotUsed p in UsedIntLoc p proof consider sil being finite Subset of Int-Locations such that A1: sil = UsedIntLoc p \/ {intloc 0} & FirstNotUsed p = FirstNotIn sil by Def7; not FirstNotUsed p in sil by A1,Th52; hence thesis by A1,XBOOLE_0:def 2; end; theorem :: FUi15: a:=b in rng p or AddTo(a, b) in rng p or SubFrom(a, b) in rng p or MultBy(a, b) in rng p or Divide(a, b) in rng p implies FirstNotUsed p <> a & FirstNotUsed p <> b proof assume a:=b in rng p or AddTo(a, b) in rng p or SubFrom(a, b) in rng p or MultBy(a, b) in rng p or Divide(a, b) in rng p; then consider i being Instruction of SCM+FSA such that A1: i in rng p & (i = a:=b or i = AddTo(a, b) or i = SubFrom(a, b) or i = MultBy(a, b) or i = Divide(a, b)); UsedIntLoc i = {a, b} by A1,Th18; then {a, b} c= UsedIntLoc p & not FirstNotUsed p in UsedIntLoc p by A1,Th23, Th54; hence FirstNotUsed p <> a & FirstNotUsed p <> b by ZFMISC_1:38; end; theorem :: FUi78: a=0_goto l in rng p or a>0_goto l in rng p implies FirstNotUsed p <> a proof assume a=0_goto l in rng p or a>0_goto l in rng p; then consider i being Instruction of SCM+FSA such that A1: i in rng p & (i = a=0_goto l or i = a>0_goto l); UsedIntLoc i = {a} by A1,Th20; then {a} c= UsedIntLoc p & not FirstNotUsed p in UsedIntLoc p by A1,Th23, Th54; hence FirstNotUsed p <> a by ZFMISC_1:37; end; theorem :: FUi910: b := (f, a) in rng p or (f, a) := b in rng p implies FirstNotUsed p <> a & FirstNotUsed p <> b proof assume b := (f, a) in rng p or (f, a) := b in rng p; then consider i being Instruction of SCM+FSA such that A1: i in rng p & (i = b := (f, a) or i = (f, a) := b); UsedIntLoc i = {a, b} by A1,Th21; then {a, b} c= UsedIntLoc p & not FirstNotUsed p in UsedIntLoc p by A1,Th23, Th54; hence FirstNotUsed p <> a & FirstNotUsed p <> b by ZFMISC_1:38; end; theorem :: FUi1112: a :=len f in rng p or f :=<0,...,0>a in rng p implies FirstNotUsed p <> a proof assume a :=len f in rng p or f :=<0,...,0>a in rng p; then consider i being Instruction of SCM+FSA such that A1: i in rng p & (i = a :=len f or i = f :=<0,...,0>a); UsedIntLoc i = {a} by A1,Th22; then {a} c= UsedIntLoc p & not FirstNotUsed p in UsedIntLoc p by A1,Th23, Th54; hence FirstNotUsed p <> a by ZFMISC_1:37; end; begin :: Choosing finite sequence location not used in a macro instruction reserve L for finite Subset of FinSeq-Locations; definition let L be finite Subset of FinSeq-Locations; func First*NotIn L -> FinSeq-Location means :Def8: ex sn being non empty Subset of NAT st it = fsloc min sn & sn = {k where k is Nat : not fsloc k in L}; existence proof defpred X[Nat] means not fsloc $1 in L; set sn = {k where k is Nat : X[k]}; A1: sn is Subset of NAT from SubsetD; not FinSeq-Locations c= L by SCMFSA_2:23,XBOOLE_0:def 10; then consider x being set such that A2: x in FinSeq-Locations & not x in L by TARSKI:def 3; reconsider x as FinSeq-Location by A2,SCMFSA_2:12; consider k being Nat such that A3: x = fsloc k by SCMFSA_2:20; k in sn by A2,A3; then reconsider sn as non empty Subset of NAT by A1; take fsloc min sn, sn; thus thesis; end; uniqueness; end; theorem Th59: not First*NotIn L in L proof set FNI = First*NotIn L; consider sn being non empty Subset of NAT such that A1: FNI = fsloc min sn and A2: sn = {k where k is Nat : not fsloc k in L} by Def8; min sn in sn by CQC_SIM1:def 8; then consider k being Nat such that A3: k = min sn & not fsloc k in L by A2; thus not FNI in L by A1,A3; end; theorem :: FFNI2: First*NotIn L = fsloc m & not fsloc n in L implies m <= n proof assume A1: First*NotIn L = fsloc m & not fsloc n in L; consider sn being non empty Subset of NAT such that A2: First*NotIn L = fsloc min sn and A3: sn = {k where k is Nat : not fsloc k in L} by Def8; A4: m = min sn by A1,A2,SCMFSA_2:17; n in sn by A1,A3; hence m <= n by A4,CQC_SIM1:def 8; end; definition let p be programmed FinPartState of SCM+FSA; func First*NotUsed p -> FinSeq-Location means :Def9: ex sil being finite Subset of FinSeq-Locations st sil = UsedInt*Loc p & it = First*NotIn sil; existence proof take First*NotIn UsedInt*Loc p, UsedInt*Loc p; thus thesis; end; uniqueness; end; theorem Th61: not First*NotUsed p in UsedInt*Loc p proof consider sil being finite Subset of FinSeq-Locations such that A1: sil = UsedInt*Loc p & First*NotUsed p = First*NotIn sil by Def9; thus thesis by A1,Th59; end; theorem :: FFUi910: b := (f, a) in rng p or (f, a) := b in rng p implies First*NotUsed p <> f proof assume b := (f, a) in rng p or (f, a) := b in rng p; then consider i being Instruction of SCM+FSA such that A1: i in rng p & (i = b := (f, a) or i = (f, a) := b); UsedInt*Loc i = {f} by A1,Th37; then {f} c= UsedInt*Loc p & not First*NotUsed p in UsedInt*Loc p by A1,Th39,Th61; hence First*NotUsed p <> f by ZFMISC_1:37; end; theorem :: FFUi1112: a :=len f in rng p or f :=<0,...,0>a in rng p implies First*NotUsed p <> f proof assume a :=len f in rng p or f :=<0,...,0>a in rng p; then consider i being Instruction of SCM+FSA such that A1: i in rng p & (i = a :=len f or i = f :=<0,...,0>a); UsedInt*Loc i = {f} by A1,Th38; then {f} c= UsedInt*Loc p & not First*NotUsed p in UsedInt*Loc p by A1,Th39,Th61; hence First*NotUsed p <> f by ZFMISC_1:37; end; begin :: Semantics reserve s, t for State of SCM+FSA; theorem Th64: dom I misses dom Start-At insloc n proof A1: dom Start-At insloc n = {IC SCM+FSA} by AMI_3:34; A2: dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13; assume dom I /\ dom (Start-At insloc n) <> {}; then consider x being set such that A3: x in dom I /\ dom (Start-At insloc n) by XBOOLE_0:def 1; x in dom I & x in dom (Start-At insloc n) by A3,XBOOLE_0:def 3; then IC SCM+FSA in dom I by A1,TARSKI:def 1; hence contradiction by A2,AMI_1:48; end; theorem Th65: IC SCM+FSA in dom (I +* Start-At insloc n) proof dom Start-At insloc n = {IC SCM+FSA} by AMI_3:34; then IC SCM+FSA in dom Start-At insloc n by TARSKI:def 1; hence IC SCM+FSA in dom (I +* Start-At insloc n) by FUNCT_4:13; end; theorem Th66: (I +* Start-At insloc n).IC SCM+FSA = insloc n proof dom Start-At insloc n = {IC SCM+FSA} by AMI_3:34; then A1: IC SCM+FSA in dom Start-At insloc n by TARSKI:def 1; Start-At insloc n = IC SCM+FSA .--> insloc n by AMI_3:def 12; then (Start-At insloc n).IC SCM+FSA = insloc n by CQC_LANG:6; hence (I +* Start-At insloc n).IC SCM+FSA = insloc n by A1,FUNCT_4:14; end; theorem Th67: I +* Start-At insloc n c= s implies IC s = insloc n proof assume A1: I +* Start-At insloc n c= s; A2: IC SCM+FSA in dom (I +* Start-At insloc n) by Th65; thus IC s = s.IC SCM+FSA by AMI_1:def 15 .= (I +* Start-At insloc n).IC SCM+FSA by A1,A2,GRFUNC_1:8 .= insloc n by Th66; end; theorem Th68: not c in UsedIntLoc i implies Exec(i, s).c = s.c proof assume A1: not c in UsedIntLoc i; A2: InsCode i <= 11+1 by SCMFSA_2:35; A3: InsCode i <= 10+1 implies InsCode i <= 10 or InsCode i = 11 by NAT_1:26; A4: InsCode i <= 9+1 implies InsCode i <= 8+1 or InsCode i = 10 by NAT_1:26; A5: InsCode i <= 8+1 implies InsCode i <= 7+1 or InsCode i = 9 by NAT_1:26; per cases by A2,A3,A4,A5,CQC_THE1:9,NAT_1:26; suppose InsCode i = 0; then i = halt SCM+FSA by SCMFSA_2:122; hence Exec(i, s).c = s.c by AMI_1:def 8; suppose InsCode i = 1; then consider a, b such that A6: i = a:=b by SCMFSA_2:54; UsedIntLoc i = {a, b} by A6,Th18; then c <> a by A1,TARSKI:def 2; hence Exec(i, s).c = s.c by A6,SCMFSA_2:89; suppose InsCode i = 2; then consider a, b such that A7: i = AddTo(a,b) by SCMFSA_2:55; UsedIntLoc i = {a, b} by A7,Th18; then c <> a by A1,TARSKI:def 2; hence Exec(i, s).c = s.c by A7,SCMFSA_2:90; suppose InsCode i = 3; then consider a, b such that A8: i = SubFrom(a, b) by SCMFSA_2:56; UsedIntLoc i = {a, b} by A8,Th18; then c <> a by A1,TARSKI:def 2; hence Exec(i, s).c = s.c by A8,SCMFSA_2:91; suppose InsCode i = 4; then consider a, b such that A9: i = MultBy(a, b) by SCMFSA_2:57; UsedIntLoc i = {a, b} by A9,Th18; then c <> a by A1,TARSKI:def 2; hence Exec(i, s).c = s.c by A9,SCMFSA_2:92; suppose InsCode i = 5; then consider a, b such that A10: i = Divide(a, b) by SCMFSA_2:58; UsedIntLoc i = {a, b} by A10,Th18; then c <> a & c <> b by A1,TARSKI:def 2; hence Exec(i, s).c = s.c by A10,SCMFSA_2:93; suppose InsCode i = 6; then consider l such that A11: i = goto l by SCMFSA_2:59; thus Exec(i, s).c = s.c by A11,SCMFSA_2:95; suppose InsCode i = 7; then consider l, a such that A12: i = a=0_goto l by SCMFSA_2:60; thus Exec(i, s).c = s.c by A12,SCMFSA_2:96; suppose InsCode i = 8; then consider l, a such that A13: i = a>0_goto l by SCMFSA_2:61; thus Exec(i, s).c = s.c by A13,SCMFSA_2:97; suppose InsCode i = 9; then consider a, b, f such that A14: i = b:=(f,a) by SCMFSA_2:62; UsedIntLoc i = {a, b} by A14,Th21; then c <> b by A1,TARSKI:def 2; hence Exec(i, s).c = s.c by A14,SCMFSA_2:98; suppose InsCode i = 10; then consider a, b, f such that A15: i = (f,a):=b by SCMFSA_2:63; thus Exec(i, s).c = s.c by A15,SCMFSA_2:99; suppose InsCode i = 11; then consider a, f such that A16: i = a:=len f by SCMFSA_2:64; UsedIntLoc i = {a} by A16,Th22; then c <> a by A1,TARSKI:def 1; hence Exec(i, s).c = s.c by A16,SCMFSA_2:100; suppose InsCode i = 12; then consider a,f such that A17: i = f:=<0,...,0>a by SCMFSA_2:65; thus Exec(i, s).c = s.c by A17,SCMFSA_2:101; end; theorem :: UIOneS: I+*Start-At insloc 0 c= s & (for m st m < n holds IC (Computation s).m in dom I) & not a in UsedIntLoc I implies (Computation s).n.a = s.a proof assume A1: I+*Start-At insloc 0 c= s & (for m st m < n holds IC (Computation s).m in dom I) & not a in UsedIntLoc I; defpred X[Nat] means $1 <= n implies (Computation s).$1.a = s.a; A2: X[0] by AMI_1:def 19; A3: for m st X[m] holds X[m+1] proof let m; set sm = (Computation s).m; assume A4: m <= n implies sm.a = s.a; assume A5: m+1 <= n; then m < n by NAT_1:38; then A6: IC sm in dom I by A1; then A7: I.IC sm in rng I by FUNCT_1:def 5; dom I misses dom Start-At insloc 0 by Th64; then I c= I+*Start-At insloc 0 by FUNCT_4:33; then I c= s by A1,XBOOLE_1:1; then I c= sm by AMI_3:38; then I.IC sm = sm.IC sm by A6,GRFUNC_1:8; then UsedIntLoc sm.IC sm c= UsedIntLoc I by A7,Th23; then A8: not a in UsedIntLoc sm.IC sm by A1; thus (Computation s).(m+1).a = (Following sm).a by AMI_1:def 19 .= (Exec(CurInstr sm, sm)).a by AMI_1:def 18 .= (Exec(sm.IC sm, sm)).a by AMI_1:def 17 .= s.a by A4,A5,A8,Th68,NAT_1:38; end; for m holds X[m] from Ind(A2, A3); hence (Computation s).n.a = s.a; end; theorem Th70: not f in UsedInt*Loc i implies Exec(i, s).f = s.f proof assume A1: not f in UsedInt*Loc i; A2: InsCode i <= 11+1 by SCMFSA_2:35; A3: InsCode i <= 10+1 implies InsCode i <= 10 or InsCode i = 11 by NAT_1:26; A4: InsCode i <= 9+1 implies InsCode i <= 8+1 or InsCode i = 10 by NAT_1:26; A5: InsCode i <= 8+1 implies InsCode i <= 7+1 or InsCode i = 9 by NAT_1:26; per cases by A2,A3,A4,A5,CQC_THE1:9,NAT_1:26; suppose InsCode i = 0; then i = halt SCM+FSA by SCMFSA_2:122; hence Exec(i, s).f = s.f by AMI_1:def 8; suppose InsCode i = 1; then consider a, b such that A6: i = a:=b by SCMFSA_2:54; thus Exec(i, s).f = s.f by A6,SCMFSA_2:89; suppose InsCode i = 2; then consider a, b such that A7: i = AddTo(a,b) by SCMFSA_2:55; thus Exec(i, s).f = s.f by A7,SCMFSA_2:90; suppose InsCode i = 3; then consider a, b such that A8: i = SubFrom(a, b) by SCMFSA_2:56; thus Exec(i, s).f = s.f by A8,SCMFSA_2:91; suppose InsCode i = 4; then consider a, b such that A9: i = MultBy(a, b) by SCMFSA_2:57; thus Exec(i, s).f = s.f by A9,SCMFSA_2:92; suppose InsCode i = 5; then consider a, b such that A10: i = Divide(a, b) by SCMFSA_2:58; thus Exec(i, s).f = s.f by A10,SCMFSA_2:93; suppose InsCode i = 6; then consider l such that A11: i = goto l by SCMFSA_2:59; thus Exec(i, s).f = s.f by A11,SCMFSA_2:95; suppose InsCode i = 7; then consider l, a such that A12: i = a=0_goto l by SCMFSA_2:60; thus Exec(i, s).f = s.f by A12,SCMFSA_2:96; suppose InsCode i = 8; then consider l, a such that A13: i = a>0_goto l by SCMFSA_2:61; thus Exec(i, s).f = s.f by A13,SCMFSA_2:97; suppose InsCode i = 9; then consider a, b, g such that A14: i = b:=(g,a) by SCMFSA_2:62; thus Exec(i, s).f = s.f by A14,SCMFSA_2:98; suppose InsCode i = 10; then consider a, b, g such that A15: i = (g,a):=b by SCMFSA_2:63; UsedInt*Loc i = {g} by A15,Th37; then f <> g by A1,TARSKI:def 1; hence Exec(i, s).f = s.f by A15,SCMFSA_2:99; suppose InsCode i = 11; then consider a, g such that A16: i = a:=len g by SCMFSA_2:64; thus Exec(i, s).f = s.f by A16,SCMFSA_2:100; suppose InsCode i = 12; then consider a,g such that A17: i = g:=<0,...,0>a by SCMFSA_2:65; UsedInt*Loc i = {g} by A17,Th38; then f <> g by A1,TARSKI:def 1; hence Exec(i, s).f = s.f by A17,SCMFSA_2:101; end; theorem :: UIFOneS: I+*Start-At insloc 0 c= s & (for m st m < n holds IC (Computation s).m in dom I) & not f in UsedInt*Loc I implies (Computation s).n.f = s.f proof assume A1: I+*Start-At insloc 0 c= s & (for m st m < n holds IC (Computation s).m in dom I) & not f in UsedInt*Loc I; defpred X[Nat] means $1 <= n implies (Computation s).$1.f = s.f; A2: X[0] by AMI_1:def 19; A3: for m st X[m] holds X[m+1] proof let m; set sm = (Computation s).m; assume A4: m <= n implies sm.f = s.f; assume A5: m+1 <= n; then m < n by NAT_1:38; then A6: IC sm in dom I by A1; then A7: I.IC sm in rng I by FUNCT_1:def 5; dom I misses dom Start-At insloc 0 by Th64; then I c= I+*Start-At insloc 0 by FUNCT_4:33; then I c= s by A1,XBOOLE_1:1; then I c= sm by AMI_3:38; then I.IC sm = sm.IC sm by A6,GRFUNC_1:8; then UsedInt*Loc sm.IC sm c= UsedInt*Loc I by A7,Th39; then A8: not f in UsedInt*Loc sm.IC sm by A1; thus (Computation s).(m+1).f = (Following sm).f by AMI_1:def 19 .= (Exec(CurInstr sm, sm)).f by AMI_1:def 18 .= (Exec(sm.IC sm, sm)).f by AMI_1:def 17 .= s.f by A4,A5,A8,Th70,NAT_1:38; end; for m holds X[m] from Ind(A2, A3); hence (Computation s).n.f = s.f; end; theorem Th72: s | UsedIntLoc i = t | UsedIntLoc i & s | UsedInt*Loc i = t | UsedInt*Loc i & IC s = IC t implies IC Exec(i, s) = IC Exec(i, t) & Exec(i, s) | UsedIntLoc i = Exec(i, t) | UsedIntLoc i & Exec(i, s) | UsedInt*Loc i = Exec(i, t) | UsedInt*Loc i proof assume A1: s | UsedIntLoc i = t | UsedIntLoc i & s | UsedInt*Loc i = t | UsedInt*Loc i & IC s = IC t; set Es = Exec(i, s); set Et = Exec(i, t); set Ui = UsedIntLoc i; set UFi = UsedInt*Loc i; A2: dom Es = the carrier of SCM+FSA by AMI_3:36 .= dom Et by AMI_3:36; A3: InsCode i <= 11+1 by SCMFSA_2:35; A4: InsCode i <= 10+1 implies InsCode i <= 10 or InsCode i = 11 by NAT_1:26; A5: InsCode i <= 9+1 implies InsCode i <= 8+1 or InsCode i = 10 by NAT_1:26; A6: InsCode i <= 8+1 implies InsCode i <= 7+1 or InsCode i = 9 by NAT_1:26; per cases by A3,A4,A5,A6,CQC_THE1:9,NAT_1:26; suppose InsCode i = 0; then i = halt SCM+FSA by SCMFSA_2:122; then Exec(i, s) = s & Exec(i, t) = t by AMI_1:def 8; hence IC Exec(i, s) = IC Exec(i, t) & Exec(i, s) | UsedIntLoc i = Exec(i, t) | UsedIntLoc i & Exec(i, s) | UsedInt*Loc i = Exec(i, t) | UsedInt*Loc i by A1; suppose InsCode i = 1; then consider a, b such that A7: i = a:=b by SCMFSA_2:54; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A7,SCMFSA_2:89 .= Et.IC SCM+FSA by A7,SCMFSA_2:89 .= IC Et by AMI_1:def 15; A8: Ui = {a, b} & UFi = {} by A7,Th18,Th36; then A9: a in Ui & b in Ui by TARSKI:def 2; then s.a = (s | Ui).a & s.b = (s | Ui).b by FUNCT_1:72; then A10: s.a = t.a & s.b = t.b by A1,A9,FUNCT_1:72; a = b or a <> b; then Es.a = s.b & Es.b = s.b & Et.a = t.b & Et.b = t.b by A7,SCMFSA_2:89; hence Es | Ui = Et | Ui by A2,A8,A10,AMI_3:25; thus Es | UFi = {} by A8,RELAT_1:110 .= Et | UFi by A8,RELAT_1:110; suppose InsCode i = 2; then consider a, b such that A11: i = AddTo(a,b) by SCMFSA_2:55; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A11,SCMFSA_2:90 .= Et.IC SCM+FSA by A11,SCMFSA_2:90 .= IC Et by AMI_1:def 15; A12: Ui = {a, b} & UFi = {} by A11,Th18,Th36; then A13: a in Ui & b in Ui by TARSKI:def 2; then s.a = (s | Ui).a & s.b = (s | Ui).b by FUNCT_1:72; then A14: s.a = t.a & s.b = t.b by A1,A13,FUNCT_1:72; A15: Es.a = s.a + s.b & Et.a = t.a + t.b by A11,SCMFSA_2:90; now per cases; case a = b; hence Es.b = s.a + s.b & Et.b = t.a + t.b by A11,SCMFSA_2:90; case a<> b; hence Es.b = s.b & Et.b = t.b by A11,SCMFSA_2:90; end; hence Es | Ui = Et | Ui by A2,A12,A14,A15,AMI_3:25; thus Es | UFi = {} by A12,RELAT_1:110 .= Et | UFi by A12,RELAT_1:110; suppose InsCode i = 3; then consider a, b such that A16: i = SubFrom(a, b) by SCMFSA_2:56; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A16,SCMFSA_2:91 .= Et.IC SCM+FSA by A16,SCMFSA_2:91 .= IC Et by AMI_1:def 15; A17: Ui = {a, b} & UFi = {} by A16,Th18,Th36; then A18: a in Ui & b in Ui by TARSKI:def 2; then s.a = (s | Ui).a & s.b = (s | Ui).b by FUNCT_1:72; then A19: s.a = t.a & s.b = t.b by A1,A18,FUNCT_1:72; A20: Es.a = s.a - s.b & Et.a = t.a - t.b by A16,SCMFSA_2:91; now per cases; case a = b; hence Es.b = s.a - s.b & Et.b = t.a - t.b by A16,SCMFSA_2:91; case a<> b; hence Es.b = s.b & Et.b = t.b by A16,SCMFSA_2:91; end; hence Es | Ui = Et | Ui by A2,A17,A19,A20,AMI_3:25; thus Es | UFi = {} by A17,RELAT_1:110 .= Et | UFi by A17,RELAT_1:110; suppose InsCode i = 4; then consider a, b such that A21: i = MultBy(a, b) by SCMFSA_2:57; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A21,SCMFSA_2:92 .= Et.IC SCM+FSA by A21,SCMFSA_2:92 .= IC Et by AMI_1:def 15; A22: Ui = {a, b} & UFi = {} by A21,Th18,Th36; then A23: a in Ui & b in Ui by TARSKI:def 2; then s.a = (s | Ui).a & s.b = (s | Ui).b by FUNCT_1:72; then A24: s.a = t.a & s.b = t.b by A1,A23,FUNCT_1:72; A25: Es.a = s.a * s.b & Et.a = t.a * t.b by A21,SCMFSA_2:92; now per cases; case a = b; hence Es.b = s.a * s.b & Et.b = t.a * t.b by A21,SCMFSA_2:92; case a<> b; hence Es.b = s.b & Et.b = t.b by A21,SCMFSA_2:92; end; hence Es | Ui = Et | Ui by A2,A22,A24,A25,AMI_3:25; thus Es | UFi = {} by A22,RELAT_1:110 .= Et | UFi by A22,RELAT_1:110; suppose InsCode i = 5; then consider a, b such that A26: i = Divide(a, b) by SCMFSA_2:58; A27: Ui = {a, b} & UFi = {} by A26,Th18,Th36; then A28: a in Ui & b in Ui by TARSKI:def 2; then s.a = (s | Ui).a & s.b = (s | Ui).b by FUNCT_1:72; then A29: s.a = t.a & s.b = t.b by A1,A28,FUNCT_1:72; hereby per cases; suppose A30: a = b; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A26,A30,SCMFSA_2:94 .= Et.IC SCM+FSA by A26,A30,SCMFSA_2:94 .= IC Et by AMI_1:def 15; Es.a = s.a mod s.a & Et.a = t.a mod t.b by A26,A30,SCMFSA_2:94; hence Es | Ui = Et | Ui by A2,A27,A29,A30,AMI_3:25; thus Es | UFi = {} by A27,RELAT_1:110 .= Et | UFi by A27,RELAT_1:110; suppose A31: a <> b; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A26,SCMFSA_2:93 .= Et.IC SCM+FSA by A26,SCMFSA_2:93 .= IC Et by AMI_1:def 15; Es.a = s.a div s.b & Et.a = t.a div t.b & Es.b = s.a mod s.b & Et.b = t.a mod t.b by A26,A31,SCMFSA_2:93; hence Es | Ui = Et | Ui by A2,A27,A29,AMI_3:25; thus Es | UFi = {} by A27,RELAT_1:110 .= Et | UFi by A27,RELAT_1:110; end; suppose InsCode i = 6; then consider l such that A32: i = goto l by SCMFSA_2:59; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= l by A32,SCMFSA_2:95 .= Et.IC SCM+FSA by A32,SCMFSA_2:95 .= IC Et by AMI_1:def 15; A33: Ui = {} & UFi = {} by A32,Th19,Th36; hence Es | Ui = {} by RELAT_1:110 .= Et | Ui by A33,RELAT_1:110; thus Es | UFi = {} by A33,RELAT_1:110 .= Et | UFi by A33,RELAT_1:110; suppose InsCode i = 7; then consider l, a such that A34: i = a=0_goto l by SCMFSA_2:60; A35: Ui = {a} & UFi = {} by A34,Th20,Th36; then A36: a in Ui by TARSKI:def 1; then s.a = (s | Ui).a by FUNCT_1:72; then A37: s.a = t.a by A1,A36,FUNCT_1:72; hereby per cases; suppose A38: s.a = 0; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= l by A34,A38,SCMFSA_2:96 .= Et.IC SCM+FSA by A34,A37,A38,SCMFSA_2:96 .= IC Et by AMI_1:def 15; suppose A39: s.a <> 0; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC s by A34,A39,SCMFSA_2:96 .= Et.IC SCM+FSA by A1,A34,A37,A39,SCMFSA_2:96 .= IC Et by AMI_1:def 15; end; Es.a = s.a & Et.a = t.a by A34,SCMFSA_2:96; hence Es | Ui = Et | Ui by A2,A35,A37,AMI_3:24; thus Es | UFi = {} by A35,RELAT_1:110 .= Et | UFi by A35,RELAT_1:110; suppose InsCode i = 8; then consider l, a such that A40: i = a>0_goto l by SCMFSA_2:61; A41: Ui = {a} & UFi = {} by A40,Th20,Th36; then A42: a in Ui by TARSKI:def 1; then s.a = (s | Ui).a by FUNCT_1:72; then A43: s.a = t.a by A1,A42,FUNCT_1:72; hereby per cases; suppose A44: s.a > 0; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= l by A40,A44,SCMFSA_2:97 .= Et.IC SCM+FSA by A40,A43,A44,SCMFSA_2:97 .= IC Et by AMI_1:def 15; suppose A45: s.a <= 0; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC s by A40,A45,SCMFSA_2:97 .= Et.IC SCM+FSA by A1,A40,A43,A45,SCMFSA_2:97 .= IC Et by AMI_1:def 15; end; Es.a = s.a & Et.a = t.a by A40,SCMFSA_2:97; hence Es | Ui = Et | Ui by A2,A41,A43,AMI_3:24; thus Es | UFi = {} by A41,RELAT_1:110 .= Et | UFi by A41,RELAT_1:110; suppose InsCode i = 9; then consider a, b, f such that A46: i = b:=(f,a) by SCMFSA_2:62; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A46,SCMFSA_2:98 .= Et.IC SCM+FSA by A46,SCMFSA_2:98 .= IC Et by AMI_1:def 15; A47: Ui = {a, b} & UFi = {f} by A46,Th21,Th37; then A48: a in Ui & b in Ui & f in UFi by TARSKI:def 1,def 2; then s.a = (s | Ui).a & s.b = (s | Ui).b & s.f = (s | UFi).f by FUNCT_1:72 ; then A49: s.a = t.a & s.b = t.b & s.f = t.f by A1,A48,FUNCT_1:72; consider m such that A50: m = abs(s.a) & Es.b = (s.f)/.m by A46,SCMFSA_2:98; consider n such that A51: n = abs(t.a) & Et.b = (t.f)/.n by A46,SCMFSA_2:98; A52: Es.f = s.f & Et.f = t.f by A46,SCMFSA_2:98; now per cases; case a = b; thus Es.b = Et.b by A49,A50,A51; case a <> b; hence Es.a = s.a & Et.a = t.a by A46,SCMFSA_2:98; end; hence Es | Ui = Et | Ui by A2,A47,A49,A50,A51,AMI_3:25; thus Es | UFi = Et | UFi by A2,A47,A49,A52,AMI_3:24; suppose InsCode i = 10; then consider a, b, f such that A53: i = (f,a):=b by SCMFSA_2:63; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A53,SCMFSA_2:99 .= Et.IC SCM+FSA by A53,SCMFSA_2:99 .= IC Et by AMI_1:def 15; A54: Ui = {a, b} & UFi = {f} by A53,Th21,Th37; then A55: a in Ui & b in Ui & f in UFi by TARSKI:def 1,def 2; then s.a = (s | Ui).a & s.b = (s | Ui).b & s.f = (s | UFi).f by FUNCT_1:72 ; then A56: s.a = t.a & s.b = t.b & s.f = t.f by A1,A55,FUNCT_1:72; consider m such that A57: m = abs(s.a) & Es.f = s.f+*(m,s.b) by A53,SCMFSA_2:99; consider n such that A58: n = abs(t.a) & Et.f = t.f+*(n,t.b) by A53,SCMFSA_2:99; Es.a = s.a & Es.b = s.b & Et.a = t.a & Et.b = t.b by A53,SCMFSA_2:99; hence Es | Ui = Et | Ui by A2,A54,A56,AMI_3:25; thus Es | UFi = Et | UFi by A2,A54,A56,A57,A58,AMI_3:24; suppose InsCode i = 11; then consider a, f such that A59: i = a:=len f by SCMFSA_2:64; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A59,SCMFSA_2:100 .= Et.IC SCM+FSA by A59,SCMFSA_2:100 .= IC Et by AMI_1:def 15; A60: Ui = {a} & UFi = {f} by A59,Th22,Th38; then A61: a in Ui & f in UFi by TARSKI:def 1; then s.a = (s | Ui).a & s.f = (s | UFi).f by FUNCT_1:72; then A62: s.a = t.a & s.f = t.f by A1,A61,FUNCT_1:72; A63: Es.a = len(s.f) & Es.f = s.f & Et.a = len(t.f) & Et.f = t.f by A59,SCMFSA_2:100; hence Es | Ui = Et | Ui by A2,A60,A62,AMI_3:24; thus Es | UFi = Et | UFi by A2,A60,A62,A63,AMI_3:24; suppose InsCode i = 12; then consider a,f such that A64: i = f:=<0,...,0>a by SCMFSA_2:65; thus IC Es = Es.IC SCM+FSA by AMI_1:def 15 .= Next IC t by A1,A64,SCMFSA_2:101 .= Et.IC SCM+FSA by A64,SCMFSA_2:101 .= IC Et by AMI_1:def 15; A65: Ui = {a} & UFi = {f} by A64,Th22,Th38; then A66: a in Ui & f in UFi by TARSKI:def 1; then s.a = (s | Ui).a & s.f = (s | UFi).f by FUNCT_1:72; then A67: s.a = t.a & s.f = t.f by A1,A66,FUNCT_1:72; consider m such that A68: m = abs(s.a) & Es.f = m |-> 0 by A64,SCMFSA_2:101; consider n such that A69: n = abs(t.a) & Et.f = n |-> 0 by A64,SCMFSA_2:101; Es.a = s.a & Et.a = t.a by A64,SCMFSA_2:101; hence Es | Ui = Et | Ui by A2,A65,A67,AMI_3:24; thus Es | UFi = Et | UFi by A2,A65,A67,A68,A69,AMI_3:24; end; theorem :: UITwoS: I+*Start-At insloc 0 c= s & I+*Start-At insloc 0 c= t & s | UsedIntLoc I = t | UsedIntLoc I & s | UsedInt*Loc I = t | UsedInt*Loc I & (for m st m < n holds IC (Computation s).m in dom I) implies (for m st m < n holds IC (Computation t).m in dom I) & for m st m <= n holds IC (Computation s).m = IC (Computation t).m & (for a st a in UsedIntLoc I holds (Computation s).m.a = (Computation t).m.a) & for f st f in UsedInt*Loc I holds (Computation s).m.f = (Computation t).m.f proof assume that A1: I+*Start-At insloc 0 c= s & I+*Start-At insloc 0 c= t and A2: s | UsedIntLoc I = t | UsedIntLoc I & s | UsedInt*Loc I = t | UsedInt*Loc I and A3: for m st m < n holds IC (Computation s).m in dom I; defpred P[Nat] means $1 < n implies IC (Computation t).$1 in dom I & IC (Computation s).$1 = IC (Computation t).$1 & (for a st a in UsedIntLoc I holds (Computation s).$1.a = (Computation t).$1.a) & for f st f in UsedInt*Loc I holds (Computation s).$1.f = (Computation t).$1.f; A4: P[0] proof assume A5: 0 < n; A6: IC (Computation s).0 = IC s by AMI_1:def 19 .= insloc 0 by A1,Th67; A7: IC (Computation t).0 = IC t by AMI_1:def 19 .= insloc 0 by A1,Th67; hence IC (Computation t).0 in dom I by A3,A5,A6; thus IC (Computation s).0 = IC (Computation t).0 by A6,A7; hereby let a; assume A8: a in UsedIntLoc I; thus (Computation s).0.a = s.a by AMI_1:def 19 .= (s | UsedIntLoc I).a by A8,FUNCT_1:72 .= t.a by A2,A8,FUNCT_1:72 .= (Computation t).0.a by AMI_1:def 19; end; let f; assume A9: f in UsedInt*Loc I; thus (Computation s).0.f = s.f by AMI_1:def 19 .= (s | UsedInt*Loc I).f by A9,FUNCT_1:72 .= t.f by A2,A9,FUNCT_1:72 .= (Computation t).0.f by AMI_1:def 19; end; set Cs = Computation s; set Ct = Computation t; A10: now let m; assume A11: P[m]; thus P[m+1] proof set m1 = m+1; assume A12: m1 < n; then A13: m < n by NAT_1:38; A14: Cs.m1 = Following Cs.m by AMI_1:def 19 .= Exec(CurInstr Cs.m, Cs.m) by AMI_1:def 18 .= Exec(Cs.m.IC Cs.m, Cs.m) by AMI_1:def 17; A15: Ct.m1 = Following Ct.m by AMI_1:def 19 .= Exec(CurInstr Ct.m, Ct.m) by AMI_1:def 18 .= Exec(Ct.m.IC Ct.m, Ct.m) by AMI_1:def 17; dom I misses dom Start-At insloc 0 by Th64; then I c= I +* Start-At insloc 0 by FUNCT_4:33; then I c= s & I c= t by A1,XBOOLE_1:1; then A16: I c= Cs.m & I c= Ct.m by AMI_3:38; then A17: Cs.m.IC Cs.m = I.IC Cs.m by A11,A12,GRFUNC_1:8,NAT_1:38; then A18: Cs.m.IC Cs.m = Ct.m.IC Ct.m by A11,A12,A16,GRFUNC_1:8,NAT_1:38; set i = Cs.m.IC Cs.m; IC Cs.m in dom I by A3,A13; then A19: i in rng I by A17,FUNCT_1:def 5; then A20: UsedIntLoc i c= UsedIntLoc I by Th23; now thus dom (Cs.m | UsedIntLoc I) = dom (Cs.m) /\ UsedIntLoc I by RELAT_1:90 .= (dom the Object-Kind of SCM+FSA) /\ UsedIntLoc I by CARD_3:18 .= dom (Ct.m) /\ UsedIntLoc I by CARD_3:18; let x be set; assume x in dom (Cs.m | UsedIntLoc I); then A21: x in UsedIntLoc I by RELAT_1:86; then reconsider x' = x as Int-Location by SCMFSA_2:11; thus (Cs.m | UsedIntLoc I).x = Cs.m.x' by A21,FUNCT_1:72 .= Ct.m.x by A11,A12,A21,NAT_1:38; end; then A22: Cs.m | UsedIntLoc I = Ct.m | UsedIntLoc I by FUNCT_1:68; A23: Cs.m | UsedIntLoc i = (Cs.m | UsedIntLoc I) | UsedIntLoc i by A20,RELAT_1:103 .= Ct.m | UsedIntLoc i by A20,A22,RELAT_1:103; A24: UsedInt*Loc i c= UsedInt*Loc I by A19,Th39; now thus dom (Cs.m | UsedInt*Loc I) = dom (Cs.m) /\ UsedInt*Loc I by RELAT_1:90 .= (dom the Object-Kind of SCM+FSA) /\ UsedInt*Loc I by CARD_3:18 .= dom (Ct.m) /\ UsedInt*Loc I by CARD_3:18; let x be set; assume x in dom (Cs.m | UsedInt*Loc I); then A25: x in UsedInt*Loc I by RELAT_1:86; then reconsider x' = x as FinSeq-Location by SCMFSA_2:12; thus (Cs.m | UsedInt*Loc I).x = Cs.m.x' by A25,FUNCT_1:72 .= Ct.m.x by A11,A12,A25,NAT_1:38; end; then A26: Cs.m | UsedInt*Loc I = Ct.m | UsedInt*Loc I by FUNCT_1:68; Cs.m | UsedInt*Loc i = (Cs.m | UsedInt*Loc I) | UsedInt*Loc i by A24,RELAT_1:103 .= Ct.m | UsedInt*Loc i by A24,A26,RELAT_1:103; then A27: Exec(i, Cs.m) | UsedIntLoc i = Exec(i, Ct.m) | UsedIntLoc i & Exec(i, Cs.m) | UsedInt*Loc i = Exec(i, Ct.m) | UsedInt*Loc i & IC Exec(i, Cs.m) = IC Exec(i, Ct.m) by A11,A12,A23,Th72,NAT_1:38; hence IC Ct.m1 in dom I by A3,A12,A14,A15,A18; thus IC Cs.m1 = IC Ct.m1 by A11,A12,A14,A15,A16,A17,A27,GRFUNC_1:8,NAT_1:38 ; hereby let a; assume A28: a in UsedIntLoc I; per cases; suppose A29: a in UsedIntLoc i; hence Cs.m1.a = (Exec(i, Cs.m) | UsedIntLoc i).a by A14,FUNCT_1:72 .= Ct.m1.a by A15,A18,A27,A29,FUNCT_1:72; suppose A30: not a in UsedIntLoc i; hence Cs.m1.a = Cs.m.a by A14,Th68 .= Ct.m.a by A11,A12,A28,NAT_1:38 .= Ct.m1.a by A15,A18,A30,Th68; end; let f; assume A31: f in UsedInt*Loc I; per cases; suppose A32: f in UsedInt*Loc i; hence Cs.m1.f = (Exec(i, Cs.m) | UsedInt*Loc i).f by A14,FUNCT_1:72 .= Ct.m1.f by A15,A18,A27,A32,FUNCT_1:72; suppose A33: not f in UsedInt*Loc i; hence Cs.m1.f = Cs.m.f by A14,Th70 .= Ct.m.f by A11,A12,A31,NAT_1:38 .= Ct.m1.f by A15,A18,A33,Th70; end; end; A34: for m holds P[m] from Ind(A4, A10); hence for m st m < n holds IC Ct.m in dom I; let m; assume A35: m <= n; per cases by NAT_1:22; suppose A36: m = 0; A37: IC (Computation s).0 = IC s by AMI_1:def 19 .= insloc 0 by A1,Th67; IC (Computation t).0 = IC t by AMI_1:def 19 .= insloc 0 by A1,Th67; hence IC (Computation s).m = IC (Computation t).m by A36,A37; hereby let a; assume A38: a in UsedIntLoc I; thus (Computation s).m.a = s.a by A36,AMI_1:def 19 .= (s | UsedIntLoc I).a by A38,FUNCT_1:72 .= t.a by A2,A38,FUNCT_1:72 .= (Computation t).m.a by A36,AMI_1:def 19; end; let f; assume A39: f in UsedInt*Loc I; thus (Computation s).m.f = s.f by A36,AMI_1:def 19 .= (s | UsedInt*Loc I).f by A39,FUNCT_1:72 .= t.f by A2,A39,FUNCT_1:72 .= (Computation t).m.f by A36,AMI_1:def 19; suppose ex p being Nat st m = p+1; then consider p being Nat such that A40: m = p+1; set p1 = p+1; A41: p < n by A35,A40,NAT_1:38; A42: Cs.p1 = Following Cs.p by AMI_1:def 19 .= Exec(CurInstr Cs.p, Cs.p) by AMI_1:def 18 .= Exec(Cs.p.IC Cs.p, Cs.p) by AMI_1:def 17; A43: Ct.p1 = Following Ct.p by AMI_1:def 19 .= Exec(CurInstr Ct.p, Ct.p) by AMI_1:def 18 .= Exec(Ct.p.IC Ct.p, Ct.p) by AMI_1:def 17; A44: IC Cs.p = IC Ct.p & IC Cs.p in dom I by A3,A34,A41; dom I misses dom Start-At insloc 0 by Th64; then I c= I +* Start-At insloc 0 by FUNCT_4:33; then I c= s & I c= t by A1,XBOOLE_1:1; then A45: I c= Cs.p & I c= Ct.p by AMI_3:38; then A46: Cs.p.IC Cs.p = I.IC Cs.p by A44,GRFUNC_1:8; then A47: Cs.p.IC Cs.p = Ct.p.IC Ct.p by A44,A45,GRFUNC_1:8; set i = Cs.p.IC Cs.p; IC Cs.p in dom I by A3,A41; then A48: i in rng I by A46,FUNCT_1:def 5; then A49: UsedIntLoc i c= UsedIntLoc I by Th23; now thus dom (Cs.p | UsedIntLoc I) = dom (Cs.p) /\ UsedIntLoc I by RELAT_1:90 .= (dom the Object-Kind of SCM+FSA) /\ UsedIntLoc I by CARD_3:18 .= dom (Ct.p) /\ UsedIntLoc I by CARD_3:18; let x be set; assume x in dom (Cs.p | UsedIntLoc I); then A50: x in UsedIntLoc I by RELAT_1:86; then reconsider x' = x as Int-Location by SCMFSA_2:11; thus (Cs.p | UsedIntLoc I).x = Cs.p.x' by A50,FUNCT_1:72 .= Ct.p.x by A34,A41,A50; end; then A51: Cs.p | UsedIntLoc I = Ct.p | UsedIntLoc I by FUNCT_1:68; A52: Cs.p | UsedIntLoc i = (Cs.p | UsedIntLoc I) | UsedIntLoc i by A49,RELAT_1:103 .= Ct.p | UsedIntLoc i by A49,A51,RELAT_1:103; A53: UsedInt*Loc i c= UsedInt*Loc I by A48,Th39; now thus dom (Cs.p | UsedInt*Loc I) = dom (Cs.p) /\ UsedInt*Loc I by RELAT_1:90 .= (dom the Object-Kind of SCM+FSA) /\ UsedInt*Loc I by CARD_3:18 .= dom (Ct.p) /\ UsedInt*Loc I by CARD_3:18; let x be set; assume x in dom (Cs.p | UsedInt*Loc I); then A54: x in UsedInt*Loc I by RELAT_1:86; then reconsider x' = x as FinSeq-Location by SCMFSA_2:12; thus (Cs.p | UsedInt*Loc I).x = Cs.p.x' by A54,FUNCT_1:72 .= Ct.p.x by A34,A41,A54; end; then A55: Cs.p | UsedInt*Loc I = Ct.p | UsedInt*Loc I by FUNCT_1:68; A56: Cs.p | UsedInt*Loc i = (Cs.p | UsedInt*Loc I) | UsedInt*Loc i by A53,RELAT_1:103 .= Ct.p | UsedInt*Loc i by A53,A55,RELAT_1:103; then A57: Exec(i, Cs.p) | UsedIntLoc i = Exec(i, Ct.p) | UsedIntLoc i & Exec(i, Cs.p) | UsedInt*Loc i = Exec(i, Ct.p) | UsedInt*Loc i & IC Exec(i, Cs.p) = IC Exec(i, Ct.p) by A44,A52,Th72; thus IC Cs.m = IC Ct.m by A40,A42,A43,A44,A47,A52,A56,Th72; hereby let a; assume A58: a in UsedIntLoc I; per cases; suppose A59: a in UsedIntLoc i; hence Cs.m.a = (Exec(i, Cs.p) | UsedIntLoc i).a by A40,A42,FUNCT_1:72 .= Ct.m.a by A40,A43,A47,A57,A59,FUNCT_1:72; suppose A60: not a in UsedIntLoc i; hence Cs.m.a = Cs.p.a by A40,A42,Th68 .= Ct.p.a by A34,A41,A58 .= Ct.m.a by A40,A43,A47,A60,Th68; end; hereby let f; assume A61: f in UsedInt*Loc I; per cases; suppose A62: f in UsedInt*Loc i; hence Cs.m.f = (Exec(i, Cs.p) | UsedInt*Loc i).f by A40,A42,FUNCT_1:72 .= Ct.m.f by A40,A43,A47,A57,A62,FUNCT_1:72; suppose A63: not f in UsedInt*Loc i; hence Cs.m.f = Cs.p.f by A40,A42,Th70 .= Ct.p.f by A34,A41,A61 .= Ct.m.f by A40,A43,A47,A63,Th70; end; end;