set O = intloc 0 ;
set D = the Instructions of SCM+FSA ;
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
A1: IC s = insloc 0 and
A2: s . (intloc 0 ) = 1 ; :: thesis: for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
( 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 ) ) )
( intloc 0 <> intloc 1 & intloc 0 <> intloc 2 ) by AMI_3:52;
then reconsider a1 = intloc 1, a2 = intloc 2 as read-write Int-Location by SF_MASTR:def 5;
A3: a1 <> a2 by AMI_3:52;
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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>;
set q0 = (aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>;
A5: f := p = Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:def 5;
A6: dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) = { (m -' 1) where m is Element of NAT : m in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) } by SCMFSA_7:def 1;

A7: now

let k be Element of NAT ; :: thesis: ( insloc k in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc k) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) )
assume A8: insloc k in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc k) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1)
then A9: k + 1 in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:26;
thus (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc k) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (k + 1) by A8, SCMFSA_7:def 1
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) by A9, PARTFUN1:def 8 ; :: thesis: verum

end;

consider pp being FinSequence of the Instructions of SCM+FSA * such that
A10: len pp = len p and
A11: for k being Element of NAT st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq a1,k) ^ (aSeq a2,i)) ^ <*(f,a1 := a2)*> ) and
A12: aSeq f,p = FlattenSeq pp by SCMFSA_7:def 4;
set k = len (aSeq a1,(len p));
A13: len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) = (len (aSeq a1,(len p))) + 1 by FINSEQ_2:19;
A14: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>) by FINSEQ_1:45;

A15: now

(((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = (aSeq a1,(len p)) ^ (<*(f :=<0,...,0> a1)*> ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by A14, FINSEQ_1:45;
then Load (aSeq a1,(len p)) c= f := p by A5, SCMFSA_7:31;
hence Load (aSeq a1,(len p)) c= s by A4, XBOOLE_1:1; :: thesis: verum

end;

A16: now

let i be Element of NAT ; :: thesis: ( insloc i in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies s . (insloc i) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume A17: insloc i in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: s . (insloc i) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A18: i + 1 in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:26;
s . (insloc i) = (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc i) by A4, A5, A17, GRFUNC_1:8;
then s . (insloc i) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A17, SCMFSA_7:def 1;
hence s . (insloc i) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) implies (Computation s,k) . (insloc i) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume i < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) ; :: thesis: (Computation s,k) . (insloc i) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A20: insloc i in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by SCMFSA_7:29;
thus (Computation s,k) . (insloc i) = s . (insloc i) by AMI_1:54
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . g = s . g ) ) );
A21: S₁[ {} ]

proof

A22: ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * ))) = ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (<*> the Instructions of SCM+FSA ) by DTCONSTR:20
.= (aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*> 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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )

A23: now

let i be Element of NAT ; :: thesis: ( i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) implies IC (Computation s,i) = insloc i )
assume A24: i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ; :: thesis: IC (Computation s,i) = insloc i
( i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) implies i <= len (aSeq a1,(len p)) ) by A13, NAT_1:13;
hence IC (Computation s,i) = insloc i by A1, A2, A15, A24, SCMFSA_7:37; :: thesis: verum

end;

len (aSeq a1,(len p)) < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) by A13, NAT_1:13;
then A25: IC (Computation s,(len (aSeq a1,(len p)))) = insloc (len (aSeq a1,(len p))) by A23;
len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by A14, FINSEQ_1:35;
then len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by NAT_1:11;
then A26: len (aSeq a1,(len p)) < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A13, NAT_1:13;
A27: 1 <= len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) by A13, NAT_1:11;
A28: CurInstr (Computation s,(len (aSeq a1,(len p)))) = (Computation s,(len (aSeq a1,(len p)))) . (insloc (len (aSeq a1,(len p)))) by A25, AMI_1:def 17
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) by A13, A19, A26
.= ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) . (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) by A14, A27, FINSEQ_1:85
.= f :=<0,...,0> a1 by A13, FINSEQ_1:59 ;
A29: Computation s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) = Following (Computation s,(len (aSeq a1,(len p)))) by A13, AMI_1:14
.= Exec (f :=<0,...,0> a1),(Computation s,(len (aSeq a1,(len p)))) by A28, AMI_1:def 18 ;
A30: IC (Computation s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) = (Computation s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (IC (Computation s,(len (aSeq a1,(len p))))) by A29, SCMFSA_2:101
.= insloc (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) by A13, A25, NAT_1:39 ;

now

let i be Element of NAT ; :: thesis: ( i <= len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) implies IC (Computation s,i) = insloc i )
assume i <= len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ; :: thesis: IC (Computation s,i) = insloc i
then ( i < len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) or i = len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ) by XXREAL_0:1;
hence IC (Computation s,i) = insloc i by A23, A30; :: thesis: verum

