The abstract of the Mizar article:

Constant Assignment Macro Instructions of \SCMFSA. Part II

by

Noriko Asamoto

Received August 27, 1996

MML identifier: SCMFSA7B

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_3, AMI_1, SCMFSA_2, FINSEQ_1, RELAT_1, SCMFSA_7, ARYTM_1,
      FUNCT_1, CAT_1, SCMFSA6A, CARD_1, FUNCT_4, INT_1, FINSEQ_2, AMI_2,
      SCMFSA6B, SF_MASTR, BOOLE, DTCONSTR, ABSVALUE, AMI_5, UNIALG_2, SCMFSA_4,
      FUNCOP_1, SCMFSA7B, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_0, XREAL_0, REAL_1, NAT_1, INT_1,
      RELAT_1, FUNCT_1, FUNCT_4, FUNCT_7, FINSEQ_1, FINSEQ_2, FINSEQ_4,
      BINARITH, FINSOP_1, FUNCOP_1, DTCONSTR, CARD_1, CQC_LANG, AMI_1, AMI_3,
      AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_7, SCMFSA6A, SF_MASTR, SCMFSA6B,
      GROUP_1;
 constructors REAL_1, FINSOP_1, ENUMSET1, BINARITH, AMI_5, SCMFSA_7, SCMFSA6A,
      SF_MASTR, SCMFSA6B, FINSEQ_4, MEMBERED;
 clusters RELSET_1, FINSEQ_1, INT_1, FUNCT_1, AMI_1, SCMFSA_2, SCMFSA_4,
      SCMFSA_7, SF_MASTR, SCMFSA6B, FUNCOP_1, CQC_LANG, NAT_1, FRAENKEL,
      XREAL_0, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve m for Nat;

theorem :: SCMFSA7B:1  ::TG4
 for p being FinSequence of the Instructions of SCM+FSA holds
     dom Load p = {insloc m: m < len p};

theorem :: SCMFSA7B:2  ::T83(@AAAA)
 for p being FinSequence of the Instructions of SCM+FSA holds
     rng Load p = rng p;

definition
 let p be FinSequence of the Instructions of SCM+FSA;
 cluster Load p -> initial programmed;
end;

theorem :: SCMFSA7B:3  ::TQ50
   for i being Instruction of SCM+FSA holds
     Load <* i *> = insloc 0 .--> i;

theorem :: SCMFSA7B:4
 for i being Instruction of SCM+FSA holds
 dom Macro i = { insloc 0, insloc 1 };

theorem :: SCMFSA7B:5  ::TQ56
 for i being Instruction of SCM+FSA holds
     Macro i = Load <* i,halt SCM+FSA *>;

theorem :: SCMFSA7B:6  ::T54(@BBB8)
 for i being Instruction of SCM+FSA holds
     card Macro i = 2;

theorem :: SCMFSA7B:7  ::T25(@BBB8)
   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);

theorem :: SCMFSA7B:8  ::T26(@BBB8)
   for i being Instruction of SCM+FSA holds
     (Directed Macro i).insloc 1 = goto insloc 2;

definition
 let a be Int-Location, k be Integer;
 cluster a := k -> initial programmed;
end;

definition
 let a be Int-Location, k be Integer;
 cluster a := k -> parahalting;
end;

theorem :: SCMFSA7B:9 ::*
   for s being State of SCM+FSA
 for a being read-write Int-Location, 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);

definition
 let f be FinSeq-Location, p be FinSequence of INT;
 cluster f := p -> initial programmed;
end;

definition
 let f be FinSeq-Location, p be FinSequence of INT;
 cluster f := p -> parahalting;
end;

theorem :: SCMFSA7B:10 ::*TG1
   for s being State of SCM+FSA, f being FinSeq-Location,
 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;

definition
 let i be Instruction of SCM+FSA;
 let a be Int-Location;
 pred i does_not_refer a means
:: SCMFSA7B:def 1
 ::D20'
   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;

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

