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

A6: now

let i be Element of NAT ; :: thesis: ( i in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume A7: i in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then s . i = (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . i by A5, GRFUNC_1:8;
then A8: s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A7, Def1;
i + 1 in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A7, Th26;
hence s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) by A8, PARTFUN1:def 8; :: thesis: verum

end;

A9: now

let i, k be Element of NAT ; :: thesis: ( i < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) implies (Comput (ProgramPart s),s,k) . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume i < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) ; :: thesis: (Comput (ProgramPart s),s,k) . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A10: i in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by Th29;
thus (Comput (ProgramPart s),s,k) . i = s . i by AMI_1:54
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) by A6, A10 ; :: thesis: verum

end;

A11: now

let k be Element of NAT ; :: thesis: ( k in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) )
assume A12: k in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1)
then A13: k + 1 in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by Th26;
thus (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (k + 1) by A12, Def1
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) by A13, PARTFUN1:def 8 ; :: thesis: verum

end;

set q0 = (aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>;
A14: dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) = { (m -' 1) where m is Element of NAT : m in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) } by Def1;
consider pp being FinSequence of the Instructions of SCM+FSA * such that
A15: len pp = len p and
A16: for k being Element of NAT st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> ) and
A17: aSeq f,p = FlattenSeq pp by Def4;
len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))) + 1 by A17, FINSEQ_2:19;
then A18: len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)) < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by NAT_1:13;
defpred S₁[ 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 (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . g = s . g ) ) );
A19: intloc 2 <> intloc 0 by AMI_3:52;
A20: for r being FinSequence
for x being set st S₁[r] holds
S₁[r ^ <*x*>]

proof

let r be FinSequence; :: thesis: for x being set st S₁[r] holds
S₁[r ^ <*x*>]
let x be set ; :: thesis: ( S₁[r] implies S₁[r ^ <*x*>] )
assume A21: S₁[r] ; :: thesis: S₁[r ^ <*x*>]
set r1 = (len r) + 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 A22: (len r) + 1 in dom (r ^ <*x*>) by FINSEQ_1:def 3;
assume A23: 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 (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . g = s . g ) )
then A24: dom (r ^ <*x*>) c= dom pp by GRFUNC_1:8;
then (len r) + 1 in dom pp by A22;
then A25: (len r) + 1 in Seg (len pp) by FINSEQ_1:def 3;
then ( 1 <= (len r) + 1 & (len r) + 1 <= len pp ) by FINSEQ_1:3;
then consider pr1 being Integer such that
A26: pr1 = p . ((len r) + 1) and
A27: pp . ((len r) + 1) = ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) ^ <*(f,(intloc 1) := (intloc 2))*> by A15, A16;
r c= r ^ <*x*> by FINSEQ_6:12;
then consider pp0 being FinSequence of the Instructions of SCM+FSA * such that
A28: pp0 = r and
A29: for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i and
A30: ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) and
A31: len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = len p and
A32: for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b = s . b and
A33: for h being FinSeq-Location st h <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . h = s . h by A21, A23, XBOOLE_1:1;
A34: x = (r ^ <*x*>) . ((len r) + 1) by FINSEQ_1:59
.= pp . ((len r) + 1) by A23, A22, GRFUNC_1:8 ;
then x in the Instructions of SCM+FSA * by A22, A24, 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 (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
thus pp1 = r ^ <*x*> by A28; :: thesis: ( ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
reconsider x = x as Element of the Instructions of SCM+FSA * by A22, A24, A34, FINSEQ_2:13;
A35: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <*x*>) by PRE_POLY:3
.= (FlattenSeq pp0) ^ x by PRE_POLY:1 ;
len pp1 <= len pp by A23, A28, FINSEQ_1:84;
then A36: Seg (len pp1) c= Seg (len p) by A15, FINSEQ_1:7;
then Seg (len pp1) c= dom p by FINSEQ_1:def 3;
then A37: dom (p | (Seg (len pp1))) = Seg (len pp1) by RELAT_1:91;
len <*(f,(intloc 1) := (intloc 2))*> <= (len ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1))) + (len <*(f,(intloc 1) := (intloc 2))*>) by NAT_1:12;
then len <*(f,(intloc 1) := (intloc 2))*> <= len (((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) ^ <*(f,(intloc 1) := (intloc 2))*>) by FINSEQ_1:35;
then A38: 1 <= len x by A27, A34, FINSEQ_1:57;
A39: 1 <= len <*(f,(intloc 1) := (intloc 2))*> by FINSEQ_1:57;
set c2 = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)));
set c1 = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0));
set s1 = Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)));
set s2 = Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))));
A40: 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))) + 1 by NAT_1:11;
A41: x = (aSeq (intloc 1),((len r) + 1)) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>) by A27, A34, FINSEQ_1:45;
then A42: (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len (FlattenSeq pp1)) = (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len (((FlattenSeq pp0) ^ (aSeq (intloc 1),((len r) + 1))) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>))) by A35, FINSEQ_1:45
.= 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 FINSEQ_1:35
.= len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>)) by Lm3
.= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>)) by FINSEQ_1:35
.= (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 FINSEQ_1:35
.= (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 FINSEQ_1:56
.= ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) + 1 ;
then A43: len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) = ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) + 1 by FINSEQ_1:35;
A44: FlattenSeq pp1 c= FlattenSeq pp by A23, A28, PRE_POLY:6;

