let P be 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 f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )
set D = the InstructionsF of SCM+FSA;
set V = intloc 2;
set I = intloc 1;
set O = intloc 0;
A1:
intloc 1 <> intloc 0
by AMI_3:10;
A2:
intloc 1 <> intloc 2
by AMI_3:10;
let s be 0 -started State of SCM+FSA; ( s . (intloc 0) = 1 implies for f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) ) )
assume A3:
s . (intloc 0) = 1
; for f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )
let f be FinSeq-Location ; for p being FinSequence of INT st f := p c= P holds
( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )
let p be FinSequence of INT ; ( f := p c= P implies ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) ) )
assume A4:
f := p c= P
; ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )
set q = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA);
A5:
for i, k being Nat st i < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) holds
P . i = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) . i
by A4, GRFUNC_1:2, AFINSQ_1:86;
set q0 = (aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>;
consider pp being XFinSequence of the InstructionsF of SCM+FSA ^omega such that
A6:
len pp = len p
and
A7:
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))%> )
and
A8:
aSeq (f,p) = FlattenSeq pp
by Def3;
len (Stop SCM+FSA) = 1
by AFINSQ_1:34;
then
len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) = (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) + 1
by A8, AFINSQ_1:17;
then A9:
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA))
by NAT_1:13;
defpred S1[ XFinSequence] means ( $1 c= pp implies ex pp0 being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( pp0 = $1 & ( for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds
IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) ) );
A10:
intloc 2 <> intloc 0
by AMI_3:10;
A11:
for r being XFinSequence
for x being object st S1[r] holds
S1[r ^ <%x%>]
proof
let r be
XFinSequence;
for x being object st S1[r] holds
S1[r ^ <%x%>]let x be
object ;
( S1[r] implies S1[r ^ <%x%>] )
assume A12:
S1[
r]
;
S1[r ^ <%x%>]
set r1 =
len r;
len <%x%> = 1
by AFINSQ_1:34;
then
len (r ^ <%x%>) = (len r) + 1
by AFINSQ_1:17;
then
len r < len (r ^ <%x%>)
by XREAL_1:29;
then A13:
len r in dom (r ^ <%x%>)
by AFINSQ_1:86;
assume A14:
r ^ <%x%> c= pp
;
ex pp0 being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( pp0 = r ^ <%x%> & ( for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds
IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) )
then A15:
dom (r ^ <%x%>) c= dom pp
by GRFUNC_1:2;
then A16:
len r < len pp
by A13, AFINSQ_1:86;
then consider pr1 being
Integer such that A17:
pr1 = p . ((len r) + 1)
and A18:
pp . (len r) = ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>
by A7;
( 1
<= (len r) + 1 &
(len r) + 1
<= len pp )
by A16, NAT_1:11, NAT_1:13;
then A19:
(len r) + 1
in Seg (len pp)
;
r c= r ^ <%x%>
by AFINSQ_1:74;
then consider pp0 being
XFinSequence of the
InstructionsF of
SCM+FSA ^omega such that A20:
pp0 = r
and A21:
for
i being
Nat st
i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds
IC (Comput (P,s,i)) = i
and A22:
((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0)
and A23:
len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p
and A24:
for
b being
Int-Location st
b <> intloc 1 &
b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b
and A25:
for
h being
FinSeq-Location st
h <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . h = s . h
by A12, A14, XBOOLE_1:1;
A26:
x =
(r ^ <%x%>) . (len r)
by AFINSQ_1:36
.=
pp . (len r)
by A14, A13, GRFUNC_1:2
;
then
x in the
InstructionsF of
SCM+FSA ^omega
by A13, A15, FUNCT_1:102;
then reconsider pp1 =
pp0 ^ <%x%> as
XFinSequence of the
InstructionsF of
SCM+FSA ^omega ;
take
pp1
;
( pp1 = r ^ <%x%> & ( for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds
IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) )
thus
pp1 = r ^ <%x%>
by A20;
( ( for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds
IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) )
reconsider x =
x as
Element of the
InstructionsF of
SCM+FSA ^omega by A13, A15, A26, FUNCT_1:102;
A27:
FlattenSeq pp1 =
(FlattenSeq pp0) ^ (FlattenSeq <%x%>)
by AFINSQ_2:75
.=
(FlattenSeq pp0) ^ x
by AFINSQ_2:73
;
A28:
Seg (len p) = dom p
by FINSEQ_1:def 3;
len pp1 <= len p
by A6, A14, A20, NAT_1:43;
then A29:
Seg (len pp1) c= Seg (len p)
by FINSEQ_1:5;
then A30:
dom (p | (Seg (len pp1))) = Seg (len pp1)
by A28, RELAT_1:62;
set c2 =
len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))));
set c1 =
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0));
set s1 =
Comput (
P,
s,
(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))));
set s2 =
Comput (
P,
s,
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))));
A31:
x = (aSeq ((intloc 1),((len r) + 1))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>)
by A18, A26, AFINSQ_1:27;
then A32:
(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) =
(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>)))
by A27, AFINSQ_1:27
.=
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>)))
by AFINSQ_1:17
.=
len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>))
by Lm2
.=
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>))
by AFINSQ_1:17
.=
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + ((len (aSeq ((intloc 2),pr1))) + (len <%((f,(intloc 1)) := (intloc 2))%>))
by AFINSQ_1:17
.=
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + ((len (aSeq ((intloc 2),pr1))) + 1)
by AFINSQ_1:33
.=
((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) + 1
;
then A33:
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) = ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) + 1
by AFINSQ_1:17;
A34:
FlattenSeq pp1 c= FlattenSeq pp
by A14, A20, AFINSQ_2:82;
A35:
now for p being XFinSequence st p c= x holds
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)let p be
XFinSequence;
( p c= x implies (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA) )assume
p c= x
;
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)then
(FlattenSeq pp0) ^ p c= (FlattenSeq pp0) ^ x
by AFINSQ_2:81;
then
(FlattenSeq pp0) ^ p c= FlattenSeq pp
by A34, A27, XBOOLE_1:1;
then
((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((FlattenSeq pp0) ^ p) c= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)
by AFINSQ_2:81;
then A36:
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)
by AFINSQ_1:27;
((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)
by A8, AFINSQ_1:74;
hence
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)
by A36, XBOOLE_1:1;
verum end;
IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))
by A21;
then reconsider s1 =
Comput (
P,
s,
(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))) as
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) -started State of
SCM+FSA by MEMSTR_0:def 12;
A37:
s1 . (intloc 0) = 1
by A1, A10, A3, A24;
A38:
for
c being
Nat st
c in dom (aSeq ((intloc 1),((len r) + 1))) holds
(aSeq ((intloc 1),((len r) + 1))) . c = P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c)
proof
let c be
Nat;
( c in dom (aSeq ((intloc 1),((len r) + 1))) implies (aSeq ((intloc 1),((len r) + 1))) . c = P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) )
assume A39:
c in dom (aSeq ((intloc 1),((len r) + 1)))
;
(aSeq ((intloc 1),((len r) + 1))) . c = P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c)
then A40:
(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c in dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))
by AFINSQ_1:23;
A41:
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)
by A31, A35, AFINSQ_1:74;
then A42:
dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) c= dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA))
by GRFUNC_1:2;
thus (aSeq ((intloc 1),((len r) + 1))) . c =
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c)
by A39, AFINSQ_1:def 3
.=
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c)
by A41, A40, GRFUNC_1:2
.=
P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c)
by A4, A42, A40, GRFUNC_1:2
;
verum
end;
then A43:
(Comput (P,s1,(len (aSeq ((intloc 1),((len r) + 1)))))) . (intloc 1) = (len r) + 1
by Th4, A37, A1;
A44:
((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1) = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x
by A27, AFINSQ_1:27;
then
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA))
by A35, NAT_1:43;
then A45:
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA))
by A33, NAT_1:13;
A46:
now for i being Nat st i <= len (aSeq ((intloc 1),((len r) + 1))) holds
(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i)))let i be
Nat;
( i <= len (aSeq ((intloc 1),((len r) + 1))) implies (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) )assume
i <= len (aSeq ((intloc 1),((len r) + 1)))
;
(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i)))hence (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i =
IC (Comput (P,s1,i))
by A38, Th4, A37, A1
.=
IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i)))
by EXTPRO_1:4
;
verum end;
set c3 =
len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)));
A47:
len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) = (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))
by AFINSQ_1:17;
A48:
len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) = (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (aSeq ((intloc 1),((len r) + 1))))
by AFINSQ_1:17;
then A49:
Comput (
P,
s,
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))))
= Comput (
P,
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))),
(len (aSeq ((intloc 1),((len r) + 1)))))
by EXTPRO_1:4;
IC (Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))))) = len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))
by A48, A49, A38, Th4, A37, A1;
then reconsider s2 =
Comput (
P,
s,
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))) as
len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) -started State of
SCM+FSA by MEMSTR_0:def 12;
A50:
s2 . (intloc 0) = 1
by A49, A38, Th4, A37, A1;
A51:
for
c being
Nat st
c in dom (aSeq ((intloc 2),pr1)) holds
(aSeq ((intloc 2),pr1)) . c = P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c)
proof
let c be
Nat;
( c in dom (aSeq ((intloc 2),pr1)) implies (aSeq ((intloc 2),pr1)) . c = P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) )
assume A52:
c in dom (aSeq ((intloc 2),pr1))
;
(aSeq ((intloc 2),pr1)) . c = P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c)
then A53:
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c in dom (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))
by AFINSQ_1:23;
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)
by A18, A26, A35, AFINSQ_1:74;
then A54:
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)
by AFINSQ_1:27;
then A55:
dom (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) c= dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA))
by GRFUNC_1:2;
thus (aSeq ((intloc 2),pr1)) . c =
(((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c)
by A52, AFINSQ_1:def 3
.=
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c)
by A53, A54, GRFUNC_1:2
.=
P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c)
by A4, A55, A53, GRFUNC_1:2
;
verum
end;
then A56:
(Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . (intloc 2) = pr1
by Th4, A50, A10;
A57:
(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) . f =
(Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))))) . f
by AFINSQ_1:17
.=
(Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . f
by EXTPRO_1:4
.=
s2 . f
by A51, Th4, A50, A10
.=
s1 . f
by A49, A38, Th4, A37, A1
;
A58:
now for i being Nat st i <= len (aSeq ((intloc 2),pr1)) holds
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i = IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i)))let i be
Nat;
( i <= len (aSeq ((intloc 2),pr1)) implies (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i = IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i))) )assume
i <= len (aSeq ((intloc 2),pr1))
;
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i = IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i)))hence (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i =
IC (Comput (P,s2,i))
by A51, Th4, A50, A10
.=
IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i)))
by EXTPRO_1:4
;
verum end;
A59:
for
i being
Nat st
i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds
IC (Comput (P,s,i)) = i
proof
let i be
Nat;
( i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) implies IC (Comput (P,s,i)) = i )
assume A60:
i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))
;
IC (Comput (P,s,i)) = i
A61:
now ( not i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) & ( not (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ) implies ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) )A62:
i < (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1))
by A60, AFINSQ_1:17;
assume A63:
not
i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))
;
( ( not (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ) implies ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) )assume
( not
(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1
<= i or not
i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) )
;
( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) )hence
(
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1
<= i &
i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) )
by A32, A63, A62, NAT_1:13;
verum end;
per cases
( i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) or ( (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ) or ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) )
by A61;
suppose A64:
(
(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1
<= i &
i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) )
;
IC (Comput (P,s,i)) = ithen
((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1) - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) <= i - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))
by XREAL_1:9;
then reconsider ii =
i - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) as
Element of
NAT by INT_1:3;
i - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))
by A64, XREAL_1:9;
hence i =
IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ii)))
by A48, A46
.=
IC (Comput (P,s,i))
;
verum end; suppose A65:
(
(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1
<= i &
i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) )
;
IC (Comput (P,s,i)) = ithen
((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1) - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) <= i - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))
by XREAL_1:9;
then reconsider ii =
i - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) as
Element of
NAT by INT_1:3;
i - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) <= ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))
by A65, XREAL_1:9;
hence i =
IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + ii)))
by A58
.=
IC (Comput (P,s,i))
;
verum end;
end;
A66:
len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) = ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))
by A48, AFINSQ_1:17;
A67:
P /. (IC (Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) = P . (IC (Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))
by PBOOLE:143;
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)
by A35;
then consider rq being
XFinSequence of the
InstructionsF of
SCM+FSA such that A68:
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) ^ rq = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)
by AFINSQ_2:80;
A69:
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) = ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) + 1
by A32, AFINSQ_1:17;
then A70:
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) > (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))
by NAT_1:13;
then A71:
len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) in dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x)
by A44, A47, AFINSQ_1:66;
A72:
0 in dom <%((f,(intloc 1)) := (intloc 2))%>
by TARSKI:def 1;
len <%((f,(intloc 1)) := (intloc 2))%> = 1
by AFINSQ_1:34;
then
len (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>) = (len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 1
by AFINSQ_1:17;
then
len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) < len (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>)
by XREAL_1:29;
then A73:
len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) in dom (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>)
by AFINSQ_1:66;
CurInstr (
P,
(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) =
P . (len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))
by A47, A59, A67, A70
.=
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) . (len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))
by A5, A47, A45
.=
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ((len (aSeq ((intloc 1),((len r) + 1)))) + (len (aSeq ((intloc 2),pr1)))))
by A66, A71, A68, AFINSQ_1:def 3
.=
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1)))))
by AFINSQ_1:17
;
then A74:
CurInstr (
P,
(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) =
(((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>) . ((len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 0)
by A73, A18, A26, AFINSQ_1:def 3
.=
<%((f,(intloc 1)) := (intloc 2))%> . 0
by A72, AFINSQ_1:def 3
.=
(
f,
(intloc 1))
:= (intloc 2)
;
A75:
Comput (
P,
s,
((len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))) + 1)) =
Following (
P,
(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))
by EXTPRO_1:3
.=
Exec (
((f,(intloc 1)) := (intloc 2)),
(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))
by A74
;
then A76:
IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) =
(IC (Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) + 1
by A47, A33, SCMFSA_2:73
.=
len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))
by A47, A69, A59, A70
;
thus
for
i being
Nat st
i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds
IC (Comput (P,s,i)) = i
( ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) )proof
let i be
Nat;
( i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) implies IC (Comput (P,s,i)) = i )
assume A77:
i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))
;
IC (Comput (P,s,i)) = i
end;
A78:
(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) . (intloc 2) =
(Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))))) . (intloc 2)
by AFINSQ_1:17
.=
p . ((len r) + 1)
by A17, A56, EXTPRO_1:4
;
consider ki being
Nat such that A79:
ki = |.((Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) . (intloc 1)).|
and A80:
(Exec (((f,(intloc 1)) := (intloc 2)),(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))) . f = ((Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) . f) +* (
ki,
((Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) . (intloc 2)))
by SCMFSA_2:73;
A81:
ki =
|.((Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))))) . (intloc 1)).|
by A79, AFINSQ_1:17
.=
|.((Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . (intloc 1)).|
by EXTPRO_1:4
.=
|.(s2 . (intloc 1)).|
by A2, A51, Th4, A50, A10
.=
(len r) + 1
by A49, A43, ABSVALUE:def 1
;
A82:
dom (s1 . f) = Seg (len p)
by A23, FINSEQ_1:def 3;
for
i being
Nat st
i in Seg (len pp1) holds
(((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
proof
let i be
Nat;
( i in Seg (len pp1) implies (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i )
assume A83:
i in Seg (len pp1)
;
(((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
then A84:
i <= len pp1
by FINSEQ_1:1;
len <%x%> = 1
by AFINSQ_1:34;
then A85:
len pp1 = (len pp0) + 1
by AFINSQ_1:17;
per cases
( i = len pp1 or i <> len pp1 )
;
suppose A86:
i = len pp1
;
(((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . ithus (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i =
((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) . i
by A47, A69, A75, A80, A81, A78, A57, A86, A85, FINSEQ_1:4, FUNCT_1:49
.=
p . i
by A20, A6, A82, A86, A19, A85, FUNCT_7:31
.=
(p | (Seg (len pp1))) . i
by A86, A85, FINSEQ_1:4, FUNCT_1:49
;
verum end; suppose A87:
i <> len pp1
;
(((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . ithen
i < (len pp0) + 1
by A85, A84, XXREAL_0:1;
then A88:
i <= len pp0
by NAT_1:13;
1
<= i
by A83, FINSEQ_1:1;
then A89:
i in Seg (len pp0)
by A88;
(((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i =
((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) . i
by A47, A69, A75, A80, A81, A78, A57, A83, FUNCT_1:49
.=
(s1 . f) . i
by A85, A20, A87, FUNCT_7:32
;
hence (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i =
(p | (Seg (len pp0))) . i
by A22, A89, FUNCT_1:49
.=
p . i
by A89, FUNCT_1:49
.=
(p | (Seg (len pp1))) . i
by A83, FUNCT_1:49
;
verum end;
end;
then A90:
for
i being
object st
i in Seg (len pp1) holds
(((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
;
A91:
dom ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) = dom (s1 . f)
by FUNCT_7:30;
dom ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) =
dom ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1))))
by A33, A75, A80, A81, A78, A57, AFINSQ_1:17
.=
Seg (len p)
by A23, A91, FINSEQ_1:def 3
;
then
dom (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) = Seg (len pp1)
by A29, RELAT_1:62;
hence
((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1)
by A30, A90, FUNCT_1:2;
( len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) )
len ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) = len (s1 . f)
by A91, FINSEQ_3:29;
hence
len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p
by A23, A33, A75, A80, A81, A78, A57, AFINSQ_1:17;
( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) )
hereby for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g
let b be
Int-Location;
( b <> intloc 1 & b <> intloc 2 implies (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b )assume that A92:
b <> intloc 1
and A93:
b <> intloc 2
;
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . bthus (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b =
(Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))))) . b
by A47, A33, A75, SCMFSA_2:73
.=
(Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . b
by EXTPRO_1:4
.=
s2 . b
by A51, A93, Th4, A50, A10
.=
s1 . b
by A49, A38, A92, Th4, A37, A1
.=
s . b
by A24, A92, A93
;
verum
end;
hereby verum
let h be
FinSeq-Location ;
( h <> f implies (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = s . h )assume A94:
h <> f
;
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = s . hhence (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h =
(Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))))) . h
by A47, A33, A75, SCMFSA_2:73
.=
(Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . h
by EXTPRO_1:4
.=
s2 . h
by A51, Th4, A50, A10
.=
s1 . h
by A49, A38, Th4, A37, A1
.=
s . h
by A25, A94
;
verum
end;
end;
set k = len (aSeq ((intloc 1),(len p)));
len <%(f :=<0,...,0> (intloc 1))%> = 1
by AFINSQ_1:34;
then A95:
len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) = (len (aSeq ((intloc 1),(len p)))) + 1
by AFINSQ_1:17;
A96:
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA) = ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((aSeq (f,p)) ^ (Stop SCM+FSA))
by AFINSQ_1:27;
then
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA) = (aSeq ((intloc 1),(len p))) ^ (<%(f :=<0,...,0> (intloc 1))%> ^ ((aSeq (f,p)) ^ (Stop SCM+FSA)))
by AFINSQ_1:27;
then
aSeq ((intloc 1),(len p)) c= f := p
by AFINSQ_1:74;
then A97:
aSeq ((intloc 1),(len p)) c= P
by A4, XBOOLE_1:1;
then A98:
(Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . (intloc 1) = len p
by A1, A3, Th5;
A99:
S1[ {} ]
proof
A100:
now for i being Nat st i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) holds
IC (Comput (P,s,i)) = ilet i be
Nat;
( i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies IC (Comput (P,s,i)) = i )assume A101:
i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)
;
IC (Comput (P,s,i)) = i
(
i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies
i <= len (aSeq ((intloc 1),(len p))) )
by A95, NAT_1:13;
hence
IC (Comput (P,s,i)) = i
by A1, A3, A97, A101, Th5;
verum end;
assume
{} c= pp
;
ex pp0 being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( pp0 = {} & ( for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds
IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) )
reconsider sD =
<%> ( the InstructionsF of SCM+FSA ^omega) as
XFinSequence of the
InstructionsF of
SCM+FSA ^omega ;
take
sD
;
( sD = {} & ( for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD)) holds
IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
A102:
((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega))) =
((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (<%> the InstructionsF of SCM+FSA)
by AFINSQ_2:74
.=
((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ {}
.=
(aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>
;
A103:
len (aSeq ((intloc 1),(len p))) < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)
by A95, NAT_1:13;
then A104:
IC (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) = len (aSeq ((intloc 1),(len p)))
by A100;
A105:
P /. (IC (Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) = P . (IC (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))))
by PBOOLE:143;
len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) = (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len ((aSeq (f,p)) ^ (Stop SCM+FSA)))
by A96, AFINSQ_1:17;
then
len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA))
by NAT_1:11;
then A106:
len (aSeq ((intloc 1),(len p))) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA))
by A95, NAT_1:13;
A107:
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA) = ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((aSeq (f,p)) ^ (Stop SCM+FSA))
by AFINSQ_1:27;
A108:
len (aSeq ((intloc 1),(len p))) in dom ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)
by A103, AFINSQ_1:66;
A109:
CurInstr (
P,
(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) =
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) . (len (aSeq ((intloc 1),(len p))))
by A5, A104, A105, A106
.=
((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) . (len (aSeq ((intloc 1),(len p))))
by A107, A108, AFINSQ_1:def 3
.=
f :=<0,...,0> (intloc 1)
by AFINSQ_1:36
;
thus
sD = {}
;
( ( for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD)) holds
IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
A110:
Comput (
P,
s,
(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>))) =
Following (
P,
(Comput (P,s,(len (aSeq ((intloc 1),(len p)))))))
by A95, EXTPRO_1:3
.=
Exec (
(f :=<0,...,0> (intloc 1)),
(Comput (P,s,(len (aSeq ((intloc 1),(len p)))))))
by A109
;
then A111:
IC (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) = len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)
by A95, A104, SCMFSA_2:75;
now for i being Nat st i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) holds
IC (Comput (P,s,i)) = ilet i be
Nat;
( i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies IC (Comput (P,s,i)) = i )assume
i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)
;
IC (Comput (P,s,i)) = ithen
(
i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) or
i = len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) )
by XXREAL_0:1;
hence
IC (Comput (P,s,i)) = i
by A100, A111;
verum end;
hence
for
i being
Nat st
i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD)) holds
IC (Comput (P,s,i)) = i
by A102;
( ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
consider ki being
Nat such that A112:
ki = |.((Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . (intloc 1)).|
and A113:
(Exec ((f :=<0,...,0> (intloc 1)),(Comput (P,s,(len (aSeq ((intloc 1),(len p)))))))) . f = ki |-> 0
by SCMFSA_2:75;
((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | 0 = p | (len sD)
;
hence
((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD)
;
( len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
ki = len p
by A98, A112, ABSVALUE:def 1;
hence
len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p
by A102, A110, A113, CARD_1:def 7;
( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
now for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . blet b be
Int-Location;
( b <> intloc 1 & b <> intloc 2 implies (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . b )assume that A114:
b <> intloc 1
and
b <> intloc 2
;
(Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . bthus (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b =
(Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . b
by A110, SCMFSA_2:75
.=
s . b
by A1, A3, A97, A114, Th5
;
verum end;
hence
for
b being
Int-Location st
b <> intloc 1 &
b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b
by A102;
for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g
now for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . glet g be
FinSeq-Location ;
( g <> f implies (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . g )assume
g <> f
;
(Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . ghence (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g =
(Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . g
by A110, SCMFSA_2:75
.=
s . g
by A1, A3, A97, Th5
;
verum end;
hence
for
g being
FinSeq-Location st
g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g
by A102;
verum
end;
for r being XFinSequence holds S1[r]
from AFINSQ_1:sch 3(A99, A11);
then consider pp0 being XFinSequence of the InstructionsF of SCM+FSA ^omega such that
A115:
pp0 = pp
and
A116:
for i being Nat st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds
IC (Comput (P,s,i)) = i
and
A117:
((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0)
and
A118:
len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p
and
A119:
( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) )
;
A120:
P /. (IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) = P . (IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))))
by PBOOLE:143;
IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))
by A115, A116;
then A121: CurInstr (P,(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) =
((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop SCM+FSA)) . (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))
by A5, A9, A120
.=
halt SCM+FSA
by A8, AFINSQ_1:36
;
hence
P halts_on s
by EXTPRO_1:29; ( (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )
then A122:
Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))) = Result (P,s)
by A121, EXTPRO_1:def 9;
A123:
Seg (len pp0) = dom p
by A6, A115, FINSEQ_1:def 3;
(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f = ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0)
by A6, A115, A118, FINSEQ_3:113;
hence
(Result (P,s)) . f = p
by A123, A115, A122, A117; ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )
thus
( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result (P,s)) . g = s . g ) )
by A115, A119, A122; verum