:: SFMASTR3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: SFMASTR3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for p being Permutation of X
for x, y being Element of X holds (p +* x,(p . y)) +* y,(p . x) is Permutation of X
proof end;

theorem Th2: :: SFMASTR3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for x, y being set st x in dom f & y in dom f holds
ex p being Permutation of dom f st (f +* x,(f . y)) +* y,(f . x) = f * p
proof end;

notation
let A be non empty finite real-membered set ;
synonym min A for lower_bound A;
end;

definition
let A be non empty finite real-membered set ;
redefine func lower_bound A means :Def1: :: SFMASTR3:def 1
( it in A & ( for k being real number st k in A holds
it <= k ) );
compatibility
for b1 being set holds
( b1 = min A iff ( b1 in A & ( for k being real number st k in A holds
b1 <= k ) ) )
proof end;
end;

:: deftheorem Def1 defines min SFMASTR3:def 1 :
for A being non empty finite real-membered set
for b2 being set holds
( b2 = min A iff ( b2 in A & ( for k being real number st k in A holds
b2 <= k ) ) );

registration
let X be non empty finite natural-membered set ;
cluster min X -> integer ;
coherence
min X is integer
proof end;
end;

definition
let F be FinSequence of INT ;
let m, n be Nat;
assume A1: ( 1 <= m & m <= n & n <= len F ) ;
canceled;
func min_at F,m,n -> Nat means :Def3: :: SFMASTR3:def 3
 ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & it + 1 = ((min X) .. (m,n -cut F)) + m );
existence
ex b1 being Nat ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & b1 + 1 = ((min X) .. (m,n -cut F)) + m )
proof end;
uniqueness
for b1, b2 being Nat st ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & b1 + 1 = ((min X) .. (m,n -cut F)) + m ) & ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & b2 + 1 = ((min X) .. (m,n -cut F)) + m ) holds
b1 = b2 ;
end;

:: deftheorem SFMASTR3:def 2 :
canceled;

:: deftheorem Def3 defines min_at SFMASTR3:def 3 :
for F being FinSequence of INT
for m, n being Nat st 1 <= m & m <= n & n <= len F holds
for b4 being Nat holds
( b4 = min_at F,m,n iff ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & b4 + 1 = ((min X) .. (m,n -cut F)) + m ) );

theorem Th3: :: SFMASTR3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being FinSequence of INT
for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds
( ma = min_at F,m,n iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) ) )
proof end;

theorem Th4: :: SFMASTR3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being FinSequence of INT
for m being Nat st 1 <= m & m <= len F holds
min_at F,m,m = m
proof end;

definition
let F be FinSequence of INT ;
let m, n be Nat;
pred F is_non_decreasing_on m,n means :Def4: :: SFMASTR3:def 4
for i, j being Nat st m <= i & i <= j & j <= n holds
F . i <= F . j;
end;

:: deftheorem Def4 defines is_non_decreasing_on SFMASTR3:def 4 :
for F being FinSequence of INT
for m, n being Nat holds
( F is_non_decreasing_on m,n iff for i, j being Nat st m <= i & i <= j & j <= n holds
F . i <= F . j );

definition
let F be FinSequence of INT ;
let n be Nat;
pred F is_split_at n means :Def5: :: SFMASTR3:def 5
for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds
F . i <= F . j;
end;

:: deftheorem Def5 defines is_split_at SFMASTR3:def 5 :
for F being FinSequence of INT
for n being Nat holds
( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds
F . i <= F . j );

theorem Th5: :: SFMASTR3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, F1 being FinSequence of INT
for k, ma being Nat st k + 1 <= len F & ma = min_at F,(k + 1),(len F) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* (k + 1),(F . ma)) +* ma,(F . (k + 1)) holds
F1 is_non_decreasing_on 1,k + 1
proof end;

theorem Th6: :: SFMASTR3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, F1 being FinSequence of INT
for k, ma being Nat st k + 1 <= len F & ma = min_at F,(k + 1),(len F) & F is_split_at k & F1 = (F +* (k + 1),(F . ma)) +* ma,(F . (k + 1)) holds
F1 is_split_at k + 1
proof end;

