let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: for x being object st S1[r] holds
S1[r ^ <%x%>]
let x be object ; :: thesis: ( S1[r] implies S1[r ^ <%x%>] )
assume A12: S1[r] ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( ( 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: (((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; :: thesis: 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; :: thesis: ( 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))) ; :: thesis: (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 ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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))) ; :: thesis: (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 ;
:: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ;
:: thesis: 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; :: thesis: ( 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)) ; :: thesis: IC (Comput (P,s,i)) = i
A61: now :: thesis: ( 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)) ; :: thesis: ( ( 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)))) ) ; :: thesis: ( (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; :: thesis: 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 i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ; :: thesis: IC (Comput (P,s,i)) = i
hence IC (Comput (P,s,i)) = i by A21; :: thesis: verum
end;
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)))) ) ; :: thesis: IC (Comput (P,s,i)) = i
then ((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)) ;
:: thesis: 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))) ) ; :: thesis: IC (Comput (P,s,i)) = i
then ((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)) ;
:: thesis: verum
end;
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 :: thesis: ( ((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; :: thesis: ( 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)) ; :: thesis: IC (Comput (P,s,i)) = i
per cases ( i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) or i = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ) by A77, XXREAL_0:1;
suppose i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (P,s,i)) = i
hence IC (Comput (P,s,i)) = i by A59; :: thesis: verum
end;
suppose i = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (P,s,i)) = i
hence IC (Comput (P,s,i)) = i by A76; :: thesis: verum
end;
end;
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; :: thesis: ( 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) ; :: thesis: (((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 ; :: thesis: (((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
thus (((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 ; :: thesis: verum
end;
suppose A87: i <> len pp1 ; :: thesis: (((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 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 ;
:: thesis: verum
end;
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; :: thesis: ( 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; :: thesis: ( ( 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b
thus (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 ; :: thesis: verum
end;
hereby :: thesis: verum
let h be FinSeq-Location ; :: thesis: ( 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 ; :: thesis: (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = s . h
hence (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 ;
:: thesis: 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 :: thesis: for i being Nat st i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) holds
IC (Comput (P,s,i)) = i
let i be Nat; :: thesis: ( 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))%>) ; :: thesis: 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; :: thesis: verum
end;
assume {} c= pp ; :: thesis: 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 ; :: thesis: ( 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 = {} ; :: thesis: ( ( 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 :: thesis: for i being Nat st i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) holds
IC (Comput (P,s,i)) = i
let i be Nat; :: thesis: ( 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))%>) ; :: thesis: IC (Comput (P,s,i)) = i
then ( 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; :: thesis: 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; :: thesis: ( ((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) ; :: thesis: ( 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; :: thesis: ( ( 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 :: thesis: 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 . b
let b be Int-Location; :: thesis: ( 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 ; :: thesis: (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . b
thus (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 ; :: thesis: 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; :: thesis: 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 :: thesis: 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 . g
let g be FinSeq-Location ; :: thesis: ( g <> f implies (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . g )
assume g <> f ; :: thesis: (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . g
hence (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 ;
:: thesis: 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; :: thesis: 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; :: thesis: ( (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; :: thesis: ( ( 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; :: thesis: verum