:: by JingChao Chen

::

:: Received June 15, 1999

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

begin

theorem Th1: :: SCMPDS_4:1

for i being Instruction of SCMPDS

for s being State of SCMPDS holds

( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = succ (IC s) )

for s being State of SCMPDS holds

( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = succ (IC s) )

proof end;

theorem :: SCMPDS_4:2

for s1, s2 being State of SCMPDS st IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) holds

s1 = s2

s1 = s2

proof end;

theorem Th8: :: SCMPDS_4:8

for s1, s2 being State of SCMPDS holds

( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )

( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )

proof end;

begin

definition

let I, J be Program of SCMPDS;

for b_{1} being Program of SCMPDS holds

( b_{1} = I ';' J iff b_{1} = I +* (Shift (J,(card I))) )
by AFINSQ_1:77;

coherence

I ';' J is Program of SCMPDS ;

end;
:: original: ';'

redefine func I ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 1

I +* (Shift (J,(card I)));

compatibility redefine func I ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 1

I +* (Shift (J,(card I)));

for b

( b

coherence

I ';' J is Program of SCMPDS ;

:: deftheorem defines ';' SCMPDS_4:def 1 :

for I, J being Program of SCMPDS holds I ';' J = I +* (Shift (J,(card I)));

for I, J being Program of SCMPDS holds I ';' J = I +* (Shift (J,(card I)));

begin

definition

let i be Instruction of SCMPDS;

let J be Program of SCMPDS;

correctness

coherence

(Load i) ';' J is Program of SCMPDS;

;

end;
let J be Program of SCMPDS;

correctness

coherence

(Load i) ';' J is Program of SCMPDS;

;

:: deftheorem defines ';' SCMPDS_4:def 2 :

for i being Instruction of SCMPDS

for J being Program of SCMPDS holds i ';' J = (Load i) ';' J;

for i being Instruction of SCMPDS

for J being Program of SCMPDS holds i ';' J = (Load i) ';' J;

definition

let I be Program of SCMPDS;

let j be Instruction of SCMPDS;

correctness

coherence

I ';' (Load j) is Program of SCMPDS;

;

end;
let j be Instruction of SCMPDS;

correctness

coherence

I ';' (Load j) is Program of SCMPDS;

;

:: deftheorem defines ';' SCMPDS_4:def 3 :

for I being Program of SCMPDS

for j being Instruction of SCMPDS holds I ';' j = I ';' (Load j);

for I being Program of SCMPDS

for j being Instruction of SCMPDS holds I ';' j = I ';' (Load j);

definition

let i, j be Instruction of SCMPDS;

correctness

coherence

(Load i) ';' (Load j) is Program of SCMPDS;

;

end;
correctness

coherence

(Load i) ';' (Load j) is Program of SCMPDS;

;

:: deftheorem defines ';' SCMPDS_4:def 4 :

for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' (Load j);

for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' (Load j);

theorem :: SCMPDS_4:11

for k being Instruction of SCMPDS

for I, J being Program of SCMPDS holds (I ';' J) ';' k = I ';' (J ';' k) by AFINSQ_1:27;

for I, J being Program of SCMPDS holds (I ';' J) ';' k = I ';' (J ';' k) by AFINSQ_1:27;

theorem :: SCMPDS_4:12

for j being Instruction of SCMPDS

for I, K being Program of SCMPDS holds (I ';' j) ';' K = I ';' (j ';' K) by AFINSQ_1:27;

for I, K being Program of SCMPDS holds (I ';' j) ';' K = I ';' (j ';' K) by AFINSQ_1:27;

theorem :: SCMPDS_4:13

for j, k being Instruction of SCMPDS

for I being Program of SCMPDS holds (I ';' j) ';' k = I ';' (j ';' k) by AFINSQ_1:27;

for I being Program of SCMPDS holds (I ';' j) ';' k = I ';' (j ';' k) by AFINSQ_1:27;

theorem :: SCMPDS_4:14

for i being Instruction of SCMPDS

for J, K being Program of SCMPDS holds (i ';' J) ';' K = i ';' (J ';' K) by AFINSQ_1:27;

for J, K being Program of SCMPDS holds (i ';' J) ';' K = i ';' (J ';' K) by AFINSQ_1:27;

theorem :: SCMPDS_4:15

for i, k being Instruction of SCMPDS

for J being Program of SCMPDS holds (i ';' J) ';' k = i ';' (J ';' k) by AFINSQ_1:27;

for J being Program of SCMPDS holds (i ';' J) ';' k = i ';' (J ';' k) by AFINSQ_1:27;

theorem :: SCMPDS_4:16

for i, j being Instruction of SCMPDS

for K being Program of SCMPDS holds (i ';' j) ';' K = i ';' (j ';' K) by AFINSQ_1:27;

for K being Program of SCMPDS holds (i ';' j) ';' K = i ';' (j ';' K) by AFINSQ_1:27;

theorem :: SCMPDS_4:17

definition

let s be State of SCMPDS;

let li be Int_position;

let k be Integer;

:: original: +*

redefine func s +* (li,k) -> PartState of SCMPDS;

coherence

s +* (li,k) is PartState of SCMPDS

end;
let li be Int_position;

let k be Integer;

:: original: +*

redefine func s +* (li,k) -> PartState of SCMPDS;

coherence

s +* (li,k) is PartState of SCMPDS

proof end;

begin

definition

let I be Program of SCMPDS;

let s be State of SCMPDS;

let P be Instruction-Sequence of SCMPDS;

coherence

Result ((P +* (stop I)),s) is State of SCMPDS ;

end;
let s be State of SCMPDS;

let P be Instruction-Sequence of SCMPDS;

coherence

Result ((P +* (stop I)),s) is State of SCMPDS ;

:: deftheorem defines IExec SCMPDS_4:def 5 :

for I being Program of SCMPDS

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds IExec (I,P,s) = Result ((P +* (stop I)),s);

for I being Program of SCMPDS

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds IExec (I,P,s) = Result ((P +* (stop I)),s);

definition

let I be Program of SCMPDS;

end;
attr I is paraclosed means :Def6: :: SCMPDS_4:def 6

for s being 0 -started State of SCMPDS

for n being Element of NAT

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I);

