set a2 = intloc 2;
set a1 = intloc 1;
let s be 0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
P halts_on s
let P be Instruction-Sequence of SCM+FSA; :: thesis: for f being FinSeq-Location
for p being FinSequence of INT st f := p c= P holds
P halts_on s
A1: dom P = NAT by PARTFUN1:def 2;
set D = the Instructions of SCM+FSA;
let f be FinSeq-Location ; :: thesis: for p being FinSequence of INT st f := p c= P holds
P halts_on s
let p be FinSequence of INT ; :: thesis: ( f := p c= P implies P halts_on s )
set q = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>;
set q0 = (aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>;
assume A2: f := p c= P ; :: thesis: P halts_on s
set q = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>;
A3: 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 A4: 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 = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . i by A2, A4, GRFUNC_1:2; :: thesis: verum
end;
consider pp being XFinSequence of such that
A5: ( len pp = len p & ( 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
A6: aSeq (f,p) = FlattenSeq pp by SCMFSA_7:def 3;
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 A6, AFINSQ_1:75;
then A7: 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 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 ) ) );
A8: 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 A9: 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 A10: len r in dom (r ^ <%x%>) by NAT_1:44;
assume A11: r ^ <%x%> c= pp ; :: thesis: ex pp0 being XFinSequence of 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 ) )
then A12: dom (r ^ <%x%>) c= dom pp by GRFUNC_1:2;
then len r < len pp by A10, NAT_1:44;
then consider pr1 being Integer such that
pr1 = p . ((len r) + 1) and
A13: pp . (len r) = ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%> by A5;
r c= r ^ <%x%> by AFINSQ_1:74;
then consider pp0 being XFinSequence of such that
A14: pp0 = r and
A15: 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 by A9, A11, XBOOLE_1:1;
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));
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 A15;
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;
A16: x = (r ^ <%x%>) . (len r) by AFINSQ_1:36
.= pp . (len r) by A11, A10, GRFUNC_1:2 ;
then x in the Instructions of SCM+FSA ^omega by A10, A12, FUNCT_1:102;
then reconsider pp1 = pp0 ^ <%x%> as XFinSequence of ;
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 ) )
thus pp1 = r ^ <%x%> by A14; :: 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
reconsider x = x as Element of the Instructions of SCM+FSA ^omega by A10, A12, A16, FUNCT_1:102;
A17: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <%x%>) by AFINSQ_2:75
.= (FlattenSeq pp0) ^ x by AFINSQ_2:73 ;
set s2 = Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))));
A18: x = (aSeq ((intloc 1),((len r) + 1))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>) by A13, A16, AFINSQ_1:27;
then A19: (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 A17, 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:34
.= ((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 A20: 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;
then A21: 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;
A22: FlattenSeq pp1 c= FlattenSeq pp by A11, A14, AFINSQ_2:82;
A23: 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 A22, A17, 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 A24: (((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 A6, 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 A24, XBOOLE_1:1; :: thesis: verum
end;
A25: for c being Element of NAT st c < len (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 < len (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 c < len (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 A26: c in dom (aSeq ((intloc 1),((len r) + 1))) by AFINSQ_1:66;
then A27: (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;
A28: (((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 A18, A23, AFINSQ_1:74;
then A29: 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 A26, 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 A28, A27, GRFUNC_1:2
.= P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) by A2, A29, A27, GRFUNC_1:2 ; :: 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)));
A30: 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;
A31: ((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 A17, 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 A23, NAT_1:43;
then A32: (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 A20, NAT_1:13;
A33: 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;
A34: Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))) = Comput (P,s1,(len (aSeq ((intloc 1),((len r) + 1))))) by A30, 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 A30, A34, A25, Lm3;
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;
A35: for c being Element of NAT st c < len (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 < len (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 c < len (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 A36: c in dom (aSeq ((intloc 2),pr1)) by AFINSQ_1:66;
then A37: (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 A13, A16, A23, AFINSQ_1:74;
then A38: ((((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 A39: 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 A36, 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 A37, A38, 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 A2, A39, A37, GRFUNC_1:2 ; :: thesis: verum
end;
A40: 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 A35, Lm3
.= 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;
A41: 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 A25, Lm3
.= 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;
A42: 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 A43: i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (P,s,i)) = i
A44: now
A45: i < (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) by A43, AFINSQ_1:17;
assume A46: 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 A19, A46, A45, 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 A44;
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 A15; :: thesis: verum
end;
suppose A47: ( (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 A47, XREAL_1:9;
hence i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ii))) by A30, A41
.= IC (Comput (P,s,i)) ;
:: thesis: verum
thus verum ; :: thesis: verum
end;
suppose A48: ( (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 A48, 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 A40
.= IC (Comput (P,s,i)) ;
:: thesis: verum
end;
end;
end;
(((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 A23;
then consider rq being XFinSequence of such that
A49: ((((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;
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 A19, AFINSQ_1:17;
then A50: 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 A51: 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 A31, A33, AFINSQ_1:66;
dom <%((f,(intloc 1)) := (intloc 2))%> = 1 by AFINSQ_1:33;
then A52: 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 A53: 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;
A54: 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 A30, AFINSQ_1:17;
A55: 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 A1, PARTFUN1:def 6;
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 A33, A42, A55, A50
.= ((((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 A3, A33, A32
.= ((((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 A54, A51, A49, 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 A56: CurInstr (P,(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) = (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>) . ((len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 0) by A53, A13, A16, AFINSQ_1:def 3
.= <%((f,(intloc 1)) := (intloc 2))%> . 0 by A52, AFINSQ_1:def 3
.= (f,(intloc 1)) := (intloc 2) by AFINSQ_1:34 ;
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 A56 ;
then A57: IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) = (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)))))))) . (IC ) by A20, AFINSQ_1:17
.= 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 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 A33, A42, A21 ;
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: verum
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 A58: 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 A58, 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 A42; :: 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 A33, A20, A57, NAT_1:38; :: thesis: verum
end;
end;
end;
end;
set k = len (aSeq ((intloc 1),(len p)));
A59: len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) = (len (aSeq ((intloc 1),(len p)))) + 1 by AFINSQ_1:75;
(((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
.= (aSeq ((intloc 1),(len p))) ^ (<%(f :=<0,...,0> (intloc 1))%> ^ ((aSeq (f,p)) ^ <%(halt SCM+FSA)%>)) by AFINSQ_1:27 ;
then A60: aSeq ((intloc 1),(len p)) c= f := p by AFINSQ_1:74;
A61: S1[ {} ]
proof
assume {} c= pp ; :: thesis: ex pp0 being XFinSequence of 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 ) )
take <%> ( the Instructions of SCM+FSA ^omega) ; :: thesis: ( <%> ( the Instructions of SCM+FSA ^omega) = {} & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the Instructions of SCM+FSA ^omega)))) holds
IC (Comput (P,s,i)) = i ) )
thus <%> ( the Instructions of SCM+FSA ^omega) = {} ; :: thesis: for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the Instructions of SCM+FSA ^omega)))) holds
IC (Comput (P,s,i)) = i
A62: (((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 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 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 A63: len (aSeq ((intloc 1),(len p))) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by A59, NAT_1:13;
A64: 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))) by A59, NAT_1:13;
hence IC (Comput (P,s,i)) = i by A2, A60, Lm4, XBOOLE_1:1; :: thesis: verum
end;
A65: len (aSeq ((intloc 1),(len p))) < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A59, NAT_1:13;
then A66: len (aSeq ((intloc 1),(len p))) in dom ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by AFINSQ_1:66;
A67: IC (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) = len (aSeq ((intloc 1),(len p))) by A64, A65;
then A68: CurInstr (P,(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) = P . (len (aSeq ((intloc 1),(len p)))) by A1, PARTFUN1:def 6
.= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . (len (aSeq ((intloc 1),(len p)))) by A3, A63
.= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) . (len (aSeq ((intloc 1),(len p)))) by A62, A66, AFINSQ_1:def 3
.= f :=<0,...,0> (intloc 1) by AFINSQ_1:36 ;
A69: 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 A59, EXTPRO_1:3
.= Exec ((f :=<0,...,0> (intloc 1)),(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) by A68 ;
A70: 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 A69, SCMFSA_2:75
.= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A59, A67, NAT_1:38 ;
A71: 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 A64, A70; :: thesis: verum
end;
((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 ;
hence for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the Instructions of SCM+FSA ^omega)))) holds
IC (Comput (P,s,i)) = i by A71; :: thesis: verum
end;
for r being XFinSequence holds S1[r] from AFINSQ_1:sch 3(A61, A8);
 then ex pp0 being XFinSequence of st
( pp0 = pp & ( 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 ) ) ;
then 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)) ;
then CurInstr (P,(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) = P . (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) by A1, PARTFUN1:def 6
.= ((((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 A3, A7
.= halt SCM+FSA by A6, AFINSQ_1:36 ;
hence P halts_on s by EXTPRO_1:29; :: thesis: verum