A45: now

let p be FinSequence; :: 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 FINSEQ_6:15;
then (FlattenSeq pp0) ^ p c= FlattenSeq pp by A44, A35, XBOOLE_1:1;
then ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ ((FlattenSeq pp0) ^ p) c= ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp) by FINSEQ_6:15;
then A46: (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ p c= ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp) by FINSEQ_1:45;
((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A17, FINSEQ_6:12;
hence (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A46, XBOOLE_1:1; :: thesis: verum

end;

A47: ( (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (intloc 0 ) = 1 & IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) & intloc 1 <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq (intloc 1),((len r) + 1)) holds
(aSeq (intloc 1),((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1) ) )

proof

thus (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (intloc 0 ) = 1 by A1, A19, A4, A32; :: thesis: ( IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) & intloc 1 <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq (intloc 1),((len r) + 1)) holds
(aSeq (intloc 1),((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1) ) )
thus IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) by A29; :: thesis: ( intloc 1 <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq (intloc 1),((len r) + 1)) holds
(aSeq (intloc 1),((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1) ) )
thus intloc 1 <> intloc 0 by AMI_3:52; :: thesis: for c being Element of NAT st c in dom (aSeq (intloc 1),((len r) + 1)) holds
(aSeq (intloc 1),((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)
let c be Element of NAT ; :: thesis: ( c in dom (aSeq (intloc 1),((len r) + 1)) implies (aSeq (intloc 1),((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1) )
assume A48: c in dom (aSeq (intloc 1),((len r) + 1)) ; :: thesis: (aSeq (intloc 1),((len r) + 1)) . c = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)
then A49: (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) by FINSEQ_1:41;
then (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c >= 1 by FINSEQ_3:27;
then ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1 = ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) - 1 by XREAL_1:235;
then A50: (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1) + 1 = (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c ;
A51: (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A41, A45, FINSEQ_6:12;
then dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) c= dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
then A52: ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1 in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by A14, A49;
thus (aSeq (intloc 1),((len r) + 1)) . c = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) by A48, FINSEQ_1:def 7
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) by A51, A49, GRFUNC_1:8
.= (Load ((((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) -' 1) by A11, A52, A50
.= s . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1) by A5, A52, GRFUNC_1:8
.= (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1) by AMI_1:54 ; :: thesis: verum

end;

then A53: (Comput (ProgramPart (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))))),(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),(len (aSeq (intloc 1),((len r) + 1)))) . (intloc 1) = (len r) + 1 by Th36;
A54: ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1) = (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x by A35, FINSEQ_1:45;
then len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A45, FINSEQ_1:84;
then A55: (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A43, NAT_1:13;

A56: now

let i be Element of NAT ; :: thesis: ( i <= len (aSeq (intloc 1),((len r) + 1)) implies (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i)) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) by AMI_1:123;
assume i <= len (aSeq (intloc 1),((len r) + 1)) ; :: thesis: (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i))
hence (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),i) by A47, Th36, T
.= IC (Comput (ProgramPart s),s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i)) by AMI_1:51 ;
:: thesis: verum

end;

set c3 = len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1));
A57: len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) = (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) by FINSEQ_1:35;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) by AMI_1:123;
A58: len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) = (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (len (aSeq (intloc 1),((len r) + 1))) by FINSEQ_1:35;
then A59: Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) = Comput (ProgramPart s),(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),(len (aSeq (intloc 1),((len r) + 1))) by AMI_1:51;
A60: ( (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (intloc 0 ) = 1 & IC (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) & intloc 2 <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq (intloc 2),pr1) holds
(aSeq (intloc 2),pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1) ) )

