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

set SA0 = Start-At (insloc 0);

theorem :: SCMFSA6C:1  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 s being State of SCM+FSA
for I being parahalting keeping_0 Macro-Instruction
for J being parahalting Macro-Instruction holds (IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a
proof end;

theorem :: SCMFSA6C:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSeq-Location
for s being State of SCM+FSA
for I being parahalting keeping_0 Macro-Instruction
for J being parahalting Macro-Instruction holds (IExec (I ';' J),s) . f = (IExec J,(IExec I,s)) . f
proof end;

definition
let i be Instruction of SCM+FSA ;
attr i is parahalting means :Def1: :: SCMFSA6C:def 1
 Macro i is parahalting;
attr i is keeping_0 means :Def2: :: SCMFSA6C:def 2
 Macro i is keeping_0;
end;

:: deftheorem Def1 defines parahalting SCMFSA6C:def 1 :
for i being Instruction of SCM+FSA holds
( i is parahalting iff Macro i is parahalting );

:: deftheorem Def2 defines keeping_0 SCMFSA6C:def 2 :
for i being Instruction of SCM+FSA holds
( i is keeping_0 iff Macro i is keeping_0 );

Lm1: Macro (halt SCM+FSA ) is parahalting
proof end;

Lm2: ( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting )
proof end;

registration
cluster halt SCM+FSA -> parahalting keeping_0 ;
coherence
( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting )
proof end;
end;

registration
cluster parahalting keeping_0 Element of the Instructions of SCM+FSA ;
existence
ex b1 being Instruction of SCM+FSA st
( b1 is keeping_0 & b1 is parahalting )
proof end;
end;

registration
let i be parahalting Instruction of SCM+FSA ;
cluster Macro i -> parahalting ;
coherence
Macro i is parahalting by Def1;
end;

registration
let i be keeping_0 Instruction of SCM+FSA ;
cluster Macro i -> keeping_0 ;
coherence
Macro i is keeping_0 by Def2;
end;

registration
let a, b be Int-Location ;
cluster a := b -> parahalting ;
coherence
a := b is parahalting
proof end;
cluster AddTo a,b -> parahalting ;
coherence
AddTo a,b is parahalting
proof end;
cluster SubFrom a,b -> parahalting ;
coherence
SubFrom a,b is parahalting
proof end;
cluster MultBy a,b -> parahalting ;
coherence
MultBy a,b is parahalting
proof end;
cluster Divide a,b -> parahalting ;
coherence
Divide a,b is parahalting
proof end;
let f be FinSeq-Location ;
cluster b := f,a -> parahalting ;
coherence
b := f,a is parahalting
proof end;
cluster f,a := b -> parahalting keeping_0 ;
coherence
( f,a := b is parahalting & f,a := b is keeping_0 )
proof end;
end;

registration
let a be Int-Location ;
let f be FinSeq-Location ;
cluster a :=len f -> parahalting ;
coherence
a :=len f is parahalting
proof end;
cluster f :=<0,...,0> a -> parahalting keeping_0 ;
coherence
( f :=<0,...,0> a is parahalting & f :=<0,...,0> a is keeping_0 )
proof end;
end;

registration
let a be read-write Int-Location ;
let b be Int-Location ;
cluster a := b -> parahalting keeping_0 ;
coherence
a := b is keeping_0
proof end;
cluster AddTo a,b -> parahalting keeping_0 ;
coherence
AddTo a,b is keeping_0
proof end;
cluster SubFrom a,b -> parahalting keeping_0 ;
coherence
SubFrom a,b is keeping_0
proof end;
cluster MultBy a,b -> parahalting keeping_0 ;
coherence
MultBy a,b is keeping_0
proof end;
end;

registration
let a, b be read-write Int-Location ;
cluster Divide a,b -> parahalting keeping_0 ;
coherence
Divide a,b is keeping_0
proof end;
end;

registration
let a be Int-Location ;
let f be FinSeq-Location ;
let b be read-write Int-Location ;
cluster b := f,a -> parahalting keeping_0 ;
coherence
b := f,a is keeping_0
proof end;
end;

registration
let f be FinSeq-Location ;
let b be read-write Int-Location ;
cluster b :=len f -> parahalting keeping_0 ;
coherence
b :=len f is keeping_0
proof end;
end;

registration
let i be parahalting Instruction of SCM+FSA ;
let J be parahalting Macro-Instruction;
cluster i ';' J -> parahalting ;
coherence
i ';' J is parahalting
proof end;
end;

registration
let I be parahalting Macro-Instruction;
let j be parahalting Instruction of SCM+FSA ;
cluster I ';' j -> parahalting ;
coherence
I ';' j is parahalting
proof end;
end;

registration
let i, j be parahalting Instruction of SCM+FSA ;
cluster i ';' j -> parahalting ;
coherence
i ';' j is parahalting
proof end;
end;

registration
let i be keeping_0 Instruction of SCM+FSA ;
let J be keeping_0 Macro-Instruction;
cluster i ';' J -> keeping_0 ;
coherence
i ';' J is keeping_0
proof end;
end;

registration
let I be keeping_0 Macro-Instruction;
let j be keeping_0 Instruction of SCM+FSA ;
cluster I ';' j -> keeping_0 ;
coherence
I ';' j is keeping_0
proof end;
end;

registration
let i, j be keeping_0 Instruction of SCM+FSA ;
cluster i ';' j -> keeping_0 ;
coherence
i ';' j is keeping_0
proof end;
end;

definition
let s be State of SCM+FSA ;
func Initialize s -> State of SCM+FSA equals :: SCMFSA6C:def 3
(s +* ((intloc 0) .--> 1)) +* (Start-At (insloc 0));
coherence
(s +* ((intloc 0) .--> 1)) +* (Start-At (insloc 0)) is State of SCM+FSA
proof end;
end;

:: deftheorem defines Initialize SCMFSA6C:def 3 :
for s being State of SCM+FSA holds Initialize s = (s +* ((intloc 0) .--> 1)) +* (Start-At (insloc 0));

theorem Th3: :: SCMFSA6C: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 holds
( IC (Initialize s) = insloc 0 & (Initialize s) . (intloc 0) = 1 & ( for a being read-write Int-Location holds (Initialize s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialize s) . f = s . f ) & ( for l being Instruction-Location of SCM+FSA holds (Initialize s) . l = s . l ) )
proof end;

theorem Th4: :: SCMFSA6C:4  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 holds
( s1,s2 equal_outside the Instruction-Locations of SCM+FSA iff s1 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = s2 | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) )
proof end;

