:: SF_MASTR semantic presentation begin theorem Th1: :: SF_MASTR:1 for a1, b1, a2, b2 being Int-Location st a1 := b1 = a2 := b2 holds ( a1 = a2 & b1 = b2 ) proof let a1, b1, a2, b2 be Int-Location; ::_thesis: ( a1 := b1 = a2 := b2 implies ( a1 = a2 & b1 = b2 ) ) assume A1: a1 := b1 = a2 := b2 ; ::_thesis: ( a1 = a2 & b1 = b2 ) consider A1, B1 being Data-Location such that A2: ( a1 = A1 & b1 = B1 & a1 := b1 = A1 := B1 ) by SCMFSA_2:def_8; consider A2, B2 being Data-Location such that A3: ( a2 = A2 & b2 = B2 & a2 := b2 = A2 := B2 ) by SCMFSA_2:def_8; A4: ( <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:44; ( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 ) by FINSEQ_1:44; hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, A4, XTUPLE_0:3; ::_thesis: verum end; theorem Th2: :: SF_MASTR:2 for a1, b1, a2, b2 being Int-Location st AddTo (a1,b1) = AddTo (a2,b2) holds ( a1 = a2 & b1 = b2 ) proof let a1, b1, a2, b2 be Int-Location; ::_thesis: ( AddTo (a1,b1) = AddTo (a2,b2) implies ( a1 = a2 & b1 = b2 ) ) assume A1: AddTo (a1,b1) = AddTo (a2,b2) ; ::_thesis: ( a1 = a2 & b1 = b2 ) consider A1, B1 being Data-Location such that A2: ( a1 = A1 & b1 = B1 & AddTo (a1,b1) = AddTo (A1,B1) ) by SCMFSA_2:def_9; consider A2, B2 being Data-Location such that A3: ( a2 = A2 & b2 = B2 & AddTo (a2,b2) = AddTo (A2,B2) ) by SCMFSA_2:def_9; A4: ( <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:44; ( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 ) by FINSEQ_1:44; hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, A4, XTUPLE_0:3; ::_thesis: verum end; theorem Th3: :: SF_MASTR:3 for a1, b1, a2, b2 being Int-Location st SubFrom (a1,b1) = SubFrom (a2,b2) holds ( a1 = a2 & b1 = b2 ) proof let a1, b1, a2, b2 be Int-Location; ::_thesis: ( SubFrom (a1,b1) = SubFrom (a2,b2) implies ( a1 = a2 & b1 = b2 ) ) assume A1: SubFrom (a1,b1) = SubFrom (a2,b2) ; ::_thesis: ( a1 = a2 & b1 = b2 ) consider A1, B1 being Data-Location such that A2: ( a1 = A1 & b1 = B1 & SubFrom (a1,b1) = SubFrom (A1,B1) ) by SCMFSA_2:def_10; consider A2, B2 being Data-Location such that A3: ( a2 = A2 & b2 = B2 & SubFrom (a2,b2) = SubFrom (A2,B2) ) by SCMFSA_2:def_10; A4: ( <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:44; ( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 ) by FINSEQ_1:44; hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, A4, XTUPLE_0:3; ::_thesis: verum end; theorem Th4: :: SF_MASTR:4 for a1, b1, a2, b2 being Int-Location st MultBy (a1,b1) = MultBy (a2,b2) holds ( a1 = a2 & b1 = b2 ) proof let a1, b1, a2, b2 be Int-Location; ::_thesis: ( MultBy (a1,b1) = MultBy (a2,b2) implies ( a1 = a2 & b1 = b2 ) ) assume A1: MultBy (a1,b1) = MultBy (a2,b2) ; ::_thesis: ( a1 = a2 & b1 = b2 ) consider A1, B1 being Data-Location such that A2: ( a1 = A1 & b1 = B1 & MultBy (a1,b1) = MultBy (A1,B1) ) by SCMFSA_2:def_11; consider A2, B2 being Data-Location such that A3: ( a2 = A2 & b2 = B2 & MultBy (a2,b2) = MultBy (A2,B2) ) by SCMFSA_2:def_11; A4: ( <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:44; ( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 ) by FINSEQ_1:44; hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, A4, XTUPLE_0:3; ::_thesis: verum end; theorem Th5: :: SF_MASTR:5 for a1, b1, a2, b2 being Int-Location st Divide (a1,b1) = Divide (a2,b2) holds ( a1 = a2 & b1 = b2 ) proof let a1, b1, a2, b2 be Int-Location; ::_thesis: ( Divide (a1,b1) = Divide (a2,b2) implies ( a1 = a2 & b1 = b2 ) ) assume A1: Divide (a1,b1) = Divide (a2,b2) ; ::_thesis: ( a1 = a2 & b1 = b2 ) consider A1, B1 being Data-Location such that A2: ( a1 = A1 & b1 = B1 & Divide (a1,b1) = Divide (A1,B1) ) by SCMFSA_2:def_12; consider A2, B2 being Data-Location such that A3: ( a2 = A2 & b2 = B2 & Divide (a2,b2) = Divide (A2,B2) ) by SCMFSA_2:def_12; A4: ( <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:44; ( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 ) by FINSEQ_1:44; hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, A4, XTUPLE_0:3; ::_thesis: verum end; theorem :: SF_MASTR:6 for l1, l2 being Element of NAT st goto l1 = goto l2 holds l1 = l2 proof let l1, l2 be Element of NAT ; ::_thesis: ( goto l1 = goto l2 implies l1 = l2 ) assume A1: goto l1 = goto l2 ; ::_thesis: l1 = l2 ( <*l1*> . 1 = l1 & <*l2*> . 1 = l2 ) by FINSEQ_1:40; hence l1 = l2 by A1, XTUPLE_0:3; ::_thesis: verum end; theorem Th7: :: SF_MASTR:7 for a1, a2 being Int-Location for l1, l2 being Element of NAT st a1 =0_goto l1 = a2 =0_goto l2 holds ( a1 = a2 & l1 = l2 ) proof let a1, a2 be Int-Location; ::_thesis: for l1, l2 being Element of NAT st a1 =0_goto l1 = a2 =0_goto l2 holds ( a1 = a2 & l1 = l2 ) let l1, l2 be Element of NAT ; ::_thesis: ( a1 =0_goto l1 = a2 =0_goto l2 implies ( a1 = a2 & l1 = l2 ) ) assume A1: a1 =0_goto l1 = a2 =0_goto l2 ; ::_thesis: ( a1 = a2 & l1 = l2 ) consider A1 being Data-Location such that A2: ( a1 = A1 & a1 =0_goto l1 = A1 =0_goto l1 ) by SCMFSA_2:def_14; consider A2 being Data-Location such that A3: ( a2 = A2 & a2 =0_goto l2 = A2 =0_goto l2 ) by SCMFSA_2:def_14; A4: ( <*l2*> . 1 = l2 & <*A2*> . 1 = A2 ) by FINSEQ_1:40; ( <*l1*> . 1 = l1 & <*A1*> . 1 = A1 ) by FINSEQ_1:40; hence ( a1 = a2 & l1 = l2 ) by A1, A2, A3, A4, XTUPLE_0:3; ::_thesis: verum end; theorem Th8: :: SF_MASTR:8 for a1, a2 being Int-Location for l1, l2 being Element of NAT st a1 >0_goto l1 = a2 >0_goto l2 holds ( a1 = a2 & l1 = l2 ) proof let a1, a2 be Int-Location; ::_thesis: for l1, l2 being Element of NAT st a1 >0_goto l1 = a2 >0_goto l2 holds ( a1 = a2 & l1 = l2 ) let l1, l2 be Element of NAT ; ::_thesis: ( a1 >0_goto l1 = a2 >0_goto l2 implies ( a1 = a2 & l1 = l2 ) ) assume A1: a1 >0_goto l1 = a2 >0_goto l2 ; ::_thesis: ( a1 = a2 & l1 = l2 ) consider A1 being Data-Location such that A2: ( a1 = A1 & a1 >0_goto l1 = A1 >0_goto l1 ) by SCMFSA_2:def_15; consider A2 being Data-Location such that A3: ( a2 = A2 & a2 >0_goto l2 = A2 >0_goto l2 ) by SCMFSA_2:def_15; A4: ( <*l2*> . 1 = l2 & <*A2*> . 1 = A2 ) by FINSEQ_1:40; ( <*l1*> . 1 = l1 & <*A1*> . 1 = A1 ) by FINSEQ_1:40; hence ( a1 = a2 & l1 = l2 ) by A1, A2, A3, A4, XTUPLE_0:3; ::_thesis: verum end; theorem Th9: :: SF_MASTR:9 for b1, a1, b2, a2 being Int-Location for f1, f2 being FinSeq-Location st b1 := (f1,a1) = b2 := (f2,a2) holds ( a1 = a2 & b1 = b2 & f1 = f2 ) proof let b1, a1, b2, a2 be Int-Location; ::_thesis: for f1, f2 being FinSeq-Location st b1 := (f1,a1) = b2 := (f2,a2) holds ( a1 = a2 & b1 = b2 & f1 = f2 ) let f1, f2 be FinSeq-Location ; ::_thesis: ( b1 := (f1,a1) = b2 := (f2,a2) implies ( a1 = a2 & b1 = b2 & f1 = f2 ) ) A1: ( <*b1,f1,a1*> . 1 = b1 & <*b1,f1,a1*> . 2 = f1 ) by FINSEQ_1:45; A2: ( <*b1,f1,a1*> . 3 = a1 & <*b2,f2,a2*> . 1 = b2 ) by FINSEQ_1:45; A3: ( <*b2,f2,a2*> . 2 = f2 & <*b2,f2,a2*> . 3 = a2 ) by FINSEQ_1:45; assume b1 := (f1,a1) = b2 := (f2,a2) ; ::_thesis: ( a1 = a2 & b1 = b2 & f1 = f2 ) hence ( a1 = a2 & b1 = b2 & f1 = f2 ) by A1, A2, A3, XTUPLE_0:3; ::_thesis: verum end; theorem Th10: :: SF_MASTR:10 for a1, b1, a2, b2 being Int-Location for f1, f2 being FinSeq-Location st (f1,a1) := b1 = (f2,a2) := b2 holds ( a1 = a2 & b1 = b2 & f1 = f2 ) proof let a1, b1, a2, b2 be Int-Location; ::_thesis: for f1, f2 being FinSeq-Location st (f1,a1) := b1 = (f2,a2) := b2 holds ( a1 = a2 & b1 = b2 & f1 = f2 ) let f1, f2 be FinSeq-Location ; ::_thesis: ( (f1,a1) := b1 = (f2,a2) := b2 implies ( a1 = a2 & b1 = b2 & f1 = f2 ) ) A1: ( <*b1,f1,a1*> . 1 = b1 & <*b1,f1,a1*> . 2 = f1 ) by FINSEQ_1:45; A2: ( <*b1,f1,a1*> . 3 = a1 & <*b2,f2,a2*> . 1 = b2 ) by FINSEQ_1:45; A3: ( <*b2,f2,a2*> . 2 = f2 & <*b2,f2,a2*> . 3 = a2 ) by FINSEQ_1:45; assume (f1,a1) := b1 = (f2,a2) := b2 ; ::_thesis: ( a1 = a2 & b1 = b2 & f1 = f2 ) hence ( a1 = a2 & b1 = b2 & f1 = f2 ) by A1, A2, A3, XTUPLE_0:3; ::_thesis: verum end; theorem Th11: :: SF_MASTR:11 for a1, a2 being Int-Location for f1, f2 being FinSeq-Location st a1 :=len f1 = a2 :=len f2 holds ( a1 = a2 & f1 = f2 ) proof let a1, a2 be Int-Location; ::_thesis: for f1, f2 being FinSeq-Location st a1 :=len f1 = a2 :=len f2 holds ( a1 = a2 & f1 = f2 ) let f1, f2 be FinSeq-Location ; ::_thesis: ( a1 :=len f1 = a2 :=len f2 implies ( a1 = a2 & f1 = f2 ) ) A1: ( <*a1,f1*> . 1 = a1 & <*a1,f1*> . 2 = f1 ) by FINSEQ_1:44; A2: ( <*a2,f2*> . 1 = a2 & <*a2,f2*> . 2 = f2 ) by FINSEQ_1:44; assume a1 :=len f1 = a2 :=len f2 ; ::_thesis: ( a1 = a2 & f1 = f2 ) hence ( a1 = a2 & f1 = f2 ) by A1, A2, XTUPLE_0:3; ::_thesis: verum end; theorem Th12: :: SF_MASTR:12 for a1, a2 being Int-Location for f1, f2 being FinSeq-Location st f1 :=<0,...,0> a1 = f2 :=<0,...,0> a2 holds ( a1 = a2 & f1 = f2 ) proof let a1, a2 be Int-Location; ::_thesis: for f1, f2 being FinSeq-Location st f1 :=<0,...,0> a1 = f2 :=<0,...,0> a2 holds ( a1 = a2 & f1 = f2 ) let f1, f2 be FinSeq-Location ; ::_thesis: ( f1 :=<0,...,0> a1 = f2 :=<0,...,0> a2 implies ( a1 = a2 & f1 = f2 ) ) A1: ( <*a1,f1*> . 1 = a1 & <*a1,f1*> . 2 = f1 ) by FINSEQ_1:44; A2: ( <*a2,f2*> . 1 = a2 & <*a2,f2*> . 2 = f2 ) by FINSEQ_1:44; assume f1 :=<0,...,0> a1 = f2 :=<0,...,0> a2 ; ::_thesis: ( a1 = a2 & f1 = f2 ) hence ( a1 = a2 & f1 = f2 ) by A1, A2, XTUPLE_0:3; ::_thesis: verum end; begin definition let i be Instruction of SCM+FSA; func UsedIntLoc i -> Element of Fin Int-Locations means :Def1: :: SF_MASTR:def 1 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 ex l being Element of NAT 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 ex 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 ex 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 ( ( InsCode i in {1,2,3,4,5} implies ex b1 being Element of Fin Int-Locations 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) ) & b1 = {a,b} ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b1 being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin Int-Locations st b1 = {} ) ) proof hereby ::_thesis: ( ( ( InsCode i = 7 or InsCode i = 8 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b1 being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin Int-Locations st b1 = {} ) ) assume InsCode i in {1,2,3,4,5} ; ::_thesis: ex IT being Element of Fin Int-Locations 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} ) then ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) by ENUMSET1:def_3; 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:30, SCMFSA_2:31, SCMFSA_2:32, SCMFSA_2:33, SCMFSA_2:34; reconsider a9 = a, b9 = b as Element of Int-Locations by AMI_2:def_16; reconsider IT = {.a9,b9.} as Element of Fin Int-Locations ; take IT = IT; ::_thesis: 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} ) take a = a; ::_thesis: ex 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} ) take b = b; ::_thesis: ( ( 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} ) 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; ::_thesis: verum end; hereby ::_thesis: ( ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b1 being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin Int-Locations st b1 = {} ) ) assume ( InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: ex IT being Element of Fin Int-Locations ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} ) then consider l being Element of NAT , a being Int-Location such that A2: ( i = a =0_goto l or i = a >0_goto l ) by SCMFSA_2:36, SCMFSA_2:37; reconsider a9 = a as Element of Int-Locations by AMI_2:def_16; reconsider IT = {.a9.} as Element of Fin Int-Locations ; take IT = IT; ::_thesis: ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} ) take a = a; ::_thesis: ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} ) take l = l; ::_thesis: ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} ) thus ( ( i = a =0_goto l or i = a >0_goto l ) & IT = {a} ) by A2; ::_thesis: verum end; hereby ::_thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin Int-Locations st b1 = {} ) ) assume ( InsCode i = 9 or InsCode i = 10 ) ; ::_thesis: ex IT being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) 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:38, SCMFSA_2:39; reconsider a9 = a, b9 = b as Element of Int-Locations by AMI_2:def_16; reconsider IT = {.a9,b9.} as Element of Fin Int-Locations ; take IT = IT; ::_thesis: ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) take a = a; ::_thesis: ex b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) take b = b; ::_thesis: ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) take f = f; ::_thesis: ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) thus ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {a,b} ) by A3; ::_thesis: verum end; hereby ::_thesis: ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin Int-Locations st b1 = {} ) assume ( InsCode i = 11 or InsCode i = 12 ) ; ::_thesis: ex IT being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} ) 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:40, SCMFSA_2:41; reconsider a9 = a as Element of Int-Locations by AMI_2:def_16; reconsider IT = {.a9.} as Element of Fin Int-Locations ; take IT = IT; ::_thesis: ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} ) take a = a; ::_thesis: ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} ) take f = f; ::_thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} ) thus ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {a} ) by A4; ::_thesis: verum end; {} in Fin Int-Locations by FINSUB_1:7; hence ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin Int-Locations st b1 = {} ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of Fin Int-Locations holds ( ( InsCode i in {1,2,3,4,5} & 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) ) & b1 = {a,b} ) & 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) ) & b2 = {a,b} ) implies b1 = b2 ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) & ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b2 = {a} ) implies b1 = b2 ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b2 = {a,b} ) implies b1 = b2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {a} ) implies b1 = b2 ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not b1 = {} or not b2 = {} or b1 = b2 ) ) proof let it1, it2 be Element of Fin Int-Locations; ::_thesis: ( ( InsCode i in {1,2,3,4,5} & 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) ) & it1 = {a,b} ) & 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) ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & it1 = {a} ) & ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & it2 = {a} ) implies it1 = it2 ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ) hereby ::_thesis: ( ( ( InsCode i = 7 or InsCode i = 8 ) & ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & it1 = {a} ) & ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & it2 = {a} ) implies it1 = it2 ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ) assume InsCode i in {1,2,3,4,5} ; ::_thesis: ( ex a1, b1 being Int-Location st ( ( 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} ) & ex a2, b2 being Int-Location st ( ( 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} ) implies it1 = it2 ) 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) ) and A6: it1 = {a1,b1} ; ::_thesis: ( ex a2, b2 being Int-Location st ( ( 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} ) implies it1 = it2 ) given a2, b2 being Int-Location such that A7: ( i = a2 := b2 or i = AddTo (a2,b2) or i = SubFrom (a2,b2) or i = MultBy (a2,b2) or i = Divide (a2,b2) ) and A8: it2 = {a2,b2} ; ::_thesis: it1 = it2 A9: ( ( i = AddTo (a1,b1) or i = AddTo (a2,b2) ) implies InsCode i = 2 ) by SCMFSA_2:19; A10: ( ( i = Divide (a1,b1) or i = Divide (a2,b2) ) implies InsCode i = 5 ) by SCMFSA_2:22; A11: ( ( i = MultBy (a1,b1) or i = MultBy (a2,b2) ) implies InsCode i = 4 ) by SCMFSA_2:21; A12: ( ( i = SubFrom (a1,b1) or i = SubFrom (a2,b2) ) implies InsCode i = 3 ) by SCMFSA_2:20; percases ( ( i = a1 := b1 & i = a2 := b2 ) or ( i = AddTo (a1,b1) & i = AddTo (a2,b2) ) or ( i = SubFrom (a1,b1) & i = SubFrom (a2,b2) ) or ( i = MultBy (a1,b1) & i = MultBy (a2,b2) ) or ( i = Divide (a1,b1) & i = Divide (a2,b2) ) ) by A5, A7, A9, A12, A11, A10, SCMFSA_2:18; supposeA13: ( i = a1 := b1 & i = a2 := b2 ) ; ::_thesis: it1 = it2 then a1 = a2 by Th1; hence it1 = it2 by A6, A8, A13, Th1; ::_thesis: verum end; supposeA14: ( i = AddTo (a1,b1) & i = AddTo (a2,b2) ) ; ::_thesis: it1 = it2 then a1 = a2 by Th2; hence it1 = it2 by A6, A8, A14, Th2; ::_thesis: verum end; supposeA15: ( i = SubFrom (a1,b1) & i = SubFrom (a2,b2) ) ; ::_thesis: it1 = it2 then a1 = a2 by Th3; hence it1 = it2 by A6, A8, A15, Th3; ::_thesis: verum end; supposeA16: ( i = MultBy (a1,b1) & i = MultBy (a2,b2) ) ; ::_thesis: it1 = it2 then a1 = a2 by Th4; hence it1 = it2 by A6, A8, A16, Th4; ::_thesis: verum end; supposeA17: ( i = Divide (a1,b1) & i = Divide (a2,b2) ) ; ::_thesis: it1 = it2 then a1 = a2 by Th5; hence it1 = it2 by A6, A8, A17, Th5; ::_thesis: verum end; end; end; hereby ::_thesis: ( ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {a,b} ) implies it1 = it2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ) assume ( InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: ( ex a1 being Int-Location ex l1 being Element of NAT st ( ( i = a1 =0_goto l1 or i = a1 >0_goto l1 ) & it1 = {a1} ) & ex a2 being Int-Location ex l2 being Element of NAT st ( ( i = a2 =0_goto l2 or i = a2 >0_goto l2 ) & it2 = {a2} ) implies it1 = it2 ) given a1 being Int-Location, l1 being Element of NAT such that A18: ( i = a1 =0_goto l1 or i = a1 >0_goto l1 ) and A19: it1 = {a1} ; ::_thesis: ( ex a2 being Int-Location ex l2 being Element of NAT st ( ( i = a2 =0_goto l2 or i = a2 >0_goto l2 ) & it2 = {a2} ) implies it1 = it2 ) given a2 being Int-Location, l2 being Element of NAT such that A20: ( i = a2 =0_goto l2 or i = a2 >0_goto l2 ) and A21: it2 = {a2} ; ::_thesis: it1 = it2 A22: ( ( i = a1 >0_goto l1 or i = a2 >0_goto l2 ) implies InsCode i = 8 ) by SCMFSA_2:25; percases ( ( i = a1 =0_goto l1 & i = a2 =0_goto l2 ) or ( i = a1 >0_goto l1 & i = a2 >0_goto l2 ) ) by A18, A20, A22, SCMFSA_2:24; suppose ( i = a1 =0_goto l1 & i = a2 =0_goto l2 ) ; ::_thesis: it1 = it2 hence it1 = it2 by A19, A21, Th7; ::_thesis: verum end; suppose ( i = a1 >0_goto l1 & i = a2 >0_goto l2 ) ; ::_thesis: it1 = it2 hence it1 = it2 by A19, A21, Th8; ::_thesis: verum end; end; end; hereby ::_thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {a} ) implies it1 = it2 ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ) assume ( InsCode i = 9 or InsCode i = 10 ) ; ::_thesis: ( ex a1, b1 being Int-Location ex f1 being FinSeq-Location st ( ( i = b1 := (f1,a1) or i = (f1,a1) := b1 ) & it1 = {a1,b1} ) & ex a2, b2 being Int-Location ex f2 being FinSeq-Location st ( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {a2,b2} ) implies it1 = it2 ) given a1, b1 being Int-Location, f1 being FinSeq-Location such that A23: ( i = b1 := (f1,a1) or i = (f1,a1) := b1 ) and A24: it1 = {a1,b1} ; ::_thesis: ( ex a2, b2 being Int-Location ex f2 being FinSeq-Location st ( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {a2,b2} ) implies it1 = it2 ) given a2, b2 being Int-Location, f2 being FinSeq-Location such that A25: ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) and A26: it2 = {a2,b2} ; ::_thesis: it1 = it2 A27: ( ( i = (f1,a1) := b1 or i = (f2,a2) := b2 ) implies InsCode i = 10 ) by SCMFSA_2:27; percases ( ( i = b1 := (f1,a1) & i = b2 := (f2,a2) ) or ( i = (f1,a1) := b1 & i = (f2,a2) := b2 ) ) by A23, A25, A27, SCMFSA_2:26; supposeA28: ( i = b1 := (f1,a1) & i = b2 := (f2,a2) ) ; ::_thesis: it1 = it2 then a1 = a2 by Th9; hence it1 = it2 by A24, A26, A28, Th9; ::_thesis: verum end; supposeA29: ( i = (f1,a1) := b1 & i = (f2,a2) := b2 ) ; ::_thesis: it1 = it2 then a1 = a2 by Th10; hence it1 = it2 by A24, A26, A29, Th10; ::_thesis: verum end; end; end; hereby ::_thesis: ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) assume ( InsCode i = 11 or InsCode i = 12 ) ; ::_thesis: ( ex a1 being Int-Location ex f1 being FinSeq-Location st ( ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) & it1 = {a1} ) & ex a2 being Int-Location ex f2 being FinSeq-Location st ( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {a2} ) implies it1 = it2 ) given a1 being Int-Location, f1 being FinSeq-Location such that A30: ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) and A31: it1 = {a1} ; ::_thesis: ( ex a2 being Int-Location ex f2 being FinSeq-Location st ( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {a2} ) implies it1 = it2 ) given a2 being Int-Location, f2 being FinSeq-Location such that A32: ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) and A33: it2 = {a2} ; ::_thesis: it1 = it2 A34: ( ( i = f1 :=<0,...,0> a1 or i = f2 :=<0,...,0> a2 ) implies InsCode i = 12 ) by SCMFSA_2:29; percases ( ( i = a1 :=len f1 & i = a2 :=len f2 ) or ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ) by A30, A32, A34, SCMFSA_2:28; suppose ( i = a1 :=len f1 & i = a2 :=len f2 ) ; ::_thesis: it1 = it2 hence it1 = it2 by A31, A33, Th11; ::_thesis: verum end; suppose ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ; ::_thesis: it1 = it2 hence it1 = it2 by A31, A33, Th12; ::_thesis: verum end; end; end; thus ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ; ::_thesis: verum end; consistency for b1 being Element of Fin Int-Locations holds ( ( InsCode i in {1,2,3,4,5} & ( InsCode i = 7 or InsCode i = 8 ) implies ( 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) ) & b1 = {a,b} ) iff ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) ) ) & ( InsCode i in {1,2,3,4,5} & ( InsCode i = 9 or InsCode i = 10 ) implies ( 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) ) & b1 = {a,b} ) iff ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) ) & ( InsCode i in {1,2,3,4,5} & ( InsCode i = 11 or InsCode i = 12 ) implies ( 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) ) & b1 = {a,b} ) iff ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ( InsCode i = 9 or InsCode i = 10 ) implies ( ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) iff ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ( InsCode i = 11 or InsCode i = 12 ) implies ( ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) iff ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ( InsCode i = 11 or InsCode i = 12 ) implies ( ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) iff ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) ) ) by ENUMSET1:def_3; end; :: deftheorem Def1 defines UsedIntLoc SF_MASTR:def_1_:_ for i being Instruction of SCM+FSA for b2 being Element of Fin Int-Locations holds ( ( InsCode i in {1,2,3,4,5} implies ( b2 = UsedIntLoc i iff 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) ) & b2 = {a,b} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) implies ( b2 = UsedIntLoc i iff ex a being Int-Location ex l being Element of NAT st ( ( i = a =0_goto l or i = a >0_goto l ) & b2 = {a} ) ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b2 = UsedIntLoc i iff ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b2 = {a,b} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b2 = UsedIntLoc i iff ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {a} ) ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b2 = UsedIntLoc i iff b2 = {} ) ) ); theorem Th13: :: SF_MASTR:13 UsedIntLoc (halt SCM+FSA) = {} proof A1: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70; not 0 in {1,2,3,4,5} ; hence UsedIntLoc (halt SCM+FSA) = {} by Def1, A1; ::_thesis: verum end; theorem Th14: :: SF_MASTR:14 for a, b being Int-Location for i being Instruction of SCM+FSA st ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) holds UsedIntLoc i = {a,b} proof let a, b be Int-Location; ::_thesis: for i being Instruction of SCM+FSA st ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) holds UsedIntLoc i = {a,b} let i be Instruction of SCM+FSA; ::_thesis: ( ( 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} ) reconsider ab = {a,b} as Element of Fin Int-Locations by FINSUB_1:def_5; 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) ) ; ::_thesis: UsedIntLoc i = {a,b} then ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) by SCMFSA_2:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22; then InsCode i in {1,2,3,4,5} by ENUMSET1:def_3; then UsedIntLoc i = ab by A1, Def1; hence UsedIntLoc i = {a,b} ; ::_thesis: verum end; theorem Th15: :: SF_MASTR:15 for l being Element of NAT holds UsedIntLoc (goto l) = {} proof let l be Element of NAT ; ::_thesis: UsedIntLoc (goto l) = {} ( InsCode (goto l) = 6 & not 6 in {1,2,3,4,5} ) by ENUMSET1:def_3, SCMFSA_2:23; hence UsedIntLoc (goto l) = {} by Def1; ::_thesis: verum end; theorem Th16: :: SF_MASTR:16 for a being Int-Location for l being Element of NAT for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds UsedIntLoc i = {a} proof let a be Int-Location; ::_thesis: for l being Element of NAT for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds UsedIntLoc i = {a} let l be Element of NAT ; ::_thesis: for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds UsedIntLoc i = {a} let i be Instruction of SCM+FSA; ::_thesis: ( ( i = a =0_goto l or i = a >0_goto l ) implies UsedIntLoc i = {a} ) reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def_5; assume A1: ( i = a =0_goto l or i = a >0_goto l ) ; ::_thesis: UsedIntLoc i = {a} then ( InsCode i = 7 or InsCode i = 8 ) by SCMFSA_2:24, SCMFSA_2:25; then UsedIntLoc i = ab by A1, Def1; hence UsedIntLoc i = {a} ; ::_thesis: verum end; theorem Th17: :: SF_MASTR:17 for b, a being Int-Location for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds UsedIntLoc i = {a,b} proof let b, a be Int-Location; ::_thesis: for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds UsedIntLoc i = {a,b} let f be FinSeq-Location ; ::_thesis: for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds UsedIntLoc i = {a,b} let i be Instruction of SCM+FSA; ::_thesis: ( ( i = b := (f,a) or i = (f,a) := b ) implies UsedIntLoc i = {a,b} ) reconsider ab = {a,b} as Element of Fin Int-Locations by FINSUB_1:def_5; assume A1: ( i = b := (f,a) or i = (f,a) := b ) ; ::_thesis: UsedIntLoc i = {a,b} then ( InsCode i = 9 or InsCode i = 10 ) by SCMFSA_2:26, SCMFSA_2:27; then UsedIntLoc i = ab by A1, Def1; hence UsedIntLoc i = {a,b} ; ::_thesis: verum end; theorem Th18: :: SF_MASTR:18 for a being Int-Location for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds UsedIntLoc i = {a} proof let a be Int-Location; ::_thesis: for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds UsedIntLoc i = {a} let f be FinSeq-Location ; ::_thesis: for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds UsedIntLoc i = {a} let i be Instruction of SCM+FSA; ::_thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) implies UsedIntLoc i = {a} ) reconsider ab = {a} as Element of Fin Int-Locations by FINSUB_1:def_5; assume A1: ( i = a :=len f or i = f :=<0,...,0> a ) ; ::_thesis: UsedIntLoc i = {a} then ( InsCode i = 11 or InsCode i = 12 ) by SCMFSA_2:28, SCMFSA_2:29; then UsedIntLoc i = ab by A1, Def1; hence UsedIntLoc i = {a} ; ::_thesis: verum end; definition let p be Function; func UsedIntLoc p -> Subset of Int-Locations means :Def2: :: SF_MASTR:def 2 ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & it = Union (UIL * p) ); existence ex b1 being Subset of Int-Locations ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b1 = Union (UIL * p) ) proof defpred S1[ set , set ] means ex I being Instruction of SCM+FSA st ( $1 = I & $2 = UsedIntLoc I ); A1: for e being Element of the InstructionsF of SCM+FSA ex u being Element of Fin Int-Locations st S1[e,u] proof let e be Element of the InstructionsF of SCM+FSA; ::_thesis: ex u being Element of Fin Int-Locations st S1[e,u] reconsider f = e as Instruction of SCM+FSA ; reconsider u = UsedIntLoc f as Element of Fin Int-Locations ; take u ; ::_thesis: S1[e,u] take f ; ::_thesis: ( e = f & u = UsedIntLoc f ) thus ( e = f & u = UsedIntLoc f ) ; ::_thesis: verum end; consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A2: for i being Element of the InstructionsF of SCM+FSA holds S1[i,UIL . i] from FUNCT_2:sch_3(A1); set IT = Union (UIL * p); set dp = dom p; set Up = UIL * p; take Union (UIL * p) ; ::_thesis: ( Union (UIL * p) is Subset of Int-Locations & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & Union (UIL * p) = Union (UIL * p) ) ) Fin Int-Locations c= bool Int-Locations by FINSUB_1:13; then ( rng (UIL * p) c= rng UIL & rng UIL c= bool Int-Locations ) by RELAT_1:26, XBOOLE_1:1; then rng (UIL * p) c= bool Int-Locations by XBOOLE_1:1; then ( Union (UIL * p) = union (rng (UIL * p)) & union (rng (UIL * p)) c= union (bool Int-Locations) ) by CARD_3:def_4, ZFMISC_1:77; hence Union (UIL * p) is Subset of Int-Locations by ZFMISC_1:81; ::_thesis: ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & Union (UIL * p) = Union (UIL * p) ) take UIL ; ::_thesis: ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & Union (UIL * p) = Union (UIL * p) ) hereby ::_thesis: Union (UIL * p) = Union (UIL * p) let i be Instruction of SCM+FSA; ::_thesis: UIL . i = UsedIntLoc i S1[i,UIL . i] by A2; hence UIL . i = UsedIntLoc i ; ::_thesis: verum end; thus Union (UIL * p) = Union (UIL * p) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of Int-Locations st ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b1 = Union (UIL * p) ) & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b2 = Union (UIL * p) ) holds b1 = b2 proof let IT1, IT2 be Subset of Int-Locations; ::_thesis: ( ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & IT1 = Union (UIL * p) ) & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & IT2 = Union (UIL * p) ) implies IT1 = IT2 ) given UIL1 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i and A4: IT1 = Union (UIL1 * p) ; ::_thesis: ( for UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) holds ( ex i being Instruction of SCM+FSA st not UIL . i = UsedIntLoc i or not IT2 = Union (UIL * p) ) or IT1 = IT2 ) given UIL2 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A5: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and A6: IT2 = Union (UIL2 * p) ; ::_thesis: IT1 = IT2 for c being Element of the InstructionsF of SCM+FSA holds UIL1 . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL1 . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL1 . c = UsedIntLoc d by A3 .= UIL2 . c by A5 ; ::_thesis: verum end; hence IT1 = IT2 by A4, A6, FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines UsedIntLoc SF_MASTR:def_2_:_ for p being Function for b2 being Subset of Int-Locations holds ( b2 = UsedIntLoc p iff ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b2 = Union (UIL * p) ) ); registration let p be preProgram of SCM+FSA; cluster UsedIntLoc p -> finite ; coherence UsedIntLoc p is finite proof reconsider dp = dom p as finite set ; consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A1: UsedIntLoc p = Union (UIL * p) by Def2; rng p c= the InstructionsF of SCM+FSA ; then reconsider p9 = p as Function of dp, the InstructionsF of SCM+FSA by FUNCT_2:2; reconsider Up = UIL * p9 as Function of dp,(Fin Int-Locations) ; Union Up is finite ; hence UsedIntLoc p is finite by A1; ::_thesis: verum end; end; theorem Th19: :: SF_MASTR:19 for i being Instruction of SCM+FSA for p being preProgram of SCM+FSA st i in rng p holds UsedIntLoc i c= UsedIntLoc p proof let i be Instruction of SCM+FSA; ::_thesis: for p being preProgram of SCM+FSA st i in rng p holds UsedIntLoc i c= UsedIntLoc p let p be preProgram of SCM+FSA; ::_thesis: ( i in rng p implies UsedIntLoc i c= UsedIntLoc p ) assume i in rng p ; ::_thesis: UsedIntLoc i c= UsedIntLoc p then consider x being set such that A1: ( x in dom p & i = p . x ) by FUNCT_1:def_3; consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A2: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A3: UsedIntLoc p = Union (UIL * p) by Def2; A4: UsedIntLoc p = union (rng (UIL * p)) by A3, CARD_3:def_4; dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then x in dom (UIL * p) by A1, FUNCT_1:11; then A5: (UIL * p) . x in rng (UIL * p) by FUNCT_1:def_3; (UIL * p) . x = UIL . i by A1, FUNCT_1:13 .= UsedIntLoc i by A2 ; hence UsedIntLoc i c= UsedIntLoc p by A5, A4, ZFMISC_1:74; ::_thesis: verum end; theorem :: SF_MASTR:20 for p, r being preProgram of SCM+FSA holds UsedIntLoc (p +* r) c= (UsedIntLoc p) \/ (UsedIntLoc r) proof let p, r be preProgram of SCM+FSA; ::_thesis: UsedIntLoc (p +* r) c= (UsedIntLoc p) \/ (UsedIntLoc r) consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A2: UsedIntLoc (p +* r) = Union (UIL * (p +* r)) by Def2; consider UIL1 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i and A4: UsedIntLoc p = Union (UIL1 * p) by Def2; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL1 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL1 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedIntLoc d by A1 .= UIL1 . c by A3 ; ::_thesis: verum end; then A5: UIL = UIL1 by FUNCT_2:63; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A6: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and A7: UsedIntLoc r = Union (UIL2 * r) by Def2; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedIntLoc d by A1 .= UIL2 . c by A6 ; ::_thesis: verum end; then A8: UIL = UIL2 by FUNCT_2:63; dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then rng r c= dom UIL ; then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:9; then A9: ( Union (UIL * r) = union (rng (UIL * r)) & union (rng (UIL * (p +* r))) c= union ((rng (UIL * p)) \/ (rng (UIL * r))) ) by CARD_3:def_4, FUNCT_4:17, ZFMISC_1:77; ( Union (UIL * (p +* r)) = union (rng (UIL * (p +* r))) & Union (UIL * p) = union (rng (UIL * p)) ) by CARD_3:def_4; hence UsedIntLoc (p +* r) c= (UsedIntLoc p) \/ (UsedIntLoc r) by A2, A4, A7, A5, A8, A9, ZFMISC_1:78; ::_thesis: verum end; theorem Th21: :: SF_MASTR:21 for p, r being preProgram of SCM+FSA st dom p misses dom r holds UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r) proof let p, r be preProgram of SCM+FSA; ::_thesis: ( dom p misses dom r implies UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r) ) consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A2: UsedIntLoc (p +* r) = Union (UIL * (p +* r)) by Def2; assume dom p misses dom r ; ::_thesis: UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r) then ( dom (UIL * p) c= dom p & dom p misses dom (UIL * r) ) by RELAT_1:25, XBOOLE_1:63; then A3: (UIL * p) +* (UIL * r) = (UIL * p) \/ (UIL * r) by FUNCT_4:31, XBOOLE_1:63; dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then rng r c= dom UIL ; then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:9; then A4: ( Union (UIL * r) = union (rng (UIL * r)) & union (rng (UIL * (p +* r))) = union ((rng (UIL * p)) \/ (rng (UIL * r))) ) by A3, CARD_3:def_4, RELAT_1:12; consider UIL1 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A5: for i being Instruction of SCM+FSA holds UIL1 . i = UsedIntLoc i and A6: UsedIntLoc p = Union (UIL1 * p) by Def2; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL1 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL1 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedIntLoc d by A1 .= UIL1 . c by A5 ; ::_thesis: verum end; then A7: UIL = UIL1 by FUNCT_2:63; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A8: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and A9: UsedIntLoc r = Union (UIL2 * r) by Def2; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedIntLoc d by A1 .= UIL2 . c by A8 ; ::_thesis: verum end; then A10: UIL = UIL2 by FUNCT_2:63; ( Union (UIL * (p +* r)) = union (rng (UIL * (p +* r))) & Union (UIL * p) = union (rng (UIL * p)) ) by CARD_3:def_4; hence UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r) by A2, A6, A9, A7, A10, A4, ZFMISC_1:78; ::_thesis: verum end; theorem Th22: :: SF_MASTR:22 for p being preProgram of SCM+FSA for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (Shift (p,k)) proof let p be preProgram of SCM+FSA; ::_thesis: for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (Shift (p,k)) let k be Element of NAT ; ::_thesis: UsedIntLoc p = UsedIntLoc (Shift (p,k)) set Sp = Shift (p,k); consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A2: UsedIntLoc p = Union (UIL * p) by Def2; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and A4: UsedIntLoc (Shift (p,k)) = Union (UIL2 * (Shift (p,k))) by Def2; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedIntLoc d by A1 .= UIL2 . c by A3 ; ::_thesis: verum end; then A5: UIL = UIL2 by FUNCT_2:63; A6: dom (Shift (p,k)) = { (m + k) where m is Element of NAT : m in dom p } by VALUED_1:def_12; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_(Shift_(p,k))_implies_y_in_rng_p_)_&_(_y_in_rng_p_implies_y_in_rng_(Shift_(p,k))_)_) let y be set ; ::_thesis: ( ( y in rng (Shift (p,k)) implies y in rng p ) & ( y in rng p implies y in rng (Shift (p,k)) ) ) hereby ::_thesis: ( y in rng p implies y in rng (Shift (p,k)) ) assume y in rng (Shift (p,k)) ; ::_thesis: y in rng p then consider x being set such that A7: x in dom (Shift (p,k)) and A8: y = (Shift (p,k)) . x by FUNCT_1:def_3; consider m being Element of NAT such that A9: x = m + k and A10: m in dom p by A6, A7; (Shift (p,k)) . x = p . m by A9, A10, VALUED_1:def_12; hence y in rng p by A8, A10, FUNCT_1:def_3; ::_thesis: verum end; assume y in rng p ; ::_thesis: y in rng (Shift (p,k)) then consider x being set such that A11: x in dom p and A12: y = p . x by FUNCT_1:def_3; reconsider x9 = x as Element of NAT by A11; reconsider m = x9 as Element of NAT ; ( m + k in dom (Shift (p,k)) & (Shift (p,k)) . (m + k) = p . m ) by A6, A11, VALUED_1:def_12; hence y in rng (Shift (p,k)) by A12, FUNCT_1:def_3; ::_thesis: verum end; then A13: rng (Shift (p,k)) = rng p by TARSKI:1; A14: Union (UIL * (Shift (p,k))) = union (rng (UIL * (Shift (p,k)))) by CARD_3:def_4; rng (UIL * (Shift (p,k))) = UIL .: (rng (Shift (p,k))) by RELAT_1:127 .= rng (UIL * p) by A13, RELAT_1:127 ; hence UsedIntLoc p = UsedIntLoc (Shift (p,k)) by A2, A4, A5, A14, CARD_3:def_4; ::_thesis: verum end; theorem Th23: :: SF_MASTR:23 for i being Instruction of SCM+FSA for k being Element of NAT holds UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) proof let i be Instruction of SCM+FSA; ::_thesis: for k being Element of NAT holds UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) let k be Element of NAT ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) A1: InsCode i <= 12 by SCMFSA_2:16; percases ( 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 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A1, NAT_1:36; suppose InsCode i = 0 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then i = halt SCM+FSA by SCMFSA_2:95; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a, b being Int-Location st i = a := b by SCMFSA_2:30; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 2 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:31; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 3 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:32; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:33; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:34; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 6 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then consider l being Element of NAT such that A2: i = goto l by SCMFSA_2:35; IncAddr (i,k) = goto (l + k) by A2, SCMFSA_4:1; hence UsedIntLoc (IncAddr (i,k)) = {} by Th15 .= UsedIntLoc i by A2, Th15 ; ::_thesis: verum end; suppose InsCode i = 7 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then consider l being Element of NAT , a being Int-Location such that A3: i = a =0_goto l by SCMFSA_2:36; IncAddr (i,k) = a =0_goto (l + k) by A3, SCMFSA_4:2; hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16 .= UsedIntLoc i by A3, Th16 ; ::_thesis: verum end; suppose InsCode i = 8 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then consider l being Element of NAT , a being Int-Location such that A4: i = a >0_goto l by SCMFSA_2:37; IncAddr (i,k) = a >0_goto (l + k) by A4, SCMFSA_4:3; hence UsedIntLoc (IncAddr (i,k)) = {a} by Th16 .= UsedIntLoc i by A4, Th16 ; ::_thesis: verum end; suppose InsCode i = 9 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) by SCMFSA_2:38; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 10 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 11 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a being Int-Location ex f being FinSeq-Location st i = a :=len f by SCMFSA_2:40; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 12 ; ::_thesis: UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41; hence UsedIntLoc i = UsedIntLoc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; end; end; theorem Th24: :: SF_MASTR:24 for p being preProgram of SCM+FSA for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (IncAddr (p,k)) proof let p be preProgram of SCM+FSA; ::_thesis: for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (IncAddr (p,k)) let k be Element of NAT ; ::_thesis: UsedIntLoc p = UsedIntLoc (IncAddr (p,k)) set Ip = IncAddr (p,k); consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A2: UsedIntLoc p = Union (UIL * p) by Def2; set g = UIL * p; set f = UIL * (IncAddr (p,k)); consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and A4: UsedIntLoc (IncAddr (p,k)) = Union (UIL2 * (IncAddr (p,k))) by Def2; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedIntLoc d by A1 .= UIL2 . c by A3 ; ::_thesis: verum end; then A5: UIL = UIL2 by FUNCT_2:63; now__::_thesis:_(_dom_(UIL_*_(IncAddr_(p,k)))_=_dom_(UIL_*_p)_&_(_for_x_being_set_st_x_in_dom_(UIL_*_(IncAddr_(p,k)))_holds_ (UIL_*_(IncAddr_(p,k)))_._x_=_(UIL_*_p)_._x_)_) A6: dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then A7: rng p c= dom UIL ; rng (IncAddr (p,k)) c= dom UIL by A6; then A8: dom (UIL * (IncAddr (p,k))) = dom (IncAddr (p,k)) by RELAT_1:27; A9: dom (IncAddr (p,k)) = dom p by COMPOS_1:def_21; hence dom (UIL * (IncAddr (p,k))) = dom (UIL * p) by A7, A8, RELAT_1:27; ::_thesis: for x being set st x in dom (UIL * (IncAddr (p,k))) holds (UIL * (IncAddr (p,k))) . x = (UIL * p) . x let x be set ; ::_thesis: ( x in dom (UIL * (IncAddr (p,k))) implies (UIL * (IncAddr (p,k))) . x = (UIL * p) . x ) assume A10: x in dom (UIL * (IncAddr (p,k))) ; ::_thesis: (UIL * (IncAddr (p,k))) . x = (UIL * p) . x then p . x in rng p by A9, A8, FUNCT_1:def_3; then reconsider px = p . x as Instruction of SCM+FSA ; reconsider x9 = x as Element of NAT by A8, A10; reconsider m = x9 as Element of NAT ; A11: (IncAddr (p,k)) . x = IncAddr ((p /. m),k) by A9, A8, A10, COMPOS_1:def_21 .= IncAddr (px,k) by A9, A8, A10, PARTFUN1:def_6 ; (IncAddr (p,k)) . x in rng (IncAddr (p,k)) by A8, A10, FUNCT_1:def_3; then reconsider Ipx = (IncAddr (p,k)) . x as Instruction of SCM+FSA ; thus (UIL * (IncAddr (p,k))) . x = UIL . Ipx by A10, FUNCT_1:12 .= UsedIntLoc Ipx by A1 .= UsedIntLoc px by A11, Th23 .= UIL . px by A3, A5 .= (UIL * p) . x by A9, A8, A10, FUNCT_1:13 ; ::_thesis: verum end; hence UsedIntLoc p = UsedIntLoc (IncAddr (p,k)) by A2, A4, A5, FUNCT_1:2; ::_thesis: verum end; theorem Th25: :: SF_MASTR:25 for I being Program of for k being Element of NAT holds UsedIntLoc I = UsedIntLoc (Reloc (I,k)) proof let I be Program of ; ::_thesis: for k being Element of NAT holds UsedIntLoc I = UsedIntLoc (Reloc (I,k)) let k be Element of NAT ; ::_thesis: UsedIntLoc I = UsedIntLoc (Reloc (I,k)) A1: Reloc (I,k) = IncAddr ((Shift (I,k)),k) by COMPOS_1:34; UsedIntLoc (Reloc (I,k)) = UsedIntLoc (Reloc (I,k)) .= UsedIntLoc (Shift (I,k)) by Th24, A1 .= UsedIntLoc I by Th22 ; hence UsedIntLoc I = UsedIntLoc (Reloc (I,k)) ; ::_thesis: verum end; theorem Th26: :: SF_MASTR:26 for I being Program of holds UsedIntLoc I = UsedIntLoc (Directed I) proof let I be Program of ; ::_thesis: UsedIntLoc I = UsedIntLoc (Directed I) consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A2: UsedIntLoc I = Union (UIL * I) by Def2; A3: ( dom UIL = the InstructionsF of SCM+FSA & UIL . (halt SCM+FSA) = {} ) by A1, Th13, FUNCT_2:def_1; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A4: for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i and A5: UsedIntLoc (Directed I) = Union (UIL2 * (Directed I)) by Def2; A6: for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedIntLoc d by A1 .= UIL2 . c by A4 ; ::_thesis: verum end; A7: UIL . (goto (card I)) = UsedIntLoc (goto (card I)) by A1 .= {} by Th15 ; rng I c= the InstructionsF of SCM+FSA ; then UIL * (Directed I) = UIL * (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I)))) * I) by FUNCT_7:116 .= (UIL * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))))) * I by RELAT_1:36 .= UIL * I by A3, A7, FUNCT_7:108 ; hence UsedIntLoc I = UsedIntLoc (Directed I) by A2, A5, A6, FUNCT_2:63; ::_thesis: verum end; theorem Th27: :: SF_MASTR:27 for I, J being Program of holds UsedIntLoc (I ";" J) = (UsedIntLoc I) \/ (UsedIntLoc J) proof let I, J be Program of ; ::_thesis: UsedIntLoc (I ";" J) = (UsedIntLoc I) \/ (UsedIntLoc J) dom I = dom (Directed I) by FUNCT_4:99; then dom (Directed I) misses dom (Reloc (J,(card I))) by COMPOS_1:48; hence UsedIntLoc (I ";" J) = (UsedIntLoc (Directed I)) \/ (UsedIntLoc (Reloc (J,(card I)))) by Th21 .= (UsedIntLoc I) \/ (UsedIntLoc (Reloc (J,(card I)))) by Th26 .= (UsedIntLoc I) \/ (UsedIntLoc J) by Th25 ; ::_thesis: verum end; theorem Th28: :: SF_MASTR:28 for i being Instruction of SCM+FSA holds UsedIntLoc (Macro i) = UsedIntLoc i proof let i be Instruction of SCM+FSA; ::_thesis: UsedIntLoc (Macro i) = UsedIntLoc i consider UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and A2: UsedIntLoc (Macro i) = Union (UIL * (Macro i)) by Def2; A3: ( rng (Macro i) = {i,(halt SCM+FSA)} & dom UIL = the InstructionsF of SCM+FSA ) by COMPOS_1:67, FUNCT_2:def_1; thus UsedIntLoc (Macro i) = union (rng (UIL * (Macro i))) by A2, CARD_3:def_4 .= union (UIL .: (rng (Macro i))) by RELAT_1:127 .= union {(UIL . i),(UIL . (halt SCM+FSA))} by A3, FUNCT_1:60 .= (UIL . i) \/ (UIL . (halt SCM+FSA)) by ZFMISC_1:75 .= (UsedIntLoc i) \/ (UIL . (halt SCM+FSA)) by A1 .= (UsedIntLoc i) \/ (UsedIntLoc (halt SCM+FSA)) by A1 .= UsedIntLoc i by Th13 ; ::_thesis: verum end; theorem :: SF_MASTR:29 for i being Instruction of SCM+FSA for J being Program of holds UsedIntLoc (i ";" J) = (UsedIntLoc i) \/ (UsedIntLoc J) proof let i be Instruction of SCM+FSA; ::_thesis: for J being Program of holds UsedIntLoc (i ";" J) = (UsedIntLoc i) \/ (UsedIntLoc J) let J be Program of ; ::_thesis: UsedIntLoc (i ";" J) = (UsedIntLoc i) \/ (UsedIntLoc J) thus UsedIntLoc (i ";" J) = (UsedIntLoc (Macro i)) \/ (UsedIntLoc J) by Th27 .= (UsedIntLoc i) \/ (UsedIntLoc J) by Th28 ; ::_thesis: verum end; theorem :: SF_MASTR:30 for j being Instruction of SCM+FSA for I being Program of holds UsedIntLoc (I ";" j) = (UsedIntLoc I) \/ (UsedIntLoc j) proof let j be Instruction of SCM+FSA; ::_thesis: for I being Program of holds UsedIntLoc (I ";" j) = (UsedIntLoc I) \/ (UsedIntLoc j) let I be Program of ; ::_thesis: UsedIntLoc (I ";" j) = (UsedIntLoc I) \/ (UsedIntLoc j) thus UsedIntLoc (I ";" j) = (UsedIntLoc I) \/ (UsedIntLoc (Macro j)) by Th27 .= (UsedIntLoc I) \/ (UsedIntLoc j) by Th28 ; ::_thesis: verum end; theorem :: SF_MASTR:31 for i, j being Instruction of SCM+FSA holds UsedIntLoc (i ";" j) = (UsedIntLoc i) \/ (UsedIntLoc j) proof let i, j be Instruction of SCM+FSA; ::_thesis: UsedIntLoc (i ";" j) = (UsedIntLoc i) \/ (UsedIntLoc j) thus UsedIntLoc (i ";" j) = (UsedIntLoc (Macro i)) \/ (UsedIntLoc (Macro j)) by Th27 .= (UsedIntLoc (Macro i)) \/ (UsedIntLoc j) by Th28 .= (UsedIntLoc i) \/ (UsedIntLoc j) by Th28 ; ::_thesis: verum end; begin definition let i be Instruction of SCM+FSA; func UsedInt*Loc i -> Element of Fin FinSeq-Locations means :Def3: :: SF_MASTR:def 3 ex a, b being Int-Location ex 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 ex 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 ( ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b1 being Element of Fin FinSeq-Locations ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {f} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin FinSeq-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {f} ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin FinSeq-Locations st b1 = {} ) ) proof hereby ::_thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin FinSeq-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {f} ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin FinSeq-Locations st b1 = {} ) ) assume ( InsCode i = 9 or InsCode i = 10 ) ; ::_thesis: ex IT being Element of Fin FinSeq-Locations ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} ) 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:38, SCMFSA_2:39; reconsider f9 = f as Element of FinSeq-Locations by SCMFSA_2:def_5; reconsider IT = {.f9.} as Element of Fin FinSeq-Locations ; take IT = IT; ::_thesis: ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} ) take a = a; ::_thesis: ex b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} ) take b = b; ::_thesis: ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} ) take f = f; ::_thesis: ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} ) thus ( ( i = b := (f,a) or i = (f,a) := b ) & IT = {f} ) by A1; ::_thesis: verum end; hereby ::_thesis: ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin FinSeq-Locations st b1 = {} ) assume ( InsCode i = 11 or InsCode i = 12 ) ; ::_thesis: ex IT being Element of Fin FinSeq-Locations ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} ) 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:40, SCMFSA_2:41; reconsider f9 = f as Element of FinSeq-Locations by SCMFSA_2:def_5; reconsider IT = {.f9.} as Element of Fin FinSeq-Locations ; take IT = IT; ::_thesis: ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} ) take a = a; ::_thesis: ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} ) take f = f; ::_thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} ) thus ( ( i = a :=len f or i = f :=<0,...,0> a ) & IT = {f} ) by A2; ::_thesis: verum end; {} in Fin FinSeq-Locations by FINSUB_1:7; hence ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin FinSeq-Locations st b1 = {} ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of Fin FinSeq-Locations holds ( ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {f} ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b2 = {f} ) implies b1 = b2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {f} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {f} ) implies b1 = b2 ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not b1 = {} or not b2 = {} or b1 = b2 ) ) proof let it1, it2 be Element of Fin FinSeq-Locations; ::_thesis: ( ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it1 = {f} ) & ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & it2 = {f} ) implies it1 = it2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {f} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {f} ) implies it1 = it2 ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ) hereby ::_thesis: ( ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it1 = {f} ) & ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & it2 = {f} ) implies it1 = it2 ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ) assume ( InsCode i = 9 or InsCode i = 10 ) ; ::_thesis: ( ex a1, b1 being Int-Location ex f1 being FinSeq-Location st ( ( i = b1 := (f1,a1) or i = (f1,a1) := b1 ) & it1 = {f1} ) & ex a2, b2 being Int-Location ex f2 being FinSeq-Location st ( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {f2} ) implies it1 = it2 ) given a1, b1 being Int-Location, f1 being FinSeq-Location such that A3: ( i = b1 := (f1,a1) or i = (f1,a1) := b1 ) and A4: it1 = {f1} ; ::_thesis: ( ex a2, b2 being Int-Location ex f2 being FinSeq-Location st ( ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) & it2 = {f2} ) implies it1 = it2 ) given a2, b2 being Int-Location, f2 being FinSeq-Location such that A5: ( i = b2 := (f2,a2) or i = (f2,a2) := b2 ) and A6: it2 = {f2} ; ::_thesis: it1 = it2 A7: ( ( i = (f1,a1) := b1 or i = (f2,a2) := b2 ) implies InsCode i = 10 ) by SCMFSA_2:27; percases ( ( i = b1 := (f1,a1) & i = b2 := (f2,a2) ) or ( i = (f1,a1) := b1 & i = (f2,a2) := b2 ) ) by A3, A5, A7, SCMFSA_2:26; suppose ( i = b1 := (f1,a1) & i = b2 := (f2,a2) ) ; ::_thesis: it1 = it2 hence it1 = it2 by A4, A6, Th9; ::_thesis: verum end; suppose ( i = (f1,a1) := b1 & i = (f2,a2) := b2 ) ; ::_thesis: it1 = it2 hence it1 = it2 by A4, A6, Th10; ::_thesis: verum end; end; end; hereby ::_thesis: ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) assume ( InsCode i = 11 or InsCode i = 12 ) ; ::_thesis: ( ex a1 being Int-Location ex f1 being FinSeq-Location st ( ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) & it1 = {f1} ) & ex a2 being Int-Location ex f2 being FinSeq-Location st ( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {f2} ) implies it1 = it2 ) given a1 being Int-Location, f1 being FinSeq-Location such that A8: ( i = a1 :=len f1 or i = f1 :=<0,...,0> a1 ) and A9: it1 = {f1} ; ::_thesis: ( ex a2 being Int-Location ex f2 being FinSeq-Location st ( ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) & it2 = {f2} ) implies it1 = it2 ) given a2 being Int-Location, f2 being FinSeq-Location such that A10: ( i = a2 :=len f2 or i = f2 :=<0,...,0> a2 ) and A11: it2 = {f2} ; ::_thesis: it1 = it2 A12: ( ( i = f1 :=<0,...,0> a1 or i = f2 :=<0,...,0> a2 ) implies InsCode i = 12 ) by SCMFSA_2:29; percases ( ( i = a1 :=len f1 & i = a2 :=len f2 ) or ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ) by A8, A10, A12, SCMFSA_2:28; suppose ( i = a1 :=len f1 & i = a2 :=len f2 ) ; ::_thesis: it1 = it2 hence it1 = it2 by A9, A11, Th11; ::_thesis: verum end; suppose ( i = f1 :=<0,...,0> a1 & i = f2 :=<0,...,0> a2 ) ; ::_thesis: it1 = it2 hence it1 = it2 by A9, A11, Th12; ::_thesis: verum end; end; end; thus ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not it1 = {} or not it2 = {} or it1 = it2 ) ; ::_thesis: verum end; consistency for b1 being Element of Fin FinSeq-Locations st ( InsCode i = 9 or InsCode i = 10 ) & ( InsCode i = 11 or InsCode i = 12 ) holds ( ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {f} ) iff ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {f} ) ) ; end; :: deftheorem Def3 defines UsedInt*Loc SF_MASTR:def_3_:_ for i being Instruction of SCM+FSA for b2 being Element of Fin FinSeq-Locations holds ( ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b2 = UsedInt*Loc i iff ex a, b being Int-Location ex f being FinSeq-Location st ( ( i = b := (f,a) or i = (f,a) := b ) & b2 = {f} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b2 = UsedInt*Loc i iff ex a being Int-Location ex f being FinSeq-Location st ( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {f} ) ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b2 = UsedInt*Loc i iff b2 = {} ) ) ); theorem Th32: :: SF_MASTR:32 for a, b being Int-Location for l being Element of NAT for i being Instruction of SCM+FSA st ( 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 ) holds UsedInt*Loc i = {} proof let a, b be Int-Location; ::_thesis: for l being Element of NAT for i being Instruction of SCM+FSA st ( 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 ) holds UsedInt*Loc i = {} let l be Element of NAT ; ::_thesis: for i being Instruction of SCM+FSA st ( 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 ) holds UsedInt*Loc i = {} let i be Instruction of SCM+FSA; ::_thesis: ( ( 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 = {} ) 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 ) ; ::_thesis: UsedInt*Loc i = {} 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 COMPOS_1:70, SCMFSA_2:18, SCMFSA_2:19, SCMFSA_2:20, SCMFSA_2:21, SCMFSA_2:22, SCMFSA_2:23, SCMFSA_2:24, SCMFSA_2:25; hence UsedInt*Loc i = {} by Def3; ::_thesis: verum end; theorem Th33: :: SF_MASTR:33 for b, a being Int-Location for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds UsedInt*Loc i = {f} proof let b, a be Int-Location; ::_thesis: for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds UsedInt*Loc i = {f} let f be FinSeq-Location ; ::_thesis: for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds UsedInt*Loc i = {f} let i be Instruction of SCM+FSA; ::_thesis: ( ( i = b := (f,a) or i = (f,a) := b ) implies UsedInt*Loc i = {f} ) f in FinSeq-Locations by SCMFSA_2:def_5; then {f} c= FinSeq-Locations by ZFMISC_1:31; then reconsider ab = {f} as Element of Fin FinSeq-Locations by FINSUB_1:def_5; assume A1: ( i = b := (f,a) or i = (f,a) := b ) ; ::_thesis: UsedInt*Loc i = {f} then ( InsCode i = 9 or InsCode i = 10 ) by SCMFSA_2:26, SCMFSA_2:27; then UsedInt*Loc i = ab by A1, Def3; hence UsedInt*Loc i = {f} ; ::_thesis: verum end; theorem Th34: :: SF_MASTR:34 for a being Int-Location for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds UsedInt*Loc i = {f} proof let a be Int-Location; ::_thesis: for f being FinSeq-Location for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds UsedInt*Loc i = {f} let f be FinSeq-Location ; ::_thesis: for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds UsedInt*Loc i = {f} let i be Instruction of SCM+FSA; ::_thesis: ( ( i = a :=len f or i = f :=<0,...,0> a ) implies UsedInt*Loc i = {f} ) f in FinSeq-Locations by SCMFSA_2:def_5; then {f} c= FinSeq-Locations by ZFMISC_1:31; then reconsider ab = {f} as Element of Fin FinSeq-Locations by FINSUB_1:def_5; assume A1: ( i = a :=len f or i = f :=<0,...,0> a ) ; ::_thesis: UsedInt*Loc i = {f} then ( InsCode i = 11 or InsCode i = 12 ) by SCMFSA_2:28, SCMFSA_2:29; then UsedInt*Loc i = ab by A1, Def3; hence UsedInt*Loc i = {f} ; ::_thesis: verum end; definition let p be Function; func UsedInt*Loc p -> Subset of FinSeq-Locations means :Def4: :: SF_MASTR:def 4 ex UIL being Function of the InstructionsF 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 ex b1 being Subset of FinSeq-Locations ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b1 = Union (UIL * p) ) proof defpred S1[ set , set ] means ex I being Instruction of SCM+FSA st ( $1 = I & $2 = UsedInt*Loc I ); A1: for e being Element of the InstructionsF of SCM+FSA ex u being Element of Fin FinSeq-Locations st S1[e,u] proof let e be Element of the InstructionsF of SCM+FSA; ::_thesis: ex u being Element of Fin FinSeq-Locations st S1[e,u] reconsider f = e as Instruction of SCM+FSA ; reconsider u = UsedInt*Loc f as Element of Fin FinSeq-Locations ; take u ; ::_thesis: S1[e,u] take f ; ::_thesis: ( e = f & u = UsedInt*Loc f ) thus ( e = f & u = UsedInt*Loc f ) ; ::_thesis: verum end; consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A2: for i being Element of the InstructionsF of SCM+FSA holds S1[i,UIL . i] from FUNCT_2:sch_3(A1); set IT = Union (UIL * p); set dp = dom p; set Up = UIL * p; take Union (UIL * p) ; ::_thesis: ( Union (UIL * p) is Subset of FinSeq-Locations & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & Union (UIL * p) = Union (UIL * p) ) ) Fin FinSeq-Locations c= bool FinSeq-Locations by FINSUB_1:13; then ( rng (UIL * p) c= rng UIL & rng UIL c= bool FinSeq-Locations ) by RELAT_1:26, XBOOLE_1:1; then rng (UIL * p) c= bool FinSeq-Locations by XBOOLE_1:1; then ( Union (UIL * p) = union (rng (UIL * p)) & union (rng (UIL * p)) c= union (bool FinSeq-Locations) ) by CARD_3:def_4, ZFMISC_1:77; hence Union (UIL * p) is Subset of FinSeq-Locations by ZFMISC_1:81; ::_thesis: ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & Union (UIL * p) = Union (UIL * p) ) take UIL ; ::_thesis: ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & Union (UIL * p) = Union (UIL * p) ) hereby ::_thesis: Union (UIL * p) = Union (UIL * p) let i be Instruction of SCM+FSA; ::_thesis: UIL . i = UsedInt*Loc i S1[i,UIL . i] by A2; hence UIL . i = UsedInt*Loc i ; ::_thesis: verum end; thus Union (UIL * p) = Union (UIL * p) ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of FinSeq-Locations st ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b1 = Union (UIL * p) ) & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b2 = Union (UIL * p) ) holds b1 = b2 proof let IT1, IT2 be Subset of FinSeq-Locations; ::_thesis: ( ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & IT1 = Union (UIL * p) ) & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & IT2 = Union (UIL * p) ) implies IT1 = IT2 ) given UIL1 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL1 . i = UsedInt*Loc i and A4: IT1 = Union (UIL1 * p) ; ::_thesis: ( for UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) holds ( ex i being Instruction of SCM+FSA st not UIL . i = UsedInt*Loc i or not IT2 = Union (UIL * p) ) or IT1 = IT2 ) given UIL2 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A5: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and A6: IT2 = Union (UIL2 * p) ; ::_thesis: IT1 = IT2 for c being Element of the InstructionsF of SCM+FSA holds UIL1 . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL1 . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL1 . c = UsedInt*Loc d by A3 .= UIL2 . c by A5 ; ::_thesis: verum end; hence IT1 = IT2 by A4, A6, FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines UsedInt*Loc SF_MASTR:def_4_:_ for p being Function for b2 being Subset of FinSeq-Locations holds ( b2 = UsedInt*Loc p iff ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b2 = Union (UIL * p) ) ); registration let p be preProgram of SCM+FSA; cluster UsedInt*Loc p -> finite ; coherence UsedInt*Loc p is finite proof reconsider dp = dom p as finite set ; consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A1: UsedInt*Loc p = Union (UIL * p) by Def4; rng p c= the InstructionsF of SCM+FSA ; then reconsider p9 = p as Function of dp, the InstructionsF of SCM+FSA by FUNCT_2:2; reconsider Up = UIL * p9 as Function of dp,(Fin FinSeq-Locations) ; Union Up is finite ; hence UsedInt*Loc p is finite by A1; ::_thesis: verum end; end; theorem Th35: :: SF_MASTR:35 for i being Instruction of SCM+FSA for p being preProgram of SCM+FSA st i in rng p holds UsedInt*Loc i c= UsedInt*Loc p proof let i be Instruction of SCM+FSA; ::_thesis: for p being preProgram of SCM+FSA st i in rng p holds UsedInt*Loc i c= UsedInt*Loc p let p be preProgram of SCM+FSA; ::_thesis: ( i in rng p implies UsedInt*Loc i c= UsedInt*Loc p ) assume i in rng p ; ::_thesis: UsedInt*Loc i c= UsedInt*Loc p then consider x being set such that A1: ( x in dom p & i = p . x ) by FUNCT_1:def_3; consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A2: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A3: UsedInt*Loc p = Union (UIL * p) by Def4; A4: UsedInt*Loc p = union (rng (UIL * p)) by A3, CARD_3:def_4; dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then x in dom (UIL * p) by A1, FUNCT_1:11; then A5: (UIL * p) . x in rng (UIL * p) by FUNCT_1:def_3; (UIL * p) . x = UIL . i by A1, FUNCT_1:13 .= UsedInt*Loc i by A2 ; hence UsedInt*Loc i c= UsedInt*Loc p by A5, A4, ZFMISC_1:74; ::_thesis: verum end; theorem :: SF_MASTR:36 for p, r being preProgram of SCM+FSA holds UsedInt*Loc (p +* r) c= (UsedInt*Loc p) \/ (UsedInt*Loc r) proof let p, r be preProgram of SCM+FSA; ::_thesis: UsedInt*Loc (p +* r) c= (UsedInt*Loc p) \/ (UsedInt*Loc r) consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A2: UsedInt*Loc (p +* r) = Union (UIL * (p +* r)) by Def4; consider UIL1 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL1 . i = UsedInt*Loc i and A4: UsedInt*Loc p = Union (UIL1 * p) by Def4; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL1 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL1 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedInt*Loc d by A1 .= UIL1 . c by A3 ; ::_thesis: verum end; then A5: UIL = UIL1 by FUNCT_2:63; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A6: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and A7: UsedInt*Loc r = Union (UIL2 * r) by Def4; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedInt*Loc d by A1 .= UIL2 . c by A6 ; ::_thesis: verum end; then A8: UIL = UIL2 by FUNCT_2:63; dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then rng r c= dom UIL ; then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:9; then A9: ( Union (UIL * r) = union (rng (UIL * r)) & union (rng (UIL * (p +* r))) c= union ((rng (UIL * p)) \/ (rng (UIL * r))) ) by CARD_3:def_4, FUNCT_4:17, ZFMISC_1:77; ( Union (UIL * (p +* r)) = union (rng (UIL * (p +* r))) & Union (UIL * p) = union (rng (UIL * p)) ) by CARD_3:def_4; hence UsedInt*Loc (p +* r) c= (UsedInt*Loc p) \/ (UsedInt*Loc r) by A2, A4, A7, A5, A8, A9, ZFMISC_1:78; ::_thesis: verum end; theorem Th37: :: SF_MASTR:37 for p, r being preProgram of SCM+FSA st dom p misses dom r holds UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r) proof let p, r be preProgram of SCM+FSA; ::_thesis: ( dom p misses dom r implies UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r) ) consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A2: UsedInt*Loc (p +* r) = Union (UIL * (p +* r)) by Def4; assume dom p misses dom r ; ::_thesis: UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r) then ( dom (UIL * p) c= dom p & dom p misses dom (UIL * r) ) by RELAT_1:25, XBOOLE_1:63; then A3: (UIL * p) +* (UIL * r) = (UIL * p) \/ (UIL * r) by FUNCT_4:31, XBOOLE_1:63; dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then rng r c= dom UIL ; then UIL * (p +* r) = (UIL * p) +* (UIL * r) by FUNCT_7:9; then A4: ( Union (UIL * r) = union (rng (UIL * r)) & union (rng (UIL * (p +* r))) = union ((rng (UIL * p)) \/ (rng (UIL * r))) ) by A3, CARD_3:def_4, RELAT_1:12; consider UIL1 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A5: for i being Instruction of SCM+FSA holds UIL1 . i = UsedInt*Loc i and A6: UsedInt*Loc p = Union (UIL1 * p) by Def4; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL1 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL1 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedInt*Loc d by A1 .= UIL1 . c by A5 ; ::_thesis: verum end; then A7: UIL = UIL1 by FUNCT_2:63; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A8: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and A9: UsedInt*Loc r = Union (UIL2 * r) by Def4; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedInt*Loc d by A1 .= UIL2 . c by A8 ; ::_thesis: verum end; then A10: UIL = UIL2 by FUNCT_2:63; ( Union (UIL * (p +* r)) = union (rng (UIL * (p +* r))) & Union (UIL * p) = union (rng (UIL * p)) ) by CARD_3:def_4; hence UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r) by A2, A6, A9, A7, A10, A4, ZFMISC_1:78; ::_thesis: verum end; theorem Th38: :: SF_MASTR:38 for p being preProgram of SCM+FSA for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (Shift (p,k)) proof let p be preProgram of SCM+FSA; ::_thesis: for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (Shift (p,k)) let k be Element of NAT ; ::_thesis: UsedInt*Loc p = UsedInt*Loc (Shift (p,k)) set Sp = Shift (p,k); consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A2: UsedInt*Loc p = Union (UIL * p) by Def4; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and A4: UsedInt*Loc (Shift (p,k)) = Union (UIL2 * (Shift (p,k))) by Def4; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedInt*Loc d by A1 .= UIL2 . c by A3 ; ::_thesis: verum end; then A5: UIL = UIL2 by FUNCT_2:63; A6: dom (Shift (p,k)) = { (m + k) where m is Element of NAT : m in dom p } by VALUED_1:def_12; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_rng_(Shift_(p,k))_implies_y_in_rng_p_)_&_(_y_in_rng_p_implies_y_in_rng_(Shift_(p,k))_)_) let y be set ; ::_thesis: ( ( y in rng (Shift (p,k)) implies y in rng p ) & ( y in rng p implies y in rng (Shift (p,k)) ) ) hereby ::_thesis: ( y in rng p implies y in rng (Shift (p,k)) ) assume y in rng (Shift (p,k)) ; ::_thesis: y in rng p then consider x being set such that A7: x in dom (Shift (p,k)) and A8: y = (Shift (p,k)) . x by FUNCT_1:def_3; consider m being Element of NAT such that A9: x = m + k and A10: m in dom p by A6, A7; (Shift (p,k)) . x = p . m by A9, A10, VALUED_1:def_12; hence y in rng p by A8, A10, FUNCT_1:def_3; ::_thesis: verum end; assume y in rng p ; ::_thesis: y in rng (Shift (p,k)) then consider x being set such that A11: x in dom p and A12: y = p . x by FUNCT_1:def_3; reconsider x9 = x as Element of NAT by A11; reconsider m = x9 as Element of NAT ; ( m + k in dom (Shift (p,k)) & (Shift (p,k)) . (m + k) = p . m ) by A6, A11, VALUED_1:def_12; hence y in rng (Shift (p,k)) by A12, FUNCT_1:def_3; ::_thesis: verum end; then A13: rng (Shift (p,k)) = rng p by TARSKI:1; A14: Union (UIL * (Shift (p,k))) = union (rng (UIL * (Shift (p,k)))) by CARD_3:def_4; rng (UIL * (Shift (p,k))) = UIL .: (rng (Shift (p,k))) by RELAT_1:127 .= rng (UIL * p) by A13, RELAT_1:127 ; hence UsedInt*Loc p = UsedInt*Loc (Shift (p,k)) by A2, A4, A5, A14, CARD_3:def_4; ::_thesis: verum end; theorem Th39: :: SF_MASTR:39 for i being Instruction of SCM+FSA for k being Element of NAT holds UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) proof let i be Instruction of SCM+FSA; ::_thesis: for k being Element of NAT holds UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) let k be Element of NAT ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) A1: InsCode i <= 12 by SCMFSA_2:16; percases ( 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 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A1, NAT_1:36; suppose InsCode i = 0 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then i = halt SCM+FSA by SCMFSA_2:95; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a, b being Int-Location st i = a := b by SCMFSA_2:30; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 2 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:31; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 3 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:32; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:33; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:34; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 6 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then consider l being Element of NAT such that A2: i = goto l by SCMFSA_2:35; IncAddr (i,k) = goto (l + k) by A2, SCMFSA_4:1; hence UsedInt*Loc (IncAddr (i,k)) = {} by Th32 .= UsedInt*Loc i by A2, Th32 ; ::_thesis: verum end; suppose InsCode i = 7 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then consider l being Element of NAT , a being Int-Location such that A3: i = a =0_goto l by SCMFSA_2:36; IncAddr (i,k) = a =0_goto (l + k) by A3, SCMFSA_4:2; hence UsedInt*Loc (IncAddr (i,k)) = {} by Th32 .= UsedInt*Loc i by A3, Th32 ; ::_thesis: verum end; suppose InsCode i = 8 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then consider l being Element of NAT , a being Int-Location such that A4: i = a >0_goto l by SCMFSA_2:37; IncAddr (i,k) = a >0_goto (l + k) by A4, SCMFSA_4:3; hence UsedInt*Loc (IncAddr (i,k)) = {} by Th32 .= UsedInt*Loc i by A4, Th32 ; ::_thesis: verum end; suppose InsCode i = 9 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a, b being Int-Location ex f being FinSeq-Location st i = b := (f,a) by SCMFSA_2:38; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 10 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 11 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a being Int-Location ex f being FinSeq-Location st i = a :=len f by SCMFSA_2:40; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; suppose InsCode i = 12 ; ::_thesis: UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41; hence UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k)) by COMPOS_0:4; ::_thesis: verum end; end; end; theorem Th40: :: SF_MASTR:40 for p being preProgram of SCM+FSA for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k)) proof let p be preProgram of SCM+FSA; ::_thesis: for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k)) let k be Element of NAT ; ::_thesis: UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k)) set Ip = IncAddr (p,k); consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A2: UsedInt*Loc p = Union (UIL * p) by Def4; set g = UIL * p; set f = UIL * (IncAddr (p,k)); consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A3: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and A4: UsedInt*Loc (IncAddr (p,k)) = Union (UIL2 * (IncAddr (p,k))) by Def4; for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedInt*Loc d by A1 .= UIL2 . c by A3 ; ::_thesis: verum end; then A5: UIL = UIL2 by FUNCT_2:63; now__::_thesis:_(_dom_(UIL_*_(IncAddr_(p,k)))_=_dom_(UIL_*_p)_&_(_for_x_being_set_st_x_in_dom_(UIL_*_(IncAddr_(p,k)))_holds_ (UIL_*_(IncAddr_(p,k)))_._x_=_(UIL_*_p)_._x_)_) A6: dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; then A7: rng p c= dom UIL ; rng (IncAddr (p,k)) c= dom UIL by A6; then A8: dom (UIL * (IncAddr (p,k))) = dom (IncAddr (p,k)) by RELAT_1:27; A9: dom (IncAddr (p,k)) = dom p by COMPOS_1:def_21; hence dom (UIL * (IncAddr (p,k))) = dom (UIL * p) by A7, A8, RELAT_1:27; ::_thesis: for x being set st x in dom (UIL * (IncAddr (p,k))) holds (UIL * (IncAddr (p,k))) . x = (UIL * p) . x let x be set ; ::_thesis: ( x in dom (UIL * (IncAddr (p,k))) implies (UIL * (IncAddr (p,k))) . x = (UIL * p) . x ) assume A10: x in dom (UIL * (IncAddr (p,k))) ; ::_thesis: (UIL * (IncAddr (p,k))) . x = (UIL * p) . x then p . x in rng p by A9, A8, FUNCT_1:def_3; then reconsider px = p . x as Instruction of SCM+FSA ; reconsider x9 = x as Element of NAT by A8, A10; reconsider m = x9 as Element of NAT ; A11: (IncAddr (p,k)) . x = IncAddr ((p /. m),k) by A9, A8, A10, COMPOS_1:def_21 .= IncAddr (px,k) by A9, A8, A10, PARTFUN1:def_6 ; (IncAddr (p,k)) . x in rng (IncAddr (p,k)) by A8, A10, FUNCT_1:def_3; then reconsider Ipx = (IncAddr (p,k)) . x as Instruction of SCM+FSA ; thus (UIL * (IncAddr (p,k))) . x = UIL . Ipx by A10, FUNCT_1:12 .= UsedInt*Loc Ipx by A1 .= UsedInt*Loc px by A11, Th39 .= UIL . px by A3, A5 .= (UIL * p) . x by A9, A8, A10, FUNCT_1:13 ; ::_thesis: verum end; hence UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k)) by A2, A4, A5, FUNCT_1:2; ::_thesis: verum end; theorem Th41: :: SF_MASTR:41 for I being Program of for k being Element of NAT holds UsedInt*Loc I = UsedInt*Loc (Reloc (I,k)) proof let I be Program of ; ::_thesis: for k being Element of NAT holds UsedInt*Loc I = UsedInt*Loc (Reloc (I,k)) let k be Element of NAT ; ::_thesis: UsedInt*Loc I = UsedInt*Loc (Reloc (I,k)) A1: Reloc (I,k) = IncAddr ((Shift (I,k)),k) by COMPOS_1:34; UsedInt*Loc (Reloc (I,k)) = UsedInt*Loc (Reloc (I,k)) .= UsedInt*Loc (Shift (I,k)) by Th40, A1 .= UsedInt*Loc I by Th38 ; hence UsedInt*Loc I = UsedInt*Loc (Reloc (I,k)) ; ::_thesis: verum end; theorem Th42: :: SF_MASTR:42 for I being Program of holds UsedInt*Loc I = UsedInt*Loc (Directed I) proof let I be Program of ; ::_thesis: UsedInt*Loc I = UsedInt*Loc (Directed I) consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A2: UsedInt*Loc I = Union (UIL * I) by Def4; A3: UIL . (halt SCM+FSA) = UsedInt*Loc (halt SCM+FSA) by A1 .= {} by Th32 ; consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A4: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and A5: UsedInt*Loc (Directed I) = Union (UIL2 * (Directed I)) by Def4; A6: for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c proof let c be Element of the InstructionsF of SCM+FSA; ::_thesis: UIL . c = UIL2 . c reconsider d = c as Instruction of SCM+FSA ; thus UIL . c = UsedInt*Loc d by A1 .= UIL2 . c by A4 ; ::_thesis: verum end; A7: UIL . (goto (card I)) = UsedInt*Loc (goto (card I)) by A1 .= {} by Th32 ; A8: dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def_1; rng I c= the InstructionsF of SCM+FSA ; then UIL * (Directed I) = UIL * (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I)))) * I) by FUNCT_7:116 .= (UIL * ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card I))))) * I by RELAT_1:36 .= UIL * I by A8, A3, A7, FUNCT_7:108 ; hence UsedInt*Loc I = UsedInt*Loc (Directed I) by A2, A5, A6, FUNCT_2:63; ::_thesis: verum end; theorem Th43: :: SF_MASTR:43 for I, J being Program of holds UsedInt*Loc (I ";" J) = (UsedInt*Loc I) \/ (UsedInt*Loc J) proof let I, J be Program of ; ::_thesis: UsedInt*Loc (I ";" J) = (UsedInt*Loc I) \/ (UsedInt*Loc J) dom I = dom (Directed I) by FUNCT_4:99; then dom (Directed I) misses dom (Reloc (J,(card I))) by COMPOS_1:48; hence UsedInt*Loc (I ";" J) = (UsedInt*Loc (Directed I)) \/ (UsedInt*Loc (Reloc (J,(card I)))) by Th37 .= (UsedInt*Loc I) \/ (UsedInt*Loc (Reloc (J,(card I)))) by Th42 .= (UsedInt*Loc I) \/ (UsedInt*Loc J) by Th41 ; ::_thesis: verum end; theorem Th44: :: SF_MASTR:44 for i being Instruction of SCM+FSA holds UsedInt*Loc (Macro i) = UsedInt*Loc i proof let i be Instruction of SCM+FSA; ::_thesis: UsedInt*Loc (Macro i) = UsedInt*Loc i consider UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and A2: UsedInt*Loc (Macro i) = Union (UIL * (Macro i)) by Def4; A3: ( rng (Macro i) = {i,(halt SCM+FSA)} & dom UIL = the InstructionsF of SCM+FSA ) by COMPOS_1:67, FUNCT_2:def_1; thus UsedInt*Loc (Macro i) = union (rng (UIL * (Macro i))) by A2, CARD_3:def_4 .= union (UIL .: (rng (Macro i))) by RELAT_1:127 .= union {(UIL . i),(UIL . (halt SCM+FSA))} by A3, FUNCT_1:60 .= (UIL . i) \/ (UIL . (halt SCM+FSA)) by ZFMISC_1:75 .= (UsedInt*Loc i) \/ (UIL . (halt SCM+FSA)) by A1 .= (UsedInt*Loc i) \/ (UsedInt*Loc (halt SCM+FSA)) by A1 .= (UsedInt*Loc i) \/ {} by Th32 .= UsedInt*Loc i ; ::_thesis: verum end; theorem :: SF_MASTR:45 for i being Instruction of SCM+FSA for J being Program of holds UsedInt*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedInt*Loc J) proof let i be Instruction of SCM+FSA; ::_thesis: for J being Program of holds UsedInt*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedInt*Loc J) let J be Program of ; ::_thesis: UsedInt*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedInt*Loc J) thus UsedInt*Loc (i ";" J) = (UsedInt*Loc (Macro i)) \/ (UsedInt*Loc J) by Th43 .= (UsedInt*Loc i) \/ (UsedInt*Loc J) by Th44 ; ::_thesis: verum end; theorem :: SF_MASTR:46 for j being Instruction of SCM+FSA for I being Program of holds UsedInt*Loc (I ";" j) = (UsedInt*Loc I) \/ (UsedInt*Loc j) proof let j be Instruction of SCM+FSA; ::_thesis: for I being Program of holds UsedInt*Loc (I ";" j) = (UsedInt*Loc I) \/ (UsedInt*Loc j) let I be Program of ; ::_thesis: UsedInt*Loc (I ";" j) = (UsedInt*Loc I) \/ (UsedInt*Loc j) thus UsedInt*Loc (I ";" j) = (UsedInt*Loc I) \/ (UsedInt*Loc (Macro j)) by Th43 .= (UsedInt*Loc I) \/ (UsedInt*Loc j) by Th44 ; ::_thesis: verum end; theorem :: SF_MASTR:47 for i, j being Instruction of SCM+FSA holds UsedInt*Loc (i ";" j) = (UsedInt*Loc i) \/ (UsedInt*Loc j) proof let i, j be Instruction of SCM+FSA; ::_thesis: UsedInt*Loc (i ";" j) = (UsedInt*Loc i) \/ (UsedInt*Loc j) thus UsedInt*Loc (i ";" j) = (UsedInt*Loc (Macro i)) \/ (UsedInt*Loc (Macro j)) by Th43 .= (UsedInt*Loc (Macro i)) \/ (UsedInt*Loc j) by Th44 .= (UsedInt*Loc i) \/ (UsedInt*Loc j) by Th44 ; ::_thesis: verum end; begin definition canceled; end; :: deftheorem SF_MASTR:def_5_:_ canceled; theorem :: SF_MASTR:48 for L being finite Subset of Int-Locations holds not FirstNotIn L in L by SCMFSA_M:14; theorem :: SF_MASTR:49 for m, n being Element of NAT for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds m <= n by SCMFSA_M:15; definition let p be preProgram of SCM+FSA; func FirstNotUsed p -> Int-Location means :Def6: :: SF_MASTR:def 6 ex sil being finite Subset of Int-Locations st ( sil = (UsedIntLoc p) \/ {(intloc 0)} & it = FirstNotIn sil ); existence ex b1 being Int-Location ex sil being finite Subset of Int-Locations st ( sil = (UsedIntLoc p) \/ {(intloc 0)} & b1 = FirstNotIn sil ) proof reconsider i0 = {(intloc 0)} as finite Subset of Int-Locations ; reconsider sil = (UsedIntLoc p) \/ i0 as finite Subset of Int-Locations ; take FirstNotIn sil ; ::_thesis: ex sil being finite Subset of Int-Locations st ( sil = (UsedIntLoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil ) take sil ; ::_thesis: ( sil = (UsedIntLoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil ) thus ( sil = (UsedIntLoc p) \/ {(intloc 0)} & FirstNotIn sil = FirstNotIn sil ) ; ::_thesis: verum end; uniqueness for b1, b2 being Int-Location st ex sil being finite Subset of Int-Locations st ( sil = (UsedIntLoc p) \/ {(intloc 0)} & b1 = FirstNotIn sil ) & ex sil being finite Subset of Int-Locations st ( sil = (UsedIntLoc p) \/ {(intloc 0)} & b2 = FirstNotIn sil ) holds b1 = b2 ; end; :: deftheorem Def6 defines FirstNotUsed SF_MASTR:def_6_:_ for p being preProgram of SCM+FSA for b2 being Int-Location holds ( b2 = FirstNotUsed p iff ex sil being finite Subset of Int-Locations st ( sil = (UsedIntLoc p) \/ {(intloc 0)} & b2 = FirstNotIn sil ) ); registration let p be preProgram of SCM+FSA; cluster FirstNotUsed p -> read-write ; coherence not FirstNotUsed p is read-only proof consider sil being finite Subset of Int-Locations such that A1: sil = (UsedIntLoc p) \/ {(intloc 0)} and A2: FirstNotUsed p = FirstNotIn sil by Def6; now__::_thesis:_not_FirstNotIn_sil_=_intloc_0 assume FirstNotIn sil = intloc 0 ; ::_thesis: contradiction then not intloc 0 in sil by SCMFSA_M:14; hence contradiction by A1, ZFMISC_1:136; ::_thesis: verum end; hence not FirstNotUsed p is read-only by A2, SCMFSA_M:def_2; ::_thesis: verum end; end; theorem Th50: :: SF_MASTR:50 for p being preProgram of SCM+FSA holds not FirstNotUsed p in UsedIntLoc p proof let p be preProgram of SCM+FSA; ::_thesis: not FirstNotUsed p in UsedIntLoc p consider sil being finite Subset of Int-Locations such that A1: sil = (UsedIntLoc p) \/ {(intloc 0)} and A2: FirstNotUsed p = FirstNotIn sil by Def6; not FirstNotUsed p in sil by A2, SCMFSA_M:14; hence not FirstNotUsed p in UsedIntLoc p by A1, XBOOLE_0:def_3; ::_thesis: verum end; theorem :: SF_MASTR:51 for a, b being Int-Location for p being preProgram of SCM+FSA st ( 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 ) holds ( FirstNotUsed p <> a & FirstNotUsed p <> b ) proof let a, b be Int-Location; ::_thesis: for p being preProgram of SCM+FSA st ( 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 ) holds ( FirstNotUsed p <> a & FirstNotUsed p <> b ) let p be preProgram of SCM+FSA; ::_thesis: ( ( 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 ) ) 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 ) ; ::_thesis: ( FirstNotUsed p <> a & FirstNotUsed p <> b ) then consider i being Instruction of SCM+FSA such that A1: i in rng p and A2: ( 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 A2, Th14; then A3: {a,b} c= UsedIntLoc p by A1, Th19; not FirstNotUsed p in UsedIntLoc p by Th50; hence ( FirstNotUsed p <> a & FirstNotUsed p <> b ) by A3, ZFMISC_1:32; ::_thesis: verum end; theorem :: SF_MASTR:52 for a being Int-Location for l being Element of NAT for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds FirstNotUsed p <> a proof let a be Int-Location; ::_thesis: for l being Element of NAT for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds FirstNotUsed p <> a let l be Element of NAT ; ::_thesis: for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds FirstNotUsed p <> a let p be preProgram of SCM+FSA; ::_thesis: ( ( a =0_goto l in rng p or a >0_goto l in rng p ) implies FirstNotUsed p <> a ) assume ( a =0_goto l in rng p or a >0_goto l in rng p ) ; ::_thesis: FirstNotUsed p <> a then consider i being Instruction of SCM+FSA such that A1: i in rng p and A2: ( i = a =0_goto l or i = a >0_goto l ) ; UsedIntLoc i = {a} by A2, Th16; then A3: {a} c= UsedIntLoc p by A1, Th19; not FirstNotUsed p in UsedIntLoc p by Th50; hence FirstNotUsed p <> a by A3, ZFMISC_1:31; ::_thesis: verum end; theorem :: SF_MASTR:53 for b, a being Int-Location for f being FinSeq-Location for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds ( FirstNotUsed p <> a & FirstNotUsed p <> b ) proof let b, a be Int-Location; ::_thesis: for f being FinSeq-Location for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds ( FirstNotUsed p <> a & FirstNotUsed p <> b ) let f be FinSeq-Location ; ::_thesis: for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds ( FirstNotUsed p <> a & FirstNotUsed p <> b ) let p be preProgram of SCM+FSA; ::_thesis: ( ( b := (f,a) in rng p or (f,a) := b in rng p ) implies ( FirstNotUsed p <> a & FirstNotUsed p <> b ) ) assume ( b := (f,a) in rng p or (f,a) := b in rng p ) ; ::_thesis: ( FirstNotUsed p <> a & FirstNotUsed p <> b ) then consider i being Instruction of SCM+FSA such that A1: i in rng p and A2: ( i = b := (f,a) or i = (f,a) := b ) ; UsedIntLoc i = {a,b} by A2, Th17; then A3: {a,b} c= UsedIntLoc p by A1, Th19; not FirstNotUsed p in UsedIntLoc p by Th50; hence ( FirstNotUsed p <> a & FirstNotUsed p <> b ) by A3, ZFMISC_1:32; ::_thesis: verum end; theorem :: SF_MASTR:54 for a being Int-Location for f being FinSeq-Location for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds FirstNotUsed p <> a proof let a be Int-Location; ::_thesis: for f being FinSeq-Location for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds FirstNotUsed p <> a let f be FinSeq-Location ; ::_thesis: for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds FirstNotUsed p <> a let p be preProgram of SCM+FSA; ::_thesis: ( ( a :=len f in rng p or f :=<0,...,0> a in rng p ) implies FirstNotUsed p <> a ) assume ( a :=len f in rng p or f :=<0,...,0> a in rng p ) ; ::_thesis: FirstNotUsed p <> a then consider i being Instruction of SCM+FSA such that A1: i in rng p and A2: ( i = a :=len f or i = f :=<0,...,0> a ) ; UsedIntLoc i = {a} by A2, Th18; then A3: {a} c= UsedIntLoc p by A1, Th19; not FirstNotUsed p in UsedIntLoc p by Th50; hence FirstNotUsed p <> a by A3, ZFMISC_1:31; ::_thesis: verum end; begin definition canceled; end; :: deftheorem SF_MASTR:def_7_:_ canceled; theorem :: SF_MASTR:55 for L being finite Subset of FinSeq-Locations holds not First*NotIn L in L by SCMFSA_M:16; theorem :: SF_MASTR:56 for m, n being Element of NAT for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds m <= n by SCMFSA_M:17; definition let p be preProgram of SCM+FSA; func First*NotUsed p -> FinSeq-Location means :Def8: :: SF_MASTR:def 8 ex sil being finite Subset of FinSeq-Locations st ( sil = UsedInt*Loc p & it = First*NotIn sil ); existence ex b1 being FinSeq-Location ex sil being finite Subset of FinSeq-Locations st ( sil = UsedInt*Loc p & b1 = First*NotIn sil ) proof take First*NotIn (UsedInt*Loc p) ; ::_thesis: ex sil being finite Subset of FinSeq-Locations st ( sil = UsedInt*Loc p & First*NotIn (UsedInt*Loc p) = First*NotIn sil ) take UsedInt*Loc p ; ::_thesis: ( UsedInt*Loc p = UsedInt*Loc p & First*NotIn (UsedInt*Loc p) = First*NotIn (UsedInt*Loc p) ) thus ( UsedInt*Loc p = UsedInt*Loc p & First*NotIn (UsedInt*Loc p) = First*NotIn (UsedInt*Loc p) ) ; ::_thesis: verum end; uniqueness for b1, b2 being FinSeq-Location st ex sil being finite Subset of FinSeq-Locations st ( sil = UsedInt*Loc p & b1 = First*NotIn sil ) & ex sil being finite Subset of FinSeq-Locations st ( sil = UsedInt*Loc p & b2 = First*NotIn sil ) holds b1 = b2 ; end; :: deftheorem Def8 defines First*NotUsed SF_MASTR:def_8_:_ for p being preProgram of SCM+FSA for b2 being FinSeq-Location holds ( b2 = First*NotUsed p iff ex sil being finite Subset of FinSeq-Locations st ( sil = UsedInt*Loc p & b2 = First*NotIn sil ) ); theorem Th57: :: SF_MASTR:57 for p being preProgram of SCM+FSA holds not First*NotUsed p in UsedInt*Loc p proof let p be preProgram of SCM+FSA; ::_thesis: not First*NotUsed p in UsedInt*Loc p ex sil being finite Subset of FinSeq-Locations st ( sil = UsedInt*Loc p & First*NotUsed p = First*NotIn sil ) by Def8; hence not First*NotUsed p in UsedInt*Loc p by SCMFSA_M:16; ::_thesis: verum end; theorem :: SF_MASTR:58 for b, a being Int-Location for f being FinSeq-Location for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds First*NotUsed p <> f proof let b, a be Int-Location; ::_thesis: for f being FinSeq-Location for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds First*NotUsed p <> f let f be FinSeq-Location ; ::_thesis: for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds First*NotUsed p <> f let p be preProgram of SCM+FSA; ::_thesis: ( ( b := (f,a) in rng p or (f,a) := b in rng p ) implies First*NotUsed p <> f ) assume ( b := (f,a) in rng p or (f,a) := b in rng p ) ; ::_thesis: First*NotUsed p <> f then consider i being Instruction of SCM+FSA such that A1: i in rng p and A2: ( i = b := (f,a) or i = (f,a) := b ) ; UsedInt*Loc i = {f} by A2, Th33; then A3: {f} c= UsedInt*Loc p by A1, Th35; not First*NotUsed p in UsedInt*Loc p by Th57; hence First*NotUsed p <> f by A3, ZFMISC_1:31; ::_thesis: verum end; theorem :: SF_MASTR:59 for a being Int-Location for f being FinSeq-Location for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds First*NotUsed p <> f proof let a be Int-Location; ::_thesis: for f being FinSeq-Location for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds First*NotUsed p <> f let f be FinSeq-Location ; ::_thesis: for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds First*NotUsed p <> f let p be preProgram of SCM+FSA; ::_thesis: ( ( a :=len f in rng p or f :=<0,...,0> a in rng p ) implies First*NotUsed p <> f ) assume ( a :=len f in rng p or f :=<0,...,0> a in rng p ) ; ::_thesis: First*NotUsed p <> f then consider i being Instruction of SCM+FSA such that A1: i in rng p and A2: ( i = a :=len f or i = f :=<0,...,0> a ) ; UsedInt*Loc i = {f} by A2, Th34; then A3: {f} c= UsedInt*Loc p by A1, Th35; not First*NotUsed p in UsedInt*Loc p by Th57; hence First*NotUsed p <> f by A3, ZFMISC_1:31; ::_thesis: verum end; begin theorem Th60: :: SF_MASTR:60 for c being Int-Location for i being Instruction of SCM+FSA for s being State of SCM+FSA st not c in UsedIntLoc i holds (Exec (i,s)) . c = s . c proof let c be Int-Location; ::_thesis: for i being Instruction of SCM+FSA for s being State of SCM+FSA st not c in UsedIntLoc i holds (Exec (i,s)) . c = s . c let i be Instruction of SCM+FSA; ::_thesis: for s being State of SCM+FSA st not c in UsedIntLoc i holds (Exec (i,s)) . c = s . c let s be State of SCM+FSA; ::_thesis: ( not c in UsedIntLoc i implies (Exec (i,s)) . c = s . c ) assume A1: not c in UsedIntLoc i ; ::_thesis: (Exec (i,s)) . c = s . c A2: InsCode i <= 12 by SCMFSA_2:16; percases ( 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 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A2, NAT_1:36; suppose InsCode i = 0 ; ::_thesis: (Exec (i,s)) . c = s . c then i = halt SCM+FSA by SCMFSA_2:95; hence (Exec (i,s)) . c = s . c by EXTPRO_1:def_3; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: (Exec (i,s)) . c = s . c then consider a, b being Int-Location such that A3: i = a := b by SCMFSA_2:30; UsedIntLoc i = {a,b} by A3, Th14; then c <> a by A1, TARSKI:def_2; hence (Exec (i,s)) . c = s . c by A3, SCMFSA_2:63; ::_thesis: verum end; suppose InsCode i = 2 ; ::_thesis: (Exec (i,s)) . c = s . c then consider a, b being Int-Location such that A4: i = AddTo (a,b) by SCMFSA_2:31; UsedIntLoc i = {a,b} by A4, Th14; then c <> a by A1, TARSKI:def_2; hence (Exec (i,s)) . c = s . c by A4, SCMFSA_2:64; ::_thesis: verum end; suppose InsCode i = 3 ; ::_thesis: (Exec (i,s)) . c = s . c then consider a, b being Int-Location such that A5: i = SubFrom (a,b) by SCMFSA_2:32; UsedIntLoc i = {a,b} by A5, Th14; then c <> a by A1, TARSKI:def_2; hence (Exec (i,s)) . c = s . c by A5, SCMFSA_2:65; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: (Exec (i,s)) . c = s . c then consider a, b being Int-Location such that A6: i = MultBy (a,b) by SCMFSA_2:33; UsedIntLoc i = {a,b} by A6, Th14; then c <> a by A1, TARSKI:def_2; hence (Exec (i,s)) . c = s . c by A6, SCMFSA_2:66; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: (Exec (i,s)) . c = s . c then consider a, b being Int-Location such that A7: i = Divide (a,b) by SCMFSA_2:34; UsedIntLoc i = {a,b} by A7, Th14; then ( c <> a & c <> b ) by A1, TARSKI:def_2; hence (Exec (i,s)) . c = s . c by A7, SCMFSA_2:67; ::_thesis: verum end; suppose InsCode i = 6 ; ::_thesis: (Exec (i,s)) . c = s . c then ex l being Element of NAT st i = goto l by SCMFSA_2:35; hence (Exec (i,s)) . c = s . c by SCMFSA_2:69; ::_thesis: verum end; suppose InsCode i = 7 ; ::_thesis: (Exec (i,s)) . c = s . c then ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36; hence (Exec (i,s)) . c = s . c by SCMFSA_2:70; ::_thesis: verum end; suppose InsCode i = 8 ; ::_thesis: (Exec (i,s)) . c = s . c then ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37; hence (Exec (i,s)) . c = s . c by SCMFSA_2:71; ::_thesis: verum end; suppose InsCode i = 9 ; ::_thesis: (Exec (i,s)) . c = s . c then consider a, b being Int-Location, f being FinSeq-Location such that A8: i = b := (f,a) by SCMFSA_2:38; UsedIntLoc i = {a,b} by A8, Th17; then c <> b by A1, TARSKI:def_2; hence (Exec (i,s)) . c = s . c by A8, SCMFSA_2:72; ::_thesis: verum end; suppose InsCode i = 10 ; ::_thesis: (Exec (i,s)) . c = s . c then ex a, b being Int-Location ex f being FinSeq-Location st i = (f,a) := b by SCMFSA_2:39; hence (Exec (i,s)) . c = s . c by SCMFSA_2:73; ::_thesis: verum end; suppose InsCode i = 11 ; ::_thesis: (Exec (i,s)) . c = s . c then consider a being Int-Location, f being FinSeq-Location such that A9: i = a :=len f by SCMFSA_2:40; UsedIntLoc i = {a} by A9, Th18; then c <> a by A1, TARSKI:def_1; hence (Exec (i,s)) . c = s . c by A9, SCMFSA_2:74; ::_thesis: verum end; suppose InsCode i = 12 ; ::_thesis: (Exec (i,s)) . c = s . c then ex a being Int-Location ex f being FinSeq-Location st i = f :=<0,...,0> a by SCMFSA_2:41; hence (Exec (i,s)) . c = s . c by SCMFSA_2:75; ::_thesis: verum end; end; end; theorem :: SF_MASTR:61 for a being Int-Location for I being Program of for n being Element of NAT for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I holds (Comput (P,s,n)) . a = s . a proof let a be Int-Location; ::_thesis: for I being Program of for n being Element of NAT for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I holds (Comput (P,s,n)) . a = s . a let I be Program of ; ::_thesis: for n being Element of NAT for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I holds (Comput (P,s,n)) . a = s . a let n be Element of NAT ; ::_thesis: for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I holds (Comput (P,s,n)) . a = s . a let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I holds (Comput (P,s,n)) . a = s . a let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I implies (Comput (P,s,n)) . a = s . a ) assume that A1: I c= P and A2: for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I and A3: not a in UsedIntLoc I ; ::_thesis: (Comput (P,s,n)) . a = s . a defpred S1[ Nat] means ( $1 <= n implies (Comput (P,s,$1)) . a = s . a ); A4: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) set sm = Comput (P,s,m); assume A5: ( m <= n implies (Comput (P,s,m)) . a = s . a ) ; ::_thesis: S1[m + 1] assume A6: m + 1 <= n ; ::_thesis: (Comput (P,s,(m + 1))) . a = s . a then m < n by NAT_1:13; then A7: IC (Comput (P,s,m)) in dom I by A2; then A8: I . (IC (Comput (P,s,m))) in rng I by FUNCT_1:def_3; dom P = NAT by PARTFUN1:def_2; then A9: P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PARTFUN1:def_6; I . (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by A7, A1, GRFUNC_1:2; then UsedIntLoc (P . (IC (Comput (P,s,m)))) c= UsedIntLoc I by A8, Th19; then A10: not a in UsedIntLoc (P . (IC (Comput (P,s,m)))) by A3; thus (Comput (P,s,(m + 1))) . a = (Following (P,(Comput (P,s,m)))) . a by EXTPRO_1:3 .= s . a by A5, A6, A10, Th60, A9, NAT_1:13 ; ::_thesis: verum end; A11: S1[ 0 ] ; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A11, A4); hence (Comput (P,s,n)) . a = s . a ; ::_thesis: verum end; theorem Th62: :: SF_MASTR:62 for f being FinSeq-Location for i being Instruction of SCM+FSA for s being State of SCM+FSA st not f in UsedInt*Loc i holds (Exec (i,s)) . f = s . f proof let f be FinSeq-Location ; ::_thesis: for i being Instruction of SCM+FSA for s being State of SCM+FSA st not f in UsedInt*Loc i holds (Exec (i,s)) . f = s . f let i be Instruction of SCM+FSA; ::_thesis: for s being State of SCM+FSA st not f in UsedInt*Loc i holds (Exec (i,s)) . f = s . f let s be State of SCM+FSA; ::_thesis: ( not f in UsedInt*Loc i implies (Exec (i,s)) . f = s . f ) assume A1: not f in UsedInt*Loc i ; ::_thesis: (Exec (i,s)) . f = s . f A2: InsCode i <= 12 by SCMFSA_2:16; percases ( 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 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A2, NAT_1:36; suppose InsCode i = 0 ; ::_thesis: (Exec (i,s)) . f = s . f then i = halt SCM+FSA by SCMFSA_2:95; hence (Exec (i,s)) . f = s . f by EXTPRO_1:def_3; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: (Exec (i,s)) . f = s . f then ex a, b being Int-Location st i = a := b by SCMFSA_2:30; hence (Exec (i,s)) . f = s . f by SCMFSA_2:63; ::_thesis: verum end; suppose InsCode i = 2 ; ::_thesis: (Exec (i,s)) . f = s . f then ex a, b being Int-Location st i = AddTo (a,b) by SCMFSA_2:31; hence (Exec (i,s)) . f = s . f by SCMFSA_2:64; ::_thesis: verum end; suppose InsCode i = 3 ; ::_thesis: (Exec (i,s)) . f = s . f then ex a, b being Int-Location st i = SubFrom (a,b) by SCMFSA_2:32; hence (Exec (i,s)) . f = s . f by SCMFSA_2:65; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: (Exec (i,s)) . f = s . f then ex a, b being Int-Location st i = MultBy (a,b) by SCMFSA_2:33; hence (Exec (i,s)) . f = s . f by SCMFSA_2:66; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: (Exec (i,s)) . f = s . f then ex a, b being Int-Location st i = Divide (a,b) by SCMFSA_2:34; hence (Exec (i,s)) . f = s . f by SCMFSA_2:67; ::_thesis: verum end; suppose InsCode i = 6 ; ::_thesis: (Exec (i,s)) . f = s . f then ex l being Element of NAT st i = goto l by SCMFSA_2:35; hence (Exec (i,s)) . f = s . f by SCMFSA_2:69; ::_thesis: verum end; suppose InsCode i = 7 ; ::_thesis: (Exec (i,s)) . f = s . f then ex l being Element of NAT ex a being Int-Location st i = a =0_goto l by SCMFSA_2:36; hence (Exec (i,s)) . f = s . f by SCMFSA_2:70; ::_thesis: verum end; suppose InsCode i = 8 ; ::_thesis: (Exec (i,s)) . f = s . f then ex l being Element of NAT ex a being Int-Location st i = a >0_goto l by SCMFSA_2:37; hence (Exec (i,s)) . f = s . f by SCMFSA_2:71; ::_thesis: verum end; suppose InsCode i = 9 ; ::_thesis: (Exec (i,s)) . f = s . f then ex a, b being Int-Location ex g being FinSeq-Location st i = b := (g,a) by SCMFSA_2:38; hence (Exec (i,s)) . f = s . f by SCMFSA_2:72; ::_thesis: verum end; suppose InsCode i = 10 ; ::_thesis: (Exec (i,s)) . f = s . f then consider a, b being Int-Location, g being FinSeq-Location such that A3: i = (g,a) := b by SCMFSA_2:39; UsedInt*Loc i = {g} by A3, Th33; then f <> g by A1, TARSKI:def_1; hence (Exec (i,s)) . f = s . f by A3, SCMFSA_2:73; ::_thesis: verum end; suppose InsCode i = 11 ; ::_thesis: (Exec (i,s)) . f = s . f then ex a being Int-Location ex g being FinSeq-Location st i = a :=len g by SCMFSA_2:40; hence (Exec (i,s)) . f = s . f by SCMFSA_2:74; ::_thesis: verum end; suppose InsCode i = 12 ; ::_thesis: (Exec (i,s)) . f = s . f then consider a being Int-Location, g being FinSeq-Location such that A4: i = g :=<0,...,0> a by SCMFSA_2:41; UsedInt*Loc i = {g} by A4, Th34; then f <> g by A1, TARSKI:def_1; hence (Exec (i,s)) . f = s . f by A4, SCMFSA_2:75; ::_thesis: verum end; end; end; theorem :: SF_MASTR:63 for f being FinSeq-Location for I being Program of for n being Element of NAT for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds (Comput (P,s,n)) . f = s . f proof let f be FinSeq-Location ; ::_thesis: for I being Program of for n being Element of NAT for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds (Comput (P,s,n)) . f = s . f let I be Program of ; ::_thesis: for n being Element of NAT for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds (Comput (P,s,n)) . f = s . f let n be Element of NAT ; ::_thesis: for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds (Comput (P,s,n)) . f = s . f let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds (Comput (P,s,n)) . f = s . f let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( I c= P & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I implies (Comput (P,s,n)) . f = s . f ) assume that A1: I c= P and A2: for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I and A3: not f in UsedInt*Loc I ; ::_thesis: (Comput (P,s,n)) . f = s . f defpred S1[ Nat] means ( $1 <= n implies (Comput (P,s,$1)) . f = s . f ); A4: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) set sm = Comput (P,s,m); assume A5: ( m <= n implies (Comput (P,s,m)) . f = s . f ) ; ::_thesis: S1[m + 1] assume A6: m + 1 <= n ; ::_thesis: (Comput (P,s,(m + 1))) . f = s . f then m < n by NAT_1:13; then A7: IC (Comput (P,s,m)) in dom I by A2; then A8: I . (IC (Comput (P,s,m))) in rng I by FUNCT_1:def_3; dom P = NAT by PARTFUN1:def_2; then A9: P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PARTFUN1:def_6; I . (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by A7, A1, GRFUNC_1:2; then UsedInt*Loc (P . (IC (Comput (P,s,m)))) c= UsedInt*Loc I by A8, Th35; then A10: not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) by A3; thus (Comput (P,s,(m + 1))) . f = (Following (P,(Comput (P,s,m)))) . f by EXTPRO_1:3 .= s . f by A5, A6, A10, Th62, A9, NAT_1:13 ; ::_thesis: verum end; A11: S1[ 0 ] ; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A11, A4); hence (Comput (P,s,n)) . f = s . f ; ::_thesis: verum end; theorem Th64: :: SF_MASTR:64 for i being Instruction of SCM+FSA for s, t being State of SCM+FSA st s | (UsedIntLoc i) = t | (UsedIntLoc i) & s | (UsedInt*Loc i) = t | (UsedInt*Loc i) & IC s = IC t holds ( 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 let i be Instruction of SCM+FSA; ::_thesis: for s, t being State of SCM+FSA st s | (UsedIntLoc i) = t | (UsedIntLoc i) & s | (UsedInt*Loc i) = t | (UsedInt*Loc i) & IC s = IC t holds ( 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) ) let s, t be State of SCM+FSA; ::_thesis: ( 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) ) ) assume that A1: s | (UsedIntLoc i) = t | (UsedIntLoc i) and A2: s | (UsedInt*Loc i) = t | (UsedInt*Loc i) and A3: IC s = IC t ; ::_thesis: ( 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) ) set UFi = UsedInt*Loc i; set Ui = UsedIntLoc i; set Et = Exec (i,t); set Es = Exec (i,s); A4: dom (Exec (i,s)) = the carrier of SCM+FSA by PARTFUN1:def_2 .= dom (Exec (i,t)) by PARTFUN1:def_2 ; A5: InsCode i <= 12 by SCMFSA_2:16; percases ( 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 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by A5, NAT_1:36; suppose InsCode i = 0 ; ::_thesis: ( 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) ) then A6: i = halt SCM+FSA by SCMFSA_2:95; then Exec (i,s) = s by EXTPRO_1:def_3; 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, A2, A3, A6, EXTPRO_1:def_3; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: ( 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) ) then consider a, b being Int-Location such that A7: i = a := b by SCMFSA_2:30; A8: UsedIntLoc i = {a,b} by A7, Th14; then A9: b in UsedIntLoc i by TARSKI:def_2; then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49; then A10: s . b = t . b by A1, A9, FUNCT_1:49; thus IC (Exec (i,s)) = succ (IC t) by A3, A7, SCMFSA_2:63 .= IC (Exec (i,t)) by A7, SCMFSA_2:63 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) ( a = b or a <> b ) ; then A11: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A7, SCMFSA_2:63; ( (Exec (i,s)) . a = s . b & (Exec (i,t)) . a = t . b ) by A7, SCMFSA_2:63; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A8, A10, A11, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A12: UsedInt*Loc i = {} by A7, Th32; hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A12, RELAT_1:81 ; ::_thesis: verum end; suppose InsCode i = 2 ; ::_thesis: ( 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) ) then consider a, b being Int-Location such that A13: i = AddTo (a,b) by SCMFSA_2:31; thus IC (Exec (i,s)) = succ (IC t) by A3, A13, SCMFSA_2:64 .= IC (Exec (i,t)) by A13, SCMFSA_2:64 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A14: UsedIntLoc i = {a,b} by A13, Th14; then A15: a in UsedIntLoc i by TARSKI:def_2; then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A16: s . a = t . a by A1, A15, FUNCT_1:49; A17: now__::_thesis:_(_(_a_=_b_&_(Exec_(i,s))_._b_=_(s_._a)_+_(s_._b)_&_(Exec_(i,t))_._b_=_(t_._a)_+_(t_._b)_)_or_(_a_<>_b_&_(Exec_(i,s))_._b_=_s_._b_&_(Exec_(i,t))_._b_=_t_._b_)_) percases ( a = b or a <> b ) ; case a = b ; ::_thesis: ( (Exec (i,s)) . b = (s . a) + (s . b) & (Exec (i,t)) . b = (t . a) + (t . b) ) hence ( (Exec (i,s)) . b = (s . a) + (s . b) & (Exec (i,t)) . b = (t . a) + (t . b) ) by A13, SCMFSA_2:64; ::_thesis: verum end; case a <> b ; ::_thesis: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) hence ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A13, SCMFSA_2:64; ::_thesis: verum end; end; end; A18: b in UsedIntLoc i by A14, TARSKI:def_2; then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49; then A19: s . b = t . b by A1, A18, FUNCT_1:49; ( (Exec (i,s)) . a = (s . a) + (s . b) & (Exec (i,t)) . a = (t . a) + (t . b) ) by A13, SCMFSA_2:64; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A14, A16, A19, A17, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A20: UsedInt*Loc i = {} by A13, Th32; hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A20, RELAT_1:81 ; ::_thesis: verum end; suppose InsCode i = 3 ; ::_thesis: ( 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) ) then consider a, b being Int-Location such that A21: i = SubFrom (a,b) by SCMFSA_2:32; thus IC (Exec (i,s)) = succ (IC t) by A3, A21, SCMFSA_2:65 .= IC (Exec (i,t)) by A21, SCMFSA_2:65 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A22: UsedIntLoc i = {a,b} by A21, Th14; then A23: a in UsedIntLoc i by TARSKI:def_2; then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A24: s . a = t . a by A1, A23, FUNCT_1:49; A25: now__::_thesis:_(_(_a_=_b_&_(Exec_(i,s))_._b_=_(s_._a)_-_(s_._b)_&_(Exec_(i,t))_._b_=_(t_._a)_-_(t_._b)_)_or_(_a_<>_b_&_(Exec_(i,s))_._b_=_s_._b_&_(Exec_(i,t))_._b_=_t_._b_)_) percases ( a = b or a <> b ) ; case a = b ; ::_thesis: ( (Exec (i,s)) . b = (s . a) - (s . b) & (Exec (i,t)) . b = (t . a) - (t . b) ) hence ( (Exec (i,s)) . b = (s . a) - (s . b) & (Exec (i,t)) . b = (t . a) - (t . b) ) by A21, SCMFSA_2:65; ::_thesis: verum end; case a <> b ; ::_thesis: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) hence ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A21, SCMFSA_2:65; ::_thesis: verum end; end; end; A26: b in UsedIntLoc i by A22, TARSKI:def_2; then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49; then A27: s . b = t . b by A1, A26, FUNCT_1:49; ( (Exec (i,s)) . a = (s . a) - (s . b) & (Exec (i,t)) . a = (t . a) - (t . b) ) by A21, SCMFSA_2:65; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A22, A24, A27, A25, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A28: UsedInt*Loc i = {} by A21, Th32; hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A28, RELAT_1:81 ; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: ( 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) ) then consider a, b being Int-Location such that A29: i = MultBy (a,b) by SCMFSA_2:33; thus IC (Exec (i,s)) = succ (IC t) by A3, A29, SCMFSA_2:66 .= IC (Exec (i,t)) by A29, SCMFSA_2:66 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A30: UsedIntLoc i = {a,b} by A29, Th14; then A31: a in UsedIntLoc i by TARSKI:def_2; then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A32: s . a = t . a by A1, A31, FUNCT_1:49; A33: now__::_thesis:_(_(_a_=_b_&_(Exec_(i,s))_._b_=_(s_._a)_*_(s_._b)_&_(Exec_(i,t))_._b_=_(t_._a)_*_(t_._b)_)_or_(_a_<>_b_&_(Exec_(i,s))_._b_=_s_._b_&_(Exec_(i,t))_._b_=_t_._b_)_) percases ( a = b or a <> b ) ; case a = b ; ::_thesis: ( (Exec (i,s)) . b = (s . a) * (s . b) & (Exec (i,t)) . b = (t . a) * (t . b) ) hence ( (Exec (i,s)) . b = (s . a) * (s . b) & (Exec (i,t)) . b = (t . a) * (t . b) ) by A29, SCMFSA_2:66; ::_thesis: verum end; case a <> b ; ::_thesis: ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) hence ( (Exec (i,s)) . b = s . b & (Exec (i,t)) . b = t . b ) by A29, SCMFSA_2:66; ::_thesis: verum end; end; end; A34: b in UsedIntLoc i by A30, TARSKI:def_2; then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49; then A35: s . b = t . b by A1, A34, FUNCT_1:49; ( (Exec (i,s)) . a = (s . a) * (s . b) & (Exec (i,t)) . a = (t . a) * (t . b) ) by A29, SCMFSA_2:66; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A30, A32, A35, A33, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A36: UsedInt*Loc i = {} by A29, Th32; hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A36, RELAT_1:81 ; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: ( 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) ) then consider a, b being Int-Location such that A37: i = Divide (a,b) by SCMFSA_2:34; A38: UsedIntLoc i = {a,b} by A37, Th14; then A39: a in UsedIntLoc i by TARSKI:def_2; then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A40: s . a = t . a by A1, A39, FUNCT_1:49; A41: UsedInt*Loc i = {} by A37, Th32; A42: b in UsedIntLoc i by A38, TARSKI:def_2; then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49; then A43: s . b = t . b by A1, A42, FUNCT_1:49; hereby ::_thesis: verum percases ( a = b or a <> b ) ; supposeA44: a = b ; ::_thesis: ( 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) ) hence IC (Exec (i,s)) = succ (IC t) by A3, A37, SCMFSA_2:68 .= IC (Exec (i,t)) by A37, A44, SCMFSA_2:68 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) ( (Exec (i,s)) . a = (s . a) mod (s . a) & (Exec (i,t)) . a = (t . a) mod (t . b) ) by A37, A44, SCMFSA_2:68; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A38, A40, A44, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A41, RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A41, RELAT_1:81 ; ::_thesis: verum end; supposeA45: a <> b ; ::_thesis: ( 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) ) thus IC (Exec (i,s)) = succ (IC t) by A3, A37, SCMFSA_2:67 .= IC (Exec (i,t)) by A37, SCMFSA_2:67 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A46: ( (Exec (i,s)) . b = (s . a) mod (s . b) & (Exec (i,t)) . b = (t . a) mod (t . b) ) by A37, SCMFSA_2:67; ( (Exec (i,s)) . a = (s . a) div (s . b) & (Exec (i,t)) . a = (t . a) div (t . b) ) by A37, A45, SCMFSA_2:67; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A38, A40, A43, A46, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) thus (Exec (i,s)) | (UsedInt*Loc i) = {} by A41, RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A41, RELAT_1:81 ; ::_thesis: verum end; end; end; end; suppose InsCode i = 6 ; ::_thesis: ( 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) ) then consider l being Element of NAT such that A47: i = goto l by SCMFSA_2:35; thus IC (Exec (i,s)) = l by A47, SCMFSA_2:69 .= IC (Exec (i,t)) by A47, SCMFSA_2:69 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A48: UsedIntLoc i = {} by A47, Th15; hence (Exec (i,s)) | (UsedIntLoc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedIntLoc i) by A48, RELAT_1:81 ; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A49: UsedInt*Loc i = {} by A47, Th32; hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A49, RELAT_1:81 ; ::_thesis: verum end; suppose InsCode i = 7 ; ::_thesis: ( 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) ) then consider l being Element of NAT , a being Int-Location such that A50: i = a =0_goto l by SCMFSA_2:36; A51: UsedIntLoc i = {a} by A50, Th16; then A52: a in UsedIntLoc i by TARSKI:def_1; then A53: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A54: s . a = t . a by A1, A52, FUNCT_1:49; hereby ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) percases ( s . a = 0 or s . a <> 0 ) ; supposeA55: s . a = 0 ; ::_thesis: IC (Exec (i,s)) = IC (Exec (i,t)) hence IC (Exec (i,s)) = l by A50, SCMFSA_2:70 .= IC (Exec (i,t)) by A50, A54, A55, SCMFSA_2:70 ; ::_thesis: verum end; supposeA56: s . a <> 0 ; ::_thesis: IC (Exec (i,s)) = IC (Exec (i,t)) hence IC (Exec (i,s)) = succ (IC s) by A50, SCMFSA_2:70 .= IC (Exec (i,t)) by A3, A50, A54, A56, SCMFSA_2:70 ; ::_thesis: verum end; end; end; ( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A50, SCMFSA_2:70; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A51, A52, A53, FUNCT_1:49, GRFUNC_1:29; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A57: UsedInt*Loc i = {} by A50, Th32; hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A57, RELAT_1:81 ; ::_thesis: verum end; suppose InsCode i = 8 ; ::_thesis: ( 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) ) then consider l being Element of NAT , a being Int-Location such that A58: i = a >0_goto l by SCMFSA_2:37; A59: UsedIntLoc i = {a} by A58, Th16; then A60: a in UsedIntLoc i by TARSKI:def_1; then A61: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A62: s . a = t . a by A1, A60, FUNCT_1:49; hereby ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) percases ( s . a > 0 or s . a <= 0 ) ; supposeA63: s . a > 0 ; ::_thesis: IC (Exec (i,s)) = IC (Exec (i,t)) hence IC (Exec (i,s)) = l by A58, SCMFSA_2:71 .= IC (Exec (i,t)) by A58, A62, A63, SCMFSA_2:71 ; ::_thesis: verum end; supposeA64: s . a <= 0 ; ::_thesis: IC (Exec (i,s)) = IC (Exec (i,t)) hence IC (Exec (i,s)) = succ (IC s) by A58, SCMFSA_2:71 .= IC (Exec (i,t)) by A3, A58, A62, A64, SCMFSA_2:71 ; ::_thesis: verum end; end; end; ( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A58, SCMFSA_2:71; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A59, A60, A61, FUNCT_1:49, GRFUNC_1:29; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A65: UsedInt*Loc i = {} by A58, Th32; hence (Exec (i,s)) | (UsedInt*Loc i) = {} by RELAT_1:81 .= (Exec (i,t)) | (UsedInt*Loc i) by A65, RELAT_1:81 ; ::_thesis: verum end; suppose InsCode i = 9 ; ::_thesis: ( 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) ) then consider a, b being Int-Location, f being FinSeq-Location such that A66: i = b := (f,a) by SCMFSA_2:38; A67: UsedIntLoc i = {a,b} by A66, Th17; then A68: a in UsedIntLoc i by TARSKI:def_2; then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A69: s . a = t . a by A1, A68, FUNCT_1:49; thus IC (Exec (i,s)) = succ (IC t) by A3, A66, SCMFSA_2:72 .= IC (Exec (i,t)) by A66, SCMFSA_2:72 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A70: UsedInt*Loc i = {f} by A66, Th33; then A71: f in UsedInt*Loc i by TARSKI:def_1; then A72: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49; A73: ( ex m being Element of NAT st ( m = abs (s . a) & (Exec (i,s)) . b = (s . f) /. m ) & ex n being Element of NAT st ( n = abs (t . a) & (Exec (i,t)) . b = (t . f) /. n ) ) by A66, SCMFSA_2:72; A74: now__::_thesis:_(_(_a_=_b_&_(Exec_(i,s))_._b_=_(Exec_(i,t))_._b_)_or_(_a_<>_b_&_(Exec_(i,s))_._a_=_s_._a_&_(Exec_(i,t))_._a_=_t_._a_)_) percases ( a = b or a <> b ) ; case a = b ; ::_thesis: (Exec (i,s)) . b = (Exec (i,t)) . b thus (Exec (i,s)) . b = (Exec (i,t)) . b by A2, A71, A72, A69, A73, FUNCT_1:49; ::_thesis: verum end; case a <> b ; ::_thesis: ( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) hence ( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A66, SCMFSA_2:72; ::_thesis: verum end; end; end; s . f = t . f by A2, A71, A72, FUNCT_1:49; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A67, A69, A73, A74, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ( (Exec (i,s)) . f = s . f & (Exec (i,t)) . f = t . f ) by A66, SCMFSA_2:72; hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A70, A71, A72, FUNCT_1:49, GRFUNC_1:29; ::_thesis: verum end; suppose InsCode i = 10 ; ::_thesis: ( 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) ) then consider a, b being Int-Location, f being FinSeq-Location such that A75: i = (f,a) := b by SCMFSA_2:39; thus IC (Exec (i,s)) = succ (IC t) by A3, A75, SCMFSA_2:73 .= IC (Exec (i,t)) by A75, SCMFSA_2:73 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A76: ( (Exec (i,t)) . a = t . a & (Exec (i,t)) . b = t . b ) by A75, SCMFSA_2:73; A77: UsedIntLoc i = {a,b} by A75, Th17; then A78: a in UsedIntLoc i by TARSKI:def_2; then s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; then A79: s . a = t . a by A1, A78, FUNCT_1:49; A80: b in UsedIntLoc i by A77, TARSKI:def_2; then s . b = (s | (UsedIntLoc i)) . b by FUNCT_1:49; then A81: s . b = t . b by A1, A80, FUNCT_1:49; A82: UsedInt*Loc i = {f} by A75, Th33; then A83: f in UsedInt*Loc i by TARSKI:def_1; then s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49; then A84: s . f = t . f by A2, A83, FUNCT_1:49; ( (Exec (i,s)) . a = s . a & (Exec (i,s)) . b = s . b ) by A75, SCMFSA_2:73; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A77, A79, A81, A76, GRFUNC_1:30; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ( ex m being Element of NAT st ( m = abs (s . a) & (Exec (i,s)) . f = (s . f) +* (m,(s . b)) ) & ex n being Element of NAT st ( n = abs (t . a) & (Exec (i,t)) . f = (t . f) +* (n,(t . b)) ) ) by A75, SCMFSA_2:73; hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A82, A79, A81, A84, GRFUNC_1:29; ::_thesis: verum end; suppose InsCode i = 11 ; ::_thesis: ( 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) ) then consider a being Int-Location, f being FinSeq-Location such that A85: i = a :=len f by SCMFSA_2:40; thus IC (Exec (i,s)) = succ (IC t) by A3, A85, SCMFSA_2:74 .= IC (Exec (i,t)) by A85, SCMFSA_2:74 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A86: (Exec (i,t)) . a = len (t . f) by A85, SCMFSA_2:74; A87: ( UsedIntLoc i = {a} & (Exec (i,s)) . a = len (s . f) ) by A85, Th18, SCMFSA_2:74; A88: UsedInt*Loc i = {f} by A85, Th34; then A89: f in UsedInt*Loc i by TARSKI:def_1; then A90: s . f = (s | (UsedInt*Loc i)) . f by FUNCT_1:49; then s . f = t . f by A2, A89, FUNCT_1:49; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A4, A87, A86, GRFUNC_1:29; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ( (Exec (i,s)) . f = s . f & (Exec (i,t)) . f = t . f ) by A85, SCMFSA_2:74; hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A2, A4, A88, A89, A90, FUNCT_1:49, GRFUNC_1:29; ::_thesis: verum end; suppose InsCode i = 12 ; ::_thesis: ( 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) ) then consider a being Int-Location, f being FinSeq-Location such that A91: i = f :=<0,...,0> a by SCMFSA_2:41; thus IC (Exec (i,s)) = succ (IC t) by A3, A91, SCMFSA_2:75 .= IC (Exec (i,t)) by A91, SCMFSA_2:75 ; ::_thesis: ( (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) ) A92: UsedIntLoc i = {a} by A91, Th18; then A93: a in UsedIntLoc i by TARSKI:def_1; then A94: s . a = (s | (UsedIntLoc i)) . a by FUNCT_1:49; A95: ( UsedInt*Loc i = {f} & ex m being Element of NAT st ( m = abs (s . a) & (Exec (i,s)) . f = m |-> 0 ) ) by A91, Th34, SCMFSA_2:75; ( (Exec (i,s)) . a = s . a & (Exec (i,t)) . a = t . a ) by A91, SCMFSA_2:75; hence (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) by A1, A4, A92, A93, A94, FUNCT_1:49, GRFUNC_1:29; ::_thesis: (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) A96: ex n being Element of NAT st ( n = abs (t . a) & (Exec (i,t)) . f = n |-> 0 ) by A91, SCMFSA_2:75; s . a = t . a by A1, A93, A94, FUNCT_1:49; hence (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) by A4, A95, A96, GRFUNC_1:29; ::_thesis: verum end; end; end; theorem :: SF_MASTR:65 for I being Program of for n being Element of NAT for s, t being State of SCM+FSA for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | (UsedIntLoc I) = t | (UsedIntLoc I) & s | (UsedInt*Loc I) = t | (UsedInt*Loc I) & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) holds ( ( for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ) & ( for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) proof let I be Program of ; ::_thesis: for n being Element of NAT for s, t being State of SCM+FSA for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | (UsedIntLoc I) = t | (UsedIntLoc I) & s | (UsedInt*Loc I) = t | (UsedInt*Loc I) & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) holds ( ( for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ) & ( for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) let n be Element of NAT ; ::_thesis: for s, t being State of SCM+FSA for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | (UsedIntLoc I) = t | (UsedIntLoc I) & s | (UsedInt*Loc I) = t | (UsedInt*Loc I) & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) holds ( ( for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ) & ( for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) let s, t be State of SCM+FSA; ::_thesis: for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | (UsedIntLoc I) = t | (UsedIntLoc I) & s | (UsedInt*Loc I) = t | (UsedInt*Loc I) & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) holds ( ( for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ) & ( for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) let P, Q be Instruction-Sequence of SCM+FSA; ::_thesis: ( I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | (UsedIntLoc I) = t | (UsedIntLoc I) & s | (UsedInt*Loc I) = t | (UsedInt*Loc I) & ( for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ) implies ( ( for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ) & ( for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) ) assume A1: ( I c= P & I c= Q ) ; ::_thesis: ( not Start-At (0,SCM+FSA) c= s or not Start-At (0,SCM+FSA) c= t or not s | (UsedIntLoc I) = t | (UsedIntLoc I) or not s | (UsedInt*Loc I) = t | (UsedInt*Loc I) or ex m being Element of NAT st ( m < n & not IC (Comput (P,s,m)) in dom I ) or ( ( for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ) & ( for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) ) assume that A2: Start-At (0,SCM+FSA) c= s and A3: Start-At (0,SCM+FSA) c= t and A4: s | (UsedIntLoc I) = t | (UsedIntLoc I) and A5: s | (UsedInt*Loc I) = t | (UsedInt*Loc I) and A6: for m being Element of NAT st m < n holds IC (Comput (P,s,m)) in dom I ; ::_thesis: ( ( for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ) & ( for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) defpred S1[ Nat] means ( $1 < n implies ( IC (Comput (Q,t,$1)) in dom I & IC (Comput (P,s,$1)) = IC (Comput (Q,t,$1)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,$1)) . a = (Comput (Q,t,$1)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,$1)) . f = (Comput (Q,t,$1)) . f ) ) ); A7: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_ S1[m_+_1] let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A8: S1[m] ; ::_thesis: S1[m + 1] thus S1[m + 1] ::_thesis: verum proof set i = P . (IC (Comput (P,s,m))); dom P = NAT by PARTFUN1:def_2; then A9: P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PARTFUN1:def_6; set m1 = m + 1; A10: Comput (P,s,(m + 1)) = Following (P,(Comput (P,s,m))) by EXTPRO_1:3 .= Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m))) by A9 ; assume A11: m + 1 < n ; ::_thesis: ( IC (Comput (Q,t,(m + 1))) in dom I & IC (Comput (P,s,(m + 1))) = IC (Comput (Q,t,(m + 1))) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,(m + 1))) . a = (Comput (Q,t,(m + 1))) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f ) ) now__::_thesis:_(_dom_((Comput_(P,s,m))_|_(UsedInt*Loc_I))_=_(dom_(Comput_(Q,t,m)))_/\_(UsedInt*Loc_I)_&_(_for_x_being_set_st_x_in_dom_((Comput_(P,s,m))_|_(UsedInt*Loc_I))_holds_ ((Comput_(P,s,m))_|_(UsedInt*Loc_I))_._x_=_(Comput_(Q,t,m))_._x_)_) thus dom ((Comput (P,s,m)) | (UsedInt*Loc I)) = (dom (Comput (P,s,m))) /\ (UsedInt*Loc I) by RELAT_1:61 .= the carrier of SCM+FSA /\ (UsedInt*Loc I) by PARTFUN1:def_2 .= (dom (Comput (Q,t,m))) /\ (UsedInt*Loc I) by PARTFUN1:def_2 ; ::_thesis: for x being set st x in dom ((Comput (P,s,m)) | (UsedInt*Loc I)) holds ((Comput (P,s,m)) | (UsedInt*Loc I)) . x = (Comput (Q,t,m)) . x let x be set ; ::_thesis: ( x in dom ((Comput (P,s,m)) | (UsedInt*Loc I)) implies ((Comput (P,s,m)) | (UsedInt*Loc I)) . x = (Comput (Q,t,m)) . x ) assume x in dom ((Comput (P,s,m)) | (UsedInt*Loc I)) ; ::_thesis: ((Comput (P,s,m)) | (UsedInt*Loc I)) . x = (Comput (Q,t,m)) . x then A12: x in UsedInt*Loc I by RELAT_1:57; then x in FinSeq-Locations ; then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def_5; thus ((Comput (P,s,m)) | (UsedInt*Loc I)) . x = (Comput (P,s,m)) . x9 by A12, FUNCT_1:49 .= (Comput (Q,t,m)) . x by A8, A11, A12, NAT_1:13 ; ::_thesis: verum end; then A13: (Comput (P,s,m)) | (UsedInt*Loc I) = (Comput (Q,t,m)) | (UsedInt*Loc I) by FUNCT_1:46; A14: P . (IC (Comput (P,s,m))) = I . (IC (Comput (P,s,m))) by A8, A11, A1, GRFUNC_1:2, NAT_1:13; then A15: P . (IC (Comput (P,s,m))) = Q . (IC (Comput (Q,t,m))) by A8, A11, A1, GRFUNC_1:2, NAT_1:13; now__::_thesis:_(_dom_((Comput_(P,s,m))_|_(UsedIntLoc_I))_=_(dom_(Comput_(Q,t,m)))_/\_(UsedIntLoc_I)_&_(_for_x_being_set_st_x_in_dom_((Comput_(P,s,m))_|_(UsedIntLoc_I))_holds_ ((Comput_(P,s,m))_|_(UsedIntLoc_I))_._x_=_(Comput_(Q,t,m))_._x_)_) thus dom ((Comput (P,s,m)) | (UsedIntLoc I)) = (dom (Comput (P,s,m))) /\ (UsedIntLoc I) by RELAT_1:61 .= the carrier of SCM+FSA /\ (UsedIntLoc I) by PARTFUN1:def_2 .= (dom (Comput (Q,t,m))) /\ (UsedIntLoc I) by PARTFUN1:def_2 ; ::_thesis: for x being set st x in dom ((Comput (P,s,m)) | (UsedIntLoc I)) holds ((Comput (P,s,m)) | (UsedIntLoc I)) . x = (Comput (Q,t,m)) . x let x be set ; ::_thesis: ( x in dom ((Comput (P,s,m)) | (UsedIntLoc I)) implies ((Comput (P,s,m)) | (UsedIntLoc I)) . x = (Comput (Q,t,m)) . x ) assume x in dom ((Comput (P,s,m)) | (UsedIntLoc I)) ; ::_thesis: ((Comput (P,s,m)) | (UsedIntLoc I)) . x = (Comput (Q,t,m)) . x then A16: x in UsedIntLoc I by RELAT_1:57; then x in Int-Locations ; then reconsider x9 = x as Int-Location by AMI_2:def_16; thus ((Comput (P,s,m)) | (UsedIntLoc I)) . x = (Comput (P,s,m)) . x9 by A16, FUNCT_1:49 .= (Comput (Q,t,m)) . x by A8, A11, A16, NAT_1:13 ; ::_thesis: verum end; then A17: (Comput (P,s,m)) | (UsedIntLoc I) = (Comput (Q,t,m)) | (UsedIntLoc I) by FUNCT_1:46; dom Q = NAT by PARTFUN1:def_2; then A18: Q /. (IC (Comput (Q,t,m))) = Q . (IC (Comput (Q,t,m))) by PARTFUN1:def_6; A19: Comput (Q,t,(m + 1)) = Following (Q,(Comput (Q,t,m))) by EXTPRO_1:3 .= Exec ((Q . (IC (Comput (Q,t,m)))),(Comput (Q,t,m))) by A18 ; m < n by A11, NAT_1:13; then IC (Comput (P,s,m)) in dom I by A6; then A20: P . (IC (Comput (P,s,m))) in rng I by A14, FUNCT_1:def_3; then A21: (Comput (P,s,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | (UsedInt*Loc I)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by Th35, RELAT_1:74 .= (Comput (Q,t,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by A20, A13, Th35, RELAT_1:74 ; A22: (Comput (P,s,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | (UsedIntLoc I)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A20, Th19, RELAT_1:74 .= (Comput (Q,t,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A20, A17, Th19, RELAT_1:74 ; then A23: (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) = (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by A8, A11, A21, Th64, NAT_1:13; A24: IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) = IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) by A8, A11, A22, A21, Th64, NAT_1:13; hence IC (Comput (Q,t,(m + 1))) in dom I by A6, A11, A10, A19, A15; ::_thesis: ( IC (Comput (P,s,(m + 1))) = IC (Comput (Q,t,(m + 1))) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,(m + 1))) . a = (Comput (Q,t,(m + 1))) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f ) ) thus IC (Comput (P,s,(m + 1))) = IC (Comput (Q,t,(m + 1))) by A8, A11, A10, A19, A14, A24, A1, GRFUNC_1:2, NAT_1:13; ::_thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,(m + 1))) . a = (Comput (Q,t,(m + 1))) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f ) ) A25: (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) = (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A8, A11, A22, A21, Th64, NAT_1:13; hereby ::_thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f let a be Int-Location; ::_thesis: ( a in UsedIntLoc I implies (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1 ) assume A26: a in UsedIntLoc I ; ::_thesis: (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1 percases ( a in UsedIntLoc (P . (IC (Comput (P,s,m)))) or not a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ) ; supposeA27: a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ; ::_thesis: (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1 hence (Comput (P,s,(m + 1))) . a = ((Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedIntLoc (P . (IC (Comput (P,s,m)))))) . a by A10, FUNCT_1:49 .= (Comput (Q,t,(m + 1))) . a by A19, A15, A25, A27, FUNCT_1:49 ; ::_thesis: verum end; supposeA28: not a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ; ::_thesis: (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1 hence (Comput (P,s,(m + 1))) . a = (Comput (P,s,m)) . a by A10, Th60 .= (Comput (Q,t,m)) . a by A8, A11, A26, NAT_1:13 .= (Comput (Q,t,(m + 1))) . a by A19, A15, A28, Th60 ; ::_thesis: verum end; end; end; let f be FinSeq-Location ; ::_thesis: ( f in UsedInt*Loc I implies (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f ) assume A29: f in UsedInt*Loc I ; ::_thesis: (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f percases ( f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) or not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ) ; supposeA30: f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ; ::_thesis: (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f hence (Comput (P,s,(m + 1))) . f = ((Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m)))))) . f by A10, FUNCT_1:49 .= (Comput (Q,t,(m + 1))) . f by A19, A15, A23, A30, FUNCT_1:49 ; ::_thesis: verum end; supposeA31: not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ; ::_thesis: (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f hence (Comput (P,s,(m + 1))) . f = (Comput (P,s,m)) . f by A10, Th62 .= (Comput (Q,t,m)) . f by A8, A11, A29, NAT_1:13 .= (Comput (Q,t,(m + 1))) . f by A19, A15, A31, Th62 ; ::_thesis: verum end; end; end; end; A32: S1[ 0 ] proof A33: IC (Comput (Q,t,0)) = IC t .= 0 by A3, MEMSTR_0:39 ; A34: IC (Comput (P,s,0)) = IC s .= 0 by A2, MEMSTR_0:39 ; assume 0 < n ; ::_thesis: ( IC (Comput (Q,t,0)) in dom I & IC (Comput (P,s,0)) = IC (Comput (Q,t,0)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,0)) . a = (Comput (Q,t,0)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f ) ) hence IC (Comput (Q,t,0)) in dom I by A6, A34, A33; ::_thesis: ( IC (Comput (P,s,0)) = IC (Comput (Q,t,0)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,0)) . a = (Comput (Q,t,0)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f ) ) thus IC (Comput (P,s,0)) = IC (Comput (Q,t,0)) by A34, A33; ::_thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,0)) . a = (Comput (Q,t,0)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f ) ) hereby ::_thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f let a be Int-Location; ::_thesis: ( a in UsedIntLoc I implies (Comput (P,s,0)) . a = (Comput (Q,t,0)) . a ) assume A35: a in UsedIntLoc I ; ::_thesis: (Comput (P,s,0)) . a = (Comput (Q,t,0)) . a thus (Comput (P,s,0)) . a = s . a .= (s | (UsedIntLoc I)) . a by A35, FUNCT_1:49 .= t . a by A4, A35, FUNCT_1:49 .= (Comput (Q,t,0)) . a ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: ( f in UsedInt*Loc I implies (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f ) assume A36: f in UsedInt*Loc I ; ::_thesis: (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f thus (Comput (P,s,0)) . f = s . f .= (s | (UsedInt*Loc I)) . f by A36, FUNCT_1:49 .= t . f by A5, A36, FUNCT_1:49 .= (Comput (Q,t,0)) . f ; ::_thesis: verum end; A37: for m being Element of NAT holds S1[m] from NAT_1:sch_1(A32, A7); hence for m being Element of NAT st m < n holds IC (Comput (Q,t,m)) in dom I ; ::_thesis: for m being Element of NAT st m <= n holds ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) let m be Element of NAT ; ::_thesis: ( m <= n implies ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) assume A38: m <= n ; ::_thesis: ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) percases ( m = 0 or ex p being Nat st m = p + 1 ) by NAT_1:6; supposeA39: m = 0 ; ::_thesis: ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) A40: IC (Comput (Q,t,0)) = IC t .= 0 by A3, MEMSTR_0:39 ; IC (Comput (P,s,0)) = IC s .= 0 by A2, MEMSTR_0:39 ; hence IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) by A39, A40; ::_thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) hereby ::_thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f let a be Int-Location; ::_thesis: ( a in UsedIntLoc I implies (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) assume A41: a in UsedIntLoc I ; ::_thesis: (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a thus (Comput (P,s,m)) . a = s . a by A39, EXTPRO_1:2 .= (s | (UsedIntLoc I)) . a by A41, FUNCT_1:49 .= t . a by A4, A41, FUNCT_1:49 .= (Comput (Q,t,m)) . a by A39, EXTPRO_1:2 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: ( f in UsedInt*Loc I implies (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) assume A42: f in UsedInt*Loc I ; ::_thesis: (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f thus (Comput (P,s,m)) . f = s . f by A39, EXTPRO_1:2 .= (s | (UsedInt*Loc I)) . f by A42, FUNCT_1:49 .= t . f by A5, A42, FUNCT_1:49 .= (Comput (Q,t,m)) . f by A39, EXTPRO_1:2 ; ::_thesis: verum end; suppose ex p being Nat st m = p + 1 ; ::_thesis: ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) then consider p being Nat such that A43: m = p + 1 ; reconsider p = p as Element of NAT by ORDINAL1:def_12; A44: p < n by A38, A43, NAT_1:13; then A45: IC (Comput (P,s,p)) in dom I by A6; now__::_thesis:_(_dom_((Comput_(P,s,p))_|_(UsedInt*Loc_I))_=_(dom_(Comput_(Q,t,p)))_/\_(UsedInt*Loc_I)_&_(_for_x_being_set_st_x_in_dom_((Comput_(P,s,p))_|_(UsedInt*Loc_I))_holds_ ((Comput_(P,s,p))_|_(UsedInt*Loc_I))_._x_=_(Comput_(Q,t,p))_._x_)_) thus dom ((Comput (P,s,p)) | (UsedInt*Loc I)) = (dom (Comput (P,s,p))) /\ (UsedInt*Loc I) by RELAT_1:61 .= the carrier of SCM+FSA /\ (UsedInt*Loc I) by PARTFUN1:def_2 .= (dom (Comput (Q,t,p))) /\ (UsedInt*Loc I) by PARTFUN1:def_2 ; ::_thesis: for x being set st x in dom ((Comput (P,s,p)) | (UsedInt*Loc I)) holds ((Comput (P,s,p)) | (UsedInt*Loc I)) . x = (Comput (Q,t,p)) . x let x be set ; ::_thesis: ( x in dom ((Comput (P,s,p)) | (UsedInt*Loc I)) implies ((Comput (P,s,p)) | (UsedInt*Loc I)) . x = (Comput (Q,t,p)) . x ) assume x in dom ((Comput (P,s,p)) | (UsedInt*Loc I)) ; ::_thesis: ((Comput (P,s,p)) | (UsedInt*Loc I)) . x = (Comput (Q,t,p)) . x then A46: x in UsedInt*Loc I by RELAT_1:57; then x in FinSeq-Locations ; then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def_5; thus ((Comput (P,s,p)) | (UsedInt*Loc I)) . x = (Comput (P,s,p)) . x9 by A46, FUNCT_1:49 .= (Comput (Q,t,p)) . x by A37, A44, A46 ; ::_thesis: verum end; then A47: (Comput (P,s,p)) | (UsedInt*Loc I) = (Comput (Q,t,p)) | (UsedInt*Loc I) by FUNCT_1:46; set i = P . (IC (Comput (P,s,p))); set p1 = p + 1; dom P = NAT by PARTFUN1:def_2; then A48: P /. (IC (Comput (P,s,p))) = P . (IC (Comput (P,s,p))) by PARTFUN1:def_6; A49: Comput (P,s,(p + 1)) = Following (P,(Comput (P,s,p))) by EXTPRO_1:3 .= Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p))) by A48 ; now__::_thesis:_(_dom_((Comput_(P,s,p))_|_(UsedIntLoc_I))_=_(dom_(Comput_(Q,t,p)))_/\_(UsedIntLoc_I)_&_(_for_x_being_set_st_x_in_dom_((Comput_(P,s,p))_|_(UsedIntLoc_I))_holds_ ((Comput_(P,s,p))_|_(UsedIntLoc_I))_._x_=_(Comput_(Q,t,p))_._x_)_) thus dom ((Comput (P,s,p)) | (UsedIntLoc I)) = (dom (Comput (P,s,p))) /\ (UsedIntLoc I) by RELAT_1:61 .= the carrier of SCM+FSA /\ (UsedIntLoc I) by PARTFUN1:def_2 .= (dom (Comput (Q,t,p))) /\ (UsedIntLoc I) by PARTFUN1:def_2 ; ::_thesis: for x being set st x in dom ((Comput (P,s,p)) | (UsedIntLoc I)) holds ((Comput (P,s,p)) | (UsedIntLoc I)) . x = (Comput (Q,t,p)) . x let x be set ; ::_thesis: ( x in dom ((Comput (P,s,p)) | (UsedIntLoc I)) implies ((Comput (P,s,p)) | (UsedIntLoc I)) . x = (Comput (Q,t,p)) . x ) assume x in dom ((Comput (P,s,p)) | (UsedIntLoc I)) ; ::_thesis: ((Comput (P,s,p)) | (UsedIntLoc I)) . x = (Comput (Q,t,p)) . x then A50: x in UsedIntLoc I by RELAT_1:57; then x in Int-Locations ; then reconsider x9 = x as Int-Location by AMI_2:def_16; thus ((Comput (P,s,p)) | (UsedIntLoc I)) . x = (Comput (P,s,p)) . x9 by A50, FUNCT_1:49 .= (Comput (Q,t,p)) . x by A37, A44, A50 ; ::_thesis: verum end; then A51: (Comput (P,s,p)) | (UsedIntLoc I) = (Comput (Q,t,p)) | (UsedIntLoc I) by FUNCT_1:46; A52: IC (Comput (P,s,p)) = IC (Comput (Q,t,p)) by A37, A44; A53: P . (IC (Comput (P,s,p))) = I . (IC (Comput (P,s,p))) by A45, A1, GRFUNC_1:2; dom Q = NAT by PARTFUN1:def_2; then A54: Q /. (IC (Comput (Q,t,p))) = Q . (IC (Comput (Q,t,p))) by PARTFUN1:def_6; A55: Comput (Q,t,(p + 1)) = Following (Q,(Comput (Q,t,p))) by EXTPRO_1:3 .= Exec ((Q . (IC (Comput (Q,t,p)))),(Comput (Q,t,p))) by A54 ; A56: P . (IC (Comput (P,s,p))) = Q . (IC (Comput (Q,t,p))) by A52, A45, A53, A1, GRFUNC_1:2; IC (Comput (P,s,p)) in dom I by A6, A44; then A57: P . (IC (Comput (P,s,p))) in rng I by A53, FUNCT_1:def_3; then A58: (Comput (P,s,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | (UsedInt*Loc I)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by Th35, RELAT_1:74 .= (Comput (Q,t,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by A57, A47, Th35, RELAT_1:74 ; A59: (Comput (P,s,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | (UsedIntLoc I)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A57, Th19, RELAT_1:74 .= (Comput (Q,t,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A57, A51, Th19, RELAT_1:74 ; hence IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) by A43, A49, A55, A52, A56, A58, Th64; ::_thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) A60: (Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) = (Exec ((P . (IC (Comput (P,s,p)))),(Comput (Q,t,p)))) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A52, A59, A58, Th64; hereby ::_thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f let a be Int-Location; ::_thesis: ( a in UsedIntLoc I implies (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 ) assume A61: a in UsedIntLoc I ; ::_thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 percases ( a in UsedIntLoc (P . (IC (Comput (P,s,p)))) or not a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ) ; supposeA62: a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ; ::_thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 hence (Comput (P,s,m)) . a = ((Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedIntLoc (P . (IC (Comput (P,s,p)))))) . a by A43, A49, FUNCT_1:49 .= (Comput (Q,t,m)) . a by A43, A55, A56, A60, A62, FUNCT_1:49 ; ::_thesis: verum end; supposeA63: not a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ; ::_thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 hence (Comput (P,s,m)) . a = (Comput (P,s,p)) . a by A43, A49, Th60 .= (Comput (Q,t,p)) . a by A37, A44, A61 .= (Comput (Q,t,m)) . a by A43, A55, A56, A63, Th60 ; ::_thesis: verum end; end; end; A64: (Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) = (Exec ((P . (IC (Comput (P,s,p)))),(Comput (Q,t,p)))) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by A52, A59, A58, Th64; hereby ::_thesis: verum let f be FinSeq-Location ; ::_thesis: ( f in UsedInt*Loc I implies (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 ) assume A65: f in UsedInt*Loc I ; ::_thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 percases ( f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) or not f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ) ; supposeA66: f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ; ::_thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 hence (Comput (P,s,m)) . f = ((Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedInt*Loc (P . (IC (Comput (P,s,p)))))) . f by A43, A49, FUNCT_1:49 .= (Comput (Q,t,m)) . f by A43, A55, A56, A64, A66, FUNCT_1:49 ; ::_thesis: verum end; supposeA67: not f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ; ::_thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 hence (Comput (P,s,m)) . f = (Comput (P,s,p)) . f by A43, A49, Th62 .= (Comput (Q,t,p)) . f by A37, A44, A65 .= (Comput (Q,t,m)) . f by A43, A55, A56, A67, Th62 ; ::_thesis: verum end; end; end; end; end; end;