theorem Th7: :: SFMASTR3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for aa being Int-Location
for I being Macro-Instruction st I is_closed_on Initialize s & I is_halting_on Initialize s & I does_not_destroy aa holds
(IExec I,s) . aa = (Initialize s) . aa
proof end;

theorem Th8: :: SFMASTR3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
(IExec SCM+FSA-Stop ,s) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th9: :: SFMASTR3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for aa being Int-Location holds SCM+FSA-Stop does_not_refer aa
proof end;

theorem Th10: :: SFMASTR3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for aa, bb, cc being Int-Location st aa <> bb holds
cc := bb does_not_refer aa
proof end;

theorem Th11: :: SFMASTR3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb being Int-Location
for f being FinSeq-Location holds (Exec (a := f,bb),s) . a = (s . f) /. (abs (s . bb))
proof end;

theorem Th12: :: SFMASTR3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for aa, bb being Int-Location
for f being FinSeq-Location holds (Exec (f,aa := bb),s) . f = (s . f) +* (abs (s . aa)),(s . bb)
proof end;

registration
let a be read-write Int-Location ;
let b be Int-Location ;
let I, J be good Macro-Instruction;
cluster if>0 a,b,I,J -> good ;
coherence
if>0 a,b,I,J is good
proof end;
end;

theorem Th13: :: SFMASTR3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for aa, bb being Int-Location
for I, J being Macro-Instruction holds UsedIntLoc (if>0 aa,bb,I,J) = ({aa,bb} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)
proof end;

theorem Th14: :: SFMASTR3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for aa, bb being Int-Location
for I being Macro-Instruction st I does_not_destroy aa holds
while>0 bb,I does_not_destroy aa
proof end;

theorem Th15: :: SFMASTR3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for cc, aa, bb being Int-Location
for I, J being Macro-Instruction st cc <> aa & I does_not_destroy cc & J does_not_destroy cc holds
if>0 aa,bb,I,J does_not_destroy cc
proof end;

definition
let a, b, c be Int-Location ;
let I be Macro-Instruction;
let s be State of SCM+FSA ;
func StepForUp a,b,c,I,s -> Function of NAT , product the Object-Kind of SCM+FSA equals :: SFMASTR3:def 6
 StepWhile>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1)) +* a,(s . b));
coherence
StepWhile>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1)) +* a,(s . b)) is Function of NAT , product the Object-Kind of SCM+FSA ;
end;

:: deftheorem defines StepForUp SFMASTR3:def 6 :
for a, b, c being Int-Location
for I being Macro-Instruction
for s being State of SCM+FSA holds StepForUp a,b,c,I,s = StepWhile>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(((s . c) - (s . b)) + 1)) +* a,(s . b));

theorem Th16: :: SFMASTR3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Macro-Instruction st s . (intloc 0) = 1 holds
((StepForUp a,bb,cc,I,s) . 0) . (intloc 0) = 1
proof end;

theorem Th17: :: SFMASTR3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Macro-Instruction holds ((StepForUp a,bb,cc,I,s) . 0) . a = s . bb
proof end;

theorem Th18: :: SFMASTR3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Macro-Instruction st a <> bb holds
((StepForUp a,bb,cc,I,s) . 0) . bb = s . bb
proof end;

theorem Th19: :: SFMASTR3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for cc, bb being Int-Location
for I being Macro-Instruction st a <> cc holds
((StepForUp a,bb,cc,I,s) . 0) . cc = s . cc
proof end;

theorem Th20: :: SFMASTR3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for dd, bb, cc being Int-Location
for I being Macro-Instruction st a <> dd & dd in UsedIntLoc I holds
((StepForUp a,bb,cc,I,s) . 0) . dd = s . dd
proof end;

theorem Th21: :: SFMASTR3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for f being FinSeq-Location
for I being Macro-Instruction holds ((StepForUp a,bb,cc,I,s) . 0) . f = s . f
proof end;