theorem Th5: :: SCMFSA6C: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
for s1, s2 being State of SCM+FSA st s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
(Exec i,s1) | (Int-Locations \/ FinSeq-Locations ) = (Exec i,s2) | (Int-Locations \/ FinSeq-Locations )
proof end;

Lm3: now
let I be parahalting keeping_0 Macro-Instruction; :: thesis: for s being State of SCM+FSA holds (Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,s) | (Int-Locations \/ FinSeq-Locations )
let s be State of SCM+FSA ; :: thesis: (Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,s) | (Int-Locations \/ FinSeq-Locations )
set IE = IExec I,s;
set IF = Int-Locations \/ FinSeq-Locations ;
now
A1: ( dom (Initialize (IExec I,s)) = the carrier of SCM+FSA & dom (IExec I,s) = the carrier of SCM+FSA ) by AMI_3:36;
hence A2: dom ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) = (dom (IExec I,s)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90; :: thesis: for x being set st x in dom ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) holds
((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . b2 = (IExec I,s) . b2
let x be set ; :: thesis: ( x in dom ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) implies ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . b1 = (IExec I,s) . b1 )
assume A3: x in dom ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) ; :: thesis: ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . b1 = (IExec I,s) . b1
dom (Initialize (IExec I,s)) = (Int-Locations \/ FinSeq-Locations ) \/ ({(IC SCM+FSA )} \/ the Instruction-Locations of SCM+FSA ) by A1, SCMFSA_2:8, XBOOLE_1:4;
then A4: dom ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) = Int-Locations \/ FinSeq-Locations by A1, A2, XBOOLE_1:21;
per cases ( x in Int-Locations or x in FinSeq-Locations ) by A3, A4, XBOOLE_0:def 2;
suppose x in Int-Locations ; :: thesis: ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . b1 = (IExec I,s) . b1
then reconsider x' = x as Int-Location by SCMFSA_2:11;
hereby :: thesis: verum
per cases ( not x' is read-only or x' is read-only ) ;
suppose A5: not x' is read-only ; :: thesis: ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . x = (IExec I,s) . x
thus ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . x = (Initialize (IExec I,s)) . x by A3, A4, FUNCT_1:72
.= (IExec I,s) . x by A5, Th3 ; :: thesis: verum
end;
suppose x' is read-only ; :: thesis: ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . x = (IExec I,s) . x
then A6: x' = intloc 0 by SF_MASTR:def 5;
thus ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . x = (Initialize (IExec I,s)) . x' by A3, A4, FUNCT_1:72
.= 1 by A6, Th3
.= (IExec I,s) . x by A6, SCMFSA6B:35 ; :: thesis: verum
end;
end;
end;
end;
suppose x in FinSeq-Locations ; :: thesis: ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . b1 = (IExec I,s) . b1
then reconsider x' = x as FinSeq-Location by SCMFSA_2:12;
thus ((Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations )) . x = (Initialize (IExec I,s)) . x' by A3, A4, FUNCT_1:72
.= (IExec I,s) . x by Th3 ; :: thesis: verum
end;
end;
end;
hence (Initialize (IExec I,s)) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,s) | (Int-Locations \/ FinSeq-Locations ) by FUNCT_1:68; :: thesis: verum
end;