end;

hence for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Computation s,i) = insloc i by A22; :: thesis: ( ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )
consider ki being Element of NAT such that
A31: ( ki = abs ((Computation s,(len (aSeq a1,(len p)))) . a1) & (Exec (f :=<0,...,0> a1),(Computation s,(len (aSeq a1,(len p))))) . f = ki |-> 0 ) by SCMFSA_2:101;
ki = abs (len p) by A1, A2, A15, A31, SCMFSA_7:37
.= len p by ABSVALUE:def 1 ;
hence len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g ) )

now

let b be Int-Location ; :: thesis: ( b <> a1 & b <> a2 implies (Computation s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . b = s . b )
assume A32: ( b <> a1 & b <> a2 ) ; :: thesis: (Computation s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . b = s . b
thus (Computation s,(len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>))) . b = (Computation s,(len (aSeq a1,(len p)))) . b by A29, SCMFSA_2:101
.= s . b by A1, A2, A15, A32, SCMFSA_7:37 ; :: thesis: verum

end;

hence for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))))) . g = s . g

now

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

end;

hence for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) & len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . g = s . g ) )

now

r c= r ^ <*x*> by FINSEQ_6:12;
hence r c= pp by A36, XBOOLE_1:1; :: thesis: verum

end;

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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Computation s,i) = insloc i and
A39: ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) and
A40: len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p and
A41: for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b and
A42: for h being FinSeq-Location st h <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . h = s . h by A35;
set r1 = (len r) + 1;

A43: now

len (r ^ <*x*>) = (len r) + 1 by FINSEQ_2:19;
then (len r) + 1 in Seg (len (r ^ <*x*>)) by FINSEQ_1:6;
hence (len r) + 1 in dom (r ^ <*x*>) by FINSEQ_1:def 3; :: thesis: verum

end;

A44: now

dom (r ^ <*x*>) c= dom pp by A36, GRFUNC_1:8;
hence (len r) + 1 in dom pp by A43; :: thesis: verum

end;

then A45: (len r) + 1 in Seg (len pp) by FINSEQ_1:def 3;
then ( 1 <= (len r) + 1 & (len r) + 1 <= len p ) by A10, FINSEQ_1:3;
then consider pr1 being Integer such that
A46: pr1 = p . ((len r) + 1) and
A47: pp . ((len r) + 1) = ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*> by A11;

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 * & x is Element of the Instructions of SCM+FSA * ) by 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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
thus pp1 = r ^ <*x*> by A37; :: thesis: ( ( for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Computation s,i) = insloc i ) & ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
reconsider x = x as Element of the Instructions of SCM+FSA * by A44, A48, FINSEQ_2:13;
A49: x = (aSeq a1,((len r) + 1)) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>) by A47, A48, FINSEQ_1:45;
A50: FlattenSeq pp1 c= FlattenSeq pp by A36, A37, DTCONSTR:24;

A51: now

thus FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <*x*>) by DTCONSTR:21
.= (FlattenSeq pp0) ^ x by DTCONSTR:13 ; :: thesis: verum

end;

