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

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

theorem Th1: :: SCMFSA7B:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of the Instructions of SCM+FSA holds dom (Load p) = { (insloc m) where m is Nat : m < len p }
proof end;

theorem Th2: :: SCMFSA7B:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of the Instructions of SCM+FSA holds rng (Load p) = rng p
proof end;

registration
let p be FinSequence of the Instructions of SCM+FSA ;
cluster Load p -> programmed initial ;
coherence
( Load p is initial & Load p is programmed )
proof end;
end;

theorem :: SCMFSA7B:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds Load <*i*> = (insloc 0) .--> i
proof end;

theorem Th4: :: SCMFSA7B:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds dom (Macro i) = {(insloc 0),(insloc 1)}
proof end;

theorem Th5: :: SCMFSA7B:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds Macro i = Load <*i,(halt SCM+FSA )*>
proof end;

theorem Th6: :: SCMFSA7B:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds card (Macro i) = 2
proof end;

theorem :: SCMFSA7B:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds
( ( i = halt SCM+FSA implies (Directed (Macro i)) . (insloc 0) = goto (insloc 2) ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . (insloc 0) = i ) )
proof end;

theorem :: SCMFSA7B:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds (Directed (Macro i)) . (insloc 1) = goto (insloc 2)
proof end;

registration
let a be Int-Location ;
let k be Integer;
cluster a := k -> programmed initial ;
coherence
( a := k is initial & a := k is programmed )
proof end;
end;

Lm1: for s being State of SCM+FSA st IC s = insloc 0 holds
for a being Int-Location
for k being Integer st a := k c= s holds
s is halting
proof end;

registration
let a be Int-Location ;
let k be Integer;
cluster a := k -> programmed initial parahalting ;
correctness
coherence
a := k is parahalting
;
proof end;
end;

theorem :: SCMFSA7B:9  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 k being Integer holds
( (IExec (a := k),s) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec (a := k),s) . b = s . b ) & ( for f being FinSeq-Location holds (IExec (a := k),s) . f = s . f ) )
proof end;

Lm2: for p1, p2, p3, p4 being FinSequence holds ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4)
proof end;

Lm3: for p1, p2, p3 being FinSequence holds
( ((len p1) + (len p2)) + (len p3) = len ((p1 ^ p2) ^ p3) & ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )
proof end;

Lm4: for s being State of SCM+FSA st IC s = insloc 0 & s . (intloc 0) = 1 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
( s is halting & (Result s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )
proof end;

Lm5: for s being State of SCM+FSA
for c0 being Nat st IC s = insloc c0 holds
for a being Int-Location
for k being Integer st ( for c being Nat st c < len (aSeq a,k) holds
(aSeq a,k) . (c + 1) = s . (insloc (c0 + c)) ) holds
for i being Nat st i <= len (aSeq a,k) holds
IC ((Computation s) . i) = insloc (c0 + i)
proof end;

Lm6: for s being State of SCM+FSA st IC s = insloc 0 holds
for a being Int-Location
for k being Integer st Load (aSeq a,k) c= s holds
for i being Nat st i <= len (aSeq a,k) holds
IC ((Computation s) . i) = insloc i
proof end;

Lm7: for s being State of SCM+FSA st IC s = insloc 0 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
s is halting
proof end;

registration
let f be FinSeq-Location ;
let p be FinSequence of INT ;
cluster f := p -> programmed initial ;
coherence
( f := p is initial & f := p is programmed )
proof end;
end;

registration
let f be FinSeq-Location ;
let p be FinSequence of INT ;
cluster f := p -> programmed initial parahalting ;
correctness
coherence
f := p is parahalting
;
proof end;
end;

theorem :: SCMFSA7B: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 f being FinSeq-Location
for p being FinSequence of INT holds
( (IExec (f := p),s) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec (f := p),s) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec (f := p),s) . g = s . g ) )
proof end;

definition
let i be Instruction of SCM+FSA ;
let a be Int-Location ;
pred i does_not_refer a means :: SCMFSA7B:def 1
for b being Int-Location
for l being Instruction-Location of SCM+FSA
for f being FinSeq-Location holds
( b := a <> i & AddTo b,a <> i & SubFrom b,a <> i & MultBy b,a <> i & Divide b,a <> i & Divide a,b <> i & a =0_goto l <> i & a >0_goto l <> i & b := f,a <> i & f,b := a <> i & f,a := b <> i & f :=<0,...,0> a <> i );
end;

