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:52;
A2: intloc 1 <> intloc 2 by AMI_3:52;
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= s holds
( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) ) )
assume A4: s . (intloc 0) = 1 ; :: thesis: for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) )
let f be FinSeq-Location ; :: thesis: for p being FinSequence of INT st f := p c= s holds
( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) )
let p be FinSequence of INT ; :: thesis: ( f := p c= s implies ( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) ) )
assume A5: f := p c= s ; :: thesis: ( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) )
set q = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>;

A9: 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 (Comput ((ProgramPart s),s,k)) . 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: (Comput ((ProgramPart s),s,k)) . i = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . i
then A10: i in dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by NAT_1:45;
thus (Comput ((ProgramPart s),s,k)) . i = s . i by AMI_1:54
.= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . i by A5, A10, GRFUNC_1:8 ; :: 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
A15: len pp = len p and
A16: 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
A17: aSeq (f,p) = FlattenSeq pp by Def4;
len <%(halt SCM+FSA)%> = 1 by AFINSQ_1:38;
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 A17, AFINSQ_1:20;
then A18: 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 S₁[ 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 ((ProgramPart s),s,i)) = i ) & ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) ) );
A19: intloc 2 <> intloc 0 by AMI_3:52;
A20: for r being XFinSequence
for x being set st S₁[r] holds
S₁[r ^ <%x%>]

proof

