:: SCMFSA7B semantic presentation

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

theorem Th1: :: SCMFSA7B:1

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

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

proof end;

end;

theorem :: SCMFSA7B:3

for i being Instruction of SCM+FSA holds Load <*i*> = (insloc 0) .--> i

proof end;

theorem Th4: :: SCMFSA7B:4

for i being Instruction of SCM+FSA holds dom (Macro i) = {(insloc 0),(insloc 1)}

proof end;

theorem Th5: :: SCMFSA7B:5

for i being Instruction of SCM+FSA holds Macro i = Load <*i,(halt SCM+FSA )*>

proof end;

theorem Th6: :: SCMFSA7B:6

for i being Instruction of SCM+FSA holds card (Macro i) = 2

proof end;

theorem :: SCMFSA7B:7

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

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

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

proof end;

end;

theorem :: SCMFSA7B:9

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

proof end;

end;

registration

let f be FinSeq-Location ;
let p be FinSequence of INT ;
cluster f := p -> programmed initial parahalting ;
correctness

proof end;

end;

theorem :: SCMFSA7B:10

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 :

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 :

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 :

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 :

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 :

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 :

registration

cluster good halt-free FinPartState of SCM+FSA ;
existence

proof end;

end;

theorem Th11: :: SCMFSA7B:11

for a being Int-Location holds halt SCM+FSA does_not_destroy a

proof end;

theorem Th12: :: SCMFSA7B:12

for a, b, c being Int-Location st a <> b holds
b := c does_not_destroy a

proof end;

theorem Th13: :: SCMFSA7B:13

for a, b, c being Int-Location st a <> b holds
AddTo b,c does_not_destroy a

proof end;

theorem Th14: :: SCMFSA7B:14

for a, b, c being Int-Location st a <> b holds
SubFrom b,c does_not_destroy a

proof end;

theorem :: SCMFSA7B:15

for a, b, c being Int-Location st a <> b holds
MultBy b,c does_not_destroy a

proof end;

theorem :: SCMFSA7B:16

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

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

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

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

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

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

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

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 :

:: deftheorem Def8 defines is_halting_on SCMFSA7B:def 8 :

theorem Th24: :: SCMFSA7B:24

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

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

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

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

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

proof end;

end;

registration

cluster SCM+FSA-Stop -> parahalting good ;
coherence by Def5, Lm8, Th28;

end;

registration

cluster paraclosed good -> keeping_0 FinPartState of SCM+FSA ;
correctness

proof end;

end;

theorem Th29: :: SCMFSA7B:29

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

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

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 ;

end;