definition
 let i be Instruction of SCM+FSA;
 let a be Int-Location;
 pred i does_not_destroy a means
:: SCMFSA7B:def 3
 ::D19'
 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;

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

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

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

definition
 cluster halt-free good Macro-Instruction;
end;

theorem :: SCMFSA7B:11  ::R0''
 for a being Int-Location holds
     halt SCM+FSA does_not_destroy a;

theorem :: SCMFSA7B:12  ::R1''
 for a,b,c being Int-Location holds
     a <> b implies b := c does_not_destroy a;

theorem :: SCMFSA7B:13  ::R2''
 for a,b,c being Int-Location holds
     a <> b implies AddTo(b,c) does_not_destroy a;

theorem :: SCMFSA7B:14  ::R3''
 for a,b,c being Int-Location holds
     a <> b implies SubFrom(b,c) does_not_destroy a;

theorem :: SCMFSA7B:15  ::R4''
   for a,b,c being Int-Location holds
     a <> b implies MultBy(b,c) does_not_destroy a;

theorem :: SCMFSA7B:16  ::R5''
   for a,b,c being Int-Location holds
     a <> b & a <> c implies Divide(b,c) does_not_destroy a;

theorem :: SCMFSA7B:17  ::R6''
   for a being Int-Location, l being Instruction-Location of SCM+FSA holds
     goto l does_not_destroy a;

theorem :: SCMFSA7B:18  ::R7''
   for a,b being Int-Location, l being Instruction-Location of SCM+FSA holds
     b =0_goto l does_not_destroy a;

theorem :: SCMFSA7B:19  ::R8''
   for a,b being Int-Location, l being Instruction-Location of SCM+FSA holds
     b >0_goto l does_not_destroy a;

theorem :: SCMFSA7B:20  ::R9''
   for a,b,c being Int-Location, f being FinSeq-Location holds
     a <> b implies b := (f,c) does_not_destroy a;

theorem :: SCMFSA7B:21  ::R10''
   for a,b,c being Int-Location, f being FinSeq-Location holds
     (f,c):= b does_not_destroy a;

theorem :: SCMFSA7B:22  ::R11''
   for a,b being Int-Location, f being FinSeq-Location holds
     a <> b implies b :=len f does_not_destroy a;

theorem :: SCMFSA7B:23  ::R12''
   for a,b being Int-Location, f being FinSeq-Location holds
     f :=<0,...,0> b does_not_destroy a;

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

theorem :: SCMFSA7B:24  ::TQ6
 for I being Macro-Instruction holds
     I is paraclosed iff for s being State of SCM+FSA holds I is_closed_on s;

theorem :: SCMFSA7B:25 ::*TQ6'
   for I being Macro-Instruction holds
     I is parahalting iff for s being State of SCM+FSA holds I is_halting_on s;

theorem :: SCMFSA7B:26  ::TA10
 for i being Instruction of SCM+FSA, a being Int-Location,
 s being State of SCM+FSA holds
     i does_not_destroy a implies Exec(i,s).a = s.a;

theorem :: SCMFSA7B:27  ::TQ9''
 for s being State of SCM+FSA, I being Macro-Instruction, 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;

theorem :: SCMFSA7B:28  ::TQ7
 SCM+FSA-Stop does_not_destroy intloc 0;

definition
 cluster parahalting good Macro-Instruction;
end;

definition
 cluster SCM+FSA-Stop -> parahalting good;
end;

definition
 cluster paraclosed good -> keeping_0 Macro-Instruction;
end;

theorem :: SCMFSA7B:29  ::TS3
 for a being Int-Location, k being Integer holds
     rng aSeq(a,k) c=
         {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)};

theorem :: SCMFSA7B:30  ::TS1
 for a being Int-Location, k being Integer holds
     rng (a := k) c=
         {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)};

definition
 let a be read-write Int-Location, k be Integer;
 cluster a := k -> good;
end;

definition
 let a be read-write Int-Location, k be Integer;
 cluster a := k -> keeping_0;
end;