let r be XFinSequence; :: thesis: for x being set st S₁[r] holds
S₁[r ^ <%x%>]
let x be set ; :: thesis: ( S₁[r] implies S₁[r ^ <%x%>] )
assume A21: S₁[r] ; :: thesis: S₁[r ^ <%x%>]
set r1 = len r;
len <%x%> = 1 by AFINSQ_1:38;
then len (r ^ <%x%>) = (len r) + 1 by AFINSQ_1:20;
then len r < len (r ^ <%x%>) by XREAL_1:31;
then A22: len r in dom (r ^ <%x%>) by NAT_1:45;
assume A23: 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 ((ProgramPart s),s,i)) = i ) & ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) )
then A24: dom (r ^ <%x%>) c= dom pp by GRFUNC_1:8;
then uu: len r < len pp by A22, NAT_1:45;
then consider pr1 being Integer such that
A26: pr1 = p . ((len r) + 1) and
A27: pp . (len r) = ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%> by A16;
( 1 <= (len r) + 1 & (len r) + 1 <= len pp ) by uu, NAT_1:11, NAT_1:13;
then OO: (len r) + 1 in Seg (len pp) ;
r c= r ^ <%x%> by AFINSQ_1:78;
then consider pp0 being XFinSequence of the Instructions of SCM+FSA ^omega such that
A28: pp0 = r and
A29: for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds
IC (Comput ((ProgramPart s),s,i)) = i and
A30: ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) and
A31: len ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p and
A32: for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b and
A33: for h being FinSeq-Location st h <> f holds
(Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . h = s . h by A21, A23, XBOOLE_1:1;
A34: x = (r ^ <%x%>) . (len r) by AFINSQ_1:40
.= pp . (len r) by A23, A22, GRFUNC_1:8 ;
then x in the Instructions of SCM+FSA ^omega by A22, A24, FUNCT_1:172;
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 ((ProgramPart s),s,i)) = i ) & ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) )
thus pp1 = r ^ <%x%> by A28; :: 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 ((ProgramPart s),s,i)) = i ) & ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),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 A22, A24, A34, FUNCT_1:172;
A35: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <%x%>) by AFINSQ_2:87
.= (FlattenSeq pp0) ^ x by AFINSQ_2:85 ;
TT: Seg (len p) = dom p by FINSEQ_1:def 3;
len pp1 <= len p by A15, A23, A28, NAT_1:44;
then FF: Seg (len pp1) c= Seg (len p) by FINSEQ_1:7;
then A37: dom (p | (Seg (len pp1))) = Seg (len pp1) by TT, RELAT_1:91;
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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))));
set s2 = Comput ((ProgramPart s),s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))));
A41: x = (aSeq ((intloc 1),((len r) + 1))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>) by A27, A34, AFINSQ_1:30;
then A42: (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 A35, AFINSQ_1:30
.= 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:20
.= 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 Lm3
.= (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:20
.= (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:20
.= (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:36
.= ((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 A43: 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:20;
A44: FlattenSeq pp1 c= FlattenSeq pp by A23, A28, AFINSQ_2:94;

A45: 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_1:79, AFINSQ_1:82, AFINSQ_2:93;
then (FlattenSeq pp0) ^ p c= FlattenSeq pp by A44, A35, 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_1:79, AFINSQ_1:82, AFINSQ_2:93;
then A46: (((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:30;
((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 A17, AFINSQ_1:78;
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 A46, XBOOLE_1:1; :: thesis: verum

end;

IC (Comput ((ProgramPart s),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 A29;
then reconsider s1 = Comput ((ProgramPart s),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 COMPOS_1:def 20;
B47: s1 . (intloc 0) = 1 by A1, A19, A4, A32;
A47: for c being Element of NAT st c in dom (aSeq ((intloc 1),((len r) + 1))) holds
(aSeq ((intloc 1),((len r) + 1))) . c = s1 . ((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 = s1 . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) )
assume A48: c in dom (aSeq ((intloc 1),((len r) + 1))) ; :: thesis: (aSeq ((intloc 1),((len r) + 1))) . c = s1 . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c)
then A49: (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:26;
A51: (((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 A41, A45, AFINSQ_1:78;
then B52: 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:8;
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 A48, AFINSQ_1:def 4
.= ((((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 A51, A49, GRFUNC_1:8
.= s . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) by A5, B52, A49, GRFUNC_1:8
.= s1 . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) by AMI_1:54 ; :: thesis: verum

end;

then A53: (Comput ((ProgramPart s1),s1,(len (aSeq ((intloc 1),((len r) + 1)))))) . (intloc 1) = (len r) + 1 by Th36, B47, A1;
A54: ((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 A35, AFINSQ_1:30;
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 A45, NAT_1:44;
then A55: (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 A43, NAT_1:13;

A56: 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 ((ProgramPart s),s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) )
T: ProgramPart s = ProgramPart s1 by AMI_1:123;
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 ((ProgramPart s),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 ((ProgramPart s),s1,i)) by A47, Th36, T, B47, A1
.= IC (Comput ((ProgramPart s),s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) by EXTPRO_1:5 ;
:: 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)));
A57: 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:20;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) by AMI_1:123;
A58: 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:20;
then A59: Comput ((ProgramPart s),s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))),(len (aSeq ((intloc 1),((len r) + 1))))) by EXTPRO_1:5;
IC (Comput ((ProgramPart s),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 A58, A59, A47, Th36, T, B47, A1;
then reconsider s2 = Comput ((ProgramPart s),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 COMPOS_1:def 20;
B60: s2 . (intloc 0) = 1 by A59, A47, Th36, T, B47, A1;
A60: for c being Element of NAT st c in dom (aSeq ((intloc 2),pr1)) holds
(aSeq ((intloc 2),pr1)) . c = s2 . ((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 = s2 . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) )
assume A61: c in dom (aSeq ((intloc 2),pr1)) ; :: thesis: (aSeq ((intloc 2),pr1)) . c = s2 . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c)
then A62: (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:26;
(((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 A27, A34, A45, AFINSQ_1:78;
then A64: ((((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:30;
then B65: 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:8;
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 A61, AFINSQ_1:def 4
.= ((((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 A62, A64, GRFUNC_1:8
.= s . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) by A5, B65, A62, GRFUNC_1:8
.= s2 . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) by AMI_1:54 ; :: thesis: verum

end;

then A66: (Comput ((ProgramPart s2),s2,(len (aSeq ((intloc 2),pr1))))) . (intloc 2) = pr1 by Th36, B60, A19;
S: ProgramPart s = ProgramPart s2 by AMI_1:123;
A67: (Comput ((ProgramPart s),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 ((ProgramPart s),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:20
.= (Comput ((ProgramPart s),s2,(len (aSeq ((intloc 2),pr1))))) . f by EXTPRO_1:5
.= s2 . f by A60, Th36, S, B60, A19
.= s1 . f by A59, A47, Th36, T, B47, A1 ;

A68: 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 ((ProgramPart s),s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i))) )
T: ProgramPart s = ProgramPart s2 by AMI_1:123;
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 ((ProgramPart s),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 ((ProgramPart s),s2,i)) by A60, Th36, T, B60, A19
.= IC (Comput ((ProgramPart s),s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i))) by EXTPRO_1:5 ;
:: thesis: verum

end;

A69: for i being Element of NAT st i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds
IC (Comput ((ProgramPart s),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 ((ProgramPart s),s,i)) = i )
assume A70: i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i

A71: now

A72: i < (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) by A70, AFINSQ_1:20;
assume A73: 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 A42, A73, A72, 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 A71;

suppose i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i

hence IC (Comput ((ProgramPart s),s,i)) = i by A29; :: thesis: verum

end;

suppose A74: ( (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 ((ProgramPart s),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:11;
then reconsider ii = i - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) as Element of NAT by INT_1:16;
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 A74, XREAL_1:11;
hence i = IC (Comput ((ProgramPart s),s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ii))) by A58, A56
.= IC (Comput ((ProgramPart s),s,i)) ;
:: thesis: verum

end;

suppose A75: ( (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 ((ProgramPart s),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:11;
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:16;
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 A75, XREAL_1:11;
hence i = IC (Comput ((ProgramPart s),s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + ii))) by A68
.= IC (Comput ((ProgramPart s),s,i)) ;
:: thesis: verum

end;

end;

end;

A76: 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 A58, AFINSQ_1:20;
Y: (ProgramPart (Comput ((ProgramPart s),s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) /. (IC (Comput ((ProgramPart s),s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) = (Comput ((ProgramPart s),s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))) . (IC (Comput ((ProgramPart s),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 COMPOS_1:38;
(((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 A45;
then consider rq being XFinSequence of the Instructions of SCM+FSA such that
W: ((((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:92;
A77: 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 A42, AFINSQ_1:20;
then A78: 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 YY: 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 A54, A57, AFINSQ_1:70;
dom <%((f,(intloc 1)) := (intloc 2))%> = 1 by AFINSQ_1:36;
then SS: 0 in dom <%((f,(intloc 1)) := (intloc 2))%> by CARD_1:87, TARSKI:def 1;
len <%((f,(intloc 1)) := (intloc 2))%> = 1 by AFINSQ_1:38;
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:20;
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:31;
then ZZ: 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:70;
CurInstr ((ProgramPart (Comput ((ProgramPart s),s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))),(Comput ((ProgramPart s),s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) = (Comput ((ProgramPart s),s,(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)))) ^ (aSeq ((intloc 2),pr1)))) by A57, A69, Y, A78
.= ((((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 A9, A57, A55
.= ((((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 A76, YY, W, AFINSQ_1:def 4
.= ((((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:20 ;
then A79: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))),(Comput ((ProgramPart s),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 ZZ, A27, A34, AFINSQ_1:def 4
.= <%((f,(intloc 1)) := (intloc 2))%> . 0 by SS, AFINSQ_1:def 4
.= (f,(intloc 1)) := (intloc 2) by AFINSQ_1:38 ;
A80: Comput ((ProgramPart s),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 ((ProgramPart s),(Comput ((ProgramPart s),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:4
.= Exec (((f,(intloc 1)) := (intloc 2)),(Comput ((ProgramPart s),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 A79, AMI_1:123 ;
then A81: IC (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) = succ (IC (Comput ((ProgramPart s),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 A57, A43, SCMFSA_2:99
.= 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 A57, A69, A78
.= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) by A57, A77, NAT_1:39 ;
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 ((ProgramPart s),s,i)) = i :: thesis: ( ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,i)) = i )
assume A82: i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput ((ProgramPart s),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 A82, XXREAL_0:1;

suppose i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i

hence IC (Comput ((ProgramPart s),s,i)) = i by A69; :: thesis: verum

end;

suppose i = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i

hence IC (Comput ((ProgramPart s),s,i)) = i by A81; :: thesis: verum

end;

end;

end;

t: ProgramPart s = ProgramPart s2 by AMI_1:123;
A83: (Comput ((ProgramPart s),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 ((ProgramPart s),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:20
.= p . ((len r) + 1) by A26, A66, t, EXTPRO_1:5 ;
S: ProgramPart s = ProgramPart s2 by AMI_1:123;
consider ki being Element of NAT such that
A84: ki = abs ((Comput ((ProgramPart s),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
A85: (Exec (((f,(intloc 1)) := (intloc 2)),(Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),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:99;
A86: ki = abs ((Comput ((ProgramPart s),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 A84, AFINSQ_1:20
.= abs ((Comput ((ProgramPart s),s2,(len (aSeq ((intloc 2),pr1))))) . (intloc 1)) by EXTPRO_1:5
.= abs (s2 . (intloc 1)) by A2, A60, Th36, S, B60, A19
.= (len r) + 1 by A59, A53, T, ABSVALUE:def 1 ;
A87: dom (s1 . f) = Seg (len p) by A31, FINSEQ_1:def 3;
for i being Element of NAT st i in Seg (len pp1) holds
(((Comput ((ProgramPart s),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 ((ProgramPart s),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 A88: i in Seg (len pp1) ; :: thesis: (((Comput ((ProgramPart s),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 A89: i <= len pp1 by FINSEQ_1:3;
len <%x%> = 1 by AFINSQ_1:38;
then KK: len pp1 = (len pp0) + 1 by AFINSQ_1:20;

per cases ( i = len pp1 or i <> len pp1 ) ;

suppose A90: i = len pp1 ; :: thesis: (((Comput ((ProgramPart s),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 ((ProgramPart s),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 A57, A77, A80, A85, A86, A83, A67, A90, KK, FINSEQ_1:6, FUNCT_1:72
.= p . i by A28, A15, A87, A90, OO, KK, FUNCT_7:33
.= (p | (Seg (len pp1))) . i by A90, KK, FINSEQ_1:6, FUNCT_1:72 ; :: thesis: verum

end;

suppose A92: i <> len pp1 ; :: thesis: (((Comput ((ProgramPart s),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 KK, A89, XXREAL_0:1;
then A93: i <= len pp0 by NAT_1:13;
1 <= i by A88, FINSEQ_1:3;
then A94: i in Seg (len pp0) by A93;
(((Comput ((ProgramPart s),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 A57, A77, A80, A85, A86, A83, A67, A88, FUNCT_1:72
.= (s1 . f) . i by KK, A28, A92, FUNCT_7:34 ;
hence (((Comput ((ProgramPart s),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 A30, A94, FUNCT_1:72
.= p . i by A94, FUNCT_1:72
.= (p | (Seg (len pp1))) . i by A88, FUNCT_1:72 ;
:: thesis: verum

end;

end;

end;

then A96: for i being set st i in Seg (len pp1) holds
(((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i ;
A97: dom ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) = dom (s1 . f) by FUNCT_7:32;
dom ((Comput ((ProgramPart s),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 A43, A80, A85, A86, A83, A67, AFINSQ_1:20
.= Seg (len p) by A31, A97, FINSEQ_1:def 3 ;
then dom (((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) = Seg (len pp1) by FF, RELAT_1:91;
hence ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) by A37, A96, FUNCT_1:9; :: thesis: ( len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),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 A97, FINSEQ_3:31;
hence len ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p by A31, A43, A80, A85, A86, A83, A67, AFINSQ_1:20; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b )
assume that
A98: b <> intloc 1 and
A99: b <> intloc 2 ; :: thesis: (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b
S: ProgramPart s = ProgramPart s2 by AMI_1:123;
thus (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = (Comput ((ProgramPart s),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 A57, A43, A80, SCMFSA_2:99
.= (Comput ((ProgramPart s),s2,(len (aSeq ((intloc 2),pr1))))) . b by EXTPRO_1:5
.= s2 . b by A60, A99, Th36, S, B60, A19
.= s1 . b by A59, A47, A98, Th36, T, B47, A1
.= s . b by A32, A98, A99 ; :: thesis: verum

end;

hereby :: thesis: verum

let h be FinSeq-Location ; :: thesis: ( h <> f implies (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = s . h )
S: ProgramPart s = ProgramPart s2 by AMI_1:123;
assume A100: h <> f ; :: thesis: (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = s . h
hence (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = (Comput ((ProgramPart s),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 A57, A43, A80, SCMFSA_2:99
.= (Comput ((ProgramPart s),s2,(len (aSeq ((intloc 2),pr1))))) . h by EXTPRO_1:5
.= s2 . h by A60, Th36, S, B60, A19
.= s1 . h by A59, A47, Th36, T, B47, A1
.= s . h by A33, A100 ;
:: thesis: verum

end;

end;

set k = len (aSeq ((intloc 1),(len p)));
len <%(f :=<0,...,0> (intloc 1))%> = 1 by AFINSQ_1:38;
then A101: len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) = (len (aSeq ((intloc 1),(len p)))) + 1 by AFINSQ_1:20;
A102: (((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:30;
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:30;
then aSeq ((intloc 1),(len p)) c= f := p by AFINSQ_1:78;
then A103: aSeq ((intloc 1),(len p)) c= s by A5, XBOOLE_1:1;
then A104: (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p)))))) . (intloc 1) = len p by A1, A4, Th37;
A105: S₁[ {} ]

proof

A106: now

let i be Element of NAT ; :: thesis: ( i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies IC (Comput ((ProgramPart s),s,i)) = i )
assume A107: i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i
( i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies i <= len (aSeq ((intloc 1),(len p))) ) by A101, NAT_1:13;
hence IC (Comput ((ProgramPart s),s,i)) = i by A1, A4, A103, A107, 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 ((ProgramPart s),s,i)) = i ) & ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,i)) = i ) & ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
A109: ((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:86
.= (aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%> by AFINSQ_1:32 ;
OO: len (aSeq ((intloc 1),(len p))) < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A101, NAT_1:13;
then A110: IC (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p)))))) = len (aSeq ((intloc 1),(len p))) by A106;
Y: (ProgramPart (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p))))))) /. (IC (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p))))))) = (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p)))))) . (IC (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p))))))) by COMPOS_1:38;
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 A102, AFINSQ_1:20;
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 QQ: len (aSeq ((intloc 1),(len p))) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by A101, NAT_1:13;
NN: (((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:30;
RR: len (aSeq ((intloc 1),(len p))) in dom ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by OO, AFINSQ_1:70;
A111: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p))))))),(Comput ((ProgramPart s),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 A9, A110, Y, QQ
.= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) . (len (aSeq ((intloc 1),(len p)))) by NN, RR, AFINSQ_1:def 4
.= f :=<0,...,0> (intloc 1) by AFINSQ_1:40 ;
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 ((ProgramPart s),s,i)) = i ) & ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
A112: Comput ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>))) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p))))))) by A101, EXTPRO_1:4
.= Exec ((f :=<0,...,0> (intloc 1)),(Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p))))))) by A111, AMI_1:123 ;
then A113: IC (Comput ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) = succ (IC (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p))))))) by SCMFSA_2:101
.= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A101, A110, NAT_1:39 ;

now

let i be Element of NAT ; :: thesis: ( i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies IC (Comput ((ProgramPart s),s,i)) = i )
assume i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ; :: thesis: IC (Comput ((ProgramPart s),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 ((ProgramPart s),s,i)) = i by A106, A113; :: 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 ((ProgramPart s),s,i)) = i by A109; :: thesis: ( ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),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
A114: ki = abs ((Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p)))))) . (intloc 1)) and
A115: (Exec ((f :=<0,...,0> (intloc 1)),(Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p)))))))) . f = ki |-> 0 by SCMFSA_2:101;
((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | 0 = p | (len sD) ;
hence ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) ; :: thesis: ( len ((Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) )
ki = len p by A104, A114, ABSVALUE:def 1;
hence len ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p by A109, A112, A115, FINSEQ_1:def 18; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . b )
assume that
A116: b <> intloc 1 and
b <> intloc 2 ; :: thesis: (Comput ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . b
thus (Comput ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p)))))) . b by A112, SCMFSA_2:101
.= s . b by A1, A4, A103, A116, Th37 ; :: thesis: verum

end;

hence for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b by A109; :: thesis: for g being FinSeq-Location st g <> f holds
(Comput ((ProgramPart s),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 ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . g )
assume g <> f ; :: thesis: (Comput ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . g
hence (Comput ((ProgramPart s),s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = (Comput ((ProgramPart s),s,(len (aSeq ((intloc 1),(len p)))))) . g by A112, SCMFSA_2:101
.= s . g by A1, A4, A103, Th37 ;
:: thesis: verum

end;

hence for g being FinSeq-Location st g <> f holds
(Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g by A109; :: thesis: verum

end;

for r being XFinSequence holds S₁[r] from AFINSQ_1:sch 3(A105, A20);
then consider pp0 being XFinSequence of the Instructions of SCM+FSA ^omega such that
A117: pp0 = pp and
A118: for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds
IC (Comput ((ProgramPart s),s,i)) = i and
A119: ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) and
A120: len ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p and
A121: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput ((ProgramPart s),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 ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) ) ;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) by AMI_1:123;
Y: (ProgramPart (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) /. (IC (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) = (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) . (IC (Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) by COMPOS_1:38;
IC (Comput ((ProgramPart s),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 A117, A118;
then A123: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),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 A9, A18, Y, TX
.= halt SCM+FSA by A17, AFINSQ_1:40 ;
hence ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: ( (Result ((ProgramPart s),s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) )
then A124: Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))) = Result ((ProgramPart s),s) by A123, EXTPRO_1:def 8;
TT: Seg (len pp0) = dom p by A15, A117, FINSEQ_1:def 3;
(Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f = ((Comput ((ProgramPart s),s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) by A15, A117, A120, FINSEQ_3:122;
hence (Result ((ProgramPart s),s)) . f = p by TT, A117, A124, A119, RELAT_1:97; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) )
thus ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result ((ProgramPart s),s)) . g = s . g ) ) by A117, A121, A124; :: thesis: verum