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

set D = Int-Locations \/ FinSeq-Locations ;

set SAt = Start-At (insloc 0);

set IL = the Instruction-Locations of SCM+FSA ;

theorem Th1: :: SFMASTR2:1  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 b being Int-Location
for I being Macro-Instruction st I is_closed_on Initialize s & I is_halting_on Initialize s & not b in UsedIntLoc I holds
(IExec I,s) . b = (Initialize s) . b
proof end;

theorem :: SFMASTR2:2  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 I being Macro-Instruction st I is_closed_on Initialize s & I is_halting_on Initialize s & not f in UsedInt*Loc I holds
(IExec I,s) . f = (Initialize s) . f
proof end;

theorem Th3: :: SFMASTR2:3  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 Int-Location
for I being Macro-Instruction st ( ( I is_closed_on Initialize s & I is_halting_on Initialize s ) or I is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) & not a in UsedIntLoc I holds
(IExec I,s) . a = s . a
proof end;

theorem Th4: :: SFMASTR2:4  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 I being Macro-Instruction st s . (intloc 0) = 1 holds
( I is_closed_on s iff I is_closed_on Initialize s )
proof end;

theorem Th5: :: SFMASTR2:5  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 I being Macro-Instruction st s . (intloc 0) = 1 holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialize s & I is_halting_on Initialize s ) )
proof end;

theorem Th6: :: SFMASTR2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations
for Floc being Subset of FinSeq-Locations holds
( s1 | (Iloc \/ Floc) = s2 | (Iloc \/ Floc) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location st x in Floc holds
s1 . x = s2 . x ) ) )
proof end;

theorem Th7: :: SFMASTR2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for Iloc being Subset of Int-Locations holds
( s1 | (Iloc \/ FinSeq-Locations ) = s2 | (Iloc \/ FinSeq-Locations ) iff ( ( for x being Int-Location st x in Iloc holds
s1 . x = s2 . x ) & ( for x being FinSeq-Location holds s1 . x = s2 . x ) ) )
proof end;

definition
let a be Int-Location ;
let I be Macro-Instruction;
set aux = 1 -stRWNotIn ({a} \/ (UsedIntLoc I));
func times a,I -> Macro-Instruction equals :: SFMASTR2:def 1
((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ';' (while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))));
correctness
coherence
((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a) ';' (while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0)))) is Macro-Instruction
;
;
end;

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

notation
let a be Int-Location ;
let I be Macro-Instruction;
synonym a times I for times a,I;
end;

theorem Th8: :: SFMASTR2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being Int-Location
for I being Macro-Instruction holds {b} \/ (UsedIntLoc I) c= UsedIntLoc (times b,I)
proof end;

theorem :: SFMASTR2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being Int-Location
for I being Macro-Instruction holds UsedInt*Loc (times b,I) = UsedInt*Loc I
proof end;

registration
let I be good Macro-Instruction;
let a be Int-Location ;
cluster times a,I -> good ;
coherence
times a,I is good
;
end;

definition
let s be State of SCM+FSA ;
let I be Macro-Instruction;
let a be Int-Location ;
set aux = 1 -stRWNotIn ({a} \/ (UsedIntLoc I));
func StepTimes a,I,s -> Function of NAT , product the Object-Kind of SCM+FSA equals :: SFMASTR2:def 2
StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialize s));
correctness
coherence
StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialize s)) is Function of NAT , product the Object-Kind of SCM+FSA
;
;
end;

:: deftheorem defines StepTimes SFMASTR2:def 2 :
for s being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location holds StepTimes a,I,s = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(I ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc I))),(intloc 0))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc I))) := a),(Initialize s));

theorem Th10: :: SFMASTR2:10  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 Int-Location
for J being good Macro-Instruction holds ((StepTimes a,J,s) . 0) . (intloc 0) = 1
proof end;

theorem Th11: :: SFMASTR2: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 Int-Location
for J being good Macro-Instruction st ( s . (intloc 0) = 1 or not a is read-only ) holds
((StepTimes a,J,s) . 0) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = s . a
proof end;

theorem Th12: :: SFMASTR2: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 a being Int-Location
for J being good Macro-Instruction
for k being Nat st ((StepTimes a,J,s) . k) . (intloc 0) = 1 & J is_closed_on (StepTimes a,J,s) . k & J is_halting_on (StepTimes a,J,s) . k holds
( ((StepTimes a,J,s) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 implies ((StepTimes a,J,s) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) - 1 ) )
proof end;

theorem Th13: :: SFMASTR2:13  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 Int-Location
for I being Macro-Instruction st ( s . (intloc 0) = 1 or not a is read-only ) holds
((StepTimes a,I,s) . 0) . a = s . a
proof end;

theorem :: SFMASTR2:14  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 Int-Location
for f being FinSeq-Location
for I being Macro-Instruction holds ((StepTimes a,I,s) . 0) . f = s . f
proof end;

definition
let s be State of SCM+FSA ;
let a be Int-Location ;
let I be Macro-Instruction;
pred ProperTimesBody a,I,s means :Def3: :: SFMASTR2:def 3
for k being Nat st k < s . a holds
( I is_closed_on (StepTimes a,I,s) . k & I is_halting_on (StepTimes a,I,s) . k );
end;

