environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, SETFAM_1, AMI_1, FSM_1, FUNCT_4, FUNCOP_1, RELAT_1, TARSKI, STRUCT_0, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2, CAT_1, NAT_1, GLIB_000, XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, CARD_1, GOBOARD5, FUNCT_2, FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, AMISTD_1, EXTPRO_1, COMPOS_1, AMISTD_2, SCMFSA6B, QUANTAL1, GOBRD13, MEMSTR_0, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, ORDINAL1, CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1, PARTFUN1, XTUPLE_0, MCART_1, VALUED_1, DOMAIN_1, CARD_3, FINSEQ_1, FINSEQ_4, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_7, AFINSQ_1, PBOOLE, MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_2;
definitions TARSKI, COMPOS_1, EXTPRO_1, XBOOLE_0, MEMSTR_0, FUNCT_1, COMPOS_0;
theorems TARSKI, FINSEQ_4, FINSEQ_1, NAT_1, FUNCT_4, FUNCT_1, FUNCT_2, ENUMSET1, ZFMISC_1, FUNCOP_1, CARD_3, ORDINAL1, FINSEQ_3, INT_1, SETFAM_1, REVROT_1, EXTPRO_1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, COMPOS_1, FUNCT_7, PARTFUN1, XREAL_0, NAT_D, PBOOLE, MEMSTR_0, GRFUNC_1, PARTFUN2, MEASURE6, RELAT_1;
schemes NAT_1, FINSEQ_2, FUNCT_2;
registrations SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, STRUCT_0, CARD_1, RELSET_1, FUNCT_4, AFINSQ_1, COMPOS_1, EXTPRO_1, PRE_POLY, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0, INT_1;
constructors HIDDEN, WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, COMPOS_1, EXTPRO_1, RELSET_1, PRE_POLY, GRAPH_2, AFINSQ_1, MCART_1, FUNCT_7, PBOOLE, XXREAL_1, FUNCT_4, MEASURE6, MEMSTR_0, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, REAL, SUBSET, ARITHM;
equalities STRUCT_0, COMPOS_1, EXTPRO_1, XBOOLE_0, MEMSTR_0, FUNCOP_1, NAT_1, AFINSQ_1, COMPOS_0, ORDINAL1;
expansions XBOOLE_0, MEMSTR_0;
Lm1:
now for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Element of the InstructionsF of S
for l being Nat
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)
let N be
with_zero set ;
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Element of the InstructionsF of S
for l being Nat
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)let S be non
empty with_non-empty_values IC-Ins-separated AMI-Struct over
N;
for i being Element of the InstructionsF of S
for l being Nat
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)let i be
Element of the
InstructionsF of
S;
for l being Nat
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)let l be
Nat;
for s being State of S
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)let s be
State of
S;
for P being Instruction-Sequence of S holds IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)let P be
Instruction-Sequence of
S;
IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (i,l)reconsider t =
s +* (
(IC ),
l) as
Element of
product (the_Values_of S) by CARD_3:107;
l in NAT
by ORDINAL1:def 12;
then A1:
l in dom P
by PARTFUN1:def 2;
IC in dom s
by MEMSTR_0:2;
then A2:
IC t = l
by FUNCT_7:31;
then CurInstr (
(P +* (l,i)),
t) =
(P +* (l,i)) . l
by PBOOLE:143
.=
i
by A1, FUNCT_7:31
;
hence
IC (Following ((P +* (l,i)),(s +* ((IC ),l)))) in NIC (
i,
l)
by A2;
verum
end;
Lm2:
for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N ex f being non empty FinSequence of NAT st
( f /. 1 = k & f /. (len f) = k & ( for n being Nat st 1 <= n & n < len f holds
f /. (n + 1) in SUCC ((f /. n),S) ) )
set III = {[1,{},{}],[0,{},{}]};
definition
let N be
with_zero set ;
func STC N -> strict AMI-Struct over
N means :
Def7:
( the
carrier of
it = {0} &
IC = 0 & the
InstructionsF of
it = {[0,0,0],[1,0,0]} & the
Object-Kind of
it = 0 .--> 0 & the
ValuesF of
it = N --> NAT & ex
f being
Function of
(product (the_Values_of it)),
(product (the_Values_of it)) st
( ( for
s being
Element of
product (the_Values_of it) holds
f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the
Execution of
it = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of it)))) ) );
existence
ex b1 being strict AMI-Struct over N st
( the carrier of b1 = {0} & IC = 0 & the InstructionsF of b1 = {[0,0,0],[1,0,0]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & ex f being Function of (product (the_Values_of b1)),(product (the_Values_of b1)) st
( ( for s being Element of product (the_Values_of b1) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b1)))) ) )
uniqueness
for b1, b2 being strict AMI-Struct over N st the carrier of b1 = {0} & IC = 0 & the InstructionsF of b1 = {[0,0,0],[1,0,0]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & ex f being Function of (product (the_Values_of b1)),(product (the_Values_of b1)) st
( ( for s being Element of product (the_Values_of b1) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b1 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b1)))) ) & the carrier of b2 = {0} & IC = 0 & the InstructionsF of b2 = {[0,0,0],[1,0,0]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & ex f being Function of (product (the_Values_of b2)),(product (the_Values_of b2)) st
( ( for s being Element of product (the_Values_of b2) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b2)))) ) holds
b1 = b2
end;
::
deftheorem Def7 defines
STC AMISTD_1:def 7 :
for N being with_zero set
for b2 being strict AMI-Struct over N holds
( b2 = STC N iff ( the carrier of b2 = {0} & IC = 0 & the InstructionsF of b2 = {[0,0,0],[1,0,0]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & ex f being Function of (product (the_Values_of b2)),(product (the_Values_of b2)) st
( ( for s being Element of product (the_Values_of b2) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of b2 = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of b2)))) ) ) );
Lm3:
for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec (i,s)) . (IC ) = (IC s) + 1
Lm4:
for z being Nat
for N being with_zero set
for l being Nat
for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
Lm5:
for N being with_zero set
for i being Element of the InstructionsF of (STC N) holds JUMP i is empty
canceled;
Lm6:
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for F being preProgram of S holds
( F is really-closed iff for s being State of S st IC s in dom F holds
for P being Instruction-Sequence of S st F c= P holds
for k being Nat holds IC (Comput (P,s,k)) in dom F )