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

A6: now

let k be Element of NAT ; :: thesis: ( insloc 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 )*>)) . (insloc k) = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) )
assume A7: insloc 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 )*>)) . (insloc k) = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1)
then A8: 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 )*>)) . (insloc k) = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (k + 1) by A7, Def1
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) by A8, PARTFUN1:def 8 ; :: thesis: verum

end;

consider pp being FinSequence of the Instructions of SCM+FSA * such that
A9: len pp = len p and
A10: 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
A11: aSeq f,p = FlattenSeq pp by Def4;
set k = len (aSeq (intloc 1),(len p));
A12: len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) = (len (aSeq (intloc 1),(len p))) + 1 by FINSEQ_2:19;
A13: (((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 A14: Load (aSeq (intloc 1),(len p)) c= s by A4, XBOOLE_1:1;
then A15: ( ( for i being Element of NAT st i <= len (aSeq (intloc 1),(len p)) holds
( IC (Computation s,i) = insloc i & ( for b being Int-Location st b <> intloc 1 holds
(Computation s,i) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,i) . f = s . f ) ) ) & (Computation s,(len (aSeq (intloc 1),(len p)))) . (intloc 1) = len p ) by A1, A2, A3, Th37;

A16: now

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

end;

A19: 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 (Computation s,k) . (insloc 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: (Computation s,k) . (insloc i) = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A20: insloc i in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by Th29;
thus (Computation s,k) . (insloc i) = s . (insloc i) by AMI_1:54
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) by A16, A20 ; :: thesis: verum

end;

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 (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Computation 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
(Computation 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
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . g = s . g ) ) );
A21: S₁[ {} ]

proof

A22: ((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 DTCONSTR:20
.= (aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*> by FINSEQ_1:47 ;
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 (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Computation 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
(Computation 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
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . g = s . g ) )
take <*> (the Instructions of SCM+FSA * ) ; :: thesis: ( <*> (the Instructions of SCM+FSA * ) = {} & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) | (Seg (len (<*> (the Instructions of SCM+FSA * )))) = p | (Seg (len (<*> (the Instructions of SCM+FSA * )))) & len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )
thus <*> (the Instructions of SCM+FSA * ) = {} ; :: thesis: ( ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) | (Seg (len (<*> (the Instructions of SCM+FSA * )))) = p | (Seg (len (<*> (the Instructions of SCM+FSA * )))) & len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )

A23: now

let i be Element of NAT ; :: thesis: ( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies IC (Computation s,i) = insloc i )
assume A24: i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ; :: thesis: IC (Computation s,i) = insloc i
( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies i <= len (aSeq (intloc 1),(len p)) ) by A12, NAT_1:13;
hence IC (Computation s,i) = insloc i by A1, A2, A3, A14, A24, Th37; :: thesis: verum

end;

len (aSeq (intloc 1),(len p)) < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A12, NAT_1:13;
then A25: IC (Computation s,(len (aSeq (intloc 1),(len p)))) = insloc (len (aSeq (intloc 1),(len p))) by A23;
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 A13, 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 A26: len (aSeq (intloc 1),(len p)) < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A12, NAT_1:13;
A27: 1 <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A12, NAT_1:11;
A28: CurInstr (Computation 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 A12, A19, A25, A26
.= ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) . (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) by A13, A27, FINSEQ_1:85
.= f :=<0,...,0> (intloc 1) by A12, FINSEQ_1:59 ;
A29: Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) = Following (Computation s,(len (aSeq (intloc 1),(len p)))) by A12, AMI_1:14
.= Exec (f :=<0,...,0> (intloc 1)),(Computation s,(len (aSeq (intloc 1),(len p)))) by A28 ;
then A30: IC (Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) = Next (IC (Computation s,(len (aSeq (intloc 1),(len p))))) by SCMFSA_2:101
.= insloc (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) by A12, A25, 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 (Computation s,i) = insloc i )
assume i <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ; :: thesis: IC (Computation s,i) = insloc 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 (Computation s,i) = insloc i by A23, A30; :: thesis: verum