:: deftheorem Def3 defines ProperTimesBody SFMASTR2:def 3 :
for s being State of SCM+FSA
for a being Int-Location
for I being Macro-Instruction holds
( ProperTimesBody a,I,s iff for k being Nat st k < s . a holds
( I is_closed_on (StepTimes a,I,s) . k & I is_halting_on (StepTimes a,I,s) . k ) );

theorem Th15: :: SFMASTR2:15  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 Int-Location
for I being Macro-Instruction st I is parahalting holds
ProperTimesBody a,I,s
proof end;

theorem Th16: :: SFMASTR2: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 Int-Location
for J being good Macro-Instruction st ProperTimesBody a,J,s holds
for k being Nat st k <= s . a holds
((StepTimes a,J,s) . k) . (intloc 0) = 1
proof end;

theorem Th17: :: SFMASTR2: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 Int-Location
for J being good Macro-Instruction st ( s . (intloc 0) = 1 or not a is read-only ) & ProperTimesBody a,J,s holds
for k being Nat st k <= s . a holds
(((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a
proof end;

theorem Th18: :: SFMASTR2: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 Int-Location
for J being good Macro-Instruction st ProperTimesBody a,J,s & 0 <= s . a & ( s . (intloc 0) = 1 or not a is read-only ) holds
for k being Nat st k >= s . a holds
( ((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0 & ((StepTimes a,J,s) . k) . (intloc 0) = 1 )
proof end;

theorem Th19: :: SFMASTR2: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 Int-Location
for I being Macro-Instruction st s . (intloc 0) = 1 holds
((StepTimes a,I,s) . 0) | ((UsedIntLoc I) \/ FinSeq-Locations ) = s | ((UsedIntLoc I) \/ FinSeq-Locations )
proof end;

theorem Th20: :: SFMASTR2: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 Int-Location
for J being good Macro-Instruction
for k being Nat st ((StepTimes a,J,s) . k) . (intloc 0) = 1 & J is_halting_on Initialize ((StepTimes a,J,s) . k) & J is_closed_on Initialize ((StepTimes a,J,s) . k) & ((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 holds
((StepTimes a,J,s) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations ) = (IExec J,((StepTimes a,J,s) . k)) | ((UsedIntLoc J) \/ FinSeq-Locations )
proof end;

theorem Th21: :: SFMASTR2: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 Int-Location
for J being good Macro-Instruction
for k being Nat st ( ProperTimesBody a,J,s or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or not a is read-only ) holds
((StepTimes a,J,s) . (k + 1)) | ((UsedIntLoc J) \/ FinSeq-Locations ) = (IExec J,((StepTimes a,J,s) . k)) | ((UsedIntLoc J) \/ FinSeq-Locations )
proof end;

theorem :: SFMASTR2: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 Int-Location
for I being Macro-Instruction st s . a <= 0 & s . (intloc 0) = 1 holds
(IExec (times a,I),s) | ((UsedIntLoc I) \/ FinSeq-Locations ) = s | ((UsedIntLoc I) \/ FinSeq-Locations )
proof end;

theorem Th23: :: SFMASTR2: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 a being Int-Location
for J being good Macro-Instruction
for k being Nat st s . a = k & ( ProperTimesBody a,J,s or J is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) holds
(IExec (times a,J),s) | (Int-Locations \/ FinSeq-Locations ) = ((StepTimes a,J,s) . k) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th24: :: SFMASTR2: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 Int-Location
for J being good Macro-Instruction st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s or J is parahalting ) holds
( times a,J is_closed_on s & times a,J is_halting_on s )
proof end;

definition
let d be read-write Int-Location ;
func triv-times d -> Macro-Instruction equals :: SFMASTR2:def 4
times d,((while=0 d,(Macro (d := d))) ';' (SubFrom d,(intloc 0)));
correctness
coherence
times d,((while=0 d,(Macro (d := d))) ';' (SubFrom d,(intloc 0))) is Macro-Instruction
;
;
end;

:: deftheorem defines triv-times SFMASTR2:def 4 :
for d being read-write Int-Location holds triv-times d = times d,((while=0 d,(Macro (d := d))) ';' (SubFrom d,(intloc 0)));

theorem :: SFMASTR2: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 d being read-write Int-Location st s . d <= 0 holds
(IExec (triv-times d),s) . d = s . d
proof end;

theorem :: SFMASTR2: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 d being read-write Int-Location st 0 <= s . d holds
(IExec (triv-times d),s) . d = 0
proof end;

definition
let N, result be Int-Location ;
set next = 1 -stRWNotIn {N,result};
set Nsave = 1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))));
func Fib-macro N,result -> Macro-Instruction equals :: SFMASTR2:def 5
(((((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) ';' (N := (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))));
correctness
coherence
(((((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) ';' (N := (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result})))))) is Macro-Instruction
;
;
end;

:: deftheorem defines Fib-macro SFMASTR2:def 5 :
for N, result being Int-Location holds Fib-macro N,result = (((((1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) ';' (N := (1 -stNotUsed (times N,((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))));

theorem :: SFMASTR2: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 N, result being read-write Int-Location st N <> result holds
for n being Nat st n = s . N holds
( (IExec (Fib-macro N,result),s) . result = Fib n & (IExec (Fib-macro N,result),s) . N = s . N )
proof end;