:: deftheorem defines does_not_refer SCMFSA7B:def 1 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i does_not_refer a iff for b being Int-Location
for l being Instruction-Location of SCM+FSA
for f being FinSeq-Location holds
( b := a <> i & AddTo b,a <> i & SubFrom b,a <> i & MultBy b,a <> i & Divide b,a <> i & Divide a,b <> i & a =0_goto l <> i & a >0_goto l <> i & b := f,a <> i & f,b := a <> i & f,a := b <> i & f :=<0,...,0> a <> i ) );

definition
let I be programmed FinPartState of SCM+FSA ;
let a be Int-Location ;
pred I does_not_refer a means :: SCMFSA7B:def 2
for i being Instruction of SCM+FSA st i in rng I holds
i does_not_refer a;
end;

:: deftheorem defines does_not_refer SCMFSA7B:def 2 :
for I being programmed FinPartState of SCM+FSA
for a being Int-Location holds
( I does_not_refer a iff for i being Instruction of SCM+FSA st i in rng I holds
i does_not_refer a );

definition
let i be Instruction of SCM+FSA ;
let a be Int-Location ;
pred i does_not_destroy a means :Def3: :: SCMFSA7B:def 3
for b being Int-Location
for f being FinSeq-Location holds
( a := b <> i & AddTo a,b <> i & SubFrom a,b <> i & MultBy a,b <> i & Divide a,b <> i & Divide b,a <> i & a := f,b <> i & a :=len f <> i );
end;

:: deftheorem Def3 defines does_not_destroy SCMFSA7B:def 3 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i does_not_destroy a iff for b being Int-Location
for f being FinSeq-Location holds
( a := b <> i & AddTo a,b <> i & SubFrom a,b <> i & MultBy a,b <> i & Divide a,b <> i & Divide b,a <> i & a := f,b <> i & a :=len f <> i ) );

definition
let I be FinPartState of SCM+FSA ;
let a be Int-Location ;
pred I does_not_destroy a means :Def4: :: SCMFSA7B:def 4
for i being Instruction of SCM+FSA st i in rng I holds
i does_not_destroy a;
end;

:: deftheorem Def4 defines does_not_destroy SCMFSA7B:def 4 :
for I being FinPartState of SCM+FSA
for a being Int-Location holds
( I does_not_destroy a iff for i being Instruction of SCM+FSA st i in rng I holds
i does_not_destroy a );

definition
let I be FinPartState of SCM+FSA ;
attr I is good means :Def5: :: SCMFSA7B:def 5
I does_not_destroy intloc 0;
end;

:: deftheorem Def5 defines good SCMFSA7B:def 5 :
for I being FinPartState of SCM+FSA holds
( I is good iff I does_not_destroy intloc 0 );

definition
let I be FinPartState of SCM+FSA ;
attr I is halt-free means :Def6: :: SCMFSA7B:def 6
not halt SCM+FSA in rng I;
end;

:: deftheorem Def6 defines halt-free SCMFSA7B:def 6 :
for I being FinPartState of SCM+FSA holds
( I is halt-free iff not halt SCM+FSA in rng I );

registration
cluster good halt-free FinPartState of SCM+FSA ;
existence
ex b1 being Macro-Instruction st
( b1 is halt-free & b1 is good )
proof end;
end;

theorem Th11: :: SCMFSA7B:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location holds halt SCM+FSA does_not_destroy a
proof end;

theorem Th12: :: SCMFSA7B:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location st a <> b holds
b := c does_not_destroy a
proof end;

theorem Th13: :: SCMFSA7B:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location st a <> b holds
AddTo b,c does_not_destroy a
proof end;

theorem Th14: :: SCMFSA7B:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location st a <> b holds
SubFrom b,c does_not_destroy a
proof end;

theorem :: SCMFSA7B:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location st a <> b holds
MultBy b,c does_not_destroy a
proof end;

theorem :: SCMFSA7B:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location st a <> b & a <> c holds
Divide b,c does_not_destroy a
proof end;

theorem :: SCMFSA7B:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for l being Instruction-Location of SCM+FSA holds goto l does_not_destroy a
proof end;