proof

thus (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (intloc 0 ) = 1 by A59, A47, Th36, T; :: thesis: ( IC (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) & intloc 2 <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq (intloc 2),pr1) holds
(aSeq (intloc 2),pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1) ) )
thus IC (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) by A58, A59, A47, Th36, T; :: thesis: ( intloc 2 <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq (intloc 2),pr1) holds
(aSeq (intloc 2),pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1) ) )
thus intloc 2 <> intloc 0 by AMI_3:52; :: thesis: for c being Element of NAT st c in dom (aSeq (intloc 2),pr1) holds
(aSeq (intloc 2),pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1)
let c be Element of NAT ; :: thesis: ( c in dom (aSeq (intloc 2),pr1) implies (aSeq (intloc 2),pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1) )
assume A61: c in dom (aSeq (intloc 2),pr1) ; :: thesis: (aSeq (intloc 2),pr1) . c = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1)
then A62: (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c in dom (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) by FINSEQ_1:41;
then (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c >= 1 by FINSEQ_3:27;
then ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1 = ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) - 1 by XREAL_1:235;
then A63: (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1) + 1 = (len ((((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))*>) ^ (FlattenSeq pp0)) ^ ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A27, A34, A45, FINSEQ_6:12;
then A64: ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by FINSEQ_1:45;
then dom (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) c= dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
then A65: ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1 in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by A14, A62;
thus (aSeq (intloc 2),pr1) . c = (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) by A61, FINSEQ_1:def 7
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) by A62, A64, GRFUNC_1:8
.= (Load ((((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) -' 1) by A11, A65, A63
.= s . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1) by A5, A65, GRFUNC_1:8
.= (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1) by AMI_1:54 ; :: thesis: verum

end;

then A66: (Comput (ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))))),(Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),(len (aSeq (intloc 2),pr1))) . (intloc 2) = pr1 by Th36;
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) by AMI_1:123;
A67: (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . f = (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)))) . f by FINSEQ_1:35
.= (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),(len (aSeq (intloc 2),pr1))) . f by AMI_1:51
.= (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . f by A60, Th36, S
.= (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f by A59, A47, Th36, T ;

A68: now

let i be Element of NAT ; :: thesis: ( i <= len (aSeq (intloc 2),pr1) implies (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i = IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i)) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) by AMI_1:123;
assume i <= len (aSeq (intloc 2),pr1) ; :: thesis: (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i = IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i))
hence (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i = IC (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),i) by A60, Th36, T
.= IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i)) by AMI_1:51 ;
:: thesis: verum

end;

A69: for i being Element of NAT st i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i

proof

