environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, ARYTM_3, ORDINAL4, ARYTM_1, AMI_1, SCMFSA_2, RELAT_1, FUNCT_1, PARTFUN1, TARSKI, XXREAL_0, NAT_1, CARD_1, XBOOLE_0, INT_1, GRAPHSP, FINSEQ_2, AMI_3, PRE_POLY, FSM_1, CIRCUIT2, MSUALG_1, COMPLEX1, FUNCT_4, SCMFSA_7, EXTPRO_1, AFINSQ_1, FUNCOP_1, PBOOLE, FINSET_1, AMISTD_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, NAT_1, INT_2, NAT_D, INT_1, RELAT_1, PARTFUN1, FINSET_1, FINSEQ_1, AFINSQ_1, FINSEQ_2, FUNCT_1, FUNCOP_1, FUNCT_7, PBOOLE, XXREAL_0, MEMSTR_0, COMPOS_1, EXTPRO_1, SCMFSA_2, AFINSQ_2;
definitions ;
theorems FUNCT_1, SCMFSA_2, INT_1, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, RELAT_1, CARD_1, TARSKI, GRFUNC_1, ABSVALUE, FUNCT_7, XBOOLE_1, XREAL_1, XXREAL_0, FUNCOP_1, AMI_3, AFINSQ_1, AFINSQ_2, EXTPRO_1, PBOOLE, MEMSTR_0;
schemes NAT_1, STIRL2_1, AFINSQ_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, INT_1, FINSEQ_1, FUNCT_7, SCMFSA_2, FINSEQ_2, AFINSQ_1, FUNCOP_1, MEMSTR_0, PBOOLE, AMI_3, COMPOS_0, COMPOS_1;
constructors HIDDEN, REAL_1, AMI_3, SCMFSA_2, NAT_D, RELSET_1, PRE_POLY, AFINSQ_2, FUNCT_7;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities EXTPRO_1, FINSEQ_1, SCMFSA_2, AFINSQ_1, FUNCOP_1, MEMSTR_0, CARD_1, ORDINAL1, COMPOS_1;
expansions ;
Lm1:
for p1, p2, p3, p4 being XFinSequence holds
( ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ p2) ^ (p3 ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 )
Lm2:
for p1, p2, p3, p4, p5 being XFinSequence holds
( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
deffunc H1( Nat) -> Element of NAT = $1 -' 1;
definition
let f be
FinSeq-Location ;
let p be
FinSequence of
INT ;
existence
ex b1 being XFinSequence of the InstructionsF of SCM+FSA ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b1 = FlattenSeq pp )
uniqueness
for b1, b2 being XFinSequence of the InstructionsF of SCM+FSA st ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b1 = FlattenSeq pp ) & ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b2 = FlattenSeq pp ) holds
b1 = b2
correctness
;
end;
theorem Th4:
for
P being the
InstructionsF of
SCM+FSA -valued ManySortedSet of
NAT for
c0 being
Nat for
s being
b2 -started State of
SCM+FSA st
s . (intloc 0) = 1 holds
for
a being
Int-Location for
k being
Integer st
a <> intloc 0 & ( for
c being
Nat st
c in dom (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
( ( for
i being
Nat st
i <= len (aSeq (a,k)) holds
(
IC (Comput (P,s,i)) = c0 + i & ( for
b being
Int-Location st
b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Comput (P,s,i)) . f = s . f ) ) ) &
(Comput (P,s,(len (aSeq (a,k))))) . a = k )
theorem Th5:
for
P being the
InstructionsF of
SCM+FSA -valued ManySortedSet of
NAT for
s being
0 -started State of
SCM+FSA st
s . (intloc 0) = 1 holds
for
a being
Int-Location for
k being
Integer st
aSeq (
a,
k)
c= P &
a <> intloc 0 holds
( ( for
i being
Nat st
i <= len (aSeq (a,k)) holds
(
IC (Comput (P,s,i)) = i & ( for
b being
Int-Location st
b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Comput (P,s,i)) . f = s . f ) ) ) &
(Comput (P,s,(len (aSeq (a,k))))) . a = k )