theorem Th6: :: SCMFSA6C:6  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 parahalting Instruction of SCM+FSA holds Exec i,(Initialize s) = IExec (Macro i),s
proof end;

theorem Th7: :: SCMFSA6C:7  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 s being State of SCM+FSA
for I being parahalting keeping_0 Macro-Instruction
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a
proof end;

theorem Th8: :: SCMFSA6C:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSeq-Location
for s being State of SCM+FSA
for I being parahalting keeping_0 Macro-Instruction
for j being parahalting Instruction of SCM+FSA holds (IExec (I ';' j),s) . f = (Exec j,(IExec I,s)) . f
proof end;

theorem Th9: :: SCMFSA6C:9  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 s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a
proof end;

theorem :: SCMFSA6C:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSeq-Location
for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec (i ';' j),s) . f = (Exec j,(Exec i,(Initialize s))) . f
proof end;

definition
let a, b be Int-Location ;
func swap a,b -> Macro-Instruction equals :: SCMFSA6C:def 4
(((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b))));
correctness
coherence
(((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b)))) is Macro-Instruction;
;
end;

:: deftheorem defines swap SCMFSA6C:def 4 :
for a, b being Int-Location holds swap a,b = (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b))));

registration
let a, b be Int-Location ;
cluster swap a,b -> parahalting ;
coherence
swap a,b is parahalting ;
end;

registration
let a, b be read-write Int-Location ;
cluster swap a,b -> parahalting keeping_0 ;
coherence
swap a,b is keeping_0 ;
end;

theorem :: SCMFSA6C: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, b being read-write Int-Location holds
( (IExec (swap a,b),s) . a = s . b & (IExec (swap a,b),s) . b = s . a )
proof end;

theorem :: SCMFSA6C:12  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 holds UsedInt*Loc (swap a,b) = {}
proof end;