then A52: ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1) = (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x by FINSEQ_1:45;
set c1 = len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0));
set c2 = len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)));
set c3 = len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1));
A53: len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) = (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + (len (aSeq a1,((len r) + 1))) by FINSEQ_1:35;
then A54: Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) = Computation (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))),(len (aSeq a1,((len r) + 1))) by AMI_1:51;
A55: len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) = ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + (len (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) by A53, FINSEQ_1:35;
A56: len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) = (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) by FINSEQ_1:35;

A57: now

let p be FinSequence; :: thesis: ( p c= x implies (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> )
assume p c= x ; :: thesis: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>
then (FlattenSeq pp0) ^ p c= (FlattenSeq pp0) ^ x by FINSEQ_6:15;
then (FlattenSeq pp0) ^ p c= FlattenSeq pp by A50, A51, XBOOLE_1:1;
then ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ ((FlattenSeq pp0) ^ p) c= ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp) by FINSEQ_6:15;
then A58: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp) by FINSEQ_1:45;
((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A12, FINSEQ_6:12;
hence (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A58, XBOOLE_1:1; :: thesis: verum

end;

A59: for c being Element of NAT st c in dom (aSeq a1,((len r) + 1)) holds
(aSeq a1,((len r) + 1)) . c = (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1))

proof

let c be Element of NAT ; :: thesis: ( c in dom (aSeq a1,((len r) + 1)) implies (aSeq a1,((len r) + 1)) . c = (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1)) )
assume A60: c in dom (aSeq a1,((len r) + 1)) ; :: thesis: (aSeq a1,((len r) + 1)) . c = (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1))
A61: (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A49, A57, FINSEQ_6:12;
then A62: dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) c= dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
A63: (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c in dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) by A60, FINSEQ_1:41;
then A64: insloc (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by A6, A62;

A65: now

(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c >= 1 by A63, FINSEQ_3:27;
then ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1 = ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) - 1 by XREAL_1:235;
hence (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) + 1 = (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c ; :: thesis: verum

end;

thus (aSeq a1,((len r) + 1)) . c = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) by A60, FINSEQ_1:def 7
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1) + 1) by A61, A63, A65, GRFUNC_1:8
.= (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1)) by A7, A64
.= s . (insloc (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1)) by A4, A5, A64, GRFUNC_1:8
.= (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (insloc (((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + c) -' 1)) by AMI_1:54 ; :: thesis: verum

end;

A66: ( (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . (intloc 0 ) = 1 & IC (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) = insloc (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) ) by A2, A38, A41;

A67: now

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

end;

A68: now

let c be Element of NAT ; :: thesis: ( c in dom (aSeq a2,pr1) implies (aSeq a2,pr1) . c = (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (insloc (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1)) )
assume A69: c in dom (aSeq a2,pr1) ; :: thesis: (aSeq a2,pr1) . c = (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (insloc (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1))
then A70: (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c in dom (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) by FINSEQ_1:41;

A71: now

(((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A47, A48, A57, FINSEQ_6:12;
hence ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1) c= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by FINSEQ_1:45; :: thesis: verum

end;

A72: now

dom (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) c= dom ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A71, GRFUNC_1:8;
hence insloc (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1) in dom (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by A6, A70; :: thesis: verum

end;

A73: now

(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c >= 1 by A70, FINSEQ_3:27;
hence (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1) + 1 = (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) - 1) + 1 by XREAL_1:235
.= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c ;
:: thesis: verum

end;

thus (aSeq a2,pr1) . c = (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)) . ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) by A69, FINSEQ_1:def 7
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) by A70, A71, GRFUNC_1:8
.= (Load ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . (insloc (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1)) by A7, A72, A73
.= s . (insloc (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1)) by A4, A5, A72, GRFUNC_1:8
.= (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (insloc (((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + c) -' 1)) by AMI_1:54 ; :: thesis: verum

end;

A74: ( (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . (intloc 0 ) = 1 & IC (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) = insloc (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) ) by A53, A54, A59, A66, SCMFSA_7:36;

A75: now

let i be Element of NAT ; :: thesis: ( i <= len (aSeq a2,pr1) implies insloc ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i) = IC (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i)) )
assume i <= len (aSeq a2,pr1) ; :: thesis: insloc ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i) = IC (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i))
hence insloc ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i) = IC (Computation (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),i) by A68, A74, SCMFSA_7:36
.= IC (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + i)) by AMI_1:51 ;
:: thesis: verum

end;

A76: now

thus (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (FlattenSeq pp1)) = (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (((FlattenSeq pp0) ^ (aSeq a1,((len r) + 1))) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>))) by A49, A51, FINSEQ_1:45
.= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (((FlattenSeq pp0) ^ (aSeq a1,((len r) + 1))) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>))) by FINSEQ_1:35
.= len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>)) by Lm2
.= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len ((aSeq a2,pr1) ^ <*(f,a1 := a2)*>)) by FINSEQ_1:35
.= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + ((len (aSeq a2,pr1)) + (len <*(f,a1 := a2)*>)) by FINSEQ_1:35 ; :: thesis: verum

end;

A77: now

thus (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (FlattenSeq pp1)) = (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + ((len (aSeq a2,pr1)) + 1) by A76, FINSEQ_1:56
.= ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) + 1 ; :: thesis: verum

end;

A78: for i being Element of NAT st i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Computation s,i) = insloc i

proof

let i be Element of NAT ; :: thesis: ( i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) implies IC (Computation s,i) = insloc i )
assume A79: i < len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Computation s,i) = insloc i

