:: 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;