for s being 0 -started State of SCMPDS

for n being Element of NAT

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I);

attr I is parahalting means :Def7: :: SCMPDS_4:def 7

for s being 0 -started State of SCMPDS

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

P halts_on s;

for s being 0 -started State of SCMPDS

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

P halts_on s;

:: deftheorem Def6 defines paraclosed SCMPDS_4:def 6 :

for I being Program of SCMPDS holds

( I is paraclosed iff for s being 0 -started State of SCMPDS

for n being Element of NAT

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I) );

for I being Program of SCMPDS holds

( I is paraclosed iff for s being 0 -started State of SCMPDS

for n being Element of NAT

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

IC (Comput (P,s,n)) in dom (stop I) );

:: deftheorem Def7 defines parahalting SCMPDS_4:def 7 :

for I being Program of SCMPDS holds

( I is parahalting iff for s being 0 -started State of SCMPDS

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

P halts_on s );

for I being Program of SCMPDS holds

( I is parahalting iff for s being 0 -started State of SCMPDS

for P being Instruction-Sequence of SCMPDS st stop I c= P holds

P halts_on s );

Lm1: Load (halt SCMPDS) is parahalting

proof end;

registration

ex b_{1} being Program of SCMPDS st b_{1} is parahalting
by Lm1;

end;

cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() parahalting for set ;

existence ex b

theorem Th20: :: SCMPDS_4:20

for s being State of SCMPDS

for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds

not Q halts_on s

for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds

not Q halts_on s

proof end;

theorem Th21: :: SCMPDS_4:21

for n being Element of NAT

for I being Program of SCMPDS

for s1, s2 being State of SCMPDS

for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds

IC (Comput (P2,s2,m)) in dom I ) holds

for m being Element of NAT st m <= n holds

Comput (P1,s1,m) = Comput (P2,s2,m)