theorem Th22: :: SFMASTR3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Macro-Instruction st s . (intloc 0) = 1 holds
for aux being read-write Int-Location st aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) holds
(IExec ((((aux := cc) ';' (SubFrom aux,bb)) ';' (AddTo aux,(intloc 0))) ';' (a := bb)),s) | (Int-Locations \/ FinSeq-Locations ) = ((s +* aux,(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) | (Int-Locations \/ FinSeq-Locations )
proof end;

definition
let a, b, c be Int-Location ;
let I be Macro-Instruction;
let s be State of SCM+FSA ;
pred ProperForUpBody a,b,c,I,s means :Def7: :: SFMASTR3:def 7
for i being Nat st i < ((s . c) - (s . b)) + 1 holds
( I is_closed_on (StepForUp a,b,c,I,s) . i & I is_halting_on (StepForUp a,b,c,I,s) . i );
end;

:: deftheorem Def7 defines ProperForUpBody SFMASTR3:def 7 :
for a, b, c being Int-Location
for I being Macro-Instruction
for s being State of SCM+FSA holds
( ProperForUpBody a,b,c,I,s iff for i being Nat st i < ((s . c) - (s . b)) + 1 holds
( I is_closed_on (StepForUp a,b,c,I,s) . i & I is_halting_on (StepForUp a,b,c,I,s) . i ) );

theorem Th23: :: SFMASTR3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for aa, bb, cc being Int-Location
for I being parahalting Macro-Instruction holds ProperForUpBody aa,bb,cc,I,s
proof end;

theorem Th24: :: SFMASTR3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Macro-Instruction
for k being Nat st ((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0) = 1 & Ig is_closed_on (StepForUp a,bb,cc,Ig,s) . k & Ig is_halting_on (StepForUp a,bb,cc,Ig,s) . k holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) . (intloc 0) = 1
proof end;

theorem Th25: :: SFMASTR3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Macro-Instruction st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Nat st k <= ((s . cc) - (s . bb)) + 1 holds
( ((StepForUp a,bb,cc,Ig,s) . k) . (intloc 0) = 1 & ( Ig does_not_destroy a implies ( ((StepForUp a,bb,cc,Ig,s) . k) . a = k + (s . bb) & ((StepForUp a,bb,cc,Ig,s) . k) . a <= (s . cc) + 1 ) ) & (((StepForUp a,bb,cc,Ig,s) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig)))) + k = ((s . cc) - (s . bb)) + 1 )
proof end;

theorem Th26: :: SFMASTR3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Macro-Instruction st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s holds
for k being Nat holds
( ((StepForUp a,bb,cc,Ig,s) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc Ig))) > 0 iff k < ((s . cc) - (s . bb)) + 1 )
proof end;

theorem Th27: :: SFMASTR3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Macro-Instruction
for k being Nat st s . (intloc 0) = 1 & ProperForUpBody a,bb,cc,Ig,s & k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp a,bb,cc,Ig,s) . (k + 1)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations ) = (IExec (Ig ';' (AddTo a,(intloc 0))),((StepForUp a,bb,cc,Ig,s) . k)) | (({a,bb,cc} \/ (UsedIntLoc Ig)) \/ FinSeq-Locations )
proof end;

definition
let a, b, c be Int-Location ;
let I be Macro-Instruction;
set aux = 1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I));
func for-up a,b,c,I -> Macro-Instruction equals :: SFMASTR3:def 8
(((((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))) := c) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),b)) ';' (AddTo (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := b)) ';' (while>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))));
coherence
(((((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))) := c) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),b)) ';' (AddTo (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := b)) ';' (while>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0)))) is Macro-Instruction ;
end;

:: deftheorem defines for-up SFMASTR3:def 8 :
for a, b, c being Int-Location
for I being Macro-Instruction holds for-up a,b,c,I = (((((1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))) := c) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),b)) ';' (AddTo (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := b)) ';' (while>0 (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,b,c} \/ (UsedIntLoc I))),(intloc 0))));

theorem Th28: :: SFMASTR3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for aa, bb, cc being Int-Location
for I being Macro-Instruction holds {aa,bb,cc} \/ (UsedIntLoc I) c= UsedIntLoc (for-up aa,bb,cc,I)
proof end;

