:: SCMFSA_2 semantic presentation
begin
definition
func SCM+FSA -> strict AMI-Struct over 3 equals :: SCMFSA_2:def 1
AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);
coherence
AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #) is strict AMI-Struct over 3 ;
end;
:: deftheorem defines SCM+FSA SCMFSA_2:def_1_:_
SCM+FSA = AMI-Struct(# SCM+FSA-Memory,(In (NAT,SCM+FSA-Memory)),SCM+FSA-Instr,SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec #);
registration
cluster SCM+FSA -> non empty with_non-empty_values strict ;
coherence
( not SCM+FSA is empty & SCM+FSA is with_non-empty_values )
proof
thus not the carrier of SCM+FSA is empty ; :: according to STRUCT_0:def_1 ::_thesis: SCM+FSA is with_non-empty_values
thus the_Values_of SCM+FSA is non-empty ; :: according to MEMSTR_0:def_3 ::_thesis: verum
end;
end;
registration
cluster SCM+FSA -> strict with_non_trivial_Instructions ;
coherence
SCM+FSA is with_non_trivial_Instructions
proof
A: [0,{},{}] in SCM+FSA-Instr by SCMFSA_I:3;
[6,<*0*>,{}] in SCM-Instr by SCM_INST:2;
then B: [6,<*0*>,{}] in SCM+FSA-Instr by SCMFSA_I:1;
[0,{},{}] <> [6,<*0*>,{}] by XTUPLE_0:3;
hence not the InstructionsF of SCM+FSA is trivial by A, B, ZFMISC_1:def_10; :: according to AMISTD_4:def_1 ::_thesis: verum
end;
end;
theorem Th1: :: SCMFSA_2:1
IC = NAT by FUNCT_7:def_1, SCMFSA_1:5;
begin
notation
synonym Int-Locations for SCM+FSA-Data-Loc ;
end;
definition
:: original: Int-Locations
redefine func Int-Locations -> Subset of SCM+FSA;
coherence
Int-Locations is Subset of SCM+FSA
proof
Int-Locations = SCM+FSA-Data-Loc ;
hence Int-Locations is Subset of SCM+FSA ; ::_thesis: verum
end;
canceled;
func FinSeq-Locations -> Subset of SCM+FSA equals :: SCMFSA_2:def 3
SCM+FSA-Data*-Loc ;
coherence
SCM+FSA-Data*-Loc is Subset of SCM+FSA ;
end;
:: deftheorem SCMFSA_2:def_2_:_
canceled;
:: deftheorem defines FinSeq-Locations SCMFSA_2:def_3_:_
FinSeq-Locations = SCM+FSA-Data*-Loc ;
registration
cluster Int-like for Element of the carrier of SCM+FSA;
existence
ex b1 being Object of SCM+FSA st b1 is Int-like
proof
reconsider x = the Element of SCM+FSA-Data-Loc as Object of SCM+FSA ;
take x ; ::_thesis: x is Int-like
thus x is Int-like by AMI_2:def_16; ::_thesis: verum
end;
end;
definition
mode Int-Location is Int-like Object of SCM+FSA;
canceled;
mode FinSeq-Location -> Object of SCM+FSA means :Def5: :: SCMFSA_2:def 5
it in SCM+FSA-Data*-Loc ;
existence
ex b1 being Object of SCM+FSA st b1 in SCM+FSA-Data*-Loc
proof
set x = the Element of SCM+FSA-Data*-Loc ;
reconsider x = the Element of SCM+FSA-Data*-Loc as Object of SCM+FSA ;
take x ; ::_thesis: x in SCM+FSA-Data*-Loc
thus x in SCM+FSA-Data*-Loc ; ::_thesis: verum
end;
end;
:: deftheorem SCMFSA_2:def_4_:_
canceled;
:: deftheorem Def5 defines FinSeq-Location SCMFSA_2:def_5_:_
for b1 being Object of SCM+FSA holds
( b1 is FinSeq-Location iff b1 in SCM+FSA-Data*-Loc );
theorem :: SCMFSA_2:2
canceled;
theorem :: SCMFSA_2:3
canceled;
theorem :: SCMFSA_2:4
canceled;
theorem :: SCMFSA_2:5
canceled;
theorem :: SCMFSA_2:6
canceled;
definition
let k be Nat;
func intloc k -> Int-Location equals :: SCMFSA_2:def 6
dl. k;
coherence
dl. k is Int-Location
proof
A1: Int-Locations = SCM+FSA-Data-Loc ;
dl. k in SCM-Data-Loc by AMI_2:def_16;
hence dl. k is Int-Location by A1; ::_thesis: verum
end;
func fsloc k -> FinSeq-Location equals :: SCMFSA_2:def 7
- (k + 1);
coherence
- (k + 1) is FinSeq-Location
proof
reconsider k = k as Element of NAT by ORDINAL1:def_12;
- (k + 1) < - 0 by XREAL_1:24;
then ( - (k + 1) in INT & not - (k + 1) in NAT ) by INT_1:def_1;
then - (k + 1) in SCM+FSA-Data*-Loc by XBOOLE_0:def_5;
hence - (k + 1) is FinSeq-Location by Def5; ::_thesis: verum
end;
end;
:: deftheorem defines intloc SCMFSA_2:def_6_:_
for k being Nat holds intloc k = dl. k;
:: deftheorem defines fsloc SCMFSA_2:def_7_:_
for k being Nat holds fsloc k = - (k + 1);
theorem :: SCMFSA_2:7
for k1, k2 being Nat st k1 <> k2 holds
fsloc k1 <> fsloc k2 ;
theorem :: SCMFSA_2:8
for dl being Int-Location ex i being Element of NAT st dl = intloc i
proof
let dl be Int-Location; ::_thesis: ex i being Element of NAT st dl = intloc i
dl in SCM-Data-Loc by AMI_2:def_16;
then reconsider D = dl as Data-Location ;
consider i being Element of NAT such that
A1: D = dl. i by AMI_5:1;
take i ; ::_thesis: dl = intloc i
thus dl = intloc i by A1; ::_thesis: verum
end;
theorem Th9: :: SCMFSA_2:9
for fl being FinSeq-Location ex i being Element of NAT st fl = fsloc i
proof
let fl be FinSeq-Location ; ::_thesis: ex i being Element of NAT st fl = fsloc i
A1: fl in SCM+FSA-Data*-Loc by Def5;
then consider k being Element of NAT such that
A2: ( fl = k or fl = - k ) by INT_1:def_1;
k <> 0 by A1, A2, XBOOLE_0:def_5;
then consider i being Nat such that
A3: k = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
take i ; ::_thesis: fl = fsloc i
thus fl = fsloc i by A1, A2, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
registration
cluster FinSeq-Locations -> infinite ;
coherence
not FinSeq-Locations is finite
proof
deffunc H1( Element of NAT ) -> FinSeq-Location = fsloc c1;
consider f being Function of NAT, the carrier of SCM+FSA such that
A1: for k being Element of NAT holds f . k = H1(k) from FUNCT_2:sch_4();
NAT , FinSeq-Locations are_equipotent
proof
take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = NAT & proj2 f = FinSeq-Locations )
thus f is one-to-one ::_thesis: ( proj1 f = NAT & proj2 f = FinSeq-Locations )
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider k1 = x1, k2 = x2 as Element of NAT by A2;
fsloc k1 = f . k1 by A1
.= fsloc k2 by A1, A3 ;
hence x1 = x2 ; ::_thesis: verum
end;
thus dom f = NAT by FUNCT_2:def_1; ::_thesis: proj2 f = FinSeq-Locations
thus rng f c= FinSeq-Locations :: according to XBOOLE_0:def_10 ::_thesis: FinSeq-Locations c= proj2 f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in FinSeq-Locations )
assume y in rng f ; ::_thesis: y in FinSeq-Locations
then consider x being set such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A4;
y = fsloc x by A1, A5;
hence y in FinSeq-Locations by Def5; ::_thesis: verum
end;
thus FinSeq-Locations c= rng f ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in FinSeq-Locations or y in rng f )
assume y in FinSeq-Locations ; ::_thesis: y in rng f
then y is FinSeq-Location by Def5;
then consider i being Element of NAT such that
A6: y = fsloc i by Th9;
i in NAT ;
then A7: i in dom f by FUNCT_2:def_1;
y = f . i by A1, A6;
hence y in rng f by A7, FUNCT_1:def_3; ::_thesis: verum
end;
end;
hence not FinSeq-Locations is finite by CARD_1:38; ::_thesis: verum
end;
end;
theorem Th10: :: SCMFSA_2:10
for I being Int-Location holds I is Data-Location
proof
let I be Int-Location; ::_thesis: I is Data-Location
I in SCM-Data-Loc by AMI_2:def_16;
hence I is Data-Location ; ::_thesis: verum
end;
theorem Th11: :: SCMFSA_2:11
for l being Int-Location holds Values l = INT
proof
let l be Int-Location; ::_thesis: Values l = INT
l in SCM-Data-Loc by AMI_2:def_16;
hence Values l = INT by SCMFSA_1:10; ::_thesis: verum
end;
theorem Th12: :: SCMFSA_2:12
for l being FinSeq-Location holds Values l = INT *
proof
let l be FinSeq-Location ; ::_thesis: Values l = INT *
l in SCM+FSA-Data*-Loc by Def5;
hence Values l = INT * by SCMFSA_1:11; ::_thesis: verum
end;
begin
theorem :: SCMFSA_2:13
canceled;
theorem :: SCMFSA_2:14
canceled;
theorem Th15: :: SCMFSA_2:15
for I being Instruction of SCM+FSA st InsCode I <= 8 holds
I is Instruction of SCM
proof
let I be Instruction of SCM+FSA; ::_thesis: ( InsCode I <= 8 implies I is Instruction of SCM )
assume A1: InsCode I <= 8 ; ::_thesis: I is Instruction of SCM
now__::_thesis:_not_I_in__{__[K,{},<*dC,fB*>]_where_K_is_Element_of_Segm_13,_dC_is_Element_of_SCM+FSA-Data-Loc_,_fB_is_Element_of_SCM+FSA-Data*-Loc_:_K_in_{11,12}__}_
assume I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; ::_thesis: contradiction
then consider K being Element of Segm 13, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A2: I = [K,{},<*dC,fB*>] and
A3: K in {11,12} ;
A4: I `1_3 = K by A2, RECDEF_2:def_1;
( K = 12 or K = 11 ) by A3, TARSKI:def_2;
hence contradiction by A1, A4; ::_thesis: verum
end;
then A5: I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } by XBOOLE_0:def_3;
now__::_thesis:_not_I_in__{__[L,{},<*dB,fA,dA*>]_where_L_is_Element_of_Segm_13,_dB,_dA_is_Element_of_SCM+FSA-Data-Loc_,_fA_is_Element_of_SCM+FSA-Data*-Loc_:_L_in_{9,10}__}_
assume I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; ::_thesis: contradiction
then consider L being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A6: I = [L,{},<*dB,fA,dA*>] and
A7: L in {9,10} ;
A8: I `1_3 = L by A6, RECDEF_2:def_1;
( L = 9 or L = 10 ) by A7, TARSKI:def_2;
hence contradiction by A1, A8; ::_thesis: verum
end;
hence I is Instruction of SCM by A5, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th16: :: SCMFSA_2:16
for I being Instruction of SCM+FSA holds InsCode I <= 12
proof
let I be Instruction of SCM+FSA; ::_thesis: InsCode I <= 12
A1: ( I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def_3;
percases ( I in SCM-Instr or I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by A1, XBOOLE_0:def_3;
suppose I in SCM-Instr ; ::_thesis: InsCode I <= 12
then reconsider i = I as Instruction of SCM ;
InsCode i <= 8 by AMI_5:5;
hence InsCode I <= 12 by XXREAL_0:2; ::_thesis: verum
end;
suppose I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; ::_thesis: InsCode I <= 12
then consider L being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A2: I = [L,{},<*dB,fA,dA*>] and
A3: L in {9,10} ;
A4: I `1_3 = L by A2, RECDEF_2:def_1;
( L = 9 or L = 10 ) by A3, TARSKI:def_2;
hence InsCode I <= 12 by A4; ::_thesis: verum
end;
suppose I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; ::_thesis: InsCode I <= 12
then consider K being Element of Segm 13, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A5: I = [K,{},<*dC,fB*>] and
A6: K in {11,12} ;
A7: I `1_3 = K by A5, RECDEF_2:def_1;
( K = 11 or K = 12 ) by A6, TARSKI:def_2;
hence InsCode I <= 12 by A7; ::_thesis: verum
end;
end;
end;
theorem Th17: :: SCMFSA_2:17
for I being Instruction of SCM holds I is Instruction of SCM+FSA
proof
let I be Instruction of SCM; ::_thesis: I is Instruction of SCM+FSA
I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } by XBOOLE_0:def_3;
hence I is Instruction of SCM+FSA by XBOOLE_0:def_3; ::_thesis: verum
end;
definition
let a, b be Int-Location;
funca := b -> Instruction of SCM+FSA means :Def8: :: SCMFSA_2:def 8
ex A, B being Data-Location st
( a = A & b = B & it = A := B );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = A := B )
proof
reconsider A = a, B = b as Data-Location by Th10;
reconsider i = A := B as Instruction of SCM+FSA by Th17;
take i ; ::_thesis: ex A, B being Data-Location st
( a = A & b = B & i = A := B )
take A ; ::_thesis: ex B being Data-Location st
( a = A & b = B & i = A := B )
take B ; ::_thesis: ( a = A & b = B & i = A := B )
thus ( a = A & b = B & i = A := B ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = A := B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = A := B ) holds
b1 = b2;
;
func AddTo (a,b) -> Instruction of SCM+FSA means :Def9: :: SCMFSA_2:def 9
ex A, B being Data-Location st
( a = A & b = B & it = AddTo (A,B) );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo (A,B) )
proof
reconsider A = a, B = b as Data-Location by Th10;
reconsider i = AddTo (A,B) as Instruction of SCM+FSA by Th17;
take i ; ::_thesis: ex A, B being Data-Location st
( a = A & b = B & i = AddTo (A,B) )
take A ; ::_thesis: ex B being Data-Location st
( a = A & b = B & i = AddTo (A,B) )
take B ; ::_thesis: ( a = A & b = B & i = AddTo (A,B) )
thus ( a = A & b = B & i = AddTo (A,B) ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = AddTo (A,B) ) holds
b1 = b2;
;
func SubFrom (a,b) -> Instruction of SCM+FSA means :Def10: :: SCMFSA_2:def 10
ex A, B being Data-Location st
( a = A & b = B & it = SubFrom (A,B) );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom (A,B) )
proof
reconsider A = a, B = b as Data-Location by Th10;
reconsider i = SubFrom (A,B) as Instruction of SCM+FSA by Th17;
take i ; ::_thesis: ex A, B being Data-Location st
( a = A & b = B & i = SubFrom (A,B) )
take A ; ::_thesis: ex B being Data-Location st
( a = A & b = B & i = SubFrom (A,B) )
take B ; ::_thesis: ( a = A & b = B & i = SubFrom (A,B) )
thus ( a = A & b = B & i = SubFrom (A,B) ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = SubFrom (A,B) ) holds
b1 = b2;
;
func MultBy (a,b) -> Instruction of SCM+FSA means :Def11: :: SCMFSA_2:def 11
ex A, B being Data-Location st
( a = A & b = B & it = MultBy (A,B) );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy (A,B) )
proof
reconsider A = a, B = b as Data-Location by Th10;
reconsider i = MultBy (A,B) as Instruction of SCM+FSA by Th17;
take i ; ::_thesis: ex A, B being Data-Location st
( a = A & b = B & i = MultBy (A,B) )
take A ; ::_thesis: ex B being Data-Location st
( a = A & b = B & i = MultBy (A,B) )
take B ; ::_thesis: ( a = A & b = B & i = MultBy (A,B) )
thus ( a = A & b = B & i = MultBy (A,B) ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = MultBy (A,B) ) holds
b1 = b2;
;
func Divide (a,b) -> Instruction of SCM+FSA means :Def12: :: SCMFSA_2:def 12
ex A, B being Data-Location st
( a = A & b = B & it = Divide (A,B) );
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = Divide (A,B) )
proof
reconsider A = a, B = b as Data-Location by Th10;
reconsider i = Divide (A,B) as Instruction of SCM+FSA by Th17;
take i ; ::_thesis: ex A, B being Data-Location st
( a = A & b = B & i = Divide (A,B) )
take A ; ::_thesis: ex B being Data-Location st
( a = A & b = B & i = Divide (A,B) )
take B ; ::_thesis: ( a = A & b = B & i = Divide (A,B) )
thus ( a = A & b = B & i = Divide (A,B) ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = Divide (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = Divide (A,B) ) holds
b1 = b2;
;
end;
:: deftheorem Def8 defines := SCMFSA_2:def_8_:_
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = a := b iff ex A, B being Data-Location st
( a = A & b = B & b3 = A := B ) );
:: deftheorem Def9 defines AddTo SCMFSA_2:def_9_:_
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = AddTo (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b3 = AddTo (A,B) ) );
:: deftheorem Def10 defines SubFrom SCMFSA_2:def_10_:_
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = SubFrom (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b3 = SubFrom (A,B) ) );
:: deftheorem Def11 defines MultBy SCMFSA_2:def_11_:_
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = MultBy (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b3 = MultBy (A,B) ) );
:: deftheorem Def12 defines Divide SCMFSA_2:def_12_:_
for a, b being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = Divide (a,b) iff ex A, B being Data-Location st
( a = A & b = B & b3 = Divide (A,B) ) );
definition
let la be Element of NAT ;
func goto la -> Instruction of SCM+FSA equals :: SCMFSA_2:def 13
SCM-goto la;
coherence
SCM-goto la is Instruction of SCM+FSA by Th17;
let a be Int-Location;
funca =0_goto la -> Instruction of SCM+FSA means :Def14: :: SCMFSA_2:def 14
ex A being Data-Location st
( a = A & it = A =0_goto la );
existence
ex b1 being Instruction of SCM+FSA ex A being Data-Location st
( a = A & b1 = A =0_goto la )
proof
reconsider A = a as Data-Location by Th10;
reconsider i = A =0_goto la as Instruction of SCM+FSA by Th17;
take i ; ::_thesis: ex A being Data-Location st
( a = A & i = A =0_goto la )
take A ; ::_thesis: ( a = A & i = A =0_goto la )
thus ( a = A & i = A =0_goto la ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A being Data-Location st
( a = A & b1 = A =0_goto la ) & ex A being Data-Location st
( a = A & b2 = A =0_goto la ) holds
b1 = b2;
;
funca >0_goto la -> Instruction of SCM+FSA means :Def15: :: SCMFSA_2:def 15
ex A being Data-Location st
( a = A & it = A >0_goto la );
existence
ex b1 being Instruction of SCM+FSA ex A being Data-Location st
( a = A & b1 = A >0_goto la )
proof
reconsider A = a as Data-Location by Th10;
reconsider i = A >0_goto la as Instruction of SCM+FSA by Th17;
take i ; ::_thesis: ex A being Data-Location st
( a = A & i = A >0_goto la )
take A ; ::_thesis: ( a = A & i = A >0_goto la )
thus ( a = A & i = A >0_goto la ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A being Data-Location st
( a = A & b1 = A >0_goto la ) & ex A being Data-Location st
( a = A & b2 = A >0_goto la ) holds
b1 = b2;
;
end;
:: deftheorem defines goto SCMFSA_2:def_13_:_
for la being Element of NAT holds goto la = SCM-goto la;
:: deftheorem Def14 defines =0_goto SCMFSA_2:def_14_:_
for la being Element of NAT
for a being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = a =0_goto la iff ex A being Data-Location st
( a = A & b3 = A =0_goto la ) );
:: deftheorem Def15 defines >0_goto SCMFSA_2:def_15_:_
for la being Element of NAT
for a being Int-Location
for b3 being Instruction of SCM+FSA holds
( b3 = a >0_goto la iff ex A being Data-Location st
( a = A & b3 = A >0_goto la ) );
definition
let c, i be Int-Location;
let a be FinSeq-Location ;
funcc := (a,i) -> Instruction of SCM+FSA equals :: SCMFSA_2:def 16
[9,{},<*c,a,i*>];
coherence
[9,{},<*c,a,i*>] is Instruction of SCM+FSA
proof
reconsider A = a as Element of SCM+FSA-Data*-Loc by Def5;
reconsider C = c, I = i as Element of SCM-Data-Loc by AMI_2:def_16;
9 in {9,10} by TARSKI:def_2;
then [9,{},<*C,A,I*>] in SCM+FSA-Instr by SCMFSA_I:4;
hence [9,{},<*c,a,i*>] is Instruction of SCM+FSA ; ::_thesis: verum
end;
func(a,i) := c -> Instruction of SCM+FSA equals :: SCMFSA_2:def 17
[10,{},<*c,a,i*>];
coherence
[10,{},<*c,a,i*>] is Instruction of SCM+FSA
proof
reconsider A = a as Element of SCM+FSA-Data*-Loc by Def5;
reconsider C = c, I = i as Element of SCM-Data-Loc by AMI_2:def_16;
10 in {9,10} by TARSKI:def_2;
then [10,{},<*C,A,I*>] in SCM+FSA-Instr by SCMFSA_I:4;
hence [10,{},<*c,a,i*>] is Instruction of SCM+FSA ; ::_thesis: verum
end;
end;
:: deftheorem defines := SCMFSA_2:def_16_:_
for c, i being Int-Location
for a being FinSeq-Location holds c := (a,i) = [9,{},<*c,a,i*>];
:: deftheorem defines := SCMFSA_2:def_17_:_
for c, i being Int-Location
for a being FinSeq-Location holds (a,i) := c = [10,{},<*c,a,i*>];
definition
let i be Int-Location;
let a be FinSeq-Location ;
funci :=len a -> Instruction of SCM+FSA equals :: SCMFSA_2:def 18
[11,{},<*i,a*>];
coherence
[11,{},<*i,a*>] is Instruction of SCM+FSA
proof
reconsider A = a as Element of SCM+FSA-Data*-Loc by Def5;
reconsider I = i as Element of SCM-Data-Loc by AMI_2:def_16;
11 in {11,12} by TARSKI:def_2;
then [11,{},<*I,A*>] in SCM+FSA-Instr by SCMFSA_I:5;
hence [11,{},<*i,a*>] is Instruction of SCM+FSA ; ::_thesis: verum
end;
funca :=<0,...,0> i -> Instruction of SCM+FSA equals :: SCMFSA_2:def 19
[12,{},<*i,a*>];
coherence
[12,{},<*i,a*>] is Instruction of SCM+FSA
proof
reconsider A = a as Element of SCM+FSA-Data*-Loc by Def5;
reconsider I = i as Element of SCM-Data-Loc by AMI_2:def_16;
12 in {11,12} by TARSKI:def_2;
then [12,{},<*I,A*>] in SCM+FSA-Instr by SCMFSA_I:5;
hence [12,{},<*i,a*>] is Instruction of SCM+FSA ; ::_thesis: verum
end;
end;
:: deftheorem defines :=len SCMFSA_2:def_18_:_
for i being Int-Location
for a being FinSeq-Location holds i :=len a = [11,{},<*i,a*>];
:: deftheorem defines :=<0,...,0> SCMFSA_2:def_19_:_
for i being Int-Location
for a being FinSeq-Location holds a :=<0,...,0> i = [12,{},<*i,a*>];
theorem :: SCMFSA_2:18
for a, b being Int-Location holds InsCode (a := b) = 1
proof
let a, b be Int-Location; ::_thesis: InsCode (a := b) = 1
ex A, B being Data-Location st
( a = A & b = B & a := b = A := B ) by Def8;
hence InsCode (a := b) = 1 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_2:19
for a, b being Int-Location holds InsCode (AddTo (a,b)) = 2
proof
let a, b be Int-Location; ::_thesis: InsCode (AddTo (a,b)) = 2
ex A, B being Data-Location st
( a = A & b = B & AddTo (a,b) = AddTo (A,B) ) by Def9;
hence InsCode (AddTo (a,b)) = 2 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_2:20
for a, b being Int-Location holds InsCode (SubFrom (a,b)) = 3
proof
let a, b be Int-Location; ::_thesis: InsCode (SubFrom (a,b)) = 3
ex A, B being Data-Location st
( a = A & b = B & SubFrom (a,b) = SubFrom (A,B) ) by Def10;
hence InsCode (SubFrom (a,b)) = 3 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_2:21
for a, b being Int-Location holds InsCode (MultBy (a,b)) = 4
proof
let a, b be Int-Location; ::_thesis: InsCode (MultBy (a,b)) = 4
ex A, B being Data-Location st
( a = A & b = B & MultBy (a,b) = MultBy (A,B) ) by Def11;
hence InsCode (MultBy (a,b)) = 4 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_2:22
for a, b being Int-Location holds InsCode (Divide (a,b)) = 5
proof
let a, b be Int-Location; ::_thesis: InsCode (Divide (a,b)) = 5
ex A, B being Data-Location st
( a = A & b = B & Divide (a,b) = Divide (A,B) ) by Def12;
hence InsCode (Divide (a,b)) = 5 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_2:23
for lb being Element of NAT holds InsCode (goto lb) = 6 by RECDEF_2:def_1;
theorem :: SCMFSA_2:24
for lb being Element of NAT
for a being Int-Location holds InsCode (a =0_goto lb) = 7
proof
let lb be Element of NAT ; ::_thesis: for a being Int-Location holds InsCode (a =0_goto lb) = 7
let a be Int-Location; ::_thesis: InsCode (a =0_goto lb) = 7
ex A being Data-Location st
( a = A & a =0_goto lb = A =0_goto lb ) by Def14;
hence InsCode (a =0_goto lb) = 7 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_2:25
for lb being Element of NAT
for a being Int-Location holds InsCode (a >0_goto lb) = 8
proof
let lb be Element of NAT ; ::_thesis: for a being Int-Location holds InsCode (a >0_goto lb) = 8
let a be Int-Location; ::_thesis: InsCode (a >0_goto lb) = 8
ex A being Data-Location st
( a = A & a >0_goto lb = A >0_goto lb ) by Def15;
hence InsCode (a >0_goto lb) = 8 by RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: SCMFSA_2:26
for fa being FinSeq-Location
for c, a being Int-Location holds InsCode (c := (fa,a)) = 9 by RECDEF_2:def_1;
theorem :: SCMFSA_2:27
for fa being FinSeq-Location
for a, c being Int-Location holds InsCode ((fa,a) := c) = 10 by RECDEF_2:def_1;
theorem :: SCMFSA_2:28
for fa being FinSeq-Location
for a being Int-Location holds InsCode (a :=len fa) = 11 by RECDEF_2:def_1;
theorem :: SCMFSA_2:29
for fa being FinSeq-Location
for a being Int-Location holds InsCode (fa :=<0,...,0> a) = 12 by RECDEF_2:def_1;
theorem Th30: :: SCMFSA_2:30
for ins being Instruction of SCM+FSA st InsCode ins = 1 holds
ex da, db being Int-Location st ins = da := db
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 1 implies ex da, db being Int-Location st ins = da := db )
assume A1: InsCode ins = 1 ; ::_thesis: ex da, db being Int-Location st ins = da := db
then reconsider I = ins as Instruction of SCM by Th15;
consider A, B being Data-Location such that
A2: I = A := B by A1, AMI_5:8;
A3: Int-Locations = SCM+FSA-Data-Loc ;
( A in SCM-Data-Loc & B in SCM-Data-Loc ) by AMI_2:def_16;
then reconsider da = A, db = B as Int-Location by A3;
take da ; ::_thesis: ex db being Int-Location st ins = da := db
take db ; ::_thesis: ins = da := db
thus ins = da := db by A2, Def8; ::_thesis: verum
end;
theorem Th31: :: SCMFSA_2:31
for ins being Instruction of SCM+FSA st InsCode ins = 2 holds
ex da, db being Int-Location st ins = AddTo (da,db)
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 2 implies ex da, db being Int-Location st ins = AddTo (da,db) )
assume A1: InsCode ins = 2 ; ::_thesis: ex da, db being Int-Location st ins = AddTo (da,db)
then reconsider I = ins as Instruction of SCM by Th15;
consider A, B being Data-Location such that
A2: I = AddTo (A,B) by A1, AMI_5:9;
A3: Int-Locations = SCM+FSA-Data-Loc ;
( A in SCM-Data-Loc & B in SCM-Data-Loc ) by AMI_2:def_16;
then reconsider da = A, db = B as Int-Location by A3;
take da ; ::_thesis: ex db being Int-Location st ins = AddTo (da,db)
take db ; ::_thesis: ins = AddTo (da,db)
thus ins = AddTo (da,db) by A2, Def9; ::_thesis: verum
end;
theorem Th32: :: SCMFSA_2:32
for ins being Instruction of SCM+FSA st InsCode ins = 3 holds
ex da, db being Int-Location st ins = SubFrom (da,db)
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 3 implies ex da, db being Int-Location st ins = SubFrom (da,db) )
assume A1: InsCode ins = 3 ; ::_thesis: ex da, db being Int-Location st ins = SubFrom (da,db)
then reconsider I = ins as Instruction of SCM by Th15;
consider A, B being Data-Location such that
A2: I = SubFrom (A,B) by A1, AMI_5:10;
A3: Int-Locations = SCM+FSA-Data-Loc ;
( A in SCM-Data-Loc & B in SCM-Data-Loc ) by AMI_2:def_16;
then reconsider da = A, db = B as Int-Location by A3;
take da ; ::_thesis: ex db being Int-Location st ins = SubFrom (da,db)
take db ; ::_thesis: ins = SubFrom (da,db)
thus ins = SubFrom (da,db) by A2, Def10; ::_thesis: verum
end;
theorem Th33: :: SCMFSA_2:33
for ins being Instruction of SCM+FSA st InsCode ins = 4 holds
ex da, db being Int-Location st ins = MultBy (da,db)
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 4 implies ex da, db being Int-Location st ins = MultBy (da,db) )
assume A1: InsCode ins = 4 ; ::_thesis: ex da, db being Int-Location st ins = MultBy (da,db)
then reconsider I = ins as Instruction of SCM by Th15;
consider A, B being Data-Location such that
A2: I = MultBy (A,B) by A1, AMI_5:11;
A3: Int-Locations = SCM+FSA-Data-Loc ;
( A in SCM-Data-Loc & B in SCM-Data-Loc ) by AMI_2:def_16;
then reconsider da = A, db = B as Int-Location by A3;
take da ; ::_thesis: ex db being Int-Location st ins = MultBy (da,db)
take db ; ::_thesis: ins = MultBy (da,db)
thus ins = MultBy (da,db) by A2, Def11; ::_thesis: verum
end;
theorem Th34: :: SCMFSA_2:34
for ins being Instruction of SCM+FSA st InsCode ins = 5 holds
ex da, db being Int-Location st ins = Divide (da,db)
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 5 implies ex da, db being Int-Location st ins = Divide (da,db) )
assume A1: InsCode ins = 5 ; ::_thesis: ex da, db being Int-Location st ins = Divide (da,db)
then reconsider I = ins as Instruction of SCM by Th15;
consider A, B being Data-Location such that
A2: I = Divide (A,B) by A1, AMI_5:12;
A3: Int-Locations = SCM+FSA-Data-Loc ;
( A in SCM-Data-Loc & B in SCM-Data-Loc ) by AMI_2:def_16;
then reconsider da = A, db = B as Int-Location by A3;
take da ; ::_thesis: ex db being Int-Location st ins = Divide (da,db)
take db ; ::_thesis: ins = Divide (da,db)
thus ins = Divide (da,db) by A2, Def12; ::_thesis: verum
end;
theorem Th35: :: SCMFSA_2:35
for ins being Instruction of SCM+FSA st InsCode ins = 6 holds
ex lb being Element of NAT st ins = goto lb
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 6 implies ex lb being Element of NAT st ins = goto lb )
assume A1: InsCode ins = 6 ; ::_thesis: ex lb being Element of NAT st ins = goto lb
then reconsider I = ins as Instruction of SCM by Th15;
consider La being Element of NAT such that
A2: I = SCM-goto La by A1, AMI_5:13;
reconsider loc = La as Element of NAT ;
take loc ; ::_thesis: ins = goto loc
thus ins = goto loc by A2; ::_thesis: verum
end;
theorem Th36: :: SCMFSA_2:36
for ins being Instruction of SCM+FSA st InsCode ins = 7 holds
ex lb being Element of NAT ex da being Int-Location st ins = da =0_goto lb
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 7 implies ex lb being Element of NAT ex da being Int-Location st ins = da =0_goto lb )
assume A1: InsCode ins = 7 ; ::_thesis: ex lb being Element of NAT ex da being Int-Location st ins = da =0_goto lb
then reconsider I = ins as Instruction of SCM by Th15;
consider La being Element of NAT , A being Data-Location such that
A2: I = A =0_goto La by A1, AMI_5:14;
A3: Int-Locations = SCM+FSA-Data-Loc ;
A in SCM-Data-Loc by AMI_2:def_16;
then reconsider da = A as Int-Location by A3;
reconsider loc = La as Element of NAT ;
take loc ; ::_thesis: ex da being Int-Location st ins = da =0_goto loc
take da ; ::_thesis: ins = da =0_goto loc
thus ins = da =0_goto loc by A2, Def14; ::_thesis: verum
end;
theorem Th37: :: SCMFSA_2:37
for ins being Instruction of SCM+FSA st InsCode ins = 8 holds
ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 8 implies ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb )
assume A1: InsCode ins = 8 ; ::_thesis: ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb
then reconsider I = ins as Instruction of SCM by Th15;
consider La being Element of NAT , A being Data-Location such that
A2: I = A >0_goto La by A1, AMI_5:15;
A3: Int-Locations = SCM+FSA-Data-Loc ;
A in SCM-Data-Loc by AMI_2:def_16;
then reconsider da = A as Int-Location by A3;
reconsider loc = La as Element of NAT ;
take loc ; ::_thesis: ex da being Int-Location st ins = da >0_goto loc
take da ; ::_thesis: ins = da >0_goto loc
thus ins = da >0_goto loc by A2, Def15; ::_thesis: verum
end;
theorem Th38: :: SCMFSA_2:38
for ins being Instruction of SCM+FSA st InsCode ins = 9 holds
ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a)
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 9 implies ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a) )
assume A1: InsCode ins = 9 ; ::_thesis: ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a)
A2: now__::_thesis:_not_ins_in__{__[K,{},<*dC,fB*>]_where_K_is_Element_of_Segm_13,_dC_is_Element_of_SCM+FSA-Data-Loc_,_fB_is_Element_of_SCM+FSA-Data*-Loc_:_K_in_{11,12}__}_
assume ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; ::_thesis: contradiction
then consider K being Element of Segm 13, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A3: ins = [K,{},<*dC,fB*>] and
A4: K in {11,12} ;
( K = 11 or K = 12 ) by A4, TARSKI:def_2;
hence contradiction by A1, A3, RECDEF_2:def_1; ::_thesis: verum
end;
( ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def_3;
then ( ins in SCM-Instr or ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ) by A2, XBOOLE_0:def_3;
then consider L being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A5: ins = [L,{},<*dB,fA,dA*>] and
L in {9,10} by A1, AMI_5:5;
reconsider f = fA as FinSeq-Location by Def5;
reconsider c = dB, b = dA as Int-Location by AMI_2:def_16;
take b ; ::_thesis: ex b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,b)
take c ; ::_thesis: ex fa being FinSeq-Location st ins = c := (fa,b)
take f ; ::_thesis: ins = c := (f,b)
thus ins = c := (f,b) by A1, A5, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th39: :: SCMFSA_2:39
for ins being Instruction of SCM+FSA st InsCode ins = 10 holds
ex a, b being Int-Location ex fa being FinSeq-Location st ins = (fa,a) := b
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 10 implies ex a, b being Int-Location ex fa being FinSeq-Location st ins = (fa,a) := b )
assume A1: InsCode ins = 10 ; ::_thesis: ex a, b being Int-Location ex fa being FinSeq-Location st ins = (fa,a) := b
A2: now__::_thesis:_not_ins_in__{__[K,{},<*dC,fB*>]_where_K_is_Element_of_Segm_13,_dC_is_Element_of_SCM+FSA-Data-Loc_,_fB_is_Element_of_SCM+FSA-Data*-Loc_:_K_in_{11,12}__}_
assume ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; ::_thesis: contradiction
then consider K being Element of Segm 13, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A3: ins = [K,{},<*dC,fB*>] and
A4: K in {11,12} ;
( K = 11 or K = 12 ) by A4, TARSKI:def_2;
hence contradiction by A1, A3, RECDEF_2:def_1; ::_thesis: verum
end;
( ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def_3;
then ( ins in SCM-Instr or ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ) by A2, XBOOLE_0:def_3;
then consider L being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A5: ins = [L,{},<*dB,fA,dA*>] and
L in {9,10} by A1, AMI_5:5;
reconsider f = fA as FinSeq-Location by Def5;
reconsider c = dB, b = dA as Int-Location by AMI_2:def_16;
take b ; ::_thesis: ex b being Int-Location ex fa being FinSeq-Location st ins = (fa,b) := b
take c ; ::_thesis: ex fa being FinSeq-Location st ins = (fa,b) := c
take f ; ::_thesis: ins = (f,b) := c
thus ins = (f,b) := c by A1, A5, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th40: :: SCMFSA_2:40
for ins being Instruction of SCM+FSA st InsCode ins = 11 holds
ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 11 implies ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa )
assume A1: InsCode ins = 11 ; ::_thesis: ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa
A2: now__::_thesis:_not_ins_in__{__[L,{},<*dB,fA,dA*>]_where_L_is_Element_of_Segm_13,_dB,_dA_is_Element_of_SCM+FSA-Data-Loc_,_fA_is_Element_of_SCM+FSA-Data*-Loc_:_L_in_{9,10}__}_
assume ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; ::_thesis: contradiction
then consider K being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A3: ins = [K,{},<*dB,fA,dA*>] and
A4: K in {9,10} ;
ins `1_3 = K by A3, RECDEF_2:def_1;
hence contradiction by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
A5: ( ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def_3;
not ins in SCM-Instr by A1, AMI_5:5;
then consider K being Element of Segm 13, dB being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A6: ins = [K,{},<*dB,fA*>] and
K in {11,12} by A5, A2, XBOOLE_0:def_3;
reconsider f = fA as FinSeq-Location by Def5;
reconsider c = dB as Int-Location by AMI_2:def_16;
take c ; ::_thesis: ex fa being FinSeq-Location st ins = c :=len fa
take f ; ::_thesis: ins = c :=len f
thus ins = c :=len f by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
theorem Th41: :: SCMFSA_2:41
for ins being Instruction of SCM+FSA st InsCode ins = 12 holds
ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a
proof
let ins be Instruction of SCM+FSA; ::_thesis: ( InsCode ins = 12 implies ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a )
assume A1: InsCode ins = 12 ; ::_thesis: ex a being Int-Location ex fa being FinSeq-Location st ins = fa :=<0,...,0> a
A2: now__::_thesis:_not_ins_in__{__[L,{},<*dB,fA,dA*>]_where_L_is_Element_of_Segm_13,_dB,_dA_is_Element_of_SCM+FSA-Data-Loc_,_fA_is_Element_of_SCM+FSA-Data*-Loc_:_L_in_{9,10}__}_
assume ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; ::_thesis: contradiction
then consider K being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A3: ins = [K,{},<*dB,fA,dA*>] and
A4: K in {9,10} ;
ins `1_3 = K by A3, RECDEF_2:def_1;
hence contradiction by A1, A4, TARSKI:def_2; ::_thesis: verum
end;
A5: ( ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or ins in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def_3;
not ins in SCM-Instr by A1, AMI_5:5;
then consider K being Element of Segm 13, dB being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A6: ins = [K,{},<*dB,fA*>] and
K in {11,12} by A5, A2, XBOOLE_0:def_3;
reconsider f = fA as FinSeq-Location by Def5;
reconsider c = dB as Int-Location by AMI_2:def_16;
take c ; ::_thesis: ex fa being FinSeq-Location st ins = fa :=<0,...,0> c
take f ; ::_thesis: ins = f :=<0,...,0> c
thus ins = f :=<0,...,0> c by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
begin
theorem :: SCMFSA_2:42
for s being State of SCM+FSA
for d being Int-Location holds d in dom s
proof
let s be State of SCM+FSA; ::_thesis: for d being Int-Location holds d in dom s
let d be Int-Location; ::_thesis: d in dom s
dom s = the carrier of SCM+FSA by PARTFUN1:def_2;
hence d in dom s ; ::_thesis: verum
end;
theorem :: SCMFSA_2:43
for f being FinSeq-Location
for s being State of SCM+FSA holds f in dom s
proof
let f be FinSeq-Location ; ::_thesis: for s being State of SCM+FSA holds f in dom s
let s be State of SCM+FSA; ::_thesis: f in dom s
dom s = SCM+FSA-Memory by PARTFUN1:def_2;
hence f in dom s ; ::_thesis: verum
end;
theorem Th44: :: SCMFSA_2:44
for f being FinSeq-Location
for S being State of SCM holds not f in dom S
proof
let f be FinSeq-Location ; ::_thesis: for S being State of SCM holds not f in dom S
let S be State of SCM; ::_thesis: not f in dom S
f in SCM+FSA-Data*-Loc by Def5;
hence not f in dom S by SCMFSA_1:30, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th45: :: SCMFSA_2:45
for s being State of SCM+FSA holds Int-Locations c= dom s
proof
let s be State of SCM+FSA; ::_thesis: Int-Locations c= dom s
dom s = the carrier of SCM+FSA by PARTFUN1:def_2;
hence Int-Locations c= dom s ; ::_thesis: verum
end;
theorem Th46: :: SCMFSA_2:46
for s being State of SCM+FSA holds FinSeq-Locations c= dom s
proof
let s be State of SCM+FSA; ::_thesis: FinSeq-Locations c= dom s
dom s = the carrier of SCM+FSA by PARTFUN1:def_2;
hence FinSeq-Locations c= dom s ; ::_thesis: verum
end;
theorem :: SCMFSA_2:47
for s being State of SCM+FSA holds dom (s | Int-Locations) = Int-Locations
proof
let s be State of SCM+FSA; ::_thesis: dom (s | Int-Locations) = Int-Locations
Int-Locations c= dom s by Th45;
hence dom (s | Int-Locations) = Int-Locations by RELAT_1:62; ::_thesis: verum
end;
theorem :: SCMFSA_2:48
for s being State of SCM+FSA holds dom (s | FinSeq-Locations) = FinSeq-Locations
proof
let s be State of SCM+FSA; ::_thesis: dom (s | FinSeq-Locations) = FinSeq-Locations
FinSeq-Locations c= dom s by Th46;
hence dom (s | FinSeq-Locations) = FinSeq-Locations by RELAT_1:62; ::_thesis: verum
end;
theorem Th49: :: SCMFSA_2:49
for s being State of SCM+FSA
for i being Instruction of SCM holds s | SCM-Memory is State of SCM
proof
let s be State of SCM+FSA; ::_thesis: for i being Instruction of SCM holds s | SCM-Memory is State of SCM
let i be Instruction of SCM; ::_thesis: s | SCM-Memory is State of SCM
reconsider s = s as SCM+FSA-State by CARD_3:107;
s | SCM-Memory is SCM-State by SCMFSA_1:17;
then s | SCM-Memory is State of SCM by AMI_3:29;
hence s | SCM-Memory is State of SCM ; ::_thesis: verum
end;
theorem :: SCMFSA_2:50
for s being State of SCM+FSA
for s9 being State of SCM holds s +* s9 is State of SCM+FSA
proof
let s be State of SCM+FSA; ::_thesis: for s9 being State of SCM holds s +* s9 is State of SCM+FSA
let s9 be State of SCM; ::_thesis: s +* s9 is State of SCM+FSA
reconsider s = s as SCM+FSA-State by CARD_3:107;
reconsider s9 = s9 as SCM-State by CARD_3:107;
s +* s9 is SCM+FSA-State by SCMFSA_1:18;
then s +* s9 is State of SCM+FSA ;
hence s +* s9 is State of SCM+FSA ; ::_thesis: verum
end;
theorem Th51: :: SCMFSA_2:51
for i being Instruction of SCM
for ii being Instruction of SCM+FSA
for s being State of SCM
for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds
Exec (ii,ss) = ss +* (Exec (i,s))
proof
let i be Instruction of SCM; ::_thesis: for ii being Instruction of SCM+FSA
for s being State of SCM
for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds
Exec (ii,ss) = ss +* (Exec (i,s))
let ii be Instruction of SCM+FSA; ::_thesis: for s being State of SCM
for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds
Exec (ii,ss) = ss +* (Exec (i,s))
let s be State of SCM; ::_thesis: for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds
Exec (ii,ss) = ss +* (Exec (i,s))
let ss be State of SCM+FSA; ::_thesis: ( i = ii & s = ss | SCM-Memory implies Exec (ii,ss) = ss +* (Exec (i,s)) )
assume that
A1: i = ii and
A2: s = ss | SCM-Memory ; ::_thesis: Exec (ii,ss) = ss +* (Exec (i,s))
reconsider SS = ss as SCM+FSA-State by CARD_3:107;
reconsider II = ii as Element of SCM+FSA-Instr ;
InsCode II <= 8 by A1, AMI_5:5;
then consider I being Element of SCM-Instr , S being SCM-State such that
A3: ( I = II & S = SS | SCM-Memory ) and
A4: SCM+FSA-Exec-Res (II,SS) = SS +* (SCM-Exec-Res (I,S)) by SCMFSA_1:def_16;
Exec (i,s) = SCM-Exec-Res (I,S) by A1, A2, A3, AMI_2:def_15;
hence Exec (ii,ss) = ss +* (Exec (i,s)) by A4, SCMFSA_1:def_17; ::_thesis: verum
end;
registration
let s be State of SCM+FSA;
let d be Int-Location;
clusters . d -> integer ;
coherence
s . d is integer
proof
reconsider D = d as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider S = s as SCM+FSA-State by CARD_3:107;
S . D = s . d ;
hence s . d is integer ; ::_thesis: verum
end;
end;
definition
let s be State of SCM+FSA;
let d be FinSeq-Location ;
:: original: .
redefine funcs . d -> FinSequence of INT ;
coherence
s . d is FinSequence of INT
proof
reconsider D = d as Element of SCM+FSA-Data*-Loc by Def5;
reconsider S = s as SCM+FSA-State by CARD_3:107;
S . D = s . d ;
hence s . d is FinSequence of INT ; ::_thesis: verum
end;
end;
theorem Th52: :: SCMFSA_2:52
for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory holds
s = s +* S by FUNCT_4:75;
theorem Th53: :: SCMFSA_2:53
for S being State of SCM
for s1, s being State of SCM+FSA st s1 = s +* S holds
s1 . (IC ) = S . (IC )
proof
let S be State of SCM; ::_thesis: for s1, s being State of SCM+FSA st s1 = s +* S holds
s1 . (IC ) = S . (IC )
let s1, s be State of SCM+FSA; ::_thesis: ( s1 = s +* S implies s1 . (IC ) = S . (IC ) )
A1: dom S = SCM-Memory by PARTFUN1:def_2;
assume s1 = s +* S ; ::_thesis: s1 . (IC ) = S . (IC )
hence s1 . (IC ) = S . (IC ) by A1, Th1, AMI_3:1, FUNCT_4:13; ::_thesis: verum
end;
theorem Th54: :: SCMFSA_2:54
for A being Data-Location
for a being Int-Location
for S being State of SCM
for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
proof
let A be Data-Location; ::_thesis: for a being Int-Location
for S being State of SCM
for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let a be Int-Location; ::_thesis: for S being State of SCM
for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let S be State of SCM; ::_thesis: for s1, s being State of SCM+FSA st s1 = s +* S & A = a holds
S . A = s1 . a
let s1, s be State of SCM+FSA; ::_thesis: ( s1 = s +* S & A = a implies S . A = s1 . a )
assume that
A1: s1 = s +* S and
A2: A = a ; ::_thesis: S . A = s1 . a
dom S = SCM-Memory by PARTFUN1:def_2;
hence s1 . a = S . A by A1, A2, FUNCT_4:13; ::_thesis: verum
end;
theorem Th55: :: SCMFSA_2:55
for A being Data-Location
for a being Int-Location
for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a
proof
let A be Data-Location; ::_thesis: for a being Int-Location
for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a
let a be Int-Location; ::_thesis: for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a
let S be State of SCM; ::_thesis: for s being State of SCM+FSA st S = s | SCM-Memory & A = a holds
S . A = s . a
let s be State of SCM+FSA; ::_thesis: ( S = s | SCM-Memory & A = a implies S . A = s . a )
assume S = s | SCM-Memory ; ::_thesis: ( not A = a or S . A = s . a )
then s = s +* S by Th52;
hence ( not A = a or S . A = s . a ) by Th54; ::_thesis: verum
end;
registration
cluster SCM+FSA -> IC-Ins-separated strict ;
coherence
SCM+FSA is IC-Ins-separated
proof
Values (IC ) = NAT by FUNCT_7:def_1, SCMFSA_1:5, SCMFSA_1:9;
hence SCM+FSA is IC-Ins-separated by MEMSTR_0:def_6; ::_thesis: verum
end;
end;
theorem Th56: :: SCMFSA_2:56
for dl being Int-Location holds dl <> IC
proof
let dl be Int-Location; ::_thesis: dl <> IC
dl in [:{1},NAT:] by AMI_2:def_16;
hence dl <> IC by Th1, FINSET_1:15; ::_thesis: verum
end;
theorem Th57: :: SCMFSA_2:57
for dl being FinSeq-Location holds dl <> IC
proof
let dl be FinSeq-Location ; ::_thesis: dl <> IC
now__::_thesis:_not_NAT_in_INT_\_NAT
assume NAT in INT \ NAT ; ::_thesis: contradiction
then A1: NAT in NAT \/ [:{0},NAT:] by NUMBERS:def_4, XBOOLE_0:def_5;
percases ( NAT in NAT or NAT in [:{0},NAT:] ) by A1, XBOOLE_0:def_3;
suppose NAT in NAT ; ::_thesis: contradiction
hence contradiction ; ::_thesis: verum
end;
suppose NAT in [:{0},NAT:] ; ::_thesis: contradiction
hence contradiction by FINSET_1:15; ::_thesis: verum
end;
end;
end;
hence dl <> IC by Def5, Th1; ::_thesis: verum
end;
theorem :: SCMFSA_2:58
for il being Int-Location
for dl being FinSeq-Location holds il <> dl
proof
let il be Int-Location; ::_thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; ::_thesis: il <> dl
Values dl = INT * by Th12;
hence il <> dl by Th11, FUNCT_7:16; ::_thesis: verum
end;
theorem :: SCMFSA_2:59
for il being Element of NAT
for dl being Int-Location holds il <> dl
proof
let il be Element of NAT ; ::_thesis: for dl being Int-Location holds il <> dl
let dl be Int-Location; ::_thesis: il <> dl
dl in [:{1},NAT:] by AMI_2:def_16;
then ex x, y being set st
( x in {1} & y in NAT & dl = [x,y] ) by ZFMISC_1:84;
hence il <> dl ; ::_thesis: verum
end;
theorem :: SCMFSA_2:60
for il being Element of NAT
for dl being FinSeq-Location holds il <> dl
proof
let il be Element of NAT ; ::_thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; ::_thesis: il <> dl
A1: dl in INT \ NAT by Def5;
NAT misses INT \ NAT by XBOOLE_1:79;
hence il <> dl by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: SCMFSA_2:61
for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
s1 = s2
proof
let s1, s2 be State of SCM+FSA; ::_thesis: ( IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int-Location holds s1 . a = s2 . a and
A3: for f being FinSeq-Location holds s1 . f = s2 . f ; ::_thesis: s1 = s2
s1 in product (SCM*-VAL * SCM+FSA-OK) by CARD_3:107;
then consider g1 being Function such that
A4: s1 = g1 and
A5: dom g1 = dom (SCM*-VAL * SCM+FSA-OK) and
for x being set st x in dom (SCM*-VAL * SCM+FSA-OK) holds
g1 . x in (SCM*-VAL * SCM+FSA-OK) . x by CARD_3:def_5;
s2 in product (SCM*-VAL * SCM+FSA-OK) by CARD_3:107;
then consider g2 being Function such that
A6: s2 = g2 and
A7: dom g2 = dom (SCM*-VAL * SCM+FSA-OK) and
for x being set st x in dom (SCM*-VAL * SCM+FSA-OK) holds
g2 . x in (SCM*-VAL * SCM+FSA-OK) . x by CARD_3:def_5;
A8: now__::_thesis:_for_x_being_set_st_x_in_SCM+FSA-Memory_holds_
g1_._x_=_g2_._x
let x be set ; ::_thesis: ( x in SCM+FSA-Memory implies g1 . b1 = g2 . b1 )
assume x in SCM+FSA-Memory ; ::_thesis: g1 . b1 = g2 . b1
then x in ({(IC )} \/ SCM-Data-Loc) \/ SCM+FSA-Data*-Loc by Th1;
then A9: ( x in {(IC )} \/ SCM-Data-Loc or x in SCM+FSA-Data*-Loc ) by XBOOLE_0:def_3;
A10: Int-Locations = SCM+FSA-Data-Loc ;
percases ( x in {(IC )} or x in SCM-Data-Loc or x in SCM+FSA-Data*-Loc ) by A9, XBOOLE_0:def_3;
suppose x in {(IC )} ; ::_thesis: g1 . b1 = g2 . b1
then x = IC by TARSKI:def_1;
hence g1 . x = g2 . x by A1, A4, A6; ::_thesis: verum
end;
suppose x in SCM-Data-Loc ; ::_thesis: g1 . b1 = g2 . b1
then x is Int-Location by A10, AMI_2:def_16;
hence g1 . x = g2 . x by A2, A4, A6; ::_thesis: verum
end;
suppose x in SCM+FSA-Data*-Loc ; ::_thesis: g1 . b1 = g2 . b1
then x is FinSeq-Location by Def5;
hence g1 . x = g2 . x by A3, A4, A6; ::_thesis: verum
end;
end;
end;
SCM+FSA-Memory = dom g1 by A5, SCMFSA_1:32;
hence s1 = s2 by A4, A5, A6, A7, A8, FUNCT_1:2; ::_thesis: verum
end;
theorem Th62: :: SCMFSA_2:62
for S being State of SCM
for s being State of SCM+FSA st S = s | SCM-Memory holds
IC s = IC S
proof
let S be State of SCM; ::_thesis: for s being State of SCM+FSA st S = s | SCM-Memory holds
IC s = IC S
let s be State of SCM+FSA; ::_thesis: ( S = s | SCM-Memory implies IC s = IC S )
assume S = s | SCM-Memory ; ::_thesis: IC s = IC S
then s = s +* S by Th52;
hence IC s = IC S by Th53; ::_thesis: verum
end;
begin
theorem Th63: :: SCMFSA_2:63
for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
proof
let a, b be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((a := b),s)) . (IC ) = succ (IC s) & (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: b = B and
A3: a := b = A := B by Def8;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A4: Exec ((a := b),s) = s +* (Exec ((A := B),S)) by A3, Th51;
hence (Exec ((a := b),s)) . (IC ) = (Exec ((A := B),S)) . (IC ) by Th53
.= succ (IC S) by AMI_3:2
.= succ (IC s) by Th62 ;
::_thesis: ( (Exec ((a := b),s)) . a = s . b & ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
thus (Exec ((a := b),s)) . a = (Exec ((A := B),S)) . A by A1, A4, Th54
.= S . B by AMI_3:2
.= s . b by A2, Th55 ; ::_thesis: ( ( for c being Int-Location st c <> a holds
(Exec ((a := b),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((a := b),s)) . f = s . f
let c be Int-Location; ::_thesis: ( c <> a implies (Exec ((a := b),s)) . c = s . c )
assume A5: c <> a ; ::_thesis: (Exec ((a := b),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((a := b),s)) . c = (Exec ((A := B),S)) . C by A4, Th54
.= S . C by A1, A5, AMI_3:2
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((a := b),s)) . f = s . f
A6: not f in dom (Exec ((A := B),S)) by Th44;
thus (Exec ((a := b),s)) . f = s . f by A4, A6, FUNCT_4:11; ::_thesis: verum
end;
theorem Th64: :: SCMFSA_2:64
for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) )
proof
let a, b be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: b = B and
A3: AddTo (a,b) = AddTo (A,B) by Def9;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A4: Exec ((AddTo (a,b)),s) = s +* (Exec ((AddTo (A,B)),S)) by A3, Th51;
hence (Exec ((AddTo (a,b)),s)) . (IC ) = (Exec ((AddTo (A,B)),S)) . (IC ) by Th53
.= succ (IC S) by AMI_3:3
.= succ (IC s) by Th62 ;
::_thesis: ( (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) )
thus (Exec ((AddTo (a,b)),s)) . a = (Exec ((AddTo (A,B)),S)) . A by A1, A4, Th54
.= (S . A) + (S . B) by AMI_3:3
.= (S . A) + (s . b) by A2, Th55
.= (s . a) + (s . b) by A1, Th55 ; ::_thesis: ( ( for c being Int-Location st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((AddTo (a,b)),s)) . f = s . f
let c be Int-Location; ::_thesis: ( c <> a implies (Exec ((AddTo (a,b)),s)) . c = s . c )
assume A5: c <> a ; ::_thesis: (Exec ((AddTo (a,b)),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((AddTo (a,b)),s)) . c = (Exec ((AddTo (A,B)),S)) . C by A4, Th54
.= S . C by A1, A5, AMI_3:3
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((AddTo (a,b)),s)) . f = s . f
A6: not f in dom (Exec ((AddTo (A,B)),S)) by Th44;
thus (Exec ((AddTo (a,b)),s)) . f = s . f by A4, A6, FUNCT_4:11; ::_thesis: verum
end;
theorem Th65: :: SCMFSA_2:65
for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
proof
let a, b be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: b = B and
A3: SubFrom (a,b) = SubFrom (A,B) by Def10;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A4: Exec ((SubFrom (a,b)),s) = s +* (Exec ((SubFrom (A,B)),S)) by A3, Th51;
hence (Exec ((SubFrom (a,b)),s)) . (IC ) = (Exec ((SubFrom (A,B)),S)) . (IC ) by Th53
.= succ (IC S) by AMI_3:4
.= succ (IC s) by Th62 ;
::_thesis: ( (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
thus (Exec ((SubFrom (a,b)),s)) . a = (Exec ((SubFrom (A,B)),S)) . A by A1, A4, Th54
.= (S . A) - (S . B) by AMI_3:4
.= (S . A) - (s . b) by A2, Th55
.= (s . a) - (s . b) by A1, Th55 ; ::_thesis: ( ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f
let c be Int-Location; ::_thesis: ( c <> a implies (Exec ((SubFrom (a,b)),s)) . c = s . c )
assume A5: c <> a ; ::_thesis: (Exec ((SubFrom (a,b)),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((SubFrom (a,b)),s)) . c = (Exec ((SubFrom (A,B)),S)) . C by A4, Th54
.= S . C by A1, A5, AMI_3:4
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((SubFrom (a,b)),s)) . f = s . f
A6: not f in dom (Exec ((SubFrom (A,B)),S)) by Th44;
thus (Exec ((SubFrom (a,b)),s)) . f = s . f by A4, A6, FUNCT_4:11; ::_thesis: verum
end;
theorem Th66: :: SCMFSA_2:66
for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) )
proof
let a, b be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) & (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: b = B and
A3: MultBy (a,b) = MultBy (A,B) by Def11;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A4: Exec ((MultBy (a,b)),s) = s +* (Exec ((MultBy (A,B)),S)) by A3, Th51;
hence (Exec ((MultBy (a,b)),s)) . (IC ) = (Exec ((MultBy (A,B)),S)) . (IC ) by Th53
.= succ (IC S) by AMI_3:5
.= succ (IC s) by Th62 ;
::_thesis: ( (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) )
thus (Exec ((MultBy (a,b)),s)) . a = (Exec ((MultBy (A,B)),S)) . A by A1, A4, Th54
.= (S . A) * (S . B) by AMI_3:5
.= (S . A) * (s . b) by A2, Th55
.= (s . a) * (s . b) by A1, Th55 ; ::_thesis: ( ( for c being Int-Location st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((MultBy (a,b)),s)) . f = s . f
let c be Int-Location; ::_thesis: ( c <> a implies (Exec ((MultBy (a,b)),s)) . c = s . c )
assume A5: c <> a ; ::_thesis: (Exec ((MultBy (a,b)),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((MultBy (a,b)),s)) . c = (Exec ((MultBy (A,B)),S)) . C by A4, Th54
.= S . C by A1, A5, AMI_3:5
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((MultBy (a,b)),s)) . f = s . f
A6: not f in dom (Exec ((MultBy (A,B)),S)) by Th44;
thus (Exec ((MultBy (a,b)),s)) . f = s . f by A4, A6, FUNCT_4:11; ::_thesis: verum
end;
theorem Th67: :: SCMFSA_2:67
for a, b being Int-Location
for s being State of SCM+FSA holds
( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )
proof
let a, b be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: b = B and
A3: Divide (a,b) = Divide (A,B) by Def12;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A4: Exec ((Divide (a,b)),s) = s +* (Exec ((Divide (A,B)),S)) by A3, Th51;
hence (Exec ((Divide (a,b)),s)) . (IC ) = (Exec ((Divide (A,B)),S)) . (IC ) by Th53
.= succ (IC S) by AMI_3:6
.= succ (IC s) by Th62 ;
::_thesis: ( ( a <> b implies (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) & (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )
hereby ::_thesis: ( (Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for c being Int-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )
assume A5: a <> b ; ::_thesis: (Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b)
thus (Exec ((Divide (a,b)),s)) . a = (Exec ((Divide (A,B)),S)) . A by A1, A4, Th54
.= (S . A) div (S . B) by A1, A2, A5, AMI_3:6
.= (S . A) div (s . b) by A2, Th55
.= (s . a) div (s . b) by A1, Th55 ; ::_thesis: verum
end;
thus (Exec ((Divide (a,b)),s)) . b = (Exec ((Divide (A,B)),S)) . B by A2, A4, Th54
.= (S . A) mod (S . B) by AMI_3:6
.= (S . A) mod (s . b) by A2, Th55
.= (s . a) mod (s . b) by A1, Th55 ; ::_thesis: ( ( for c being Int-Location st c <> a & c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((Divide (a,b)),s)) . f = s . f
let c be Int-Location; ::_thesis: ( c <> a & c <> b implies (Exec ((Divide (a,b)),s)) . c = s . c )
assume A6: ( c <> a & c <> b ) ; ::_thesis: (Exec ((Divide (a,b)),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((Divide (a,b)),s)) . c = (Exec ((Divide (A,B)),S)) . C by A4, Th54
.= S . C by A1, A2, A6, AMI_3:6
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((Divide (a,b)),s)) . f = s . f
A7: not f in dom (Exec ((Divide (A,B)),S)) by Th44;
thus (Exec ((Divide (a,b)),s)) . f = s . f by A4, A7, FUNCT_4:11; ::_thesis: verum
end;
theorem :: SCMFSA_2:68
for a being Int-Location
for s being State of SCM+FSA holds
( (Exec ((Divide (a,a)),s)) . (IC ) = succ (IC s) & (Exec ((Divide (a,a)),s)) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds
(Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) )
proof
let a be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((Divide (a,a)),s)) . (IC ) = succ (IC s) & (Exec ((Divide (a,a)),s)) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds
(Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((Divide (a,a)),s)) . (IC ) = succ (IC s) & (Exec ((Divide (a,a)),s)) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds
(Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1: a = A and
A2: ( a = B & Divide (a,a) = Divide (A,B) ) by Def12;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A3: Exec ((Divide (a,a)),s) = s +* (Exec ((Divide (A,A)),S)) by A1, A2, Th51;
hence (Exec ((Divide (a,a)),s)) . (IC ) = (Exec ((Divide (A,A)),S)) . (IC ) by Th53
.= succ (IC S) by AMI_3:6
.= succ (IC s) by Th62 ;
::_thesis: ( (Exec ((Divide (a,a)),s)) . a = (s . a) mod (s . a) & ( for c being Int-Location st c <> a holds
(Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) )
thus (Exec ((Divide (a,a)),s)) . a = (Exec ((Divide (A,A)),S)) . A by A1, A3, Th54
.= (S . A) mod (S . A) by AMI_3:6
.= (S . A) mod (s . a) by A1, Th55
.= (s . a) mod (s . a) by A1, Th55 ; ::_thesis: ( ( for c being Int-Location st c <> a holds
(Exec ((Divide (a,a)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((Divide (a,a)),s)) . f = s . f
let c be Int-Location; ::_thesis: ( c <> a implies (Exec ((Divide (a,a)),s)) . c = s . c )
assume A4: c <> a ; ::_thesis: (Exec ((Divide (a,a)),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((Divide (a,a)),s)) . c = (Exec ((Divide (A,A)),S)) . C by A3, Th54
.= S . C by A1, A4, AMI_3:6
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((Divide (a,a)),s)) . f = s . f
A5: not f in dom (Exec ((Divide (A,A)),S)) by Th44;
thus (Exec ((Divide (a,a)),s)) . f = s . f by A3, A5, FUNCT_4:11; ::_thesis: verum
end;
theorem Th69: :: SCMFSA_2:69
for l being Element of NAT
for s being State of SCM+FSA holds
( (Exec ((goto l),s)) . (IC ) = l & ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) )
proof
let l be Element of NAT ; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((goto l),s)) . (IC ) = l & ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((goto l),s)) . (IC ) = l & ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) )
consider La being Element of NAT such that
A1: l = La and
A2: goto l = SCM-goto La ;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A3: Exec ((goto l),s) = s +* (Exec ((SCM-goto La),S)) by A2, Th51;
hence (Exec ((goto l),s)) . (IC ) = (Exec ((SCM-goto La),S)) . (IC ) by Th53
.= l by A1, AMI_3:7 ;
::_thesis: ( ( for c being Int-Location holds (Exec ((goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f
let c be Int-Location; ::_thesis: (Exec ((goto l),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((goto l),s)) . c = (Exec ((SCM-goto La),S)) . C by A3, Th54
.= S . C by AMI_3:7
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((goto l),s)) . f = s . f
A4: not f in dom (Exec ((SCM-goto La),S)) by Th44;
thus (Exec ((goto l),s)) . f = s . f by A3, A4, FUNCT_4:11; ::_thesis: verum
end;
theorem Th70: :: SCMFSA_2:70
for l being Element of NAT
for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )
proof
let l be Element of NAT ; ::_thesis: for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )
let a be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( ( s . a = 0 implies (Exec ((a =0_goto l),s)) . (IC ) = l ) & ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )
consider A being Data-Location such that
A1: a = A and
A2: a =0_goto l = A =0_goto l by Def14;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A3: Exec ((a =0_goto l),s) = s +* (Exec ((A =0_goto l),S)) by A2, Th51;
hereby ::_thesis: ( ( s . a <> 0 implies (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )
assume s . a = 0 ; ::_thesis: (Exec ((a =0_goto l),s)) . (IC ) = l
then A4: S . A = 0 by A1, Th55;
thus (Exec ((a =0_goto l),s)) . (IC ) = (Exec ((A =0_goto l),S)) . (IC ) by A3, Th53
.= l by A4, AMI_3:8 ; ::_thesis: verum
end;
hereby ::_thesis: ( ( for c being Int-Location holds (Exec ((a =0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f ) )
assume s . a <> 0 ; ::_thesis: (Exec ((a =0_goto l),s)) . (IC ) = succ (IC s)
then A5: S . A <> 0 by A1, Th55;
thus (Exec ((a =0_goto l),s)) . (IC ) = (Exec ((A =0_goto l),S)) . (IC ) by A3, Th53
.= succ (IC S) by A5, AMI_3:8
.= succ (IC s) by Th62 ; ::_thesis: verum
end;
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((a =0_goto l),s)) . f = s . f
let c be Int-Location; ::_thesis: (Exec ((a =0_goto l),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((a =0_goto l),s)) . c = (Exec ((A =0_goto l),S)) . C by A3, Th54
.= S . C by AMI_3:8
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((a =0_goto l),s)) . f = s . f
A6: not f in dom (Exec ((A =0_goto l),S)) by Th44;
thus (Exec ((a =0_goto l),s)) . f = s . f by A3, A6, FUNCT_4:11; ::_thesis: verum
end;
theorem Th71: :: SCMFSA_2:71
for l being Element of NAT
for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )
proof
let l be Element of NAT ; ::_thesis: for a being Int-Location
for s being State of SCM+FSA holds
( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )
let a be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( ( s . a > 0 implies (Exec ((a >0_goto l),s)) . (IC ) = l ) & ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )
consider A being Data-Location such that
A1: a = A and
A2: a >0_goto l = A >0_goto l by Def15;
reconsider S = s | SCM-Memory as State of SCM by Th49;
A3: Exec ((a >0_goto l),s) = s +* (Exec ((A >0_goto l),S)) by A2, Th51;
hereby ::_thesis: ( ( s . a <= 0 implies (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s) ) & ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )
assume s . a > 0 ; ::_thesis: (Exec ((a >0_goto l),s)) . (IC ) = l
then A4: S . A > 0 by A1, Th55;
thus (Exec ((a >0_goto l),s)) . (IC ) = (Exec ((A >0_goto l),S)) . (IC ) by A3, Th53
.= l by A4, AMI_3:9 ; ::_thesis: verum
end;
hereby ::_thesis: ( ( for c being Int-Location holds (Exec ((a >0_goto l),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f ) )
assume s . a <= 0 ; ::_thesis: (Exec ((a >0_goto l),s)) . (IC ) = succ (IC s)
then A5: S . A <= 0 by A1, Th55;
thus (Exec ((a >0_goto l),s)) . (IC ) = (Exec ((A >0_goto l),S)) . (IC ) by A3, Th53
.= succ (IC S) by A5, AMI_3:9
.= succ (IC s) by Th62 ; ::_thesis: verum
end;
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((a >0_goto l),s)) . f = s . f
let c be Int-Location; ::_thesis: (Exec ((a >0_goto l),s)) . c = s . c
reconsider C = c as Data-Location by Th10;
thus (Exec ((a >0_goto l),s)) . c = (Exec ((A >0_goto l),S)) . C by A3, Th54
.= S . C by AMI_3:9
.= s . c by Th55 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((a >0_goto l),s)) . f = s . f
A6: not f in dom (Exec ((A >0_goto l),S)) by Th44;
thus (Exec ((a >0_goto l),s)) . f = s . f by A3, A6, FUNCT_4:11; ::_thesis: verum
end;
theorem Th72: :: SCMFSA_2:72
for g being FinSeq-Location
for c, a being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
proof
let g be FinSeq-Location ; ::_thesis: for c, a being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
let c, a be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider mk = a, ml = c as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = c := (g,a) as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 9 as Element of Segm 13 by NAT_1:44;
InsCode I = 9 by RECDEF_2:def_1;
then consider i being Integer, k being Element of NAT such that
A1: k = abs (S . (I int_addr2)) and
A2: i = (S . (I coll_addr1)) /. k and
A3: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr1),i)),(succ (IC S))) by SCMFSA_1:def_16;
set S1 = SCM+FSA-Chg (S,(I int_addr1),i);
A4: Exec ((c := (g,a)),s) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr1),i)),(succ (IC S))) by A3, SCMFSA_1:def_17;
hence (Exec ((c := (g,a)),s)) . (IC ) = succ (IC s) by Th1, SCMFSA_1:19; ::_thesis: ( ex k being Element of NAT st
( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
A5: ( I = [J,{},<*ml,p,mk*>] & I `3_3 = <*ml,p,mk*> ) by RECDEF_2:def_3;
then A6: I int_addr1 = ml by SCMFSA_I:def_3;
A7: I coll_addr1 = p by A5, SCMFSA_I:def_5;
hereby ::_thesis: ( ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
take k = k; ::_thesis: ( k = abs (s . a) & (Exec ((c := (g,a)),s)) . c = (s . g) /. k )
thus k = abs (s . a) by A5, A1, SCMFSA_I:def_4; ::_thesis: (Exec ((c := (g,a)),s)) . c = (s . g) /. k
thus (Exec ((c := (g,a)),s)) . c = (SCM+FSA-Chg (S,(I int_addr1),i)) . ml by A4, SCMFSA_1:20
.= (s . g) /. k by A2, A6, A7, SCMFSA_1:24 ; ::_thesis: verum
end;
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f
let b be Int-Location; ::_thesis: ( b <> c implies (Exec ((c := (g,a)),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
assume A8: b <> c ; ::_thesis: (Exec ((c := (g,a)),s)) . b = s . b
thus (Exec ((c := (g,a)),s)) . b = (SCM+FSA-Chg (S,(I int_addr1),i)) . mn by A4, SCMFSA_1:20
.= s . b by A6, A8, SCMFSA_1:25 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((c := (g,a)),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec ((c := (g,a)),s)) . f = (SCM+FSA-Chg (S,(I int_addr1),i)) . q by A4, SCMFSA_1:21
.= s . f by SCMFSA_1:26 ; ::_thesis: verum
end;
theorem Th73: :: SCMFSA_2:73
for g being FinSeq-Location
for a, c being Int-Location
for s being State of SCM+FSA holds
( (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
proof
let g be FinSeq-Location ; ::_thesis: for a, c being Int-Location
for s being State of SCM+FSA holds
( (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
let a, c be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider mk = a, ml = c as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = (g,a) := c as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 10 as Element of Segm 13 by NAT_1:44;
InsCode I = 10 by RECDEF_2:def_1;
then consider F being FinSequence of INT , k being Element of NAT such that
A1: k = abs (S . (I int_addr2)) and
A2: F = (S . (I coll_addr1)) +* (k,(S . (I int_addr1))) and
A3: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr1),F)),(succ (IC S))) by SCMFSA_1:def_16;
set S1 = SCM+FSA-Chg (S,(I coll_addr1),F);
A4: Exec (((g,a) := c),s) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr1),F)),(succ (IC S))) by A3, SCMFSA_1:def_17;
hence (Exec (((g,a) := c),s)) . (IC ) = succ (IC s) by Th1, SCMFSA_1:19; ::_thesis: ( ex k being Element of NAT st
( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
A5: ( I = [J,{},<*ml,p,mk*>] & I `3_3 = <*ml,p,mk*> ) by RECDEF_2:def_3;
then A6: I coll_addr1 = p by SCMFSA_I:def_5;
A7: I int_addr1 = ml by A5, SCMFSA_I:def_3;
hereby ::_thesis: ( ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
take k = k; ::_thesis: ( k = abs (s . a) & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) )
thus k = abs (s . a) by A5, A1, SCMFSA_I:def_4; ::_thesis: (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c))
thus (Exec (((g,a) := c),s)) . g = (SCM+FSA-Chg (S,(I coll_addr1),F)) . p by A4, SCMFSA_1:21
.= (s . g) +* (k,(s . c)) by A2, A7, A6, SCMFSA_1:27 ; ::_thesis: verum
end;
hereby ::_thesis: for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f
let b be Int-Location; ::_thesis: (Exec (((g,a) := c),s)) . b = s . b
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
thus (Exec (((g,a) := c),s)) . b = (SCM+FSA-Chg (S,(I coll_addr1),F)) . mn by A4, SCMFSA_1:20
.= s . b by SCMFSA_1:29 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: ( f <> g implies (Exec (((g,a) := c),s)) . f = s . f )
assume A8: f <> g ; ::_thesis: (Exec (((g,a) := c),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec (((g,a) := c),s)) . f = (SCM+FSA-Chg (S,(I coll_addr1),F)) . q by A4, SCMFSA_1:21
.= s . f by A6, A8, SCMFSA_1:28 ; ::_thesis: verum
end;
theorem Th74: :: SCMFSA_2:74
for g being FinSeq-Location
for c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
proof
let g be FinSeq-Location ; ::_thesis: for c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
let c be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider I = c :=len g as Element of SCM+FSA-Instr ;
set S1 = SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))));
reconsider J = 11 as Element of Segm 13 by NAT_1:44;
reconsider ml = c as Element of SCM-Data-Loc by AMI_2:def_16;
A1: InsCode I = 11 by RECDEF_2:def_1;
A2: Exec ((c :=len g),s) = SCM+FSA-Exec-Res (I,S) by SCMFSA_1:def_17
.= SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))),(succ (IC S))) by A1, SCMFSA_1:def_16 ;
hence (Exec ((c :=len g),s)) . (IC ) = succ (IC s) by Th1, SCMFSA_1:19; ::_thesis: ( (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
A3: ( I = [J,{},<*ml,p*>] & I `3_3 = <*ml,p*> ) by RECDEF_2:def_3;
then A4: I int_addr3 = ml by SCMFSA_I:def_7;
A5: I coll_addr2 = p by A3, SCMFSA_I:def_8;
thus (Exec ((c :=len g),s)) . c = (SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))) . ml by A2, SCMFSA_1:20
.= len (s . g) by A4, A5, SCMFSA_1:24 ; ::_thesis: ( ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
hereby ::_thesis: for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f
let b be Int-Location; ::_thesis: ( b <> c implies (Exec ((c :=len g),s)) . b = s . b )
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
assume A6: b <> c ; ::_thesis: (Exec ((c :=len g),s)) . b = s . b
thus (Exec ((c :=len g),s)) . b = (SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))) . mn by A2, SCMFSA_1:20
.= s . b by A4, A6, SCMFSA_1:25 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: (Exec ((c :=len g),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec ((c :=len g),s)) . f = (SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))) . q by A2, SCMFSA_1:21
.= s . f by SCMFSA_1:26 ; ::_thesis: verum
end;
theorem Th75: :: SCMFSA_2:75
for g being FinSeq-Location
for c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )
proof
let g be FinSeq-Location ; ::_thesis: for c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )
let c be Int-Location; ::_thesis: for s being State of SCM+FSA holds
( (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )
let s be State of SCM+FSA; ::_thesis: ( (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex k being Element of NAT st
( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider ml = c as Element of SCM-Data-Loc by AMI_2:def_16;
reconsider I = g :=<0,...,0> c as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 12 as Element of Segm 13 by NAT_1:44;
InsCode I = 12 by RECDEF_2:def_1;
then consider F being FinSequence of INT , k being Element of NAT such that
A1: k = abs (S . (I int_addr3)) and
A2: F = k |-> 0 and
A3: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr2),F)),(succ (IC S))) by SCMFSA_1:def_16;
set S1 = SCM+FSA-Chg (S,(I coll_addr2),F);
A4: Exec ((g :=<0,...,0> c),s) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr2),F)),(succ (IC S))) by A3, SCMFSA_1:def_17;
hence (Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) by Th1, SCMFSA_1:19; ::_thesis: ( ex k being Element of NAT st
( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )
A5: ( I = [J,{},<*ml,p*>] & I `3_3 = <*ml,p*> ) by RECDEF_2:def_3;
then A6: I coll_addr2 = p by SCMFSA_I:def_8;
hereby ::_thesis: ( ( for b being Int-Location holds (Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )
take k = k; ::_thesis: ( k = abs (s . c) & (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 )
thus k = abs (s . c) by A5, A1, SCMFSA_I:def_7; ::_thesis: (Exec ((g :=<0,...,0> c),s)) . g = k |-> 0
thus (Exec ((g :=<0,...,0> c),s)) . g = (SCM+FSA-Chg (S,(I coll_addr2),F)) . p by A4, SCMFSA_1:21
.= k |-> 0 by A2, A6, SCMFSA_1:27 ; ::_thesis: verum
end;
hereby ::_thesis: for f being FinSeq-Location st f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f
let b be Int-Location; ::_thesis: (Exec ((g :=<0,...,0> c),s)) . b = s . b
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def_16;
thus (Exec ((g :=<0,...,0> c),s)) . b = (SCM+FSA-Chg (S,(I coll_addr2),F)) . mn by A4, SCMFSA_1:20
.= s . b by SCMFSA_1:29 ; ::_thesis: verum
end;
let f be FinSeq-Location ; ::_thesis: ( f <> g implies (Exec ((g :=<0,...,0> c),s)) . f = s . f )
assume A7: f <> g ; ::_thesis: (Exec ((g :=<0,...,0> c),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec ((g :=<0,...,0> c),s)) . f = (SCM+FSA-Chg (S,(I coll_addr2),F)) . q by A4, SCMFSA_1:21
.= s . f by A6, A7, SCMFSA_1:28 ; ::_thesis: verum
end;
begin
theorem :: SCMFSA_2:76
for s being State of SCM+FSA
for S being SCM+FSA-State st S = s holds
IC s = IC S by FUNCT_7:def_1, SCMFSA_1:5;
theorem Th77: :: SCMFSA_2:77
for i being Instruction of SCM
for I being Instruction of SCM+FSA st i = I & i is halting holds
I is halting
proof
let i be Instruction of SCM; ::_thesis: for I being Instruction of SCM+FSA st i = I & i is halting holds
I is halting
let I be Instruction of SCM+FSA; ::_thesis: ( i = I & i is halting implies I is halting )
assume A1: i = I ; ::_thesis: ( not i is halting or I is halting )
assume A2: i is halting ; ::_thesis: I is halting
let S be State of SCM+FSA; :: according to EXTPRO_1:def_3 ::_thesis: Exec (I,S) = S
reconsider s = S | SCM-Memory as State of SCM by Th49;
thus Exec (I,S) = S +* (Exec (i,s)) by A1, Th51
.= S +* s by A2, EXTPRO_1:def_3
.= S by Th52 ; ::_thesis: verum
end;
theorem Th78: :: SCMFSA_2:78
for I being Instruction of SCM+FSA st ex s being State of SCM+FSA st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting
proof
let I be Instruction of SCM+FSA; ::_thesis: ( ex s being State of SCM+FSA st (Exec (I,s)) . (IC ) = succ (IC s) implies not I is halting )
given s being State of SCM+FSA such that A1: (Exec (I,s)) . (IC ) = succ (IC s) ; ::_thesis: not I is halting
reconsider T = s as SCM+FSA-State by CARD_3:107;
IC T = T . NAT ;
then reconsider w = T . NAT as Element of NAT ;
assume I is halting ; ::_thesis: contradiction
then A2: (Exec (I,s)) . (IC ) = T . NAT by Th1, EXTPRO_1:def_3;
(Exec (I,s)) . (IC ) = succ w by A1, FUNCT_7:def_1, SCMFSA_1:5;
hence contradiction by A2; ::_thesis: verum
end;
registration
let a, b be Int-Location;
set s = the State of SCM+FSA;
clustera := b -> non halting ;
coherence
not a := b is halting
proof
IC (Exec ((a := b), the State of SCM+FSA)) = succ (IC the State of SCM+FSA) by Th63;
hence not a := b is halting by Th78; ::_thesis: verum
end;
cluster AddTo (a,b) -> non halting ;
coherence
not AddTo (a,b) is halting
proof
IC (Exec ((AddTo (a,b)), the State of SCM+FSA)) = succ (IC the State of SCM+FSA) by Th64;
hence not AddTo (a,b) is halting by Th78; ::_thesis: verum
end;
cluster SubFrom (a,b) -> non halting ;
coherence
not SubFrom (a,b) is halting
proof
IC (Exec ((SubFrom (a,b)), the State of SCM+FSA)) = succ (IC the State of SCM+FSA) by Th65;
hence not SubFrom (a,b) is halting by Th78; ::_thesis: verum
end;
cluster MultBy (a,b) -> non halting ;
coherence
not MultBy (a,b) is halting
proof
IC (Exec ((MultBy (a,b)), the State of SCM+FSA)) = succ (IC the State of SCM+FSA) by Th66;
hence not MultBy (a,b) is halting by Th78; ::_thesis: verum
end;
cluster Divide (a,b) -> non halting ;
coherence
not Divide (a,b) is halting
proof
IC (Exec ((Divide (a,b)), the State of SCM+FSA)) = succ (IC the State of SCM+FSA) by Th67;
hence not Divide (a,b) is halting by Th78; ::_thesis: verum
end;
end;
theorem :: SCMFSA_2:79
for a, b being Int-Location holds not a := b is halting ;
theorem :: SCMFSA_2:80
for a, b being Int-Location holds not AddTo (a,b) is halting ;
theorem :: SCMFSA_2:81
for a, b being Int-Location holds not SubFrom (a,b) is halting ;
theorem :: SCMFSA_2:82
for a, b being Int-Location holds not MultBy (a,b) is halting ;
theorem :: SCMFSA_2:83
for a, b being Int-Location holds not Divide (a,b) is halting ;
registration
let la be Element of NAT ;
cluster goto la -> non halting ;
coherence
not goto la is halting
proof
set f = the_Values_of SCM+FSA;
set s = the SCM+FSA-State;
assume A1: goto la is halting ; ::_thesis: contradiction
reconsider a3 = la as Element of NAT ;
set t = the SCM+FSA-State +* (NAT .--> (succ a3));
dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then A2: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A3: for x being set st x in dom (the_Values_of SCM+FSA) holds
( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCM+FSA) implies ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x )
assume A4: x in dom (the_Values_of SCM+FSA) ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
percases ( x = NAT or x <> NAT ) ;
suppose x = NAT ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
hence ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x by A2, SCMFSA_1:9; ::_thesis: verum
end;
suppose x <> NAT ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
then not x in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x = the SCM+FSA-State . x by FUNCT_4:11;
hence ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x by A4, CARD_3:9; ::_thesis: verum
end;
end;
end;
A5: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5, ZFMISC_1:31;
A6: dom ( the SCM+FSA-State +* (NAT .--> (succ a3))) = (dom the SCM+FSA-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def_1
.= SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) by SCMFSA_1:33
.= SCM+FSA-Memory \/ {NAT} by FUNCOP_1:13
.= SCM+FSA-Memory by A5, XBOOLE_1:12 ;
dom (the_Values_of SCM+FSA) = SCM+FSA-Memory by SCMFSA_1:32;
then reconsider t = the SCM+FSA-State +* (NAT .--> (succ a3)) as State of SCM+FSA by A6, A3, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
dom (NAT .--> la) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> la) by TARSKI:def_1;
then A7: (w +* (NAT .--> la)) . NAT = (NAT .--> la) . NAT by FUNCT_4:13
.= la by FUNCOP_1:72 ;
(w +* (NAT .--> la)) . NAT = (SCM+FSA-Chg (w,a3)) . NAT
.= a3 by SCMFSA_1:19
.= (Exec ((goto la),t)) . NAT by Th1, Th69
.= t . NAT by A1, EXTPRO_1:def_3 ;
hence contradiction by A2, A7; ::_thesis: verum
end;
end;
theorem :: SCMFSA_2:84
for la being Element of NAT holds not goto la is halting ;
registration
let a be Int-Location;
let la be Element of NAT ;
set f = the_Values_of SCM+FSA;
set s = the SCM+FSA-State;
clustera =0_goto la -> non halting ;
coherence
not a =0_goto la is halting
proof
reconsider a3 = la as Element of NAT ;
set t = the SCM+FSA-State +* (NAT .--> (succ a3));
A1: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5, ZFMISC_1:31;
A2: dom ( the SCM+FSA-State +* (NAT .--> (succ a3))) = (dom the SCM+FSA-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def_1
.= SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) by SCMFSA_1:33
.= SCM+FSA-Memory \/ {NAT} by FUNCOP_1:13
.= SCM+FSA-Memory by A1, XBOOLE_1:12 ;
assume A3: a =0_goto la is halting ; ::_thesis: contradiction
dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then A4: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A5: for x being set st x in dom (the_Values_of SCM+FSA) holds
( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCM+FSA) implies ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x )
assume A6: x in dom (the_Values_of SCM+FSA) ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
percases ( x = NAT or x <> NAT ) ;
suppose x = NAT ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
hence ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x by A4, SCMFSA_1:9; ::_thesis: verum
end;
suppose x <> NAT ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
then not x in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x = the SCM+FSA-State . x by FUNCT_4:11;
hence ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x by A6, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom (the_Values_of SCM+FSA) = SCM+FSA-Memory by SCMFSA_1:32;
then reconsider t = the SCM+FSA-State +* (NAT .--> (succ a3)) as State of SCM+FSA by A2, A5, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
dom (NAT .--> la) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> la) by TARSKI:def_1;
then A7: (w +* (NAT .--> la)) . NAT = (NAT .--> la) . NAT by FUNCT_4:13
.= la by FUNCOP_1:72 ;
percases ( t . a <> 0 or t . a = 0 ) ;
supposeA8: t . a <> 0 ; ::_thesis: contradiction
IC w = w . NAT ;
then reconsider e = w . NAT as Element of NAT ;
IC t = IC w by FUNCT_7:def_1, SCMFSA_1:5;
then A9: (Exec ((a =0_goto la),t)) . (IC ) = succ e by A8, Th70;
(Exec ((a =0_goto la),t)) . (IC ) = w . NAT by A3, Th1, EXTPRO_1:def_3;
hence contradiction by A9; ::_thesis: verum
end;
supposeA10: t . a = 0 ; ::_thesis: contradiction
(w +* (NAT .--> la)) . NAT = (SCM+FSA-Chg (w,a3)) . NAT
.= a3 by SCMFSA_1:19
.= (Exec ((a =0_goto la),t)) . NAT by A10, Th1, Th70
.= t . NAT by A3, EXTPRO_1:def_3 ;
hence contradiction by A4, A7; ::_thesis: verum
end;
end;
end;
clustera >0_goto la -> non halting ;
coherence
not a >0_goto la is halting
proof
reconsider a3 = la as Element of NAT ;
set t = the SCM+FSA-State +* (NAT .--> (succ a3));
A11: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5, ZFMISC_1:31;
A12: dom ( the SCM+FSA-State +* (NAT .--> (succ a3))) = (dom the SCM+FSA-State) \/ (dom (NAT .--> (succ a3))) by FUNCT_4:def_1
.= SCM+FSA-Memory \/ (dom (NAT .--> (succ a3))) by SCMFSA_1:33
.= SCM+FSA-Memory \/ {NAT} by FUNCOP_1:13
.= SCM+FSA-Memory by A11, XBOOLE_1:12 ;
assume A13: a >0_goto la is halting ; ::_thesis: contradiction
dom (NAT .--> (succ a3)) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then A14: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . NAT = (NAT .--> (succ a3)) . NAT by FUNCT_4:13
.= succ a3 by FUNCOP_1:72 ;
A15: for x being set st x in dom (the_Values_of SCM+FSA) holds
( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
proof
let x be set ; ::_thesis: ( x in dom (the_Values_of SCM+FSA) implies ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x )
assume A16: x in dom (the_Values_of SCM+FSA) ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
percases ( x = NAT or x <> NAT ) ;
suppose x = NAT ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
hence ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x by A14, SCMFSA_1:9; ::_thesis: verum
end;
suppose x <> NAT ; ::_thesis: ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x
then not x in dom (NAT .--> (succ a3)) by TARSKI:def_1;
then ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x = the SCM+FSA-State . x by FUNCT_4:11;
hence ( the SCM+FSA-State +* (NAT .--> (succ a3))) . x in (the_Values_of SCM+FSA) . x by A16, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom (the_Values_of SCM+FSA) = SCM+FSA-Memory by SCMFSA_1:32;
then reconsider t = the SCM+FSA-State +* (NAT .--> (succ a3)) as State of SCM+FSA by A12, A15, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
dom (NAT .--> la) = {NAT} by FUNCOP_1:13;
then NAT in dom (NAT .--> la) by TARSKI:def_1;
then A17: (w +* (NAT .--> la)) . NAT = (NAT .--> la) . NAT by FUNCT_4:13
.= la by FUNCOP_1:72 ;
percases ( t . a <= 0 or t . a > 0 ) ;
supposeA18: t . a <= 0 ; ::_thesis: contradiction
IC w = w . NAT ;
then reconsider e = w . NAT as Element of NAT ;
IC t = IC w by FUNCT_7:def_1, SCMFSA_1:5;
then A19: (Exec ((a >0_goto la),t)) . (IC ) = succ e by A18, Th71;
(Exec ((a >0_goto la),t)) . (IC ) = w . NAT by A13, Th1, EXTPRO_1:def_3;
hence contradiction by A19; ::_thesis: verum
end;
supposeA20: t . a > 0 ; ::_thesis: contradiction
(w +* (NAT .--> la)) . NAT = (SCM+FSA-Chg (w,a3)) . NAT
.= a3 by SCMFSA_1:19
.= (Exec ((a >0_goto la),t)) . NAT by A20, Th1, Th71
.= t . NAT by A13, EXTPRO_1:def_3 ;
hence contradiction by A14, A17; ::_thesis: verum
end;
end;
end;
end;
theorem :: SCMFSA_2:85
for la being Element of NAT
for a being Int-Location holds not a =0_goto la is halting ;
theorem :: SCMFSA_2:86
for la being Element of NAT
for a being Int-Location holds not a >0_goto la is halting ;
registration
let c be Int-Location;
let f be FinSeq-Location ;
let a be Int-Location;
set s = the State of SCM+FSA;
clusterc := (f,a) -> non halting ;
coherence
not c := (f,a) is halting
proof
(Exec ((c := (f,a)), the State of SCM+FSA)) . (IC ) = succ (IC the State of SCM+FSA) by Th72;
hence not c := (f,a) is halting by Th78; ::_thesis: verum
end;
cluster(f,a) := c -> non halting ;
coherence
not (f,a) := c is halting
proof
(Exec (((f,a) := c), the State of SCM+FSA)) . (IC ) = succ (IC the State of SCM+FSA) by Th73;
hence not (f,a) := c is halting by Th78; ::_thesis: verum
end;
end;
theorem :: SCMFSA_2:87
for f being FinSeq-Location
for c, a being Int-Location holds not c := (f,a) is halting ;
theorem :: SCMFSA_2:88
for f being FinSeq-Location
for a, c being Int-Location holds not (f,a) := c is halting ;
registration
let c be Int-Location;
let f be FinSeq-Location ;
set s = the State of SCM+FSA;
clusterc :=len f -> non halting ;
coherence
not c :=len f is halting
proof
(Exec ((c :=len f), the State of SCM+FSA)) . (IC ) = succ (IC the State of SCM+FSA) by Th74;
hence not c :=len f is halting by Th78; ::_thesis: verum
end;
clusterf :=<0,...,0> c -> non halting ;
coherence
not f :=<0,...,0> c is halting
proof
(Exec ((f :=<0,...,0> c), the State of SCM+FSA)) . (IC ) = succ (IC the State of SCM+FSA) by Th75;
hence not f :=<0,...,0> c is halting by Th78; ::_thesis: verum
end;
end;
theorem :: SCMFSA_2:89
for f being FinSeq-Location
for c being Int-Location holds not c :=len f is halting ;
theorem :: SCMFSA_2:90
for f being FinSeq-Location
for c being Int-Location holds not f :=<0,...,0> c is halting ;
theorem :: SCMFSA_2:91
for I being Instruction of SCM+FSA st I = [0,{},{}] holds
I is halting by Th77, AMI_3:26;
theorem Th92: :: SCMFSA_2:92
for I being Instruction of SCM+FSA st InsCode I = 0 holds
I = [0,{},{}]
proof
let I be Instruction of SCM+FSA; ::_thesis: ( InsCode I = 0 implies I = [0,{},{}] )
assume A1: InsCode I = 0 ; ::_thesis: I = [0,{},{}]
A2: now__::_thesis:_not_I_in__{__[R,{},<*DA,DC*>]_where_R_is_Element_of_Segm_9,_DA,_DC_is_Element_of_SCM-Data-Loc_:_R_in_{1,2,3,4,5}__}_
assume I in { [R,{},<*DA,DC*>] where R is Element of Segm 9, DA, DC is Element of SCM-Data-Loc : R in {1,2,3,4,5} } ; ::_thesis: contradiction
then ex R being Element of Segm 9 ex DA, DC being Element of SCM-Data-Loc st
( I = [R,{},<*DA,DC*>] & R in {1,2,3,4,5} ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A3: now__::_thesis:_not_I_in__{__[O,<*LA*>,{}]_where_O_is_Element_of_Segm_9,_LA_is_Element_of_NAT_:_O_=_6__}_
assume I in { [O,<*LA*>,{}] where O is Element of Segm 9, LA is Element of NAT : O = 6 } ; ::_thesis: contradiction
then ex O being Element of Segm 9 ex LA being Element of NAT st
( I = [O,<*LA*>,{}] & O = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A4: now__::_thesis:_not_I_in__{__[P,<*LB*>,<*DB*>]_where_P_is_Element_of_Segm_9,_LB_is_Element_of_NAT_,_DB_is_Element_of_SCM-Data-Loc_:_P_in_{7,8}__}_
assume I in { [P,<*LB*>,<*DB*>] where P is Element of Segm 9, LB is Element of NAT , DB is Element of SCM-Data-Loc : P in {7,8} } ; ::_thesis: contradiction
then ex P being Element of Segm 9 ex LB being Element of NAT ex DB being Element of SCM-Data-Loc st
( I = [P,<*LB*>,<*DB*>] & P in {7,8} ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A5: now__::_thesis:_not_I_in__{__[K,{},<*dC,fB*>]_where_K_is_Element_of_Segm_13,_dC_is_Element_of_SCM+FSA-Data-Loc_,_fB_is_Element_of_SCM+FSA-Data*-Loc_:_K_in_{11,12}__}_
assume I in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; ::_thesis: contradiction
then ex K being Element of Segm 13 ex dC being Element of SCM+FSA-Data-Loc ex fB being Element of SCM+FSA-Data*-Loc st
( I = [K,{},<*dC,fB*>] & K in {11,12} ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A6: I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } by A5, XBOOLE_0:def_3;
now__::_thesis:_not_I_in__{__[L,{},<*dB,fA,dA*>]_where_L_is_Element_of_Segm_13,_dB,_dA_is_Element_of_SCM+FSA-Data-Loc_,_fA_is_Element_of_SCM+FSA-Data*-Loc_:_L_in_{9,10}__}_
assume I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } ; ::_thesis: contradiction
then ex L being Element of Segm 13 ex dB, dA being Element of SCM+FSA-Data-Loc ex fA being Element of SCM+FSA-Data*-Loc st
( I = [L,{},<*dB,fA,dA*>] & L in {9,10} ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
then I in SCM-Instr by A6, XBOOLE_0:def_3;
then I in ({[SCM-Halt,{},{}]} \/ { [O,<*LA*>,{}] where O is Element of Segm 9, LA is Element of NAT : O = 6 } ) \/ { [P,<*LB*>,<*DB*>] where P is Element of Segm 9, LB is Element of NAT , DB is Element of SCM-Data-Loc : P in {7,8} } by A2, XBOOLE_0:def_3;
then I in {[SCM-Halt,{},{}]} \/ { [O,<*LA*>,{}] where O is Element of Segm 9, LA is Element of NAT : O = 6 } by A4, XBOOLE_0:def_3;
then I in {[SCM-Halt,{},{}]} by A3, XBOOLE_0:def_3;
hence I = [0,{},{}] by TARSKI:def_1; ::_thesis: verum
end;
theorem Th93: :: SCMFSA_2:93
for I being set holds
( I is Instruction of SCM+FSA iff ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) )
proof
let I be set ; ::_thesis: ( I is Instruction of SCM+FSA iff ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) )
thus ( not I is Instruction of SCM+FSA or I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) ::_thesis: ( ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) implies I is Instruction of SCM+FSA )
proof
assume I is Instruction of SCM+FSA ; ::_thesis: ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a )
then reconsider J = I as Instruction of SCM+FSA ;
set n = InsCode J;
( InsCode J = 0 or InsCode J = 1 or InsCode J = 2 or InsCode J = 3 or InsCode J = 4 or InsCode J = 5 or InsCode J = 6 or InsCode J = 7 or InsCode J = 8 or InsCode J = 9 or InsCode J = 10 or InsCode J = 11 or InsCode J = 12 ) by Th16, NAT_1:36;
hence ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) by Th30, Th31, Th32, Th33, Th34, Th35, Th36, Th37, Th38, Th39, Th40, Th41, Th92; ::_thesis: verum
end;
thus ( ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a ) implies I is Instruction of SCM+FSA ) by SCMFSA_I:3; ::_thesis: verum
end;
Lm1: for W being Instruction of SCM+FSA st W is halting holds
W = [0,{},{}]
proof
set I = [0,{},{}];
let W be Instruction of SCM+FSA; ::_thesis: ( W is halting implies W = [0,{},{}] )
assume A1: W is halting ; ::_thesis: W = [0,{},{}]
assume A2: [0,{},{}] <> W ; ::_thesis: contradiction
percases ( W = [0,{},{}] or ex a, b being Int-Location st W = a := b or ex a, b being Int-Location st W = AddTo (a,b) or ex a, b being Int-Location st W = SubFrom (a,b) or ex a, b being Int-Location st W = MultBy (a,b) or ex a, b being Int-Location st W = Divide (a,b) or ex la being Element of NAT st W = goto la or ex lb being Element of NAT ex da being Int-Location st W = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st W = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st W = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st W = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st W = a :=len f or ex a being Int-Location ex f being FinSeq-Location st W = f :=<0,...,0> a ) by Th93;
suppose W = [0,{},{}] ; ::_thesis: contradiction
hence contradiction by A2; ::_thesis: verum
end;
suppose ex a, b being Int-Location st W = a := b ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st W = AddTo (a,b) ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st W = SubFrom (a,b) ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st W = MultBy (a,b) ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location st W = Divide (a,b) ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex la being Element of NAT st W = goto la ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex lb being Element of NAT ex da being Int-Location st W = da =0_goto lb ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex lb being Element of NAT ex da being Int-Location st W = da >0_goto lb ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex b, a being Int-Location ex fa being FinSeq-Location st W = a := (fa,b) ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex a, b being Int-Location ex fa being FinSeq-Location st W = (fa,a) := b ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st W = a :=len f ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose ex a being Int-Location ex f being FinSeq-Location st W = f :=<0,...,0> a ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
end;
end;
registration
cluster SCM+FSA -> strict halting ;
coherence
SCM+FSA is halting
proof
thus halt SCM+FSA is halting by Th77, AMI_3:26; :: according to EXTPRO_1:def_4 ::_thesis: verum
end;
end;
theorem Th94: :: SCMFSA_2:94
for I being Instruction of SCM+FSA st I is halting holds
I = halt SCM+FSA by Lm1;
theorem :: SCMFSA_2:95
for I being Instruction of SCM+FSA st InsCode I = 0 holds
I = halt SCM+FSA by Th92;
theorem Th96: :: SCMFSA_2:96
halt SCM = halt SCM+FSA ;
theorem :: SCMFSA_2:97
canceled;
theorem :: SCMFSA_2:98
for i being Instruction of SCM
for I being Instruction of SCM+FSA st i = I & not i is halting holds
not I is halting by Th94, Th96;
theorem :: SCMFSA_2:99
for i, j being Nat holds fsloc i <> intloc j
proof
let i, j be Nat; ::_thesis: fsloc i <> intloc j
fsloc i in FinSeq-Locations by Def5;
hence fsloc i <> intloc j by SCMFSA_1:30, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th100: :: SCMFSA_2:100
Data-Locations = Int-Locations \/ FinSeq-Locations
proof
now__::_thesis:_not_NAT_in_FinSeq-Locations
assume NAT in FinSeq-Locations ; ::_thesis: contradiction
then A1: NAT in (NAT \/ [:{0},NAT:]) \ {[0,0]} by NUMBERS:def_4;
not NAT in NAT ;
then NAT in [:{0},NAT:] by A1, XBOOLE_0:def_3;
then ex x, y being set st NAT = [x,y] by RELAT_1:def_1;
hence contradiction ; ::_thesis: verum
end;
then FinSeq-Locations misses {NAT} by ZFMISC_1:50;
then FinSeq-Locations misses {NAT} ;
then A2: FinSeq-Locations \ {NAT} = FinSeq-Locations by XBOOLE_1:83;
SCM-Data-Loc misses {NAT} by AMI_2:20, ZFMISC_1:50;
then A3: SCM-Data-Loc misses {NAT} ;
A4: SCM-Memory \ {NAT} = SCM-Data-Loc \ {NAT} by XBOOLE_1:40
.= Int-Locations by A3, XBOOLE_1:83 ;
thus Data-Locations = (SCM-Memory \/ FinSeq-Locations) \ {NAT} by FUNCT_7:def_1, SCMFSA_1:5
.= Int-Locations \/ FinSeq-Locations by A2, A4, XBOOLE_1:42 ; ::_thesis: verum
end;
theorem :: SCMFSA_2:101
for i, j being Nat st i <> j holds
intloc i <> intloc j by AMI_3:10;
theorem :: SCMFSA_2:102
for l being Element of NAT
for a being Int-Location holds not a in dom (Start-At (l,SCM+FSA))
proof
let l be Element of NAT ; ::_thesis: for a being Int-Location holds not a in dom (Start-At (l,SCM+FSA))
let a be Int-Location; ::_thesis: not a in dom (Start-At (l,SCM+FSA))
A1: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
assume a in dom (Start-At (l,SCM+FSA)) ; ::_thesis: contradiction
then a = IC by A1, TARSKI:def_1;
hence contradiction by Th56; ::_thesis: verum
end;
theorem :: SCMFSA_2:103
for l being Element of NAT
for f being FinSeq-Location holds not f in dom (Start-At (l,SCM+FSA))
proof
let l be Element of NAT ; ::_thesis: for f being FinSeq-Location holds not f in dom (Start-At (l,SCM+FSA))
let f be FinSeq-Location ; ::_thesis: not f in dom (Start-At (l,SCM+FSA))
A1: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
assume f in dom (Start-At (l,SCM+FSA)) ; ::_thesis: contradiction
then f = IC by A1, TARSKI:def_1;
hence contradiction by Th57; ::_thesis: verum
end;
theorem :: SCMFSA_2:104
for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
s1 = s2
proof
let s1, s2 be State of SCM+FSA; ::_thesis: ( IC s1 = IC s2 & ( for a being Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) implies s1 = s2 )
assume A1: IC s1 = IC s2 ; ::_thesis: ( ex a being Int-Location st not s1 . a = s2 . a or ex f being FinSeq-Location st not s1 . f = s2 . f or s1 = s2 )
( IC in dom s1 & IC in dom s2 ) by MEMSTR_0:2;
then A2: ( s1 = (DataPart s1) +* (Start-At ((IC s1),SCM+FSA)) & s2 = (DataPart s2) +* (Start-At ((IC s2),SCM+FSA)) ) by MEMSTR_0:26;
assume that
A3: for a being Int-Location holds s1 . a = s2 . a and
A4: for f being FinSeq-Location holds s1 . f = s2 . f ; ::_thesis: s1 = s2
DataPart s1 = DataPart s2
proof
A5: dom (DataPart s1) = Data-Locations by MEMSTR_0:9;
hence dom (DataPart s1) = dom (DataPart s2) by MEMSTR_0:9; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in proj1 (DataPart s1) or (DataPart s1) . b1 = (DataPart s2) . b1 )
let x be set ; ::_thesis: ( not x in proj1 (DataPart s1) or (DataPart s1) . x = (DataPart s2) . x )
assume A6: x in dom (DataPart s1) ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
then A7: x in Int-Locations \/ FinSeq-Locations by A5, Th100;
percases ( x in Int-Locations or x in FinSeq-Locations ) by A7, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
then A8: x is Int-Location by AMI_2:def_16;
thus (DataPart s1) . x = s1 . x by A6, A5, FUNCT_1:49
.= s2 . x by A8, A3
.= (DataPart s2) . x by A6, A5, FUNCT_1:49 ; ::_thesis: verum
end;
suppose x in FinSeq-Locations ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
then A9: x is FinSeq-Location by Def5;
thus (DataPart s1) . x = s1 . x by A6, A5, FUNCT_1:49
.= s2 . x by A9, A4
.= (DataPart s2) . x by A6, A5, FUNCT_1:49 ; ::_thesis: verum
end;
end;
end;
hence s1 = s2 by A1, A2; ::_thesis: verum
end;
registration
let f be FinSeq-Location ;
let w be FinSequence of INT ;
clusterf .--> w -> data-only for PartState of SCM+FSA;
coherence
for b1 being PartState of SCM+FSA st b1 = f .--> w holds
b1 is data-only
proof
let p be PartState of SCM+FSA; ::_thesis: ( p = f .--> w implies p is data-only )
assume A1: p = f .--> w ; ::_thesis: p is data-only
A2: dom p = {f} by A1, FUNCOP_1:13;
f <> IC by Th57;
then A3: {f} misses {(IC )} by ZFMISC_1:11;
dom p misses {(IC )} by A2, A3;
hence p is data-only by MEMSTR_0:def_9; ::_thesis: verum
end;
end;
registration
let x be Int-Location;
let i be Integer;
clusterx .--> i -> data-only for PartState of SCM+FSA;
coherence
for b1 being PartState of SCM+FSA st b1 = x .--> i holds
b1 is data-only
proof
let p be PartState of SCM+FSA; ::_thesis: ( p = x .--> i implies p is data-only )
assume A1: p = x .--> i ; ::_thesis: p is data-only
A2: dom p = {x} by A1, FUNCOP_1:13;
x <> IC by Th56;
then {x} misses {(IC )} by ZFMISC_1:11;
then dom p misses {(IC )} by A2;
hence p is data-only by MEMSTR_0:def_9; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
clustera := b -> No-StopCode ;
coherence
a := b is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence a := b is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
cluster AddTo (a,b) -> No-StopCode ;
coherence
AddTo (a,b) is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence AddTo (a,b) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
cluster SubFrom (a,b) -> No-StopCode ;
coherence
SubFrom (a,b) is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence SubFrom (a,b) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
cluster MultBy (a,b) -> No-StopCode ;
coherence
MultBy (a,b) is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence MultBy (a,b) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let a, b be Int-Location;
cluster Divide (a,b) -> No-StopCode ;
coherence
Divide (a,b) is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence Divide (a,b) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let lb be Element of NAT ;
cluster goto lb -> No-StopCode ;
coherence
goto lb is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence goto lb is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let lb be Element of NAT ;
let a be Int-Location;
clustera =0_goto lb -> No-StopCode ;
coherence
a =0_goto lb is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence a =0_goto lb is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let lb be Element of NAT ;
let a be Int-Location;
clustera >0_goto lb -> No-StopCode ;
coherence
a >0_goto lb is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence a >0_goto lb is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let fa be FinSeq-Location ;
let a, c be Int-Location;
clusterc := (fa,a) -> No-StopCode ;
coherence
c := (fa,a) is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence c := (fa,a) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let fa be FinSeq-Location ;
let a, c be Int-Location;
cluster(fa,a) := c -> No-StopCode ;
coherence
(fa,a) := c is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence (fa,a) := c is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let fa be FinSeq-Location ;
let a be Int-Location;
clustera :=len fa -> No-StopCode ;
coherence
a :=len fa is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence a :=len fa is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;
registration
let fa be FinSeq-Location ;
let a be Int-Location;
clusterfa :=<0,...,0> a -> No-StopCode ;
coherence
fa :=<0,...,0> a is No-StopCode
proof
InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
hence fa :=<0,...,0> a is No-StopCode by COMPOS_0:def_12; ::_thesis: verum
end;
end;