( intloc 0 <> intloc 1 & intloc 0 <> intloc 2 ) by AMI_3:52;
then reconsider a1 = intloc 1, a2 = intloc 2 as read-write Int-Location by SF_MASTR:def 5;
set D = the Instructions of SCM+FSA ;
set O = intloc 0 ;
let s be State of SCM+FSA ; :: thesis: ( IC s = 0 & 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 s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) ) )
assume that
A1: IC s = 0 and
A2: 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 s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result 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 s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )
let p be FinSequence of INT ; :: thesis: ( f := p c= s implies ( ProgramPart s halts_on s & (Result s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) ) )
set q = (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>;
set q0 = (aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>;
A3: f := p = Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:def 5;
assume A4: f := p c= s ; :: thesis: ( ProgramPart s halts_on s & (Result s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )
A5: now
let i be Element of NAT ; :: thesis: ( i in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies s . i = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume A6: i in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: s . i = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then s . i = (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . i by A4, A3, GRFUNC_1:8;
then A7: s . i = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A6, SCMFSA_7:def 1;
i + 1 in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A6, SCMFSA_7:26;
hence s . i = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) by A7, PARTFUN1:def 8; :: thesis: verum
end;
A8: now
let i, k be Element of NAT ; :: thesis: ( i < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) implies (Comput (ProgramPart s),s,k) . i = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume i < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) ; :: thesis: (Comput (ProgramPart s),s,k) . i = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A9: i in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by SCMFSA_7:29;
thus (Comput (ProgramPart s),s,k) . i = s . i by AMI_1:54
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) by A5, A9 ; :: thesis: verum
end;
A10: now
let k be Element of NAT ; :: thesis: ( k in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) )
assume A11: k in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1)
then A12: k + 1 in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:26;
thus (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (k + 1) by A11, SCMFSA_7:def 1
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) by A12, PARTFUN1:def 8 ; :: thesis: verum
end;
consider pp being FinSequence of the Instructions of SCM+FSA * such that
A13: len pp = len p and
A14: for k being Element of NAT st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq a1,k) ^ (aSeq a2,i)) ^ <*(f,a1 := a2)*> ) and
A15: aSeq f,p = FlattenSeq pp by SCMFSA_7:def 4;
defpred S1[ FinSequence] means ( $1 c= pp implies ex pp0 being FinSequence of the Instructions of SCM+FSA * st
( pp0 = $1 & ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . g = s . g ) ) );
A16: dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) = { (m -' 1) where m is Element of NAT : m in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) } by SCMFSA_7:def 1;
A17: a1 <> a2 by AMI_3:52;
A18: for r being FinSequence
for x being set st S1[r] holds
S1[r ^ <*x*>]
proof
let r be FinSequence; :: thesis: for x being set st S1[r] holds
S1[r ^ <*x*>]
let x be set ; :: thesis: ( S1[r] implies S1[r ^ <*x*>] )
assume A19: S1[r] ; :: thesis: S1[r ^ <*x*>]
set r1 = (len r) + 1;
len (r ^ <*x*>) = (len r) + 1 by FINSEQ_2:19;
then (len r) + 1 in Seg (len (r ^ <*x*>)) by FINSEQ_1:6;
then A20: (len r) + 1 in dom (r ^ <*x*>) by FINSEQ_1:def 3;
A21: 1 <= len <*(f,a1 := a2)*> by FINSEQ_1:57;
assume A22: r ^ <*x*> c= pp ; :: thesis: ex pp0 being FinSequence of the Instructions of SCM+FSA * st
( pp0 = r ^ <*x*> & ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . g = s . g ) )
then A23: dom (r ^ <*x*>) c= dom pp by GRFUNC_1:8;
then (len r) + 1 in dom pp by A20;
then A24: (len r) + 1 in Seg (len pp) by FINSEQ_1:def 3;
then ( 1 <= (len r) + 1 & (len r) + 1 <= len p ) by A13, FINSEQ_1:3;
then consider pr1 being Integer such that
A25: pr1 = p . ((len r) + 1) and
A26: pp . ((len r) + 1) = ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*> by A14;
r c= r ^ <*x*> by FINSEQ_6:12;
then consider pp0 being FinSequence of the Instructions of SCM+FSA * such that
A27: pp0 = r and
A28: for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i and
A29: ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) and
A30: len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p and
A31: for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b and
A32: for h being FinSeq-Location st h <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . h = s . h by A19, A22, XBOOLE_1:1;
A33: x = (r ^ <*x*>) . ((len r) + 1) by FINSEQ_1:59
.= pp . ((len r) + 1) by A22, A20, GRFUNC_1:8 ;
then x in the Instructions of SCM+FSA * by A20, A23, FINSEQ_2:13;
then <*x*> is FinSequence of the Instructions of SCM+FSA * by FINSEQ_1:95;
then reconsider pp1 = pp0 ^ <*x*> as FinSequence of the Instructions of SCM+FSA * by FINSEQ_1:96;
take pp1 ; :: thesis: ( pp1 = r ^ <*x*> & ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
thus pp1 = r ^ <*x*> by A27; :: thesis: ( ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
reconsider x = x as Element of the Instructions of SCM+FSA * by A20, A23, A33, FINSEQ_2:13;
A34: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <*x*>) by PRE_POLY:3
.= (FlattenSeq pp0) ^ x by PRE_POLY:1 ;
set c2 = len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)));
set c1 = len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0));
A35: 1 <= ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) + 1 by NAT_1:11;
A36: x = (aSeq a1,((len r) + 1)) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>) by A26, A33, FINSEQ_1:45;
then (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (FlattenSeq pp1)) = (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (((FlattenSeq pp0) ^ (aSeq a1,((len r) + 1))) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>))) by A34, FINSEQ_1:45
.= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (((FlattenSeq pp0) ^ (aSeq a1,((len r) + 1))) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>))) by FINSEQ_1:35
.= len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>)) by Lm2
.= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>)) by FINSEQ_1:35
.= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + ((len (aSeq a2,pr1)) + (len <*(f,a1 := a2)*>)) by FINSEQ_1:35 ;
then A37: (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (FlattenSeq pp1)) = (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + ((len (aSeq a2,pr1)) + 1) by FINSEQ_1:56
.= ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) + 1 ;
then A38: len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) = ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) + 1 by FINSEQ_1:35;
then A39: len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) > (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) by NAT_1:13;
A40: FlattenSeq pp1 c= FlattenSeq pp by A22, A27, PRE_POLY:6;
A41: now
let p be FinSequence; :: thesis: ( p c= x implies (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> )
assume p c= x ; :: thesis: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>
then (FlattenSeq pp0) ^ p c= (FlattenSeq pp0) ^ x by FINSEQ_6:15;
then (FlattenSeq pp0) ^ p c= FlattenSeq pp by A40, A34, XBOOLE_1:1;
then ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ ((FlattenSeq pp0) ^ p) c= ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp) by FINSEQ_6:15;
then A42: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp) by FINSEQ_1:45;
((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A15, FINSEQ_6:12;
hence (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A42, XBOOLE_1:1; :: thesis: verum
end;
A43: now
let c be Element of NAT ; :: thesis: ( c in dom (aSeq a2,pr1) implies (aSeq a2,pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1) )
assume A44: c in dom (aSeq a2,pr1) ; :: thesis: (aSeq a2,pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1)
then A45: (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c in dom (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) by FINSEQ_1:41;
then (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c >= 1 by FINSEQ_3:27;
then A46: (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1) + 1 = (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) - 1) + 1 by XREAL_1:235
.= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c ;
(((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A26, A33, A41, FINSEQ_6:12;
then A47: ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by FINSEQ_1:45;
then dom (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) c= dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
then A48: ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1 in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by A16, A45;
thus (aSeq a2,pr1) . c = (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) . ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) by A44, FINSEQ_1:def 7
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) by A45, A47, GRFUNC_1:8
.= (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1) by A10, A48, A46
.= s . (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1) by A4, A3, A48, GRFUNC_1:8
.= (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1) by AMI_1:54 ; :: thesis: verum
end;
len pp1 <= len pp by A22, A27, FINSEQ_1:84;
then A49: Seg (len pp1) c= Seg (len p) by A13, FINSEQ_1:7;
then Seg (len pp1) c= dom p by FINSEQ_1:def 3;
then A50: dom (p | (Seg (len pp1))) = Seg (len pp1) by RELAT_1:91;
len <*(f,a1 := a2)*> <= (len ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1))) + (len <*(f,a1 := a2)*>) by NAT_1:12;
then len <*(f,a1 := a2)*> <= len (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>) by FINSEQ_1:35;
then A51: 1 <= len x by A26, A33, FINSEQ_1:57;
set c3 = len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1));
A52: len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) = (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) by FINSEQ_1:35;
A53: for c being Element of NAT st c in dom (aSeq a1,((len r) + 1)) holds
(aSeq a1,((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1)
proof
let c be Element of NAT ; :: thesis: ( c in dom (aSeq a1,((len r) + 1)) implies (aSeq a1,((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) )
assume A54: c in dom (aSeq a1,((len r) + 1)) ; :: thesis: (aSeq a1,((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1)
then A55: (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) by FINSEQ_1:41;
then (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c >= 1 by FINSEQ_3:27;
then A56: ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1 = ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) - 1 by XREAL_1:235;
A57: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A36, A41, FINSEQ_6:12;
then dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) c= dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
then A58: ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1 in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by A16, A55;
thus (aSeq a1,((len r) + 1)) . c = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) by A54, FINSEQ_1:def 7
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) + 1) by A57, A55, A56, GRFUNC_1:8
.= (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) by A10, A58
.= s . (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) by A4, A3, A58, GRFUNC_1:8
.= (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) by AMI_1:54 ; :: thesis: verum
end;
A59: ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1) = (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x by A34, FINSEQ_1:45;
then len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A41, FINSEQ_1:84;
then A60: (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A38, NAT_1:13;
A61: ( (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (intloc 0 ) = 1 & IC (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) = len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ) by A2, A28, A31;
A62: now
let i be Element of NAT ; :: thesis: ( i <= len (aSeq a1,((len r) + 1)) implies (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),s,((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + i)) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) by AMI_1:144;
assume i <= len (aSeq a1,((len r) + 1)) ; :: thesis: (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),s,((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + i))
hence (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))),i) by A53, A61, SCMFSA_7:36, T
.= IC (Comput (ProgramPart s),s,((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + i)) by AMI_1:51 ;
:: thesis: verum
end;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) by AMI_1:144;
A63: len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) = (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + (len (aSeq a1,((len r) + 1))) by FINSEQ_1:35;
then A64: Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) = Comput (ProgramPart s),(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))),(len (aSeq a1,((len r) + 1))) by AMI_1:51;
then A65: (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (intloc 0 ) = 1 by A53, A61, SCMFSA_7:36, T;
A66: IC (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) = len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) by A63, A64, A53, A61, SCMFSA_7:36, T;
A67: now
let i be Element of NAT ; :: thesis: ( i <= len (aSeq a2,pr1) implies (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i = IC (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i)) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) by AMI_1:144;
assume i <= len (aSeq a2,pr1) ; :: thesis: (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i = IC (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i))
hence (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i = IC (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),i) by A43, A65, A66, SCMFSA_7:36, T
.= IC (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i)) by AMI_1:51 ;
:: thesis: verum
end;
A68: for i being Element of NAT st i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i
proof
let i be Element of NAT ; :: thesis: ( i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) implies IC (Comput (ProgramPart s),s,i) = i )
assume A69: i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
A70: now
A71: i < (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (FlattenSeq pp1)) by A69, FINSEQ_1:35;
assume A72: not i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ; :: thesis: ( ( not (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ) implies ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) ) )
assume ( not (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ) ; :: thesis: ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) )
hence ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) ) by A37, A72, A71, NAT_1:13; :: thesis: verum
end;
per cases ( i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) or ( (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ) or ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) ) ) by A70;
suppose i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
hence IC (Comput (ProgramPart s),s,i) = i by A28; :: thesis: verum
end;
suppose A73: ( (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
then ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + 1) - (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) <= i - (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) by XREAL_1:11;
then reconsider ii = i - (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) as Element of NAT by INT_1:16;
i - (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) - (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) by A73, XREAL_1:11;
hence i = IC (Comput (ProgramPart s),s,((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + ii)) by A63, A62
.= IC (Comput (ProgramPart s),s,i) ;
:: thesis: verum
end;
suppose A74: ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) ) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
then ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1) - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) <= i - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) by XREAL_1:11;
then reconsider ii = i - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) as Element of NAT by INT_1:16;
i - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) <= ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) by A74, XREAL_1:11;
hence i = IC (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + ii)) by A67
.= IC (Comput (ProgramPart s),s,i) ;
:: thesis: verum
end;
end;
end;
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) by AMI_1:144;
A75: (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . f = (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . f by FINSEQ_1:35
.= (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . f by AMI_1:51
.= (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . f by A43, A65, A66, SCMFSA_7:36, S
.= (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f by A64, A53, A61, SCMFSA_7:36, T ;
A76: len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) = ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + (len (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) by A63, FINSEQ_1:35;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) /. (IC (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) = (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . (IC (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) by AMI_1:150;
CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) = (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . (IC (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) by AMI_1:def 16, Y
.= (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . (len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) by A52, A68, A39
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + 1) by A8, A52, A60
.= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) . ((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + 1) by A59, A52, A41, A38, A35, FINSEQ_4:98 ;
then CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + (len <*(f,a1 := a2)*>)) by A59, FINSEQ_1:57
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + ((len (aSeq a1,((len r) + 1))) + ((len (aSeq a2,pr1)) + (len <*(f,a1 := a2)*>)))) by A76 ;
then A77: CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + (len x)) by A26, A33, Lm3
.= (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>) . (len (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>)) by A26, A33, A51, FINSEQ_1:86
.= (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>) . ((len ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1))) + (len <*(f,a1 := a2)*>)) by FINSEQ_1:35
.= <*(f,a1 := a2)*> . (len <*(f,a1 := a2)*>) by A21, FINSEQ_1:86
.= <*(f,a1 := a2)*> . 1 by FINSEQ_1:57
.= f,a1 := a2 by FINSEQ_1:57 ;
X: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by AMI_1:144;
A78: Comput (ProgramPart s),s,((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by AMI_1:14
.= Exec (f,a1 := a2),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by A77, AMI_1:def 18, X ;
then A79: IC (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) = (Exec (f,a1 := a2),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) . (IC SCM+FSA ) by A52, A38, AMI_1:def 15
.= succ (IC (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) by SCMFSA_2:99
.= succ (len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) by A52, A68, A39
.= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) by A52, A38, NAT_1:39 ;
thus for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i :: thesis: ( ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
proof
let i be Element of NAT ; :: thesis: ( i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) implies IC (Comput (ProgramPart s),s,i) = i )
assume A80: i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
per cases ( i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) or i = len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) ) by A80, XXREAL_0:1;
suppose i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
hence IC (Comput (ProgramPart s),s,i) = i by A68; :: thesis: verum
end;
suppose i = len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
hence IC (Comput (ProgramPart s),s,i) = i by A79; :: thesis: verum
end;
end;
end;
consider ki being Element of NAT such that
A81: ki = abs ((Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . a1) and
A82: (Exec (f,a1 := a2),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) . f = ((Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . f) +* ki,((Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . a2) by SCMFSA_2:99;
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) by AMI_1:144;
A83: ki = abs ((Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . a1) by A81, FINSEQ_1:35
.= abs ((Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . a1) by AMI_1:51
.= abs ((Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . a1) by A17, A43, A65, A66, SCMFSA_7:36, S
.= abs ((len r) + 1) by A64, A53, A61, SCMFSA_7:36, T
.= (len r) + 1 by ABSVALUE:def 1 ;
X: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) by AMI_1:144;
A84: (Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . a2 = (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . a2 by FINSEQ_1:35
.= (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . a2 by AMI_1:51
.= p . ((len r) + 1) by A25, A43, A65, A66, SCMFSA_7:36, X ;
A85: Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1))) = Exec (f,a1 := a2),(Comput (ProgramPart s),s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by A38, A78, FINSEQ_1:35;
for i being Element of NAT st i in Seg (len pp1) holds
(((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
proof
A86: (len r) + 1 in dom ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) by A13, A30, A24, FINSEQ_1:def 3;
let i be Element of NAT ; :: thesis: ( i in Seg (len pp1) implies (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i )
assume A87: i in Seg (len pp1) ; :: thesis: (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
then A88: i <= len pp1 by FINSEQ_1:3;
per cases ( i = len pp1 or i <> len pp1 ) ;
suppose A89: i = len pp1 ; :: thesis: (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
then A90: i = (len pp0) + 1 by FINSEQ_2:19;
hence (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A85, A82, A83, A84, A75, A89, FINSEQ_1:6, FUNCT_1:72
.= p . ((len r) + 1) by A27, A86, A90, FUNCT_7:33
.= (p | (Seg (len pp1))) . i by A27, A89, A90, FINSEQ_1:6, FUNCT_1:72 ;
:: thesis: verum
end;
suppose A91: i <> len pp1 ; :: thesis: (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
then i < len pp1 by A88, XXREAL_0:1;
then i < (len pp0) + 1 by FINSEQ_2:19;
then A92: i <= len pp0 by NAT_1:13;
1 <= i by A87, FINSEQ_1:3;
then A93: i in Seg (len pp0) by A92;
A94: i <> (len r) + 1 by A27, A91, FINSEQ_2:19;
(((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A85, A82, A83, A84, A75, A87, FUNCT_1:72
.= ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) . i by A94, FUNCT_7:34 ;
hence (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp0))) . i by A29, A93, FUNCT_1:72
.= p . i by A93, FUNCT_1:72
.= (p | (Seg (len pp1))) . i by A87, FUNCT_1:72 ;
:: thesis: verum
end;
end;
end;
then A95: for i being set st i in Seg (len pp1) holds
(((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i ;
A96: dom (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = dom ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) by FUNCT_7:32;
then dom ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = Seg (len p) by A30, A52, A38, A78, A82, A83, A84, A75, FINSEQ_1:def 3;
then dom (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) = Seg (len pp1) by A49, RELAT_1:91;
hence ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) by A50, A95, FUNCT_1:9; :: thesis: ( len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
len (((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) by A96, FINSEQ_3:31;
hence len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p by A30, A38, A78, A82, A83, A84, A75, FINSEQ_1:35; :: thesis: ( ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
hereby :: thesis: for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g
let b be Int-Location ; :: thesis: ( b <> a1 & b <> a2 implies (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b )
assume that
A97: b <> a1 and
A98: b <> a2 ; :: thesis: (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) by AMI_1:144;
thus (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . b by A52, A38, A78, SCMFSA_2:99
.= (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . b by AMI_1:51
.= (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . b by A43, A65, A66, A98, SCMFSA_7:36, S
.= (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b by A64, A53, A61, A97, SCMFSA_7:36, T
.= s . b by A31, A97, A98 ; :: thesis: verum
end;
hereby :: thesis: verum
let h be FinSeq-Location ; :: thesis: ( h <> f implies (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . h = s . h )
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) by AMI_1:144;
assume A99: h <> f ; :: thesis: (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . h = s . h
hence (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . h = (Comput (ProgramPart s),s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . h by A52, A38, A78, SCMFSA_2:99
.= (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . h by AMI_1:51
.= (Comput (ProgramPart s),s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . h by A43, A65, A66, SCMFSA_7:36, S
.= (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . h by A64, A53, A61, SCMFSA_7:36, T
.= s . h by A32, A99 ;
:: thesis: verum
end;
end;
set k = len (aSeq a1,(len p));
A100: len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) = (len (aSeq a1,(len p))) + 1 by FINSEQ_2:19;
A101: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>) by FINSEQ_1:45;
then (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = (aSeq a1,(len p)) ^ (<*(f :=<0,...,0> a1)*> ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by FINSEQ_1:45;
then Load (aSeq a1,(len p)) c= f := p by A3, SCMFSA_7:31;
then A102: Load (aSeq a1,(len p)) c= s by A4, XBOOLE_1:1;
A103: S1[ {} ]
proof
A104: now
let i be Element of NAT ; :: thesis: ( i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) implies IC (Comput (ProgramPart s),s,i) = i )
assume A105: i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
( i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) implies i <= len (aSeq a1,(len p)) ) by A100, NAT_1:13;
hence IC (Comput (ProgramPart s),s,i) = i by A1, A2, A102, A105, SCMFSA_7:37; :: thesis: verum
end;
len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by A101, FINSEQ_1:35;
then len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by NAT_1:11;
then A106: len (aSeq a1,(len p)) < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A100, NAT_1:13;
assume {} c= pp ; :: thesis: ex pp0 being FinSequence of the Instructions of SCM+FSA * st
( pp0 = {} & ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . g = s . g ) )
reconsider sD = <*> (the Instructions of SCM+FSA * ) as FinSequence of the Instructions of SCM+FSA * ;
take sD ; :: thesis: ( sD = {} & ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . g = s . g ) )
A107: ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * ))) = ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (<*> the Instructions of SCM+FSA ) by PRE_POLY:2
.= (aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*> by FINSEQ_1:47 ;
thus sD = {} ; :: thesis: ( ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . g = s . g ) )
consider ki being Element of NAT such that
A108: ki = abs ((Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) . a1) and
A109: (Exec (f :=<0,...,0> a1),(Comput (ProgramPart s),s,(len (aSeq a1,(len p))))) . f = ki |-> 0 by SCMFSA_2:101;
A110: 1 <= len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) by A100, NAT_1:11;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (aSeq a1,(len p))))) /. (IC (Comput (ProgramPart s),s,(len (aSeq a1,(len p))))) = (Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) . (IC (Comput (ProgramPart s),s,(len (aSeq a1,(len p))))) by AMI_1:150;
len (aSeq a1,(len p)) < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) by A100, NAT_1:13;
then A111: IC (Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) = len (aSeq a1,(len p)) by A104;
then A112: CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (aSeq a1,(len p))))),(Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) = (Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) . (len (aSeq a1,(len p))) by AMI_1:def 16, Y
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) by A100, A8, A106
.= ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) . (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) by A101, A110, FINSEQ_1:85
.= f :=<0,...,0> a1 by A100, FINSEQ_1:59 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) by AMI_1:144;
A113: Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) = Following (ProgramPart s),(Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) by A100, AMI_1:14
.= Exec (f :=<0,...,0> a1),(Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) by A112, AMI_1:def 18, T ;
A114: IC (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) = (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . (IC SCM+FSA ) by AMI_1:def 15
.= succ (IC (Comput (ProgramPart s),s,(len (aSeq a1,(len p))))) by A113, SCMFSA_2:101
.= len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) by A100, A111, NAT_1:39 ;
now
let i be Element of NAT ; :: thesis: ( i <= len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) implies IC (Comput (ProgramPart s),s,i) = i )
assume i <= len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
then ( i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) or i = len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ) by XXREAL_0:1;
hence IC (Comput (ProgramPart s),s,i) = i by A104, A114; :: thesis: verum
end;
hence for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)) holds
IC (Comput (ProgramPart s),s,i) = i by A107; :: thesis: ( ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) & len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . g = s . g ) )
((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) | (Seg 0 ) = p | (Seg (len sD)) ;
hence ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) ; :: thesis: ( len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . g = s . g ) )
ki = abs (len p) by A1, A2, A102, A108, SCMFSA_7:37
.= len p by ABSVALUE:def 1 ;
hence len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . f) = len p by A107, A113, A109, FINSEQ_1:def 18; :: thesis: ( ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . g = s . g ) )
now
let b be Int-Location ; :: thesis: ( b <> a1 & b <> a2 implies (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . b = s . b )
assume that
A115: b <> a1 and
b <> a2 ; :: thesis: (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . b = s . b
thus (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . b = (Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) . b by A113, SCMFSA_2:101
.= s . b by A1, A2, A102, A115, SCMFSA_7:37 ; :: thesis: verum
end;
hence for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . b = s . b by A107; :: thesis: for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . g = s . g
now
let g be FinSeq-Location ; :: thesis: ( g <> f implies (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . g = s . g )
assume g <> f ; :: thesis: (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . g = s . g
hence (Comput (ProgramPart s),s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . g = (Comput (ProgramPart s),s,(len (aSeq a1,(len p)))) . g by A113, SCMFSA_2:101
.= s . g by A1, A2, A102, SCMFSA_7:37 ;
:: thesis: verum
end;
hence for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq sD)))) . g = s . g by A107; :: thesis: verum
end;
for r being FinSequence holds S1[r] from FINSEQ_1:sch 3(A103, A18);
 then consider pp0 being FinSequence of the Instructions of SCM+FSA * such that
A116: pp0 = pp and
A117: for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i and
A118: ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) and
A119: len ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p and
A120: ( ( for b being Int-Location st b <> a1 & b <> a2 holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . g = s . g ) ) ;
A121: dom p = Seg (len pp0) by A13, A116, FINSEQ_1:def 3;
len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) + 1 by A15, FINSEQ_2:19;
then A122: len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)) < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by NAT_1:13;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))))) /. (IC (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))))) = (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) . (IC (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))))) by AMI_1:150;
IC (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) = len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)) by A116, A117;
then A123: CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))))),(Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) = (Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) . (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) by AMI_1:def 16, Y
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) + 1) by A8, A122
.= halt SCM+FSA by A15, FINSEQ_1:59 ;
hence ProgramPart s halts_on s by AMI_1:146; :: thesis: ( (Result s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )
then A124: Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) = Result s by A123, AMI_1:def 22;
dom ((Comput (ProgramPart s),s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = Seg (len pp0) by A13, A116, A119, FINSEQ_1:def 3;
then (Result s) . f = p | (Seg (len pp0)) by A116, A118, A124, RELAT_1:97;
hence (Result s) . f = p by A121, RELAT_1:97; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )
thus ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) ) by A116, A120, A124; :: thesis: verum