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