let i be Element of NAT ; :: thesis: ( i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) implies IC (Comput (ProgramPart s),s,i) = i )
assume A70: i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i

A71: now

A72: i < (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len (FlattenSeq pp1)) by A70, FINSEQ_1:35;
assume A73: not i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ; :: thesis: ( ( not (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ) implies ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) )
assume ( not (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ) ; :: thesis: ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) )
hence ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) by A42, A73, A72, NAT_1:13; :: thesis: verum

end;

per cases ( i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) or ( (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ) or ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) ) by A71;

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

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

end;

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

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

end;

suppose A75: ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i

then ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1) - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) <= i - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) by XREAL_1:11;
then reconsider ii = i - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) as Element of NAT by INT_1:16;
i - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) <= ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) by A75, XREAL_1:11;
hence i = IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + ii)) by A68
.= IC (Comput (ProgramPart s),s,i) ;
:: thesis: verum

end;

end;

end;

A76: len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) = ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (len (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) by A58, FINSEQ_1:35;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) /. (IC (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) = (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (IC (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) by COMPOS_1:38;
A77: len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) = ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) + 1 by A42, FINSEQ_1:35;
then A78: len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) > (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) by NAT_1:13;
then CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) = (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) by A57, A69, Y
.= ((((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))) + 1) by A9, A57, A55
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) + 1) by A54, A57, A45, A43, A40, FINSEQ_4:98
.= ((((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)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) + (len <*(f,(intloc 1) := (intloc 2))*>)) by FINSEQ_1:57
.= ((((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)) + (len <*(f,(intloc 1) := (intloc 2))*>)))) by A76 ;
then A79: CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (len (((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) ^ <*(f,(intloc 1) := (intloc 2))*>))) by Lm1
.= (((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)) ^ <*(f,(intloc 1) := (intloc 2))*>)) by A27, A34, A38, FINSEQ_1:86
.= (((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))) + (len <*(f,(intloc 1) := (intloc 2))*>)) by FINSEQ_1:35
.= <*(f,(intloc 1) := (intloc 2))*> . (len <*(f,(intloc 1) := (intloc 2))*>) by A39, FINSEQ_1:86
.= <*(f,(intloc 1) := (intloc 2))*> . 1 by FINSEQ_1:57
.= f,(intloc 1) := (intloc 2) by FINSEQ_1:57 ;
s: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by AMI_1:123;
A80: Comput (ProgramPart s),s,((len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by AMI_1:14
.= Exec (f,(intloc 1) := (intloc 2)),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by A79, s ;
then A81: IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) = succ (IC (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) by A57, A43, SCMFSA_2:99
.= succ (len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) by A57, A69, A78
.= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) by A57, A77, NAT_1:39 ;
thus for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i :: thesis: ( ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g ) )

proof

let i be Element of NAT ; :: thesis: ( i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) implies IC (Comput (ProgramPart s),s,i) = i )
assume A82: i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i

per cases ( i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) or i = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ) by A82, XXREAL_0:1;

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

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

end;

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

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

end;

end;

end;