end;

hence for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Computation s,i) = insloc i by A22; :: thesis: ( ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) | (Seg (len (<*> (the Instructions of SCM+FSA * )))) = p | (Seg (len (<*> (the Instructions of SCM+FSA * )))) & len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )
len (<*> (the Instructions of SCM+FSA * )) = 0 by FINSEQ_1:32;
hence ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) | (Seg (len (<*> (the Instructions of SCM+FSA * )))) = p | (Seg (len (<*> (the Instructions of SCM+FSA * )))) by FINSEQ_1:94; :: thesis: ( len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )
consider ki being Element of NAT such that
A31: ( ki = abs ((Computation s,(len (aSeq (intloc 1),(len p)))) . (intloc 1)) & (Exec (f :=<0,...,0> (intloc 1)),(Computation s,(len (aSeq (intloc 1),(len p))))) . f = ki |-> 0 ) by SCMFSA_2:101;
ki = len p by A15, A31, ABSVALUE:def 1;
hence len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p by A22, A29, A31, FINSEQ_1:def 18; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )

now

let b be Int-Location ; :: thesis: ( b <> intloc 1 & b <> intloc 2 implies (Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . b = s . b )
assume A32: ( b <> intloc 1 & b <> intloc 2 ) ; :: thesis: (Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . b = s . b
thus (Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . b = (Computation s,(len (aSeq (intloc 1),(len p)))) . b by A29, SCMFSA_2:101
.= s . b by A1, A2, A3, A14, A32, Th37 ; :: thesis: verum

end;

hence for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b by A22; :: thesis: for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g

now

let g be FinSeq-Location ; :: thesis: ( g <> f implies (Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . g = s . g )
assume A33: g <> f ; :: thesis: (Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . g = s . g
thus (Computation s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . g = (Computation s,(len (aSeq (intloc 1),(len p)))) . g by A29, A33, SCMFSA_2:101
.= s . g by A1, A2, A3, A14, Th37 ; :: thesis: verum

end;

hence for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g by A22; :: thesis: verum

end;

A34: 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 A35: S₁[r] ; :: thesis: S₁[r ^ <*x*>]
assume A36: 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 (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Computation 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
(Computation 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
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . g = s . g ) )
r c= r ^ <*x*> by FINSEQ_6:12;
then consider pp0 being FinSequence of the Instructions of SCM+FSA * such that
A37: pp0 = r and
A38: for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Computation s,i) = insloc i and
A39: ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) and
A40: len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = len p and
A41: for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b = s . b and
A42: for h being FinSeq-Location st h <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . h = s . h by A35, A36, XBOOLE_1:1;
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 A43: (len r) + 1 in dom (r ^ <*x*>) by FINSEQ_1:def 3;
A44: dom (r ^ <*x*>) c= dom pp by A36, GRFUNC_1:8;
then (len r) + 1 in dom pp by A43;
then A45: (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
A46: pr1 = p . ((len r) + 1) and
A47: pp . ((len r) + 1) = ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) ^ <*(f,(intloc 1) := (intloc 2))*> by A9, A10;

A48: now

thus x = (r ^ <*x*>) . ((len r) + 1) by FINSEQ_1:59
.= pp . ((len r) + 1) by A36, A43, GRFUNC_1:8 ; :: thesis: verum

end;

then x in the Instructions of SCM+FSA * by A43, A44, 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 (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Computation 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
(Computation 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
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
thus pp1 = r ^ <*x*> by A37; :: thesis: ( ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Computation 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
(Computation 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
(Computation 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 A43, A44, A48, FINSEQ_2:13;
A49: x = (aSeq (intloc 1),((len r) + 1)) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>) by A47, A48, FINSEQ_1:45;
A50: FlattenSeq pp1 c= FlattenSeq pp by A36, A37, DTCONSTR:24;
A51: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <*x*>) by DTCONSTR:21
.= (FlattenSeq pp0) ^ x by DTCONSTR:13 ;
then A52: ((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 FINSEQ_1:45;
set c1 = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0));
set s1 = Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)));
set c2 = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)));
set s2 = Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))));
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));
A53: 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 A54: Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) = Computation (Computation 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;
A55: 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 A53, FINSEQ_1:35;
A56: 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;

A57: 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 A50, A51, 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 A58: (((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 A11, 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 A58, XBOOLE_1:1; :: thesis: verum

end;

A59: ( (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (intloc 0 ) = 1 & IC (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = insloc (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 = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)) ) )

proof

A60: (((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 A49, A57, FINSEQ_6:12;
then A61: dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) c= dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
thus (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (intloc 0 ) = 1 by A1, A3, A41; :: thesis: ( IC (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = insloc (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 = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)) ) )
thus IC (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = insloc (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) by A38; :: 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 = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (insloc (((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 = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (insloc (((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 = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)) )
assume A62: c in dom (aSeq (intloc 1),((len r) + 1)) ; :: thesis: (aSeq (intloc 1),((len r) + 1)) . c = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1))
then A63: (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 A64: insloc (((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 A5, A61;
(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c >= 1 by A63, 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 A65: (((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 ;
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 A62, 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 A60, A63, GRFUNC_1:8
.= (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)) by A6, A64, A65
.= s . (insloc (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)) by A4, A64, GRFUNC_1:8
.= (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) -' 1)) by AMI_1:54 ; :: thesis: verum

end;

then A66: ( ( for i being Element of NAT st i <= len (aSeq (intloc 1),((len r) + 1)) holds
( IC (Computation (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),i) = insloc ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i) & ( for b being Int-Location st b <> intloc 1 holds
(Computation (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),i) . b = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b ) & ( for f being FinSeq-Location holds (Computation (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),i) . f = (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f ) ) ) & (Computation (Computation 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;

A67: now

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

end;

A68: ( (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (intloc 0 ) = 1 & IC (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = insloc (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 = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (insloc (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1)) ) )

proof

thus (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (intloc 0 ) = 1 by A54, A59, Th36; :: thesis: ( IC (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = insloc (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 = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (insloc (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1)) ) )
thus IC (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = insloc (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) by A53, A54, A59, Th36; :: 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 = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (insloc (((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 = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (insloc (((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 = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (insloc (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1)) )
assume A69: c in dom (aSeq (intloc 2),pr1) ; :: thesis: (aSeq (intloc 2),pr1) . c = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (insloc (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1))
then A70: (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;
(((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 A47, A48, A57, FINSEQ_6:12;
then A71: ((((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 A72: insloc (((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 A5, A70;
(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c >= 1 by A70, 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 A73: (((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 ;
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 A69, 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 A70, A71, GRFUNC_1:8
.= (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1)) by A6, A72, A73
.= s . (insloc (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) -' 1)) by A4, A72, GRFUNC_1:8
.= (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (insloc (((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 A74: ( ( for i being Element of NAT st i <= len (aSeq (intloc 2),pr1) holds
( IC (Computation (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),i) = insloc ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i) & ( for b being Int-Location st b <> intloc 2 holds
(Computation (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),i) . b = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . b ) & ( for f being FinSeq-Location holds (Computation (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),i) . f = (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . f ) ) ) & (Computation (Computation 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;

A75: now

let i be Element of NAT ; :: thesis: ( i <= len (aSeq (intloc 2),pr1) implies insloc ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i) = IC (Computation s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i)) )
assume i <= len (aSeq (intloc 2),pr1) ; :: thesis: insloc ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i) = IC (Computation s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i))
hence insloc ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i) = IC (Computation (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),i) by A68, Th36
.= IC (Computation 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;

A76: (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 A49, A51, 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 ;
A77: for i being Element of NAT st i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Computation s,i) = insloc 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 (Computation s,i) = insloc i )
assume A78: i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Computation s,i) = insloc i

A79: now

assume A80: 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 A81: ( 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)) )
i < (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len (FlattenSeq pp1)) by A78, FINSEQ_1:35;
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 A76, A80, A81, 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 A79;

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

hence IC (Computation s,i) = insloc i by A38; :: thesis: verum

end;

suppose A82: ( (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 (Computation s,i) = insloc i

then A83: ((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;
A84: 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 A82, XREAL_1:11;
reconsider ii = i - (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) as Element of NAT by A83, INT_1:16;
thus insloc i = IC (Computation s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + ii)) by A53, A67, A84
.= IC (Computation s,i) ; :: thesis: verum

end;

suppose A85: ( (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 (Computation s,i) = insloc i

then A86: ((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;
A87: 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 A85, XREAL_1:11;
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 A86, INT_1:16;
thus insloc i = IC (Computation s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + ii)) by A75, A87
.= IC (Computation s,i) ; :: thesis: verum

end;

end;

end;

A88: 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 A76, FINSEQ_1:35;
A89: ( 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 & 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 A76, FINSEQ_1:35, NAT_1:11;
A90: 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 A88, NAT_1:13;
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 A52, A57, FINSEQ_1:84;
then A91: (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 A89, NAT_1:13;
A92: 1 <= len <*(f,(intloc 1) := (intloc 2))*> by FINSEQ_1:57;
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 A93: 1 <= len x by A47, A48, FINSEQ_1:57;

now

thus CurInstr (Computation s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) = (Computation s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (insloc (len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by A56, A77, A90
.= ((((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 A19, A56, A91
.= ((((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 A52, A56, A57, A89, 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 A55 ; :: thesis: verum

end;

then A94: CurInstr (Computation 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 A47, A48, A93, 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 A92, FINSEQ_1:86
.= <*(f,(intloc 1) := (intloc 2))*> . 1 by FINSEQ_1:57
.= f,(intloc 1) := (intloc 2) by FINSEQ_1:57 ;

A95: now

thus Computation 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 (Computation 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)),(Computation 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 A94 ; :: thesis: verum

end;

A96: now

thus IC (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) = Next (IC (Computation s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) by A56, A89, A95, SCMFSA_2:99
.= Next (insloc (len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by A56, A77, A90
.= insloc (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1))) by A56, A88, NAT_1:39 ; :: thesis: verum

end;

thus for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Computation s,i) = insloc i :: thesis: ( ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Computation 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
(Computation 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
(Computation 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 (Computation s,i) = insloc i )
assume A97: i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Computation s,i) = insloc 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 A97, XXREAL_0:1;

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

hence IC (Computation s,i) = insloc i by A77; :: thesis: verum

end;

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

hence IC (Computation s,i) = insloc i by A96; :: thesis: verum

end;

end;

end;

consider ki being Element of NAT such that
A98: ( ki = abs ((Computation 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)) & (Exec (f,(intloc 1) := (intloc 2)),(Computation 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 = ((Computation 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,((Computation 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;

A99: now

thus ki = abs ((Computation 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 A98, FINSEQ_1:35
.= abs ((Computation (Computation 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 ((Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . (intloc 1)) by A1, A68, Th36
.= (len r) + 1 by A54, A66, ABSVALUE:def 1 ; :: thesis: verum

end;

A100: now

thus (Computation 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) = (Computation 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 A46, A74, AMI_1:51 ; :: thesis: verum

end;

A101: now

thus (Computation 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 = (Computation 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
.= (Computation (Computation 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
.= (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . f by A68, Th36
.= (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f by A54, A59, Th36 ; :: thesis: verum

end;

A102: dom ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = Seg (len p) by A40, FINSEQ_1:def 3;
A103: dom (((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = dom ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) by FUNCT_7:32;
then A104: len (((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) by FINSEQ_3:31;
len pp1 <= len pp by A36, A37, FINSEQ_1:84;
then A105: Seg (len pp1) c= Seg (len p) by A9, FINSEQ_1:7;
dom ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = Seg (len p) by A40, A56, A89, A95, A98, A99, A100, A101, A103, FINSEQ_1:def 3;
then A106: dom (((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) = Seg (len pp1) by A105, RELAT_1:91;
Seg (len pp1) c= dom p by A105, FINSEQ_1:def 3;
then A107: dom (p | (Seg (len pp1))) = Seg (len pp1) by RELAT_1:91;
for i being Element of NAT st i in Seg (len pp1) holds
(((Computation 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 (((Computation 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 A108: i in Seg (len pp1) ; :: thesis: (((Computation 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 A109: ( 1 <= i & i <= len pp1 ) by FINSEQ_1:3;

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

suppose A110: i = len pp1 ; :: thesis: (((Computation 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 A111: i = (len pp0) + 1 by FINSEQ_2:19;
hence (((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A56, A88, A95, A98, A99, A100, A101, A110, FINSEQ_1:6, FUNCT_1:72
.= p . i by A9, A37, A45, A102, A111, FUNCT_7:33
.= (p | (Seg (len pp1))) . i by A110, A111, FINSEQ_1:6, FUNCT_1:72 ;
:: thesis: verum

end;

suppose A112: i <> len pp1 ; :: thesis: (((Computation 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 A113: i <> (len r) + 1 by A37, FINSEQ_2:19;
( 1 <= i & i < len pp1 ) by A109, A112, XXREAL_0:1;
then ( 1 <= i & i < (len pp0) + 1 ) by FINSEQ_2:19;
then ( 1 <= i & i <= len pp0 ) by NAT_1:13;
then A114: i in Seg (len pp0) by FINSEQ_1:3;

now

thus (((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A56, A88, A95, A98, A99, A100, A101, A108, FUNCT_1:72
.= ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) . i by A113, FUNCT_7:34 ; :: thesis: verum

end;

hence (((Computation 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 A39, A114, FUNCT_1:72
.= p . i by A114, FUNCT_1:72
.= (p | (Seg (len pp1))) . i by A108, FUNCT_1:72 ;
:: thesis: verum

end;

end;

end;

then for i being set st i in Seg (len pp1) holds
(((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i ;
hence ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) by A106, A107, FUNCT_1:9; :: thesis: ( len ((Computation 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
(Computation 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
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
thus len ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . f) = len p by A40, A89, A95, A98, A99, A100, A101, A104, FINSEQ_1:35; :: thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Computation 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
(Computation 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
(Computation 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 (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b )
assume A115: ( b <> intloc 1 & b <> intloc 2 ) ; :: thesis: (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = s . b
thus (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . b = (Computation 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 A56, A89, A95, SCMFSA_2:99
.= (Computation (Computation 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
.= (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . b by A68, A115, Th36
.= (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b by A54, A59, A115, Th36
.= s . b by A41, A115 ; :: thesis: verum

end;

hereby :: thesis: verum

let h be FinSeq-Location ; :: thesis: ( h <> f implies (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . h = s . h )
assume A116: h <> f ; :: thesis: (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . h = s . h
hence (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) . h = (Computation 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 A56, A89, A95, SCMFSA_2:99
.= (Computation (Computation 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
.= (Computation s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . h by A68, Th36
.= (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . h by A54, A59, Th36
.= s . h by A42, A116 ;
:: thesis: verum

end;

end;

for r being FinSequence holds S₁[r] from FINSEQ_1:sch 3(A21, A34);
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 (Computation s,i) = insloc i and
A119: ((Computation 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 ((Computation 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
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . b = s . b and
A122: for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . g = s . g ;
A123: IC (Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)))) = insloc (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))) by A117, A118;
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 A11, FINSEQ_2:19;
then 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;
then A124: CurInstr (Computation 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 A19, A123
.= halt SCM+FSA by A11, FINSEQ_1:59 ;
hence s is halting by AMI_1:def 20; :: 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 A125: Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))) = Result s by A124, AMI_1:def 22;
dom ((Computation s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . f) = Seg (len pp0) by A9, A117, A120, FINSEQ_1:def 3;
then A126: (Result s) . f = p | (Seg (len pp0)) by A117, A119, A125, RELAT_1:97;
dom p = Seg (len pp0) by A9, A117, FINSEQ_1:def 3;
hence (Result s) . f = p by A126, 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 A117, A121, A122, A125; :: thesis: verum