:: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec

::

:: Received July 22, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

set SA0 = Start-At (0,SCM+FSA);

theorem :: SCMFSA6C:1

for a being Int-Location

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a

proof end;

theorem :: SCMFSA6C:2

for f being FinSeq-Location

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for J being parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f

proof end;

begin

:: deftheorem Def1 defines parahalting SCMFSA6C:def 1 :

for i being Instruction of SCM+FSA holds

( i is parahalting iff Macro i is parahalting );

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 );

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

proof end;

registration

ex b_{1} being Instruction of SCM+FSA st

( b_{1} is keeping_0 & b_{1} is parahalting )
end;

cluster with_explicit_jumps IC-relocable parahalting keeping_0 for Element of the InstructionsF of SCM+FSA;

existence ex b

( b

proof end;

registration
end;

registration
end;

registration

let a, b be Int-Location;

coherence

a := b is parahalting

AddTo (a,b) is parahalting

SubFrom (a,b) is parahalting

MultBy (a,b) is parahalting

Divide (a,b) is parahalting

coherence

b := (f,a) is parahalting

( (f,a) := b is parahalting & (f,a) := b is keeping_0 )

end;
coherence

a := b is parahalting

proof end;

coherence AddTo (a,b) is parahalting

proof end;

coherence SubFrom (a,b) is parahalting

proof end;

coherence MultBy (a,b) is parahalting

proof end;

coherence Divide (a,b) is parahalting

proof end;

let f be FinSeq-Location ;coherence

b := (f,a) is parahalting

proof end;

coherence ( (f,a) := b is parahalting & (f,a) := b is keeping_0 )

proof end;

registration

let a be Int-Location;

let f be FinSeq-Location ;

coherence

a :=len f is parahalting

( f :=<0,...,0> a is parahalting & f :=<0,...,0> a is keeping_0 )

end;
let f be FinSeq-Location ;

coherence

a :=len f is parahalting

proof end;

coherence ( f :=<0,...,0> a is parahalting & f :=<0,...,0> a is keeping_0 )

proof end;

registration

let a be read-write Int-Location;

let b be Int-Location;

coherence

a := b is keeping_0

AddTo (a,b) is keeping_0

SubFrom (a,b) is keeping_0

MultBy (a,b) is keeping_0

end;
let b be Int-Location;

coherence

a := b is keeping_0

proof end;

coherence AddTo (a,b) is keeping_0

proof end;

coherence SubFrom (a,b) is keeping_0

proof end;

coherence MultBy (a,b) is keeping_0

proof end;

registration
end;

registration

let a be Int-Location;

let f be FinSeq-Location ;

let b be read-write Int-Location;

coherence

b := (f,a) is keeping_0

end;
let f be FinSeq-Location ;

let b be read-write Int-Location;

coherence

b := (f,a) is keeping_0

proof end;

registration

let f be FinSeq-Location ;

let b be read-write Int-Location;

coherence

b :=len f is keeping_0

end;
let b be read-write Int-Location;

coherence

b :=len f is keeping_0

proof end;

registration

let i be parahalting Instruction of SCM+FSA;

let J be parahalting Program of SCM+FSA;

coherence

i ";" J is parahalting ;

end;
let J be parahalting Program of SCM+FSA;

coherence

i ";" J is parahalting ;

registration

let I be parahalting Program of SCM+FSA;

let j be parahalting Instruction of SCM+FSA;

coherence

I ";" j is parahalting ;

end;
let j be parahalting Instruction of SCM+FSA;

coherence

I ";" j is parahalting ;

registration
end;

registration

let i be keeping_0 Instruction of SCM+FSA;

let J be keeping_0 Program of SCM+FSA;

coherence

i ";" J is keeping_0 ;

end;
let J be keeping_0 Program of SCM+FSA;

coherence

i ";" J is keeping_0 ;

registration

let I be keeping_0 Program of SCM+FSA;

let j be keeping_0 Instruction of SCM+FSA;

coherence

I ";" j is keeping_0 ;

end;
let j be keeping_0 Instruction of SCM+FSA;

coherence

I ";" j is keeping_0 ;

begin

theorem Th4: :: SCMFSA6C:4

for i being Instruction of SCM+FSA

for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds

DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))

for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds

DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))

proof end;

Lm3: now :: thesis: for I being keeping_0 parahalting Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

set IF = Data-Locations ;

let I be keeping_0 parahalting Program of SCM+FSA; :: thesis: for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

let P be Instruction-Sequence of SCM+FSA; :: thesis: DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

set IE = IExec (I,P,s);

end;
let I be keeping_0 parahalting Program of SCM+FSA; :: thesis: for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

let P be Instruction-Sequence of SCM+FSA; :: thesis: DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))

set IE = IExec (I,P,s);

now :: thesis: ( dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations ) & ( for x being set st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds

(DataPart (Initialized (IExec (I,P,s)))) . x = (IExec (I,P,s)) . x ) )

hence
DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
by FUNCT_1:46; :: thesis: verum(DataPart (Initialized (IExec (I,P,s)))) . x = (IExec (I,P,s)) . x ) )