registration
let a be read-write Int-Location ;
let b, c be Int-Location ;
let I be good Macro-Instruction;
cluster for-up a,b,c,I -> good ;
coherence
for-up a,b,c,I is good ;
end;

theorem Th29: :: SFMASTR3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being read-write Int-Location
for aa, bb, cc being Int-Location
for I being Macro-Instruction st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)) & I does_not_destroy aa holds
for-up a,bb,cc,I does_not_destroy aa
proof end;

theorem Th30: :: SFMASTR3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for I being Macro-Instruction st s . (intloc 0) = 1 & s . bb > s . cc holds
( ( for x being Int-Location st x <> a & x in {bb,cc} \/ (UsedIntLoc I) holds
(IExec (for-up a,bb,cc,I),s) . x = s . x ) & ( for f being FinSeq-Location holds (IExec (for-up a,bb,cc,I),s) . f = s . f ) )
proof end;

Lm1: now
let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for bb, cc being Int-Location
for I being good Macro-Instruction st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) holds
( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s )
let a be read-write Int-Location ; :: thesis: for bb, cc being Int-Location
for I being good Macro-Instruction st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) holds
( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s )
let bb, cc be Int-Location ;
set D = Int-Locations \/ FinSeq-Locations ;
let I be good Macro-Instruction; :: thesis: ( s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) implies ( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s ) )
assume that
A1: s . (intloc 0) = 1 and
A2: ( ProperForUpBody a,bb,cc,I,s or I is parahalting ) ; :: thesis: ( ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s & WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s )
A3: ProperForUpBody a,bb,cc,I,s by A2, Th23;
set aux = 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I));
set i0 = (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc;
set i1 = SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb;
set i2 = AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0);
set i3 = a := bb;
set IB = (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0));
set s1 = IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s;
set s2 = (s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb);
A4: (IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s) | (Int-Locations \/ FinSeq-Locations ) = ((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) | (Int-Locations \/ FinSeq-Locations ) by A1, Th22;
set IB2 = (AddTo a,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0));
set SW1 = StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s);
set SW2 = StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb));
set SF = StepForUp a,bb,cc,I,s;
set scb1 = ((s . cc) - (s . bb)) + 1;
A5: (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) = I ';' ((AddTo a,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) by SCMFSA6A:65;
A6: StepForUp a,bb,cc,I,s = StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)) ;
A7: ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)),(s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb)
proof
let k be Nat; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 or ( (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k & (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k ) )
assume ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 ; :: thesis: ( (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k & (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k )
then A8: k < ((s . cc) - (s . bb)) + 1 by A1, A3, A6, Th26;
then A9: ((StepForUp a,bb,cc,I,s) . k) . (intloc 0) = 1 by A1, A3, Th25;
A10: I is_closed_on (StepForUp a,bb,cc,I,s) . k by A3, A8, Def7;
then A11: I is_closed_on Initialize ((StepForUp a,bb,cc,I,s) . k) by A9, SFMASTR2:4;
I is_halting_on (StepForUp a,bb,cc,I,s) . k by A3, A8, Def7;
then A12: I is_halting_on Initialize ((StepForUp a,bb,cc,I,s) . k) by A9, A10, SFMASTR2:5;
A13: (AddTo a,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on IExec I,((StepForUp a,bb,cc,I,s) . k) by SCMFSA7B:24;
then A14: (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on Initialize ((StepForUp a,bb,cc,I,s) . k) by A5, A11, A12, SFMASTR1:3;
hence (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k by A9, SFMASTR2:4; :: thesis: (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k
(AddTo a,(intloc 0)) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on IExec I,((StepForUp a,bb,cc,I,s) . k) by SCMFSA7B:25;
then (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on Initialize ((StepForUp a,bb,cc,I,s) . k) by A5, A11, A12, A13, SFMASTR1:4;
hence (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k by A9, A14, SFMASTR2:5; :: thesis: verum
end;
thus ProperBodyWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s :: thesis: WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s
proof
let k be Nat; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 or ( (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k & (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k ) )
assume A15: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 ; :: thesis: ( (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k & (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k )
A16: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) | (Int-Locations \/ FinSeq-Locations ) by A4, A7, SCMFSA9A:40;
then A17: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by SCMFSA6A:38;
then A18: (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k by A7, A15, SCMFSA9A:def 4;
A19: (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k by A7, A15, A17, SCMFSA9A:def 4;
thus (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k by A16, A18, SCMFSA8B:6; :: thesis: (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k
thus (I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k by A16, A18, A19, SCMFSA8B:8; :: thesis: verum
end;
deffunc H1( Element of product the Object-Kind of SCM+FSA ) -> Element of NAT = abs ($1 . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))));
consider f being Function of product the Object-Kind of SCM+FSA , NAT such that
A20: for x being Element of product the Object-Kind of SCM+FSA holds f . x = H1(x) from FUNCT_2:sch 4( product the Object-Kind of SCM+FSA NAT );
A21: for k being Nat holds
( f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
proof
let k be Nat; :: thesis: ( f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
A22: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) | (Int-Locations \/ FinSeq-Locations ) by A4, A7, SCMFSA9A:40;
then A23: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by SCMFSA6A:38;
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) | (Int-Locations \/ FinSeq-Locations ) by A4, A7, SCMFSA9A:40;
then A24: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by SCMFSA6A:38;
now
assume A25: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 ; :: thesis: f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k)
A26: f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) = abs (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) by A20
.= ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by A23, A25, ABSVALUE:def 1 ;
k < ((s . cc) - (s . bb)) + 1 by A1, A3, A6, A23, A25, Th26;
then A27: (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) + k = ((s . cc) - (s . bb)) + 1 by A1, A3, A6, Th25;
A28: k < ((s . cc) - (s . bb)) + 1 by A1, A3, A6, A23, A25, Th26;
0 <= ((s . cc) - (s . bb)) + 1 by A28;
then reconsider scb1 = ((s . cc) - (s . bb)) + 1 as Nat by INT_1:16;
A29: k + 1 <= scb1 by A28, NAT_1:38;
then A30: (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) + (k + 1) = ((s . cc) - (s . bb)) + 1 by A1, A3, A6, Th25;
per cases ( ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ) ;
suppose A31: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) > 0 ; :: thesis: f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k)
A32: f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) = abs (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) by A20
.= ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) by A24, A31, ABSVALUE:def 1
.= scb1 - (k + 1) by A30
.= (scb1 - k) - 1 ;
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = scb1 - k by A27;
hence f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) by A26, A32, XREAL_1:148; :: thesis: verum
end;
suppose A33: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ; :: thesis: f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k)
((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),((s +* (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(((s . cc) - (s . bb)) + 1)) +* a,(s . bb))) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = scb1 - (k + 1) by A30;
then A34: ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) = 0 by A24, A29, A33, XREAL_1:50;
f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) = abs (((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)))) by A20
.= 0 by A34, ABSVALUE:def 1 ;
hence f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) by A22, A25, A26, SCMFSA6A:38; :: thesis: verum
end;
end;
end;
hence ( f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (k + 1)) < f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . k) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ) ; :: thesis: verum
end;
thus WithVariantWhile>0 1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I)),(I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0)), IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s :: thesis: verum
proof
take f ; :: according to SCMFSA9A:def 5 :: thesis: for b1 being Element of NAT holds
( not f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . b1) <= f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (b1 + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . b1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 )
thus for b1 being Element of NAT holds
( not f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . b1) <= f . ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . (b1 + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo a,(intloc 0))) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))),(IExec (((((1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) := cc) ';' (SubFrom (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),bb)) ';' (AddTo (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))),(intloc 0))) ';' (a := bb)),s)) . b1) . (1 -stRWNotIn ({a,bb,cc} \/ (UsedIntLoc I))) <= 0 ) by A21; :: thesis: verum
end;
end;

