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 st aa <> c & bb <> c & s . (intloc 0) = 1 holds
( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )
let c be read-write Int-Location ; for aa, bb being Int-Location
for f being FinSeq-Location st aa <> c & bb <> c & s . (intloc 0) = 1 holds
( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )
let aa, bb be Int-Location ; for f being FinSeq-Location st aa <> c & bb <> c & s . (intloc 0) = 1 holds
( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )
let f be FinSeq-Location ; ( aa <> c & bb <> c & s . (intloc 0) = 1 implies ( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb ) )
assume that
A1:
aa <> c
and
A2:
bb <> c
and
A3:
s . (intloc 0) = 1
; ( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )
set a = aa;
set b = bb;
set i0 = c := aa;
set s1 = Exec ((c := aa),(Initialized s));
A4:
( aa = intloc 0 or not aa is read-only )
by SF_MASTR:def 5;
A5:
( bb = intloc 0 or not bb is read-only )
by SF_MASTR:def 5;
A6: (Exec ((c := aa),(Initialized s))) . bb =
(Initialized s) . bb
by A2, SCMFSA_2:89
.=
s . bb
by A3, A5, SCMFSA6C:3
;
set cv = 3 -rdRWNotIn {aa,bb,c};
set aux2 = 2 -ndRWNotIn {aa,bb,c};
set aux1 = 1 -stRWNotIn {aa,bb,c};
set i10 = (1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}));
set i11 = (2 -ndRWNotIn {aa,bb,c}) := (f,c);
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 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)))));
A7:
2 -ndRWNotIn {aa,bb,c} <> 3 -rdRWNotIn {aa,bb,c}
by SFMASTR1:22;
3 -rdRWNotIn {aa,bb,c} in {(3 -rdRWNotIn {aa,bb,c}),aa,bb}
by ENUMSET1:def 1;
then A8:
3 -rdRWNotIn {aa,bb,c} in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (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;
A9:
1 -stRWNotIn {aa,bb,c} <> 3 -rdRWNotIn {aa,bb,c}
by SFMASTR1:22;
A10:
bb in {aa,bb,c}
by ENUMSET1:def 1;
then A11:
3 -rdRWNotIn {aa,bb,c} <> bb
by SFMASTR1:21;
A12:
1 -stRWNotIn {aa,bb,c} <> bb
by A10, SFMASTR1:21;
A13:
2 -ndRWNotIn {aa,bb,c} <> bb
by A10, SFMASTR1:21;
A14: (Exec ((c := aa),(Initialized s))) . aa =
(Initialized s) . aa
by A1, SCMFSA_2:89
.=
s . aa
by A3, A4, SCMFSA6C:3
;
bb in {(3 -rdRWNotIn {aa,bb,c}),aa,bb}
by ENUMSET1:def 1;
then A15:
bb in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (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;
A16:
aa in {aa,bb,c}
by ENUMSET1:def 1;
then A17:
3 -rdRWNotIn {aa,bb,c} <> aa
by SFMASTR1:21;
A18:
1 -stRWNotIn {aa,bb,c} <> aa
by A16, SFMASTR1:21;
A19:
2 -ndRWNotIn {aa,bb,c} <> aa
by A16, SFMASTR1:21;
A20: (Exec ((c := aa),(Initialized s))) . f =
(Initialized s) . f
by SCMFSA_2:89
.=
s . f
by SCMFSA6C:3
;
aa in {(3 -rdRWNotIn {aa,bb,c}),aa,bb}
by ENUMSET1:def 1;
then A21:
aa in {(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (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;
c in {aa,bb,c}
by ENUMSET1:def 1;
then A22:
3 -rdRWNotIn {aa,bb,c} <> c
by SFMASTR1:21;
A23: (Exec ((c := aa),(Initialized s))) . (intloc 0) =
(Initialized s) . (intloc 0)
by SCMFSA_2:89
.=
1
by SCMFSA6C:3
;
then A24:
( 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_closed_on Exec ((c := aa),(Initialized s)) & 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)) )
by Th32;
per cases
( s . aa > s . bb or s . aa <= s . bb )
;
suppose A25:
s . aa > s . bb
;
( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )thus (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f =
(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)))))),(Exec ((c := aa),(Initialized s))))) . f
by A24, SFMASTR1:16
.=
s . f
by A23, A14, A6, A20, A25, Th30
;
( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )
aa in {aa,bb}
by TARSKI:def 2;
then A26:
aa in {aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (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;
thus (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa =
(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)))))),(Exec ((c := aa),(Initialized s))))) . aa
by A24, SFMASTR1:15
.=
s . aa
by A17, A23, A14, A6, A25, A26, Th30
;
(IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb
bb in {aa,bb}
by TARSKI:def 2;
then A27:
bb in {aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (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;
thus (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb =
(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)))))),(Exec ((c := aa),(Initialized s))))) . bb
by A24, SFMASTR1:15
.=
s . bb
by A11, A23, A14, A6, A25, A27, Th30
;
verum end; suppose A28:
s . aa <= s . bb
;
( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f = s . f & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )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)))),
(Exec ((c := aa),(Initialized s))));
A29:
(s . aa) - (s . aa) <= (s . bb) - (s . aa)
by A28, XREAL_1:11;
then reconsider k =
((s . bb) - (s . aa)) + 1 as
Element of
NAT by INT_1:16;
defpred S1[
Nat]
means (
0 < $1 & $1
<= k 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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . $1) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . $1) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . $1) . bb = (Exec ((c := aa),(Initialized s))) . bb ) );
A30:
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))
by Th23;
A31:
for
n being
Element of
NAT st
S1[
n] holds
S1[
n + 1]
proof
let n be
Element of
NAT ;
( S1[n] implies S1[n + 1] )
assume that A32:
S1[
n]
and
0 < n + 1
and A33:
n + 1
<= k
;
( ((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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (Exec ((c := aa),(Initialized s))) . bb )
A34:
(
((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)))),(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)))),(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)))),(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 A35:
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)))),(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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n) . (intloc 0) = 1
by A23, Th16;
( ((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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa)
by A35, 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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb
by A14, A6, A28, A35, Th17;
verum end; suppose A36:
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)))),(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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n) . (intloc 0) = 1
by A32, A33, 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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) = n + ((Exec ((c := aa),(Initialized s))) . aa)
by A32, A33, A36, 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)))),(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 A33, XREAL_1:11;
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)))),(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c}) <= (Exec ((c := aa),(Initialized s))) . bb
by A14, A6, A32, A33, A36, NAT_1:13, XREAL_1:21;
verum end;
end;
n < n + 1
by XREAL_1:31;
then
n < k
by A33, 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) | (({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) | (({(3 -rdRWNotIn {aa,bb,c}),aa,bb} \/ (UsedIntLoc ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (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 A23, A14, A6, A30, Th27;
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)))),(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . f
by SFMASTR2:7
.=
(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . f
by SFMASTR1:13
.=
(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . f
by SCMFSA_2:90
.=
(IExec ((if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . f
by SFMASTR1:9
;
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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb =
(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . bb
by A15, A37, SFMASTR2:7
.=
(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . bb
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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . bb
by A11, SCMFSA_2:90
.=
(IExec ((if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . bb
by SFMASTR1:8
;
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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa =
(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . aa
by A21, A37, SFMASTR2:7
.=
(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . aa
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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . aa
by A17, SCMFSA_2:90
.=
(IExec ((if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . aa
by SFMASTR1:8
;
A41:
((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)))),(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})
by A8, A37, SFMASTR2:7
.=
(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})
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)))),((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)))),(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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (intloc 0))
by SCMFSA_2:90
.=
((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)))),((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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SCMFSA6B:35
.=
((IExec ((if>0 ((2 -ndRWNotIn {aa,bb,c}),(1 -stRWNotIn {aa,bb,c}),(Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(Stop SCM+FSA))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SFMASTR1:8
;
set ss =
IExec (
(((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n));
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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n)))));
A42:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . f
by SCMFSA6C:10
.=
(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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . f
by SCMFSA_2:98
.=
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . f
by SCMFSA_2:98
;
A43:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . (intloc 0)
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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . (intloc 0)
by SCMFSA_2:98
.=
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . (intloc 0)
by SCMFSA_2:98
.=
1
by SCMFSA6C:3
;
then A44:
DataPart (IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))
by Th8;
A45:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . bb =
(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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . bb
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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . bb
by A13, SCMFSA_2:98
.=
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . bb
by A12, SCMFSA_2:98
;
A46:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . aa =
(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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . aa
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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . aa
by A19, SCMFSA_2:98
.=
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . aa
by A18, SCMFSA_2:98
;
A47:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . (3 -rdRWNotIn {aa,bb,c})
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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . (3 -rdRWNotIn {aa,bb,c})
by A7, SCMFSA_2:98
.=
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . (3 -rdRWNotIn {aa,bb,c})
by A9, SCMFSA_2:98
;
A48:
( 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 A7, Th9, Th10, SCMFSA8C:80;
per cases
( 0 = n or 0 < n )
;
suppose A49:
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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (Exec ((c := aa),(Initialized s))) . bb )
verumproof
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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1
by A23, A14, A6, A30, A33, Th25;
( ((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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (Exec ((c := aa),(Initialized s))) . bb )
A50:
(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . 0) . f
by A49, SCMFSA6C:3
.=
s . f
by A20, Th21
;
A51:
(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . 0) . (3 -rdRWNotIn {aa,bb,c})
by A49, SCMFSA6C:3
.=
s . aa
by A14, Th17
;
A52:
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . bb =
((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)))),(Exec ((c := aa),(Initialized s))))) . 0) . bb
by A5, A34, A49, SCMFSA6C:3
.=
(Exec ((c := aa),(Initialized s))) . bb
by A11, Th19
;
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)))),(Exec ((c := aa),(Initialized s))))) . n)) . 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)))),(Exec ((c := aa),(Initialized s))))) . 0) . aa
by A4, A34, A49, SCMFSA6C:3
.=
(Exec ((c := aa),(Initialized s))) . aa
by A17, Th18
;
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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (Exec ((c := aa),(Initialized s))) . bb )
verumproof
per cases
( (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) <= (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {aa,bb,c}) or (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) > (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {aa,bb,c}) )
;
suppose A54:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) <= (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
((IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A7, A48, A41, SCMFSA8B:43
.=
(n + 1) + ((Exec ((c := aa),(Initialized s))) . aa)
by A14, A44, A47, A49, A51, SCMFSA6A:38
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . f
by A48, A38, A54, SCMFSA8B:43
.=
(Exec ((c := aa),(Initialized s))) . f
by A20, A44, A42, A50, SCMFSA6A:38
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa =
(IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . aa
by A19, A48, A40, A54, SCMFSA8B:43
.=
(Exec ((c := aa),(Initialized s))) . aa
by A44, A46, A53, SCMFSA6A:38
;
((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb =
(IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . bb
by A13, A48, A39, A54, SCMFSA8B:43
.=
(Exec ((c := aa),(Initialized s))) . bb
by A44, A45, A52, SCMFSA6A:38
;
verum end; suppose A55:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) > (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
((IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A7, A48, A41, SCMFSA8B:43
.=
((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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SCMFSA6C:6
.=
((Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A22, SCMFSA_2:89
.=
(n + 1) + ((Exec ((c := aa),(Initialized s))) . aa)
by A14, A47, A49, A51, SCMFSA6C:3
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . f
by A48, A38, A55, SCMFSA8B:43
.=
(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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . f
by SCMFSA6C:6
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . f
by SCMFSA_2:89
.=
(Exec ((c := aa),(Initialized s))) . f
by A20, A42, A50, SCMFSA6C:3
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . aa
by A19, A48, A40, A55, SCMFSA8B:43
.=
(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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . aa
by SCMFSA6C:6
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . aa
by A1, SCMFSA_2:89
.=
(Exec ((c := aa),(Initialized s))) . aa
by A4, A43, A46, A53, SCMFSA6C:3
;
((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . bb
by A13, A48, A39, A55, SCMFSA8B:43
.=
(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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . bb
by SCMFSA6C:6
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . bb
by A2, SCMFSA_2:89
.=
(Exec ((c := aa),(Initialized s))) . bb
by A5, A43, A45, A52, SCMFSA6C:3
;
verum end;
end;
end; end; suppose A56:
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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (Exec ((c := aa),(Initialized s))) . bb )
verumproof
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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (intloc 0) = 1
by A23, A14, A6, A30, A33, Th25;
( ((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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (Exec ((c := aa),(Initialized s))) . bb )
A57:
(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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . n) . (3 -rdRWNotIn {aa,bb,c})
by SCMFSA6C:3;
A58:
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . aa = (Exec ((c := aa),(Initialized s))) . aa
by A4, A32, A33, A56, NAT_1:13, SCMFSA6C:3;
A59:
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . bb = (Exec ((c := aa),(Initialized s))) . bb
by A5, A32, A33, A56, NAT_1:13, SCMFSA6C:3;
A60:
(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)))),(Exec ((c := aa),(Initialized s))))) . n)) . f = s . f
by A20, A32, A33, A56, NAT_1:13, SCMFSA6C:3;
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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (Exec ((c := aa),(Initialized s))) . bb )
verumproof
per cases
( (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) <= (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {aa,bb,c}) or (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) > (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {aa,bb,c}) )
;
suppose A61:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) <= (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
((IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A7, A48, A41, SCMFSA8B:43
.=
((IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A44, SCMFSA6A:38
.=
(n + 1) + ((Exec ((c := aa),(Initialized s))) . aa)
by A34, A47, A57
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . f
by A48, A38, A61, SCMFSA8B:43
.=
(Exec ((c := aa),(Initialized s))) . f
by A20, A44, A42, A60, SCMFSA6A:38
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa =
(IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . aa
by A19, A48, A40, A61, SCMFSA8B:43
.=
(Exec ((c := aa),(Initialized s))) . aa
by A44, A46, A58, SCMFSA6A:38
;
((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb =
(IExec ((Stop SCM+FSA),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . bb
by A13, A48, A39, A61, SCMFSA8B:43
.=
(Exec ((c := aa),(Initialized s))) . bb
by A44, A45, A59, SCMFSA6A:38
;
verum end; suppose A62:
(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (2 -ndRWNotIn {aa,bb,c}) > (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (1 -stRWNotIn {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)))),(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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . (3 -rdRWNotIn {aa,bb,c}) =
((IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A7, A48, A41, SCMFSA8B:43
.=
((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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SCMFSA6C:6
.=
((Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by A22, SCMFSA_2:89
.=
((IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))) . (3 -rdRWNotIn {aa,bb,c})) + 1
by SCMFSA6C:3
.=
(n + 1) + ((Exec ((c := aa),(Initialized s))) . aa)
by A34, A47, A57
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f = (Exec ((c := aa),(Initialized s))) . 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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . f =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . f
by A48, A38, A62, SCMFSA8B:43
.=
(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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . f
by SCMFSA6C:6
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . f
by SCMFSA_2:89
.=
(Exec ((c := aa),(Initialized s))) . f
by A20, A42, A60, SCMFSA6C:3
;
( ((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . aa =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . aa
by A19, A48, A40, A62, SCMFSA8B:43
.=
(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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . aa
by SCMFSA6C:6
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . aa
by A1, SCMFSA_2:89
.=
(Exec ((c := aa),(Initialized s))) . aa
by A4, A43, A46, A58, SCMFSA6C:3
;
((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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb = (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)))),(Exec ((c := aa),(Initialized s))))) . (n + 1)) . bb =
(IExec ((Macro (c := (3 -rdRWNotIn {aa,bb,c}))),(IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n))))) . bb
by A13, A48, A39, A62, SCMFSA8B:43
.=
(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))),((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)))),(Exec ((c := aa),(Initialized s))))) . n)))))) . bb
by SCMFSA6C:6
.=
(Initialized (IExec ((((1 -stRWNotIn {aa,bb,c}) := (f,(3 -rdRWNotIn {aa,bb,c}))) ';' ((2 -ndRWNotIn {aa,bb,c}) := (f,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)))),(Exec ((c := aa),(Initialized s))))) . n)))) . bb
by A2, SCMFSA_2:89
.=
(Exec ((c := aa),(Initialized s))) . bb
by A5, A43, A45, A59, SCMFSA6C:3
;
verum end;
end;
end; end;
end; A63:
S1[
0 ]
;
A64:
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A63, A31);
A65:
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)))))),(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)))),(Exec ((c := aa),(Initialized s))))) . k)
by A23, A14, A6, Th31;
thus (IExec ((FinSeqMin (f,aa,bb,c)),s)) . f =
(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)))))),(Exec ((c := aa),(Initialized s))))) . f
by A24, SFMASTR1:16
.=
((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)))),(Exec ((c := aa),(Initialized s))))) . k) . f
by A65, SCMFSA6A:38
.=
s . f
by A20, A29, A64
;
( (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa = s . aa & (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bb )thus (IExec ((FinSeqMin (f,aa,bb,c)),s)) . aa =
(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)))))),(Exec ((c := aa),(Initialized s))))) . aa
by A24, SFMASTR1:15
.=
((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)))),(Exec ((c := aa),(Initialized s))))) . k) . aa
by A65, SCMFSA6A:38
.=
s . aa
by A14, A29, A64
;
(IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb = s . bbthus (IExec ((FinSeqMin (f,aa,bb,c)),s)) . bb =
(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)))))),(Exec ((c := aa),(Initialized s))))) . bb
by A24, SFMASTR1:15
.=
((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)))),(Exec ((c := aa),(Initialized s))))) . k) . bb
by A65, SCMFSA6A:38
.=
s . bb
by A6, A29, A64
;
verum end;