t: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) by AMI_1:123;
A83: (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (intloc 2) = (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)))) . (intloc 2) by FINSEQ_1:35
.= p . ((len r) + 1) by A26, A66, t, AMI_1:51 ;
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) by AMI_1:123;
consider ki being Element of NAT such that
A84: ki = abs ((Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (intloc 1)) and
A85: (Exec (f,(intloc 1) := (intloc 2)),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) . f = ((Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . f) +* ki,((Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (intloc 2)) by SCMFSA_2:99;
A86: ki = abs ((Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)))) . (intloc 1)) by A84, FINSEQ_1:35
.= abs ((Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),(len (aSeq (intloc 2),pr1))) . (intloc 1)) by AMI_1:51
.= abs ((Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (intloc 1)) by A2, A60, Th36, S
.= (len r) + 1 by A59, A53, T, ABSVALUE:def 1 ;
A87: dom ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = Seg (len p) by A31, FINSEQ_1:def 3;
for i being Element of NAT st i in Seg (len pp1) holds
(((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i

proof

let i be Element of NAT ; :: thesis: ( i in Seg (len pp1) implies (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i )
assume A88: i in Seg (len pp1) ; :: thesis: (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
then A89: i <= len pp1 by FINSEQ_1:3;

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

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

then A91: i = (len pp0) + 1 by FINSEQ_2:19;
hence (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A57, A77, A80, A85, A86, A83, A67, A90, FINSEQ_1:6, FUNCT_1:72
.= p . i by A15, A28, A25, A87, A91, FUNCT_7:33
.= (p | (Seg (len pp1))) . i by A90, A91, FINSEQ_1:6, FUNCT_1:72 ;
:: thesis: verum

end;

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

then i < len pp1 by A89, XXREAL_0:1;
then i < (len pp0) + 1 by FINSEQ_2:19;
then A93: i <= len pp0 by NAT_1:13;
1 <= i by A88, FINSEQ_1:3;
then A94: i in Seg (len pp0) by A93;
A95: i <> (len r) + 1 by A28, A92, FINSEQ_2:19;
(((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A57, A77, A80, A85, A86, A83, A67, A88, FUNCT_1:72
.= ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) . i by A95, FUNCT_7:34 ;
hence (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp0))) . i by A30, A94, FUNCT_1:72
.= p . i by A94, FUNCT_1:72
.= (p | (Seg (len pp1))) . i by A88, FUNCT_1:72 ;
:: thesis: verum

end;

end;

end;

then A96: for i being set st i in Seg (len pp1) holds
(((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i ;
A97: dom (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = dom ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) by FUNCT_7:32;
then dom ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = Seg (len p) by A31, A57, A43, A80, A85, A86, A83, A67, FINSEQ_1:def 3;
then dom (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) = Seg (len pp1) by A36, RELAT_1:91;
hence ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) by A37, A96, FUNCT_1:9; :: thesis: ( len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
len (((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) by A97, FINSEQ_3:31;
hence len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = len p by A31, A43, A80, A85, A86, A83, A67, FINSEQ_1:35; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g ) )

hereby :: thesis: for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g

let b be Int-Location ; :: thesis: ( b <> intloc 1 & b <> intloc 2 implies (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b )
assume that
A98: b <> intloc 1 and
A99: b <> intloc 2 ; :: thesis: (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) by AMI_1:123;
thus (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)))) . b by A57, A43, A80, SCMFSA_2:99
.= (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),(len (aSeq (intloc 2),pr1))) . b by AMI_1:51
.= (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . b by A60, A99, Th36, S
.= (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b by A59, A47, A98, Th36, T
.= s . b by A32, A98, A99 ; :: thesis: verum

end;

hereby :: thesis: verum

let h be FinSeq-Location ; :: thesis: ( h <> f implies (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . h = s . h )
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) by AMI_1:123;
assume A100: h <> f ; :: thesis: (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . h = s . h
hence (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . h = (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)))) . h by A57, A43, A80, SCMFSA_2:99
.= (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),(len (aSeq (intloc 2),pr1))) . h by AMI_1:51
.= (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . h by A60, Th36, S
.= (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . h by A59, A47, Th36, T
.= s . h by A33, A100 ;
:: thesis: verum

end;

end;

set k = len (aSeq (intloc 1),(len p));
A101: len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) = (len (aSeq (intloc 1),(len p))) + 1 by FINSEQ_2:19;
A102: (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>) by FINSEQ_1:45;
then (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = (aSeq (intloc 1),(len p)) ^ (<*(f :=<0,...,0> (intloc 1))*> ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by FINSEQ_1:45;
then Load (aSeq (intloc 1),(len p)) c= f := p by Th31;
then A103: Load (aSeq (intloc 1),(len p)) c= s by A5, XBOOLE_1:1;
then A104: (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) . (intloc 1) = len p by A1, A3, A4, Th37;
A105: S₁[ {} ]

proof

A106: now

let i be Element of NAT ; :: thesis: ( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies IC (Comput (ProgramPart s),s,i) = i )
assume A107: i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies i <= len (aSeq (intloc 1),(len p)) ) by A101, NAT_1:13;
hence IC (Comput (ProgramPart s),s,i) = i by A1, A3, A4, A103, A107, Th37; :: thesis: verum

end;

A108: 1 <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A101, NAT_1:11;
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 (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . g = s . g ) )
reconsider sD = <*> (the Instructions of SCM+FSA * ) as FinSequence of the Instructions of SCM+FSA * ;
take sD ; :: thesis: ( sD = {} & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . g = s . g ) )
A109: ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * ))) = ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (<*> the Instructions of SCM+FSA ) by PRE_POLY:2
.= (aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*> by FINSEQ_1:47 ;
len (aSeq (intloc 1),(len p)) < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A101, NAT_1:13;
then A110: IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) = len (aSeq (intloc 1),(len p)) by A106;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) /. (IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) = (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) . (IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) by COMPOS_1:38;
len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by A102, FINSEQ_1:35;
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 len (aSeq (intloc 1),(len p)) < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A101, NAT_1:13;
then A111: CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))),(Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) by A101, A9, A110, Y
.= ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) . (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) by A102, A108, FINSEQ_1:85
.= f :=<0,...,0> (intloc 1) by A101, FINSEQ_1:59 ;
thus sD = {} ; :: thesis: ( ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)) holds
IC (Comput (ProgramPart s),s,i) = i ) & ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . g = s . g ) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) by AMI_1:123;
A112: Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) = Following (ProgramPart s),(Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) by A101, AMI_1:14
.= Exec (f :=<0,...,0> (intloc 1)),(Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) by A111, T ;
then A113: IC (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) = succ (IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) by SCMFSA_2:101
.= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A101, A110, NAT_1:39 ;