theorem :: SCMFSA7B:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Int-Location
for l being Instruction-Location of SCM+FSA holds b =0_goto l does_not_destroy a
proof end;

theorem :: SCMFSA7B:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Int-Location
for l being Instruction-Location of SCM+FSA holds b >0_goto l does_not_destroy a
proof end;

theorem :: SCMFSA7B:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location
for f being FinSeq-Location st a <> b holds
b := f,c does_not_destroy a
proof end;

theorem :: SCMFSA7B:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location
for f being FinSeq-Location holds f,c := b does_not_destroy a
proof end;

theorem :: SCMFSA7B:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Int-Location
for f being FinSeq-Location st a <> b holds
b :=len f does_not_destroy a
proof end;

theorem :: SCMFSA7B:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Int-Location
for f being FinSeq-Location holds f :=<0,...,0> b does_not_destroy a
proof end;

definition
let I be FinPartState of SCM+FSA ;
let s be State of SCM+FSA ;
pred I is_closed_on s means :Def7: :: SCMFSA7B:def 7
for k being Nat holds IC ((Computation (s +* (I +* (Start-At (insloc 0))))) . k) in dom I;
pred I is_halting_on s means :Def8: :: SCMFSA7B:def 8
s +* (I +* (Start-At (insloc 0))) is halting;
end;

:: deftheorem Def7 defines is_closed_on SCMFSA7B:def 7 :
for I being FinPartState of SCM+FSA
for s being State of SCM+FSA holds
( I is_closed_on s iff for k being Nat holds IC ((Computation (s +* (I +* (Start-At (insloc 0))))) . k) in dom I );

:: deftheorem Def8 defines is_halting_on SCMFSA7B:def 8 :
for I being FinPartState of SCM+FSA
for s being State of SCM+FSA holds
( I is_halting_on s iff s +* (I +* (Start-At (insloc 0))) is halting );

theorem Th24: :: SCMFSA7B:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction holds
( I is paraclosed iff for s being State of SCM+FSA holds I is_closed_on s )
proof end;

theorem :: SCMFSA7B:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction holds
( I is parahalting iff for s being State of SCM+FSA holds I is_halting_on s )
proof end;

theorem Th26: :: SCMFSA7B:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA
for a being Int-Location
for s being State of SCM+FSA st i does_not_destroy a holds
(Exec i,s) . a = s . a
proof end;

theorem Th27: :: SCMFSA7B: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 I being Macro-Instruction
for a being Int-Location st I does_not_destroy a & I is_closed_on s holds
for k being Nat holds ((Computation (s +* (I +* (Start-At (insloc 0))))) . k) . a = s . a
proof end;

theorem Th28: :: SCMFSA7B:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
SCM+FSA-Stop does_not_destroy intloc 0
proof end;

Lm8: SCM+FSA-Stop is parahalting
proof end;

registration
cluster parahalting good FinPartState of SCM+FSA ;
existence
ex b1 being Macro-Instruction st
( b1 is parahalting & b1 is good )
proof end;
end;

registration
cluster SCM+FSA-Stop -> parahalting good ;
coherence
( SCM+FSA-Stop is parahalting & SCM+FSA-Stop is good )
by Def5, Lm8, Th28;
end;

registration
cluster paraclosed good -> keeping_0 FinPartState of SCM+FSA ;
correctness
coherence
for b1 being Macro-Instruction st b1 is paraclosed & b1 is good holds
b1 is keeping_0
;
proof end;
end;

theorem Th29: :: SCMFSA7B:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for k being Integer holds rng (aSeq a,k) c= {(a := (intloc 0)),(AddTo a,(intloc 0)),(SubFrom a,(intloc 0))}
proof end;

theorem Th30: :: SCMFSA7B:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for k being Integer holds rng (a := k) c= {(halt SCM+FSA ),(a := (intloc 0)),(AddTo a,(intloc 0)),(SubFrom a,(intloc 0))}
proof end;

registration
let a be read-write Int-Location ;
let k be Integer;
cluster a := k -> programmed initial parahalting keeping_0 good ;
correctness
coherence
a := k is good
;
proof end;
end;

registration
let a be read-write Int-Location ;
let k be Integer;
cluster a := k -> programmed initial parahalting keeping_0 good ;
correctness
coherence
a := k is keeping_0
;
;
end;