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 ) )
set D = Int-Locations \/ FinSeq-Locations ;
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})) refersrefer 2
-ndRWNotIn {aa,bb,c} & not
Stop SCM+FSA refersrefer 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;