let s be State of SCM+FSA; for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 holds
(IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),|.(s . aa).|,|.(s . bb).|)
let c be read-write Int-Location; for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 holds
(IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),|.(s . aa).|,|.(s . bb).|)
let aa, bb be Int-Location; for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 holds
(IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),|.(s . aa).|,|.(s . bb).|)
let f be FinSeq-Location ; for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 holds
(IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),|.(s . aa).|,|.(s . bb).|)
let p be Instruction-Sequence of SCM+FSA; ( 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 implies (IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),|.(s . aa).|,|.(s . bb).|) )
set a = aa;
set b = bb;
assume that
A1:
1 <= s . aa
and
A2:
s . aa <= s . bb
and
A3:
s . bb <= len (s . f)
and
A4:
aa <> c
and
A5:
bb <> c
and
A6:
s . (intloc 0) = 1
; (IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c = min_at ((s . f),|.(s . aa).|,|.(s . bb).|)
A7:
( bb = intloc 0 or bb is read-write )
by SCMFSA_M:def 2;
set i0 = c := aa;
set s1 = Exec ((c := aa),(Initialized s));
set p1 = p;
A8:
( aa = intloc 0 or aa is read-write )
by SCMFSA_M:def 2;
reconsider sa = |.(s . aa).| as Element of NAT ;
A9:
s . aa = sa
by A1, ABSVALUE:def 1;
(s . aa) - (s . aa) <= (s . bb) - (s . aa)
by A2, XREAL_1:9;
then reconsider sba = (s . bb) - (s . aa) as Element of NAT by INT_1:3;
A10: (Exec ((c := aa),(Initialized s))) . f =
(Initialized s) . f
by SCMFSA_2:63
.=
s . f
by SCMFSA_M:37
;
set k = sba + 1;
set cv = 3 -rdRWNotIn {aa,bb,c};
set aux2 = 2 -ndRWNotIn {aa,bb,c};
set aux1 = 1 -stRWNotIn {aa,bb,c};
A11:
1 -stRWNotIn {aa,bb,c} <> 2 -ndRWNotIn {aa,bb,c}
by SCMFSA_M:26;
set I12 = if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA));
set i10 = (1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}));
A12:
2 -ndRWNotIn {aa,bb,c} <> 3 -rdRWNotIn {aa,bb,c}
by SCMFSA_M:26;
set i11 = (2 -ndRWNotIn {aa,bb,c}) := (f,c);
A13:
1 -stRWNotIn {aa,bb,c} <> 3 -rdRWNotIn {aa,bb,c}
by SCMFSA_M:26;
A14:
c in {aa,bb,c}
by ENUMSET1:def 1;
then A15:
3 -rdRWNotIn {aa,bb,c} <> c
by SCMFSA_M:25;
set I1B = (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)));
set I1 = for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))));
set SF = StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))));
defpred S1[ Nat] means ( 0 < $1 & $1 <= sba + 1 implies ( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . $1) . (intloc 0) = 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . $1) . (3 -rdRWNotIn {aa,bb,c}) = $1 + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . $1) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ($1 + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . $1) . c = min_at ((s . f),sa,sa1) ) ) );
3 -rdRWNotIn {aa,bb,c} in {(3 -rdRWNotIn {aa,bb,c}),aa,bb}
by ENUMSET1:def 1;
then A16:
3 -rdRWNotIn {aa,bb,c} in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))))
by XBOOLE_0:def 3;
A17:
ProperForUpBody 3 -rdRWNotIn {aa,bb,c},aa,bb,(((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))), Exec ((c := aa),(Initialized s)),p
by Th15;
A18:
1 -stRWNotIn {aa,bb,c} <> c
by A14, SCMFSA_M:25;
A19:
2 -ndRWNotIn {aa,bb,c} <> c
by A14, SCMFSA_M:25;
A20: (Exec ((c := aa),(Initialized s))) . c =
(Initialized s) . aa
by SCMFSA_2:63
.=
s . aa
by A6, A8, SCMFSA_M:9, SCMFSA_M:37
;
A21: (Exec ((c := aa),(Initialized s))) . aa =
(Initialized s) . aa
by A4, SCMFSA_2:63
.=
s . aa
by A6, A8, SCMFSA_M:9, SCMFSA_M:37
;
A22:
s . aa <= len (s . f)
by A2, A3, XXREAL_0:2;
then A23:
sa in dom (s . f)
by A1, A9, FINSEQ_3:25;
A24: (Exec ((c := aa),(Initialized s))) . bb =
(Initialized s) . bb
by A5, SCMFSA_2:63
.=
s . bb
by A6, A7, SCMFSA_M:9, SCMFSA_M:37
;
A25: (Exec ((c := aa),(Initialized s))) . (intloc 0) =
(Initialized s) . (intloc 0)
by SCMFSA_2:63
.=
1
by SCMFSA_M:9
;
then A26:
DataPart (IExec ((for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))))),p,(Exec ((c := aa),(Initialized s))))) = DataPart ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (sba + 1))
by A21, A24, Th23;
c in {c,(3 -rdRWNotIn {aa,bb,c})}
by TARSKI:def 2;
then
c in UsedIntLoc (c := (3 -rdRWNotIn {aa,bb,c}))
by SF_MASTR:14;
then
c in UsedILoc (Macro (c := (3 -rdRWNotIn {aa,bb,c})))
by SF_MASTR:28;
then
c in {(2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c})} \/ (UsedILoc (Macro (c := (3 -rdRWNotIn {aa,bb,c}))))
by XBOOLE_0:def 3;
then
c in ({(2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c})} \/ (UsedILoc (Macro (c := (3 -rdRWNotIn {aa,bb,c}))))) \/ (UsedILoc (Stop SCM+FSA))
by XBOOLE_0:def 3;
then
c in UsedILoc (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))
by Th6;
then
c in (UsedILoc (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c)))) \/ (UsedILoc (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))
by XBOOLE_0:def 3;
then A27:
c in UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))
by SF_MASTR:27;
then A28:
c in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))))
by XBOOLE_0:def 3;
A29:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume that A30:
S1[
n]
and
0 < n + 1
and A31:
n + 1
<= sba + 1
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )
A32:
(
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (intloc 0) = 1 &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa) &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb )
proof
per cases
( 0 = n or 0 < n )
;
suppose A33:
0 = n
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (intloc 0) = 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb )hence
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (intloc 0) = 1
by A25, Th8;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb )thus
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa)
by A33, Th9;
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bbthus
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb
by A2, A21, A24, A33, Th9;
verum end; suppose A34:
0 < n
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (intloc 0) = 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb )hence
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (intloc 0) = 1
by A30, A31, NAT_1:13;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb )thus
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa)
by A30, A31, A34, NAT_1:13;
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb
(n + 1) - 1
<= (((s . bb) - (s . aa)) + 1) - 1
by A31, XREAL_1:9;
hence
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb
by A21, A24, A30, A34, NAT_1:13, XREAL_1:19;
verum end;
end;
set S0 =
Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n);
set S1 =
Exec (
((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)));
set S2 =
Exec (
((2 -ndRWNotIn {aa,bb,c}) := (f,c)),
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))));
A35:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . f =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . f
by SCMFSA6C:9
.=
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f
by SCMFSA_2:72
.=
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . f
by SCMFSA_2:72
;
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (intloc 0) =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . (intloc 0)
by SCMFSA6C:8
.=
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . (intloc 0)
by SCMFSA_2:72
.=
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (intloc 0)
by SCMFSA_2:72
.=
1
by SCMFSA_M:9
;
then A36:
DataPart (IExec ((Stop SCM+FSA),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) = DataPart (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))
by Th1;
n < n + 1
by XREAL_1:29;
then
n < sba + 1
by A31, XXREAL_0:2;
then A37:
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) | (({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))))) \/ FinSeq-Locations) = (IExec ((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) | (({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))))) \/ FinSeq-Locations)
by A25, A21, A24, A17, Th19;
then A38:
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . f
by SCMFSA_M:28
.=
(Exec ((AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0))),(IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . f
by SFMASTR1:12
.=
(IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . f
by SCMFSA_2:64
.=
(IExec ((if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . f
by SFMASTR1:8
;
A39:
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c =
(IExec ((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . c
by A28, A37, SCMFSA_M:28
.=
(Exec ((AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0))),(IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . c
by SFMASTR1:11
.=
(IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . c
by A15, SCMFSA_2:64
.=
(IExec ((if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . c
by SFMASTR1:7
;
A40:
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
(IExec ((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})
by A16, A37, SCMFSA_M:28
.=
(Exec ((AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0))),(IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})
by SFMASTR1:11
.=
((IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})) + ((IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (intloc 0))
by SCMFSA_2:64
.=
((IExec (((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SCMFSA6B:11
.=
((IExec ((if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SFMASTR1:7
;
A41:
( not
Macro (c := (3 -rdRWNotIn {aa,bb,c})) refers 2
-ndRWNotIn {aa,bb,c} & not
Stop SCM+FSA refers 2
-ndRWNotIn {aa,bb,c} )
by A12, Th2, Th3, SCMFSA8C:51;
A42:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . c =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . c
by SCMFSA6C:8
.=
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . c
by A19, SCMFSA_2:72
.=
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . c
by A18, SCMFSA_2:72
.=
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . c
by SCMFSA_M:37
;
A43:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c}) =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . (3 -rdRWNotIn {aa,bb,c})
by SCMFSA6C:8
.=
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . (3 -rdRWNotIn {aa,bb,c})
by A12, SCMFSA_2:72
.=
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c})
by A13, SCMFSA_2:72
;
per cases
( 0 = n or 0 < n )
;
suppose A44:
0 = n
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )thus
(
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1 &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex
sa1 being
Element of
NAT st
(
sa1 = ((n + 1) + sa) - 1 &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at (
(s . f),
sa,
sa1) ) )
verumproof
reconsider sa1 =
((n + 1) + sa) - 1 as
Element of
NAT by A44;
A45:
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . 0) . c = (Exec ((c := aa),(Initialized s))) . c
by A15, A27, Th12;
A46:
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . c =
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . c
by A18, SCMFSA_2:72
.=
s . aa
by A20, A44, A45, SCMFSA_M:37
;
thus
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1
by A25, A21, A24, A17, A31, Th17;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )
A47:
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . f =
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . 0) . f
by A44, SCMFSA_M:37
.=
s . f
by A10, Th13
;
then A48:
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f = s . f
by SCMFSA_2:72;
A49:
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c}) =
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . 0) . (3 -rdRWNotIn {aa,bb,c})
by A44, SCMFSA_M:37
.=
s . aa
by A21, Th9
;
then reconsider S0cv =
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c}) as
Element of
NAT by A1, INT_1:3;
A50:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {aa,bb,c}) =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . (1 -stRWNotIn {aa,bb,c})
by SCMFSA6C:8
.=
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . (1 -stRWNotIn {aa,bb,c})
by A11, SCMFSA_2:72
.=
((Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . f) /. |.((Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c})).|
by Th4
.=
(s . f) . S0cv
by A9, A23, A47, A49, PARTFUN1:def 6
;
A51:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . (2 -ndRWNotIn {aa,bb,c})
by SCMFSA6C:8
.=
((Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f) /. |.((Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . c).|
by Th4
.=
(s . f) . S0cv
by A9, A23, A49, A48, A46, PARTFUN1:def 6
;
hence ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
((IExec ((Stop SCM+FSA),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A12, A41, A40, A50, SCMFSA8B:40
.=
(n + 1) + ((Exec ((c := aa),(Initialized s))) . aa)
by A21, A36, A43, A44, A49, SCMFSA_M:2
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )
thus ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((Stop SCM+FSA),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . f
by A41, A38, A50, A51, SCMFSA8B:40
.=
(Exec ((c := aa),(Initialized s))) . f
by A10, A36, A35, A47, SCMFSA_M:2
;
ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) )
take
sa1
;
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) )
thus
sa1 = ((n + 1) + sa) - 1
;
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1)
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c =
(IExec ((Stop SCM+FSA),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . c
by A19, A41, A39, A50, A51, SCMFSA8B:40
.=
s . aa
by A20, A36, A42, A44, A45, SCMFSA_M:2
;
hence
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at (
(s . f),
sa,
sa1)
by A1, A22, A9, A44, FINSEQ_6:162;
verum
end; end; suppose A52:
0 < n
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )thus
(
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1 &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex
sa1 being
Element of
NAT st
(
sa1 = ((n + 1) + sa) - 1 &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at (
(s . f),
sa,
sa1) ) )
verumproof
A53:
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c}) = ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c})
by SCMFSA_M:37;
then reconsider S0cv =
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c}) as
Element of
NAT by A1, A21, A32, INT_1:3;
( 1
<= S0cv &
S0cv <= len (s . f) )
by A1, A3, A9, A21, A24, A32, A53, NAT_1:12, XXREAL_0:2;
then A54:
S0cv in dom (s . f)
by FINSEQ_3:25;
A55:
(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . f = s . f
by A10, A30, A31, A52, NAT_1:13, SCMFSA_M:37;
then A56:
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f = s . f
by SCMFSA_2:72;
A57:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {aa,bb,c}) =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . (1 -stRWNotIn {aa,bb,c})
by SCMFSA6C:8
.=
(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . (1 -stRWNotIn {aa,bb,c})
by A11, SCMFSA_2:72
.=
((Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . f) /. |.((Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c})).|
by Th4
.=
((Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . f) /. S0cv
by ABSVALUE:def 1
.=
(s . f) . S0cv
by A55, A54, PARTFUN1:def 6
;
n + (s . aa) <= len (s . f)
by A3, A21, A24, A32, XXREAL_0:2;
then
(n + (s . aa)) - 1
<= (len (s . f)) - 1
by XREAL_1:9;
then A58:
((n + (s . aa)) - 1) + 0 <= ((len (s . f)) - 1) + 1
by XREAL_1:7;
thus
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1
by A25, A21, A24, A17, A31, Th17;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )
consider sa1 being
Nat such that A59:
sa1 = (n + sa) - 1
and A60:
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . c = min_at (
(s . f),
sa,
sa1)
by A30, A31, A52, NAT_1:13;
reconsider SFnc =
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . c as
Element of
NAT by A60, ORDINAL1:def 12;
0 + 1
<= n
by A52, NAT_1:13;
then
1
- 1
<= n - 1
by XREAL_1:9;
then A61:
0 + (s . aa) <= (n - 1) + (s . aa)
by XREAL_1:6;
then A62:
sa <= SFnc
by A1, A9, A59, A60, A58, FINSEQ_6:161;
then A63:
1
<= SFnc
by A1, A9, XXREAL_0:2;
A64:
SFnc <= sa1
by A1, A9, A59, A60, A61, A58, FINSEQ_6:161;
then
SFnc <= len (s . f)
by A9, A59, A58, XXREAL_0:2;
then A65:
SFnc in dom (s . f)
by A63, FINSEQ_3:25;
A66:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) =
(Exec (((2 -ndRWNotIn {aa,bb,c}) := (f,c)),(Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . (2 -ndRWNotIn {aa,bb,c})
by SCMFSA6C:8
.=
((Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f) /. |.((Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . c).|
by Th4
.=
((Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f) /. |.((Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)) . c).|
by A18, SCMFSA_2:72
.=
((Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f) /. |.(((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . c).|
by SCMFSA_M:37
.=
((Exec (((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))),(Initialized ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f) /. SFnc
by ABSVALUE:def 1
.=
(s . f) . SFnc
by A56, A65, PARTFUN1:def 6
;
A67:
for
i being
Nat st
sa <= i &
i < ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . c holds
(s . f) . i > (s . f) . SFnc
by A1, A9, A59, A60, A61, A58, FINSEQ_6:161;
thus
(
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex
sa1 being
Element of
NAT st
(
sa1 = ((n + 1) + sa) - 1 &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at (
(s . f),
sa,
sa1) ) )
verumproof
A68:
((n + 1) + (s . aa)) - 1
<= len (s . f)
by A3, A21, A24, A32, XXREAL_0:2;
A69:
((n + 1) + (s . aa)) - 1 =
((n + (s . aa)) + 1) - 1
.=
n + sa
by A1, ABSVALUE:def 1
;
then A70:
s . aa <= ((n + 1) + (s . aa)) - 1
by NAT_1:12;
per cases
( (s . f) . S0cv < (s . f) . SFnc or (s . f) . SFnc <= (s . f) . S0cv )
;
suppose A71:
(s . f) . S0cv < (s . f) . SFnc
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )A72:
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c}) =
(Exec ((c := (3 -rdRWNotIn {aa,bb,c})),(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . (3 -rdRWNotIn {aa,bb,c})
by SCMFSA6C:5
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . (3 -rdRWNotIn {aa,bb,c})
by A15, SCMFSA_2:63
;
thus ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
((Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A72, A12, A41, A40, A57, A66, A71, SCMFSA8B:40
.=
((IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SCMFSA_M:37
.=
(n + 1) + ((Exec ((c := aa),(Initialized s))) . aa)
by A32, A43, A53
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )thus ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . f
by A41, A38, A57, A66, A71, SCMFSA8B:40
.=
(Exec ((c := (3 -rdRWNotIn {aa,bb,c})),(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . f
by SCMFSA6C:5
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . f
by SCMFSA_2:63
.=
(Exec ((c := aa),(Initialized s))) . f
by A10, A35, A55, SCMFSA_M:37
;
ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) )reconsider sa11 =
((n + 1) + sa) - 1 as
Element of
NAT by A69;
take
sa11
;
( sa11 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa11) )thus
sa11 = ((n + 1) + sa) - 1
;
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa11)A73:
for
i being
Nat st
s . aa <= i &
i <= ((n + 1) + (s . aa)) - 1 holds
(s . f) . S0cv <= (s . f) . i
proof
let i be
Nat;
( s . aa <= i & i <= ((n + 1) + (s . aa)) - 1 implies (s . f) . S0cv <= (s . f) . i )
assume that A74:
s . aa <= i
and A75:
i <= ((n + 1) + (s . aa)) - 1
;
(s . f) . S0cv <= (s . f) . i
end; A76:
for
i being
Nat st
s . aa <= i &
i < S0cv holds
(s . f) . i > (s . f) . S0cv
proof
let i be
Nat;
( s . aa <= i & i < S0cv implies (s . f) . i > (s . f) . S0cv )
assume that A77:
s . aa <= i
and A78:
i < S0cv
;
(s . f) . i > (s . f) . S0cv
i + 1
<= S0cv
by A78, NAT_1:13;
then
(i + 1) - 1
<= S0cv - 1
by XREAL_1:9;
then
(s . f) . SFnc <= (s . f) . i
by A1, A9, A21, A32, A53, A59, A60, A61, A58, A77, FINSEQ_6:161;
hence
(s . f) . i > (s . f) . S0cv
by A71, XXREAL_0:2;
verum
end; ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . c
by A19, A41, A39, A57, A66, A71, SCMFSA8B:40
.=
(Exec ((c := (3 -rdRWNotIn {aa,bb,c})),(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))))) . c
by SCMFSA6C:5
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n)))) . (3 -rdRWNotIn {aa,bb,c})
by SCMFSA_2:63
.=
S0cv
by A43, SCMFSA_M:37
;
hence
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at (
(s . f),
sa,
sa11)
by A1, A9, A21, A32, A53, A70, A68, A73, A76, FINSEQ_6:161;
verum end; suppose A79:
(s . f) . SFnc <= (s . f) . S0cv
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )thus
(
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) = (n + 1) + ((Exec ((c := aa),(Initialized s))) . aa) &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex
sa1 being
Element of
NAT st
(
sa1 = ((n + 1) + sa) - 1 &
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at (
(s . f),
sa,
sa1) ) )
verumproof
A80:
for
i being
Nat st
s . aa <= i &
i <= ((n + 1) + (s . aa)) - 1 holds
(s . f) . SFnc <= (s . f) . i
proof
let i be
Nat;
( s . aa <= i & i <= ((n + 1) + (s . aa)) - 1 implies (s . f) . SFnc <= (s . f) . i )
assume that A81:
s . aa <= i
and A82:
i <= ((n + 1) + (s . aa)) - 1
;
(s . f) . SFnc <= (s . f) . i
end;
thus ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
((IExec ((Stop SCM+FSA),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A12, A41, A40, A57, A66, A79, SCMFSA8B:40
.=
((IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A36, SCMFSA_M:2
.=
(n + 1) + ((Exec ((c := aa),(Initialized s))) . aa)
by A32, A43, A53
;
( ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . f & ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) ) )
thus ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((Stop SCM+FSA),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . f
by A41, A38, A57, A66, A79, SCMFSA8B:40
.=
(Exec ((c := aa),(Initialized s))) . f
by A10, A36, A35, A55, SCMFSA_M:2
;
ex sa1 being Element of NAT st
( sa1 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa1) )
reconsider sa11 =
((n + 1) + sa) - 1 as
Element of
NAT by A69;
take
sa11
;
( sa11 = ((n + 1) + sa) - 1 & ((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa11) )
thus
sa11 = ((n + 1) + sa) - 1
;
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at ((s . f),sa,sa11)
(n + (s . aa)) - 1
<= ((n + (s . aa)) - 1) + 1
by XREAL_1:29;
then A83:
SFnc <= ((n + 1) + (s . aa)) - 1
by A9, A59, A64, XXREAL_0:2;
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c =
(IExec ((Stop SCM+FSA),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))),(p +* (while>0 ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),((((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))) ";" (AddTo ((3 -rdRWNotIn {aa,bb,c}),(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedILoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))))),(intloc 0))))))),((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n))))) . c
by A19, A41, A39, A57, A66, A79, SCMFSA8B:40
.=
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . n) . c
by A36, A42, SCMFSA_M:2
;
hence
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (n + 1)) . c = min_at (
(s . f),
sa,
sa11)
by A1, A9, A62, A67, A70, A68, A83, A80, FINSEQ_6:161;
verum
end; end;
end;
end; end;
end;
reconsider sb = |.(s . bb).| as Element of NAT ;
A84:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A84, A29);
then consider sab being Element of NAT such that
A85:
sab = ((sba + 1) + sa) - 1
and
A86:
((StepForUp ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))),p,(Exec ((c := aa),(Initialized s))))) . (sba + 1)) . c = min_at ((s . f),sa,sab)
;
A87:
sab = sb
by A9, A85, ABSVALUE:def 1;
for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))))) is_halting_on Exec ((c := aa),(Initialized s)),p
by A25, Th24;
hence (IExec ((FinSeqMin (f,aa,bb,c)),p,s)) . c =
(IExec ((for-up ((3 -rdRWNotIn {aa,bb,c}),aa,bb,((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ";" ((2 -ndRWNotIn {aa,bb,c}) := (f,c))) ";" (if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA)))))),p,(Exec ((c := aa),(Initialized s))))) . c
by SFMASTR1:14
.=
min_at ((s . f),|.(s . aa).|,|.(s . bb).|)
by A26, A86, A87, SCMFSA_M:2
;
verum