theorem Th31: :: SFMASTR3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for cc, bb being Int-Location
for Ig being good Macro-Instruction
for k being Nat st s . (intloc 0) = 1 & k = ((s . cc) - (s . bb)) + 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
(IExec (for-up a,bb,cc,Ig),s) | (Int-Locations \/ FinSeq-Locations ) = ((StepForUp a,bb,cc,Ig,s) . k) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th32: :: SFMASTR3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a being read-write Int-Location
for bb, cc being Int-Location
for Ig being good Macro-Instruction st s . (intloc 0) = 1 & ( ProperForUpBody a,bb,cc,Ig,s or Ig is parahalting ) holds
( for-up a,bb,cc,Ig is_closed_on s & for-up a,bb,cc,Ig is_halting_on s )
proof end;

definition
let start, finish, minpos be Int-Location ;
let f be FinSeq-Location ;
set aux1 = 1 -stRWNotIn {start,finish,minpos};
set aux2 = 2 -ndRWNotIn {start,finish,minpos};
set cv = 3 -rdRWNotIn {start,finish,minpos};
func FinSeqMin f,start,finish,minpos -> Macro-Instruction equals :: SFMASTR3:def 9
(minpos := start) ';' (for-up (3 -rdRWNotIn {start,finish,minpos}),start,finish,((((1 -stRWNotIn {start,finish,minpos}) := f,(3 -rdRWNotIn {start,finish,minpos})) ';' ((2 -ndRWNotIn {start,finish,minpos}) := f,minpos)) ';' (if>0 (2 -ndRWNotIn {start,finish,minpos}),(1 -stRWNotIn {start,finish,minpos}),(Macro (minpos := (3 -rdRWNotIn {start,finish,minpos}))),SCM+FSA-Stop )));
coherence
(minpos := start) ';' (for-up (3 -rdRWNotIn {start,finish,minpos}),start,finish,((((1 -stRWNotIn {start,finish,minpos}) := f,(3 -rdRWNotIn {start,finish,minpos})) ';' ((2 -ndRWNotIn {start,finish,minpos}) := f,minpos)) ';' (if>0 (2 -ndRWNotIn {start,finish,minpos}),(1 -stRWNotIn {start,finish,minpos}),(Macro (minpos := (3 -rdRWNotIn {start,finish,minpos}))),SCM+FSA-Stop ))) is Macro-Instruction ;
end;