A1:
dom (Initialized (IExec (I,P,s))) = the carrier of SCM+FSA
by PARTFUN1:def 2;

A2: the carrier of SCM+FSA = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;

A3: dom (IExec (I,P,s)) = the carrier of SCM+FSA by PARTFUN1:def 2;

hence dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations ) by A1, RELAT_1:61; :: thesis: for x being set st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds

(DataPart (Initialized (IExec (I,P,s)))) . b_{2} = (IExec (I,P,s)) . b_{2}

then A4: dom (DataPart (Initialized (IExec (I,P,s)))) = Data-Locations by A3, A2, XBOOLE_1:21;

let x be set ; :: thesis: ( x in dom (DataPart (Initialized (IExec (I,P,s)))) implies (DataPart (Initialized (IExec (I,P,s)))) . b_{1} = (IExec (I,P,s)) . b_{1} )

assume A5: x in dom (DataPart (Initialized (IExec (I,P,s)))) ; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b_{1} = (IExec (I,P,s)) . b_{1}

end;
A2: the carrier of SCM+FSA = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;

A3: dom (IExec (I,P,s)) = the carrier of SCM+FSA by PARTFUN1:def 2;

hence dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations ) by A1, RELAT_1:61; :: thesis: for x being set st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds

(DataPart (Initialized (IExec (I,P,s)))) . b

then A4: dom (DataPart (Initialized (IExec (I,P,s)))) = Data-Locations by A3, A2, XBOOLE_1:21;

let x be set ; :: thesis: ( x in dom (DataPart (Initialized (IExec (I,P,s)))) implies (DataPart (Initialized (IExec (I,P,s)))) . b

assume A5: x in dom (DataPart (Initialized (IExec (I,P,s)))) ; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b

per cases
( x in Int-Locations or x in FinSeq-Locations )
by A5, A4, SCMFSA_2:100, XBOOLE_0:def 3;

end;

suppose
x in Int-Locations
; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b_{1} = (IExec (I,P,s)) . b_{1}

then reconsider x9 = x as Int-Location by AMI_2:def 16;

end;
per cases
( x9 is read-write or x9 is read-only )
;

end;

suppose A6:
x9 is read-write
; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b_{1} = (IExec (I,P,s)) . b_{1}

thus (DataPart (Initialized (IExec (I,P,s)))) . x =
(Initialized (IExec (I,P,s))) . x
by A5, A4, FUNCT_1:49

.= (IExec (I,P,s)) . x by A6, SCMFSA_M:37 ; :: thesis: verum

end;
.= (IExec (I,P,s)) . x by A6, SCMFSA_M:37 ; :: thesis: verum

suppose
x9 is read-only
; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b_{1} = (IExec (I,P,s)) . b_{1}

then A7:
x9 = intloc 0
by SCMFSA_M:def 2;

thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49

.= 1 by A7, SCMFSA_M:9

.= (IExec (I,P,s)) . x by A7, SCMFSA6B:11 ; :: thesis: verum

end;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49

.= 1 by A7, SCMFSA_M:9

.= (IExec (I,P,s)) . x by A7, SCMFSA6B:11 ; :: thesis: verum

suppose
x in FinSeq-Locations
; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b_{1} = (IExec (I,P,s)) . b_{1}

then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;

thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49

.= (IExec (I,P,s)) . x by SCMFSA_M:37 ; :: thesis: verum

end;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49

.= (IExec (I,P,s)) . x by SCMFSA_M:37 ; :: thesis: verum

theorem Th5: :: SCMFSA6C:5

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)

for P being Instruction-Sequence of SCM+FSA

for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)

proof end;

theorem Th6: :: SCMFSA6C:6

for a being Int-Location

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

proof end;

theorem Th7: :: SCMFSA6C:7

for f being FinSeq-Location

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being keeping_0 parahalting Program of SCM+FSA

for j being parahalting Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f

proof end;

theorem Th8: :: SCMFSA6C:8

for a being Int-Location

for s being State of SCM+FSA

for P being Instruction-Sequence 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),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a

for s being State of SCM+FSA

for P being Instruction-Sequence 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),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a

proof end;

theorem :: SCMFSA6C:9

for f being FinSeq-Location

for s being State of SCM+FSA

for P being Instruction-Sequence 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),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f

for s being State of SCM+FSA

for P being Instruction-Sequence 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),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f

proof end;

begin

definition

let a, b be Int-Location;

coherence

(((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b)))) is Program of SCM+FSA;

;

end;
func swap (a,b) -> Program of SCM+FSA equals :: SCMFSA6C:def 3

(((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b))));

correctness (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b))));

coherence

(((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b)))) is Program of SCM+FSA;

;

:: deftheorem defines swap SCMFSA6C:def 3 :

for a, b being Int-Location holds swap (a,b) = (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b))));

for a, b being Int-Location holds swap (a,b) = (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)) ";" (b := (FirstNotUsed (Macro (a := b))));

registration
end;

theorem :: SCMFSA6C:10

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for a, b being read-write Int-Location holds

( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )

for P being Instruction-Sequence of SCM+FSA

for a, b being read-write Int-Location holds

( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )

proof end;