environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, AMI_1, RELAT_1, SCMFSA_1, FUNCT_7, XBOOLE_0, TARSKI, AMI_3, ZFMISC_1, SUBSET_1, CARD_1, CAT_1, ARYTM_1, ARYTM_3, NAT_1, FINSET_1, FUNCT_1, AMI_2, XXREAL_0, FINSEQ_1, GRAPHSP, FSM_1, FUNCT_4, FUNCOP_1, INT_1, CARD_3, COMPLEX1, PARTFUN1, FINSEQ_2, GLIB_000, SCMFSA_2, RECDEF_2, GOBRD13, MEMSTR_0, AMISTD_4, SCMPDS_5;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1, XCMPLX_0, XXREAL_0, INT_1, NAT_1, RELAT_1, MCART_1, CARD_1, CARD_3, INT_2, FINSEQ_1, FUNCOP_1, STRUCT_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, FINSEQ_2, FUNCT_7, RECDEF_2, NUMBERS, MEMSTR_0, COMPOS_0, COMPOS_1, AMISTD_4, EXTPRO_1, SCM_INST, SCMFSA_I, AMI_2, AMI_3, SCMFSA_1;
definitions TARSKI, EXTPRO_1, WELLORD2, XBOOLE_0, STRUCT_0, FUNCT_1, MEMSTR_0, AMISTD_4;
theorems SCMFSA_1, TARSKI, INT_1, RELAT_1, AMI_5, FUNCT_2, FUNCT_4, CARD_3, FUNCOP_1, FUNCT_1, AMI_3, NAT_1, CARD_1, AMI_2, FUNCT_7, ZFMISC_1, ORDINAL1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, NUMBERS, FINSET_1, PARTFUN1, MEMSTR_0, SCMFSA_I, SCM_INST, XTUPLE_0, SUBSET_1;
schemes FUNCT_2;
registrations RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, INT_1, CARD_3, STRUCT_0, AMI_3, SCMFSA_1, FINSET_1, CARD_2, RELSET_1, EXTPRO_1, MEMSTR_0, COMPOS_0, SCM_INST, SCMFSA_I, XTUPLE_0;
constructors HIDDEN, WELLORD2, DOMAIN_1, REAL_1, FINSEQ_4, AMI_3, SCMFSA_1, RELSET_1, PRE_POLY, FUNCT_7, NAT_D, AMISTD_4, XTUPLE_0, XFAMILY;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TARSKI, EXTPRO_1, COMPOS_1, XBOOLE_0, AMI_2, AMI_3, STRUCT_0, SCMFSA_1, FUNCOP_1, NAT_1, MEMSTR_0, COMPOS_0, SCM_INST, SCMFSA_I;
expansions EXTPRO_1, AMI_2, FUNCT_1, MEMSTR_0, COMPOS_0;
definition
let a,
b be
Int-Location;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = A := B )
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;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo (A,B) )
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;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom (A,B) )
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;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy (A,B) )
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;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = Divide (A,B) )
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;
theorem Th60:
for
a,
b being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec ((Divide (a,b)),s)) . (IC ) = (IC s) + 1 & (
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 ) )
theorem Th66:
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 ) = (IC s) + 1 & ex
k being
Nat st
(
k = |.(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 ) )
theorem Th68:
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 ) = (IC s) + 1 & ex
k being
Nat st
(
k = |.(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 ) )
theorem Th86:
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
Nat st
I = goto la or ex
lb being
Nat ex
da being
Int-Location st
I = da =0_goto lb or ex
lb being
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 ) )
Lm1:
for W being Instruction of SCM+FSA st W is halting holds
W = [0,{},{}]