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