:: deftheorem defines FinSeqMin SFMASTR3:def 9 :
for start, finish, minpos being Int-Location
for f being FinSeq-Location holds FinSeqMin f,start,finish,minpos = (minpos := start) ';' (for-up (3 -rdRWNotIn {start,finish,minpos}),start,finish,((((1 -stRWNotIn {start,finish,minpos}) := f,(3 -rdRWNotIn {start,finish,minpos})) ';' ((2 -ndRWNotIn {start,finish,minpos}) := f,minpos)) ';' (if>0 (2 -ndRWNotIn {start,finish,minpos}),(1 -stRWNotIn {start,finish,minpos}),(Macro (minpos := (3 -rdRWNotIn {start,finish,minpos}))),SCM+FSA-Stop )));

registration
let start, finish be Int-Location ;
let minpos be read-write Int-Location ;
let f be FinSeq-Location ;
cluster FinSeqMin f,start,finish,minpos -> good ;
coherence
FinSeqMin f,start,finish,minpos is good ;
end;

theorem Th33: :: SFMASTR3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location st c <> aa holds
FinSeqMin f,aa,bb,c does_not_destroy aa
proof end;

theorem Th34: :: SFMASTR3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location holds {aa,bb,c} c= UsedIntLoc (FinSeqMin f,aa,bb,c)
proof end;

theorem Th35: :: SFMASTR3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location st s . (intloc 0) = 1 holds
( FinSeqMin f,aa,bb,c is_closed_on s & FinSeqMin f,aa,bb,c is_halting_on s )
proof end;

theorem Th36: :: SFMASTR3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location st aa <> c & bb <> c & s . (intloc 0) = 1 holds
( (IExec (FinSeqMin f,aa,bb,c),s) . f = s . f & (IExec (FinSeqMin f,aa,bb,c),s) . aa = s . aa & (IExec (FinSeqMin f,aa,bb,c),s) . bb = s . bb )
proof end;