now

let i be Element of NAT ; :: thesis: ( i <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies IC (Comput (ProgramPart s),s,i) = i )
assume i <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
then ( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) or i = len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ) by XXREAL_0:1;
hence IC (Comput (ProgramPart s),s,i) = i by A106, A113; :: thesis: verum

end;

hence for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)) holds
IC (Comput (ProgramPart s),s,i) = i by A109; :: thesis: ( ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) & len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . g = s . g ) )
consider ki being Element of NAT such that
A114: ki = abs ((Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) . (intloc 1)) and
A115: (Exec (f :=<0,...,0> (intloc 1)),(Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) . f = ki |-> 0 by SCMFSA_2:101;
((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) | (Seg 0 ) = p | (Seg (len sD)) ;
hence ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) | (Seg (len sD)) = p | (Seg (len sD)) ; :: thesis: ( len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . g = s . g ) )
ki = len p by A104, A114, ABSVALUE:def 1;
hence len ((Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . f) = len p by A109, A112, A115, FINSEQ_1:def 18; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq sD)))) . g = s . g ) )

now

let b be Int-Location ; :: thesis: ( b <> intloc 1 & b <> intloc 2 implies (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . b = s . b )
assume that
A116: b <> intloc 1 and
b <> intloc 2 ; :: thesis: (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . b = s . b
thus (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . b = (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) . b by A112, SCMFSA_2:101
.= s . b by A1, A3, A4, A103, A116, Th37 ; :: thesis: verum

end;

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

now

let g be FinSeq-Location ; :: thesis: ( g <> f implies (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . g = s . g )
assume g <> f ; :: thesis: (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . g = s . g
hence (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . g = (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) . g by A112, SCMFSA_2:101
.= s . g by A1, A3, A4, A103, Th37 ;
:: thesis: verum

end;

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

end;

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