for I being Program of SCMPDS

for s1, s2 being State of SCMPDS

for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds

IC (Comput (P2,s2,m)) in dom I ) holds

for m being Element of NAT st m <= n holds

Comput (P1,s1,m) = Comput (P2,s2,m)

proof end;

registration

for b_{1} being Program of SCMPDS st b_{1} is parahalting holds

b_{1} is paraclosed
end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V71() parahalting -> paraclosed for set ;

coherence for b

b

proof end;

begin

definition

let i be Instruction of SCMPDS;

let n be Element of NAT ;

end;
let n be Element of NAT ;

pred i valid_at n means :Def8: :: SCMPDS_4:def 8

( ( InsCode i = 14 implies ex k1 being Integer st

( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) ) );

( ( InsCode i = 14 implies ex k1 being Integer st

( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) ) );

:: deftheorem Def8 defines valid_at SCMPDS_4:def 8 :

for i being Instruction of SCMPDS

for n being Element of NAT holds

( i valid_at n iff ( ( InsCode i = 14 implies ex k1 being Integer st

( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) ) ) );

for i being Instruction of SCMPDS

for n being Element of NAT holds

( i valid_at n iff ( ( InsCode i = 14 implies ex k1 being Integer st

( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st

( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) ) ) );

:: deftheorem Def9 defines shiftable SCMPDS_4:def 9 :

for IT being NAT -defined the InstructionsF of SCMPDS -valued finite Function holds

( IT is shiftable iff for n being Element of NAT

for i being Instruction of SCMPDS st n in dom IT & i = IT . n holds

( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) );

for IT being NAT -defined the InstructionsF of SCMPDS -valued finite Function holds

( IT is shiftable iff for n being Element of NAT

for i being Instruction of SCMPDS st n in dom IT & i = IT . n holds

( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) );

Lm2: Load (halt SCMPDS) is shiftable

proof end;

theorem Th22: :: SCMPDS_4:22

for i being Instruction of SCMPDS

for m, n being Element of NAT st i valid_at m & m <= n holds

i valid_at n

for m, n being Element of NAT st i valid_at m & m <= n holds

i valid_at n

proof end;

registration

ex b_{1} being Program of SCMPDS st

( b_{1} is parahalting & b_{1} is shiftable )
by Lm1, Lm2;

end;

cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() parahalting shiftable for set ;

existence ex b

( b

:: deftheorem Def10 defines shiftable SCMPDS_4:def 10 :

for i being Instruction of SCMPDS holds

( i is shiftable iff ( InsCode i = 2 or ( InsCode i <> 14 & InsCode i > 6 ) ) );

for i being Instruction of SCMPDS holds

( i is shiftable iff ( InsCode i = 2 or ( InsCode i <> 14 & InsCode i > 6 ) ) );

registration
end;

registration
end;

registration
end;

registration

let a, b be Int_position;

let k1, k2 be Integer;

coherence

AddTo (a,k1,b,k2) is shiftable

SubFrom (a,k1,b,k2) is shiftable

MultBy (a,k1,b,k2) is shiftable

Divide (a,k1,b,k2) is shiftable

(a,k1) := (b,k2) is shiftable

end;
let k1, k2 be Integer;

coherence

AddTo (a,k1,b,k2) is shiftable

proof end;

coherence SubFrom (a,k1,b,k2) is shiftable

proof end;

coherence MultBy (a,k1,b,k2) is shiftable

proof end;

coherence Divide (a,k1,b,k2) is shiftable

proof end;

coherence (a,k1) := (b,k2) is shiftable

proof end;

registration

let I, J be shiftable Program of SCMPDS;

coherence

for b_{1} being Program of SCMPDS st b_{1} = I ';' J holds

b_{1} is shiftable

end;
coherence

for b

b

proof end;

registration

let i be shiftable Instruction of SCMPDS;

coherence

for b_{1} being Program of SCMPDS st b_{1} = Load i holds

b_{1} is shiftable

end;
coherence

for b

b

proof end;

registration

let i be shiftable Instruction of SCMPDS;

let J be shiftable Program of SCMPDS;

coherence

i ';' J is shiftable ;

end;
let J be shiftable Program of SCMPDS;

coherence

i ';' J is shiftable ;

registration

let I be shiftable Program of SCMPDS;

let j be shiftable Instruction of SCMPDS;

coherence

I ';' j is shiftable ;

end;
let j be shiftable Instruction of SCMPDS;

coherence

I ';' j is shiftable ;

registration
end;

theorem :: SCMPDS_4:23

for I being shiftable Program of SCMPDS

for k1 being Integer st (card I) + k1 >= 0 holds

I ';' (goto k1) is shiftable

for k1 being Integer st (card I) + k1 >= 0 holds

I ';' (goto k1) is shiftable

proof end;

registration

let n be Element of NAT ;

coherence

for b_{1} being Program of SCMPDS st b_{1} = Load (goto n) holds

b_{1} is shiftable

end;
coherence

for b

b

proof end;

theorem :: SCMPDS_4:24

for I being shiftable Program of SCMPDS

for k1, k2 being Integer

for a being Int_position st (card I) + k2 >= 0 holds

I ';' ((a,k1) <>0_goto k2) is shiftable

for k1, k2 being Integer

for a being Int_position st (card I) + k2 >= 0 holds

I ';' ((a,k1) <>0_goto k2) is shiftable

proof end;

registration

let k1 be Integer;

let a be Int_position;

let n be Element of NAT ;

coherence

for b_{1} being Program of SCMPDS st b_{1} = Load ((a,k1) <>0_goto n) holds

b_{1} is shiftable

end;
let a be Int_position;

let n be Element of NAT ;

coherence

for b

b

proof end;

theorem :: SCMPDS_4:25

for I being shiftable Program of SCMPDS

for k1, k2 being Integer

for a being Int_position st (card I) + k2 >= 0 holds

I ';' ((a,k1) <=0_goto k2) is shiftable

for k1, k2 being Integer

for a being Int_position st (card I) + k2 >= 0 holds

I ';' ((a,k1) <=0_goto k2) is shiftable

proof end;

registration

let k1 be Integer;

let a be Int_position;

let n be Element of NAT ;

coherence

for b_{1} being Program of SCMPDS st b_{1} = Load ((a,k1) <=0_goto n) holds

b_{1} is shiftable

end;
let a be Int_position;

let n be Element of NAT ;

coherence

for b

b

proof end;

theorem :: SCMPDS_4:26

for I being shiftable Program of SCMPDS

for k1, k2 being Integer

for a being Int_position st (card I) + k2 >= 0 holds

I ';' ((a,k1) >=0_goto k2) is shiftable

for k1, k2 being Integer

for a being Int_position st (card I) + k2 >= 0 holds

I ';' ((a,k1) >=0_goto k2) is shiftable

proof end;

registration

let k1 be Integer;

let a be Int_position;

let n be Element of NAT ;

coherence

for b_{1} being Program of SCMPDS st b_{1} = Load ((a,k1) >=0_goto n) holds

b_{1} is shiftable

end;
let a be Int_position;

let n be Element of NAT ;

coherence

for b

b

proof end;

theorem Th27: :: SCMPDS_4:27

for s1, s2 being State of SCMPDS

for n, m being Element of NAT

for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds

(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

for n, m being Element of NAT

for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds

(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

proof end;

theorem Th28: :: SCMPDS_4:28

for s1, s2 being State of SCMPDS

for n, m being Element of NAT

for i being Instruction of SCMPDS st IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds

( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )

for n, m being Element of NAT

for i being Instruction of SCMPDS st IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds

( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )

proof end;

theorem :: SCMPDS_4:29

for s2 being State of SCMPDS

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for J being parahalting shiftable Program of SCMPDS st stop J c= P1 holds

for n being Element of NAT st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Element of NAT holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for J being parahalting shiftable Program of SCMPDS st stop J c= P1 holds

for n being Element of NAT st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Element of NAT holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

proof end;