theorem Th37: :: SFMASTR3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for c being read-write Int-Location
for aa, bb being Int-Location
for f being FinSeq-Location st 1 <= s . aa & s . aa <= s . bb & s . bb <= len (s . f) & aa <> c & bb <> c & s . (intloc 0) = 1 holds
(IExec (FinSeqMin f,aa,bb,c),s) . c = min_at (s . f),(abs (s . aa)),(abs (s . bb))
proof end;

definition
let f be FinSeq-Location ;
let a, b be Int-Location ;
set aux1 = 1 -stRWNotIn {a,b};
set aux2 = 2 -ndRWNotIn {a,b};
func swap f,a,b -> Macro-Instruction equals :: SFMASTR3:def 10
((((1 -stRWNotIn {a,b}) := f,a) ';' ((2 -ndRWNotIn {a,b}) := f,b)) ';' (f,a := (2 -ndRWNotIn {a,b}))) ';' (f,b := (1 -stRWNotIn {a,b}));
coherence
((((1 -stRWNotIn {a,b}) := f,a) ';' ((2 -ndRWNotIn {a,b}) := f,b)) ';' (f,a := (2 -ndRWNotIn {a,b}))) ';' (f,b := (1 -stRWNotIn {a,b})) is Macro-Instruction ;
end;

:: deftheorem defines swap SFMASTR3:def 10 :
for f being FinSeq-Location
for a, b being Int-Location holds swap f,a,b = ((((1 -stRWNotIn {a,b}) := f,a) ';' ((2 -ndRWNotIn {a,b}) := f,b)) ';' (f,a := (2 -ndRWNotIn {a,b}))) ';' (f,b := (1 -stRWNotIn {a,b}));

registration
let f be FinSeq-Location ;
let a, b be Int-Location ;
cluster swap f,a,b -> good parahalting ;
coherence
( swap f,a,b is good & swap f,a,b is parahalting ) ;
end;

theorem Th38: :: SFMASTR3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for cc, aa, bb being Int-Location
for f being FinSeq-Location st cc <> 1 -stRWNotIn {aa,bb} & cc <> 2 -ndRWNotIn {aa,bb} holds
swap f,aa,bb does_not_destroy cc
proof end;

theorem Th39: :: SFMASTR3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for aa, bb being Int-Location
for f being FinSeq-Location st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
(IExec (swap f,aa,bb),s) . f = ((s . f) +* (s . aa),((s . f) . (s . bb))) +* (s . bb),((s . f) . (s . aa))
proof end;

theorem :: SFMASTR3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for aa, bb being Int-Location
for f being FinSeq-Location st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
( ((IExec (swap f,aa,bb),s) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec (swap f,aa,bb),s) . f) . (s . bb) = (s . f) . (s . aa) )
proof end;

theorem Th41: :: SFMASTR3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for aa, bb being Int-Location
for f being FinSeq-Location holds {aa,bb} c= UsedIntLoc (swap f,aa,bb)
proof end;

theorem :: SFMASTR3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for aa, bb being Int-Location
for f being FinSeq-Location holds UsedInt*Loc (swap f,aa,bb) = {f}
proof end;

definition
let f be FinSeq-Location ;
set cv = 1 -stRWNotIn ({} Int-Locations );
set minpos = 2 -ndRWNotIn ({} Int-Locations );
func Selection-sort f -> Macro-Instruction equals :: SFMASTR3:def 11
((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))));
coherence
((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations ))))) is Macro-Instruction ;
end;

:: deftheorem defines Selection-sort SFMASTR3:def 11 :
for f being FinSeq-Location holds Selection-sort f = ((1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))) :=len f) ';' (for-up (1 -stRWNotIn ({} Int-Locations )),(intloc 0),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),((FinSeqMin f,(1 -stRWNotIn ({} Int-Locations )),(1 -stNotUsed (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))),(2 -ndRWNotIn ({} Int-Locations ))) ';' (swap f,(1 -stRWNotIn ({} Int-Locations )),(2 -ndRWNotIn ({} Int-Locations )))));

theorem :: SFMASTR3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for f being FinSeq-Location
for S being State of SCM+FSA st S = IExec (Selection-sort f),s holds
( S . f is_non_decreasing_on 1, len (S . f) & ex p being Permutation of dom (s . f) st S . f = (s . f) * p )
proof end;