A80: now

assume A81: not i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ; :: thesis: ( ( not (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ) implies ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) ) )
assume A82: ( not (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ) ; :: thesis: ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) )
i < (len ((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>)) + (len (FlattenSeq pp1)) by A79, FINSEQ_1:35;
hence ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) ) by A77, A81, A82, NAT_1:13; :: thesis: verum

end;

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

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

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

end;

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

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

end;

suppose A86: ( (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) ) ; :: thesis: IC (Computation s,i) = insloc i

then A87: ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + 1) - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) <= i - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) by XREAL_1:11;
A88: i - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) <= ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) by A86, XREAL_1:11;
reconsider ii = i - (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) as Element of NAT by A87, INT_1:16;
thus insloc i = IC (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + ii)) by A75, A88
.= IC (Computation s,i) ; :: thesis: verum

end;

end;

end;

A89: ( len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) = ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) + 1 & 1 <= ((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1))) + 1 ) by A77, FINSEQ_1:35, NAT_1:11;
then A90: len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) > (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) by NAT_1:13;

A91: now

len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) <= len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A52, A57, FINSEQ_1:84;
hence (len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)) < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A89, NAT_1:13; :: thesis: verum

end;

A92: 1 <= len <*(f,a1 := a2)*> by FINSEQ_1:57;

A93: now

len <*(f,a1 := a2)*> <= (len ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1))) + (len <*(f,a1 := a2)*>) by NAT_1:12;
then len <*(f,a1 := a2)*> <= len (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>) by FINSEQ_1:35;
hence 1 <= len x by A47, A48, FINSEQ_1:57; :: thesis: verum

end;

A94: now

thus CurInstr (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) = (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . (IC (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) by AMI_1:def 17
.= (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . (insloc (len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by A56, A78, A90
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + 1) by A19, A56, A91
.= (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) . ((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + 1) by A52, A56, A57, A89, FINSEQ_4:98 ; :: thesis: verum

end;

A95: now

thus CurInstr (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + (len <*(f,a1 := a2)*>)) by A52, A94, FINSEQ_1:57
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + ((len (aSeq a1,((len r) + 1))) + ((len (aSeq a2,pr1)) + (len <*(f,a1 := a2)*>)))) by A55 ; :: thesis: verum

end;

A96: now

thus CurInstr (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) = ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0))) + (len x)) by A47, A48, A95, Lm3
.= (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>) . (len (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>)) by A47, A48, A93, FINSEQ_1:86
.= (((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1)) ^ <*(f,a1 := a2)*>) . ((len ((aSeq a1,((len r) + 1)) ^ (aSeq a2,pr1))) + (len <*(f,a1 := a2)*>)) by FINSEQ_1:35
.= <*(f,a1 := a2)*> . (len <*(f,a1 := a2)*>) by A92, FINSEQ_1:86
.= <*(f,a1 := a2)*> . 1 by FINSEQ_1:57
.= f,a1 := a2 by FINSEQ_1:57 ; :: thesis: verum

