let s be State of SCM+FSA ; :: thesis:
assume that
A1: IC s = 0 and
A2: s . (intloc 0 ) = 1 ; :: thesis:
let a be Int-Location ; :: thesis:
let k be Integer; :: thesis:
assume that
A3: a := k c= s and
A4: a <> intloc 0 ; :: thesis:

per cases ;

suppose A5: k > 0 ; :: thesis:

then consider k1 being Element of NAT such that
A6: k1 + 1 = k and
A7: a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by Def2;
A8: len (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (AddTo a,(intloc 0 )))) by FINSEQ_1:35
.= 1 + (len (k1 |-> (AddTo a,(intloc 0 )))) by FINSEQ_1:56
.= k by A6, FINSEQ_1:def 18 ;
reconsider k = k as Element of NAT by A5, INT_1:16;
defpred S₁[ Nat] means ( $1 <= k implies ( ( 1 <= $1 implies (Comput (ProgramPart s),s,$1) . a = $1 ) & ( for b being Int-Location st b <> a holds
(Comput (ProgramPart s),s,$1) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s),s,$1) . f = s . f ) ) );
set f = (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A9: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . 1 = (<*(a := (intloc 0 ))*> ^ ((k1 |-> (AddTo a,(intloc 0 ))) ^ <*(halt SCM+FSA )*>)) . 1 by FINSEQ_1:45
.= a := (intloc 0 ) by FINSEQ_1:58 ;
A10: len ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = (len (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))))) + (len <*(halt SCM+FSA )*>) by FINSEQ_1:35
.= k + 1 by A8, FINSEQ_1:56 ;
then A11: dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Seg (k + 1) by FINSEQ_1:def 3;

A12: now

let i be Element of NAT ; :: thesis:
assume ( 1 <= i & i <= k + 1 ) ; :: thesis:
hence A13: i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A11; :: thesis:
dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) = { (m -' 1) where m is Element of NAT : m in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) } by Def1;
hence i -' 1 in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A13; :: thesis:

end;

A14: now

let i be Element of NAT ; :: thesis:
assume that
0 <= i and
A15: i <= k ; :: thesis:
A16: ( 0 + 1 <= i + 1 & i + 1 <= k + 1 ) by A15, XREAL_1:8;
hence i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A12; :: thesis:
(i + 1) -' 1 in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A12, A16;
hence i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by NAT_D:34; :: thesis:

end;

A17: now

let i be Element of NAT ; :: thesis:
assume that
0 <= i and
A18: i <= k ; :: thesis:
A19: i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A14, A18;
hence s . i = (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . i by A3, A7, GRFUNC_1:8
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A19, Def1
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A14, A18, PARTFUN1:def 8 ;
:: thesis:

end;

then A20: s . 0 = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1)
.= a := (intloc 0 ) by A9 ;

A21: now

end;

A23: now

let i be Element of NAT ; :: thesis:
assume that
A24: 1 < i and
A25: i <= k ; :: thesis:
A26: 1 <= i - 1 by A24, INT_1:79;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
i - 1 <= k - 1 by A25, XREAL_1:11;
then A27: i1 in Seg k1 by A6, A26;
A28: len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) = Seg k by A8, FINSEQ_1:def 3;
then i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) by A24, A25;
hence ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) . i by FINSEQ_1:def 7
.= (k1 |-> (AddTo a,(intloc 0 ))) . (i - 1) by A8, A24, A25, A28, FINSEQ_1:37
.= AddTo a,(intloc 0 ) by A27, FUNCOP_1:13 ;
:: thesis:

end;

A29: now

let i be Element of NAT ; :: thesis:
assume that
A30: 0 < i and
A31: i < k ; :: thesis:
A32: ( 0 + 1 < i + 1 & i + 1 <= k ) by A30, A31, NAT_1:13, XREAL_1:8;
thus s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A17, A31
.= AddTo a,(intloc 0 ) by A23, A32 ; :: thesis:

end;

A33: for i being Element of NAT st i <= k holds
IC (Comput (ProgramPart s),s,i) = i

proof

defpred S₂[ Nat] means ( $1 <= k implies IC (Comput (ProgramPart s),s,$1) = $1 );
let i be Element of NAT ; :: thesis:
assume A34: i <= k ; :: thesis:
A35: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A36: S₂[n] ; :: thesis:
assume A37: n + 1 <= k ; :: thesis:
then A38: n < k by NAT_1:13;

per cases ;

suppose A39: n = 0 ; :: thesis:

hence IC (Comput (ProgramPart s),s,(n + 1)) = (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by A21
.= succ n by A1, A39, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis:

end;

suppose A40: n > 0 ; :: thesis:

end;

A42: S₂[ 0 ] by A1, AMI_1:13;
for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A42, A35);
hence IC (Comput (ProgramPart s),s,i) = i by A34; :: thesis:

end;

A43: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A44: S₁[n] ; :: thesis:
assume A45: n + 1 <= k ; :: thesis:

per cases ;

suppose A46: n = 0 ; :: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = (Exec (a := (intloc 0 )),s) . a by A21, A46
.= n + 1 by A2, A46, SCMFSA_2:89 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A47: b <> a ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . b = (Exec (a := (intloc 0 )),s) . b by A21, A46
.= s . b by A47, SCMFSA_2:89 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . f = (Exec (a := (intloc 0 )),s) . f by A21, A46
.= s . f by SCMFSA_2:89 ; :: thesis:

end;

suppose A48: n > 0 ; :: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = n + ((Comput (ProgramPart s),s,n) . (intloc 0 )) by A44, A45, A53, A50, A52, SCMFSA_2:90, XXREAL_0:2
.= n + 1 by A2, A4, A44, A45, A50, XXREAL_0:2 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A54: b <> a ; :: thesis:
hence (Comput (ProgramPart s),s,(n + 1)) . b = (Comput (ProgramPart s),s,n) . b by A52, SCMFSA_2:90
.= s . b by A44, A45, A50, A54, XXREAL_0:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . f = (Comput (ProgramPart s),s,n) . f by A52, SCMFSA_2:90
.= s . f by A44, A45, A50, XXREAL_0:2 ; :: thesis:

end;

end;

suppose A60: k <= 0 ; :: thesis:

then reconsider mk = - k as Element of NAT by INT_1:16;
defpred S₁[ Nat] means ( $1 <= (mk + 1) + 1 implies ( ( 1 <= $1 implies (Comput (ProgramPart s),s,$1) . a = ((- $1) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (ProgramPart s),s,$1) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s),s,$1) . f = s . f ) ) );
consider k1 being Element of NAT such that
A61: k1 + k = 1 and
A62: a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A60, Def2;
A63: len (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (SubFrom a,(intloc 0 )))) by FINSEQ_1:35
.= 1 + (len (k1 |-> (SubFrom a,(intloc 0 )))) by FINSEQ_1:56
.= (mk + 1) + 1 by A61, FINSEQ_1:def 18 ;
set f = (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A64: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . 1 = (<*(a := (intloc 0 ))*> ^ ((k1 |-> (SubFrom a,(intloc 0 ))) ^ <*(halt SCM+FSA )*>)) . 1 by FINSEQ_1:45
.= a := (intloc 0 ) by FINSEQ_1:58 ;
A65: len ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = (len (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))))) + (len <*(halt SCM+FSA )*>) by FINSEQ_1:35
.= ((mk + 1) + 1) + 1 by A63, FINSEQ_1:56 ;
then A66: dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Seg (((mk + 1) + 1) + 1) by FINSEQ_1:def 3;

A67: now

let i be Element of NAT ; :: thesis:
assume ( 1 <= i & i <= ((mk + 1) + 1) + 1 ) ; :: thesis:
hence A68: i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A66; :: thesis:
dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) = { (m -' 1) where m is Element of NAT : m in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) } by Def1;
hence i -' 1 in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A68; :: thesis:

end;

A69: now

let i be Element of NAT ; :: thesis:
assume that
0 <= i and
A70: i <= (mk + 1) + 1 ; :: thesis:
A71: ( 0 + 1 <= i + 1 & i + 1 <= ((mk + 1) + 1) + 1 ) by A70, XREAL_1:8;
hence i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A67; :: thesis:
(i + 1) -' 1 in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A67, A71;
hence i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by NAT_D:34; :: thesis:

end;

A72: now

let i be Element of NAT ; :: thesis:
assume that
0 <= i and
A73: i <= (mk + 1) + 1 ; :: thesis:
A74: i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A69, A73;
hence s . i = (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . i by A3, A62, GRFUNC_1:8
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A74, Def1
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A69, A73, PARTFUN1:def 8 ;
:: thesis:

end;

then A75: s . 0 = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1)
.= a := (intloc 0 ) by A64 ;

A76: now

end;

A78: now

A79: len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
let i be Element of NAT ; :: thesis:
assume that
A80: 1 < i and
A81: i <= (mk + 1) + 1 ; :: thesis:
A82: i - 1 <= ((mk + 1) + 1) - 1 by A81, XREAL_1:11;
A83: 1 - 1 < i - 1 by A80, XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
(1 - 1) + 1 <= i - 1 by A83, INT_1:20;
then A84: i1 in Seg k1 by A61, A82;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) = Seg ((mk + 1) + 1) by A63, FINSEQ_1:def 3;
then i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) by A80, A81;
hence ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) . i by FINSEQ_1:def 7
.= (k1 |-> (SubFrom a,(intloc 0 ))) . (i - 1) by A63, A80, A81, A79, FINSEQ_1:37
.= SubFrom a,(intloc 0 ) by A84, FUNCOP_1:13 ;
:: thesis:

end;

A85: now

let i be Element of NAT ; :: thesis:
assume that
A86: 0 < i and
A87: i < (mk + 1) + 1 ; :: thesis:
A88: ( 0 + 1 < i + 1 & i + 1 <= (mk + 1) + 1 ) by A86, A87, NAT_1:13, XREAL_1:8;
thus s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A72, A87
.= SubFrom a,(intloc 0 ) by A78, A88 ; :: thesis:

end;

A89: for i being Element of NAT st i <= (mk + 1) + 1 holds
IC (Comput (ProgramPart s),s,i) = i

proof

defpred S₂[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (ProgramPart s),s,$1) = $1 );
let i be Element of NAT ; :: thesis:
assume A90: i <= (mk + 1) + 1 ; :: thesis:
A91: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A92: S₂[n] ; :: thesis:
assume A93: n + 1 <= (mk + 1) + 1 ; :: thesis:
then A94: n < (mk + 1) + 1 by NAT_1:13;

per cases ;

suppose A95: n = 0 ; :: thesis:

hence IC (Comput (ProgramPart s),s,(n + 1)) = (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by A76
.= succ n by A1, A95, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis:

end;

suppose A96: n > 0 ; :: thesis:

end;

A98: S₂[ 0 ] by A1, AMI_1:13;
for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A98, A91);
hence IC (Comput (ProgramPart s),s,i) = i by A90; :: thesis:

end;

A99: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A100: S₁[n] ; :: thesis:
assume A101: n + 1 <= (mk + 1) + 1 ; :: thesis:

per cases ;

suppose A102: n = 0 ; :: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = (Exec (a := (intloc 0 )),s) . a by A76, A102
.= ((- (n + 1)) + 1) + 1 by A2, A102, SCMFSA_2:89 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A103: b <> a ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . b = (Exec (a := (intloc 0 )),s) . b by A76, A102
.= s . b by A103, SCMFSA_2:89 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . f = (Exec (a := (intloc 0 )),s) . f by A76, A102
.= s . f by SCMFSA_2:89 ; :: thesis:

end;

suppose A104: n > 0 ; :: thesis:

hereby :: thesis:

assume 1 <= n + 1 ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . a = (((- n) + 1) + 1) - ((Comput (ProgramPart s),s,n) . (intloc 0 )) by A100, A101, A109, A108, NAT_1:13, SCMFSA_2:91
.= (((- n) + 1) + 1) - (s . (intloc 0 )) by A4, A100, A101, A106, XXREAL_0:2
.= ((- (n + 1)) + 1) + 1 by A2 ; :: thesis:

end;

hereby :: thesis:

let b be Int-Location ; :: thesis:
assume A110: b <> a ; :: thesis:
hence (Comput (ProgramPart s),s,(n + 1)) . b = (Comput (ProgramPart s),s,n) . b by A108, SCMFSA_2:91
.= s . b by A100, A101, A106, A110, XXREAL_0:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (Comput (ProgramPart s),s,(n + 1)) . f = (Comput (ProgramPart s),s,n) . f by A108, SCMFSA_2:91
.= s . f by A100, A101, A106, XXREAL_0:2 ; :: thesis:

end;

((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (((mk + 1) + 1) + 1) = <*(halt SCM+FSA )*> . ((((mk + 1) + 1) + 1) - ((mk + 1) + 1)) by A63, A65, FINSEQ_1:37, XREAL_1:31
.= halt SCM+FSA by FINSEQ_1:def 8 ;
then A111: s . ((mk + 1) + 1) = halt SCM+FSA by A72;
Y: (ProgramPart (Comput (ProgramPart s),s,((mk + 1) + 1))) /. (IC (Comput (ProgramPart s),s,((mk + 1) + 1))) = (Comput (ProgramPart s),s,((mk + 1) + 1)) . (IC (Comput (ProgramPart s),s,((mk + 1) + 1))) by AMI_1:150;
A112: CurInstr (ProgramPart (Comput (ProgramPart s),s,((mk + 1) + 1))),(Comput (ProgramPart s),s,((mk + 1) + 1)) = (Comput (ProgramPart s),s,((mk + 1) + 1)) . ((mk + 1) + 1) by A89, Y
.= halt SCM+FSA by A111, AMI_1:54 ;
hence ProgramPart s halts_on s by AMI_1:146; :: thesis:
then A113: Comput (ProgramPart s),s,((mk + 1) + 1) = Result s by A112, AMI_1:def 22;
A114: S₁[ 0 ] by AMI_1:13;
A115: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A114, A99);
( ((- ((mk + 1) + 1)) + 1) + 1 = k & 0 + 1 <= mk + (1 + 1) ) by XREAL_1:9;
hence ( (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) ) by A115, A113; :: thesis:

end;