end;

A97: now

thus Computation s,((len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))) + 1) = Following (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by AMI_1:14
.= Exec (f,a1 := a2),(Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by A96, AMI_1:def 18 ; :: thesis: verum

end;

then A98: Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1))) = Exec (f,a1 := a2),(Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by A89, FINSEQ_1:35;

A99: now

thus IC (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) = (Exec (f,a1 := a2),(Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) . (IC SCM+FSA ) by A56, A89, A97, AMI_1:def 15
.= Next (IC (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) by SCMFSA_2:99
.= Next (insloc (len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) by A56, A78, A90
.= insloc (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1))) by A56, A89, NAT_1:39 ; :: thesis: verum

end;

thus for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) holds
IC (Computation s,i) = insloc i :: thesis: ( ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) & len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )

proof

let i be Element of NAT ; :: thesis: ( i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) implies IC (Computation s,i) = insloc i )
assume A100: i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Computation s,i) = insloc i

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

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

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

end;

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

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

end;

end;

end;

consider ki being Element of NAT such that
A101: ( ki = abs ((Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . a1) & (Exec (f,a1 := a2),(Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1))))) . f = ((Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . f) +* ki,((Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . a2) ) by SCMFSA_2:99;

A102: now

thus ki = abs ((Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . a1) by A101, FINSEQ_1:35
.= abs ((Computation (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . a1) by AMI_1:51
.= abs ((Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . a1) by A3, A68, A74, SCMFSA_7:36
.= abs ((len r) + 1) by A54, A59, A66, SCMFSA_7:36
.= (len r) + 1 by ABSVALUE:def 1 ; :: thesis: verum

end;

A103: now

thus (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . a2 = (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . a2 by FINSEQ_1:35
.= (Computation (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . a2 by AMI_1:51
.= p . ((len r) + 1) by A46, A68, A74, SCMFSA_7:36 ; :: thesis: verum

end;

A104: now

thus (Computation s,(len (((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))) ^ (aSeq a2,pr1)))) . f = (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . f by FINSEQ_1:35
.= (Computation (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . f by AMI_1:51
.= (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . f by A68, A74, SCMFSA_7:36
.= (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f by A54, A59, A66, SCMFSA_7:36 ; :: thesis: verum

end;

A105: dom (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = dom ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) by FUNCT_7:32;
then A106: len (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) = len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) by FINSEQ_3:31;
len pp1 <= len pp by A36, A37, FINSEQ_1:84;
then A107: Seg (len pp1) c= Seg (len p) by A10, FINSEQ_1:7;

A108: now

dom ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = Seg (len p) by A40, A56, A89, A97, A101, A102, A103, A104, A105, FINSEQ_1:def 3;
hence dom (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) = Seg (len pp1) by A107, RELAT_1:91; :: thesis: verum

end;

A109: now

Seg (len pp1) c= dom p by A107, FINSEQ_1:def 3;
hence dom (p | (Seg (len pp1))) = Seg (len pp1) by RELAT_1:91; :: thesis: verum

end;

for i being Element of NAT st i in Seg (len pp1) holds
(((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (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 a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i )
assume A110: i in Seg (len pp1) ; :: thesis: (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i
then A111: ( 1 <= i & i <= len pp1 ) by FINSEQ_1:3;
A112: (len r) + 1 in dom ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) by A10, A40, A45, FINSEQ_1:def 3;

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

suppose A113: i = len pp1 ; :: thesis: (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i

then A114: i = (len pp0) + 1 by FINSEQ_2:19;
hence (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A98, A101, A102, A103, A104, A113, FINSEQ_1:6, FUNCT_1:72
.= p . ((len r) + 1) by A37, A112, A114, FUNCT_7:33
.= (p | (Seg (len pp1))) . i by A37, A113, A114, FINSEQ_1:6, FUNCT_1:72 ;
:: thesis: verum

end;

suppose A115: i <> len pp1 ; :: thesis: (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i

then A116: i <> (len r) + 1 by A37, FINSEQ_2:19;
( 1 <= i & i < len pp1 ) by A111, A115, 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 A117: i in Seg (len pp0) by FINSEQ_1:3;

now

thus (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) +* ((len r) + 1),(p . ((len r) + 1))) . i by A98, A101, A102, A103, A104, A110, FUNCT_1:72
.= ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) . i by A116, FUNCT_7:34 ; :: thesis: verum

end;

hence (((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp0))) . i by A39, A117, FUNCT_1:72
.= p . i by A117, FUNCT_1:72
.= (p | (Seg (len pp1))) . i by A110, FUNCT_1:72 ;
:: thesis: verum

end;

end;

end;

then for i being set st i in Seg (len pp1) holds
(((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i ;
hence ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) | (Seg (len pp1)) = p | (Seg (len pp1)) by A108, A109, FUNCT_1:9; :: thesis: ( len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p & ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )
thus len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . f) = len p by A40, A89, A97, A101, A102, A103, A104, A106, FINSEQ_1:35; :: thesis: ( ( for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . g = s . g ) )

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

let b be Int-Location ; :: thesis: ( b <> a1 & b <> a2 implies (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b )
assume A118: ( b <> a1 & b <> a2 ) ; :: thesis: (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = s . b
thus (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . b = (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . b by A56, A89, A97, SCMFSA_2:99
.= (Computation (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . b by AMI_1:51
.= (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . b by A68, A74, A118, SCMFSA_7:36
.= (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b by A54, A59, A66, A118, SCMFSA_7:36
.= s . b by A41, A118 ; :: thesis: verum

end;

hereby :: thesis: verum

let h be FinSeq-Location ; :: thesis: ( h <> f implies (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . h = s . h )
assume A119: h <> f ; :: thesis: (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . h = s . h
hence (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp1)))) . h = (Computation s,((len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1)))) + (len (aSeq a2,pr1)))) . h by A56, A89, A97, SCMFSA_2:99
.= (Computation (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))),(len (aSeq a2,pr1))) . h by AMI_1:51
.= (Computation s,(len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) ^ (aSeq a1,((len r) + 1))))) . h by A68, A74, SCMFSA_7:36
.= (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . h by A54, A59, A66, SCMFSA_7:36
.= s . h by A42, A119 ;
:: 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
A120: pp0 = pp and
A121: for i being Element of NAT st i <= len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)) holds
IC (Computation s,i) = insloc i and
A122: ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) | (Seg (len pp0)) = p | (Seg (len pp0)) and
A123: len ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = len p and
A124: for b being Int-Location st b <> a1 & b <> a2 holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . b = s . b and
A125: for g being FinSeq-Location st g <> f holds
(Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . g = s . g ;
A126: IC (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) = insloc (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) by A120, A121;
len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) + 1 by A12, FINSEQ_2:19;
then A127: len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)) < len ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by NAT_1:13;
A128: CurInstr (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) = (Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) . (insloc (len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp)))) by A126, AMI_1:def 17
.= ((((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) + 1) by A19, A127
.= halt SCM+FSA by A12, 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 A129: Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp))) = Result s by A128, AMI_1:def 22;
dom ((Computation s,(len (((aSeq a1,(len p)) ^ <*(f :=<0,...,0> a1)*>) ^ (FlattenSeq pp0)))) . f) = Seg (len pp0) by A10, A120, A123, FINSEQ_1:def 3;
then A130: (Result s) . f = p | (Seg (len pp0)) by A120, A122, A129, RELAT_1:97;
dom p = Seg (len pp0) by A10, A120, FINSEQ_1:def 3;
hence (Result s) . f = p by A130, 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 A120, A124, A125, A129; :: thesis: verum