The Mizar abstract of SCMFSA8A

Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users
The abstract of the Mizar article:: Conditional Branch Macro Instructions of \SCMFSA. Part I
by
Noriko Asamoto
Received August 27, 1996
MML identifier: SCMFSA8A
[ Mizar article, MML identifier index ]
environ

 vocabulary AMI_3, AMI_1, SCMFSA_2, BOOLE, FUNCT_1, RELAT_1, FUNCT_4, SCM_1,
      FUNCT_7, SCMFSA6A, SCMFSA6B, SCMFSA6C, CAT_1, SF_MASTR, SCMFSA_4, CARD_1,
      SCMFSA7B, AMI_5, RELOC, SCMFSA_7, FINSEQ_1, UNIALG_2, SCMFSA8A, CARD_3;
 notation TARSKI, XBOOLE_0, XREAL_0, NAT_1, CQC_LANG, RELAT_1, FUNCT_1,
      FUNCT_4, FUNCT_7, CARD_1, FINSEQ_1, STRUCT_0, AMI_1, AMI_3, AMI_5,
      SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA_7, SCM_1, SCMFSA6A, SF_MASTR,
      SCMFSA6B, SCMFSA6C, SCMFSA7B;
 constructors AMI_5, SCMFSA_5, SCM_1, SCMFSA6A, SCMFSA6B, BINARITH, SCMFSA6C,
      SCMFSA_7, SCMFSA7B, SF_MASTR, MEMBERED;
 clusters RELSET_1, FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, SCMFSA6A,
      SF_MASTR, SCMFSA7B, INT_1, CQC_LANG, FRAENKEL, MEMBERED;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

reserve m for Nat;

canceled;

theorem :: SCMFSA8A:2  ::Lemma11
 for f,g being Function, D being set holds
     dom g misses D implies (f +* g) | D = f | D;

theorem :: SCMFSA8A:3  ::T50
 for s being State of SCM+FSA holds
     dom (s | the Instruction-Locations of SCM+FSA) =
         the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA8A:4  ::PRE8'103
 for s being State of SCM+FSA st s is halting
 for k being Nat st LifeSpan s <= k holds
     CurInstr (Computation s).k = halt SCM+FSA;

theorem :: SCMFSA8A:5  ::TQ53
 for s being State of SCM+FSA st s is halting
 for k being Nat st LifeSpan s <= k holds
     IC (Computation s).k = IC (Computation s).LifeSpan s;

theorem :: SCMFSA8A:6  ::T51(@BBB8)
 for s1,s2 being State of SCM+FSA holds
     s1,s2 equal_outside the Instruction-Locations of SCM+FSA
 iff IC s1 = IC s2 &
     s1 | (Int-Locations \/ FinSeq-Locations) =
     s2 | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8A:7  ::T27'
 for s being State of SCM+FSA, I being Macro-Instruction holds
     IC IExec(I,s) = IC Result (s +* Initialized I);

theorem :: SCMFSA8A:8  ::TI8
   for s being State of SCM+FSA, I being Macro-Instruction holds
     Initialize s +* Initialized I = s +* Initialized I;

theorem :: SCMFSA8A:9  ::TG13
 for I being Macro-Instruction, l being Instruction-Location of SCM+FSA holds
     I c= I +* Start-At l;

theorem :: SCMFSA8A:10  ::T52(@BBB8)
 for s being State of SCM+FSA, l being Instruction-Location of SCM+FSA holds
     s | (Int-Locations \/ FinSeq-Locations) =
     (s +* Start-At l) | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8A:11  ::T52'
   for s being State of SCM+FSA, I being Macro-Instruction,
 l being Instruction-Location of SCM+FSA holds
     s | (Int-Locations \/ FinSeq-Locations) =
     (s +* (I +* Start-At l)) | (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8A:12  ::T53(@BBB8)
 for s being State of SCM+FSA, l being Instruction-Location of SCM+FSA holds
     dom (s | the Instruction-Locations of SCM+FSA) misses dom Start-At l;

theorem :: SCMFSA8A:13  ::TI2
 for s being State of SCM+FSA, I being Macro-Instruction holds
     s +* Initialized I = Initialize s +* (I +* Start-At insloc 0);

theorem :: SCMFSA8A:14  ::TG14 <> T23
 for s being State of SCM+FSA, I1,I2 being Macro-Instruction,
 l being Instruction-Location of SCM+FSA holds
     s +* (I1 +* Start-At l), s +* (I2 +* Start-At l)
         equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA8A:15  ::T40(@BBB8)
     dom SCM+FSA-Stop = {insloc 0};

theorem :: SCMFSA8A:16  ::T41(@BBB8)
     insloc 0 in dom SCM+FSA-Stop & SCM+FSA-Stop.insloc 0 = halt SCM+FSA;

theorem :: SCMFSA8A:17  ::T20(@BBB8)
     card SCM+FSA-Stop = 1;

definition
 let P be programmed FinPartState of SCM+FSA;
 let l be Instruction-Location of SCM+FSA;
 func Directed(P,l) -> programmed FinPartState of SCM+FSA equals
:: SCMFSA8A:def 1
 ::D7
 ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .--> goto l)) * P;
end;

theorem :: SCMFSA8A:18  ::T38
 for I being programmed FinPartState of SCM+FSA holds
     Directed I = Directed(I,insloc card I);

definition
 let P be programmed FinPartState of SCM+FSA;
 let l be Instruction-Location of SCM+FSA;
 cluster Directed(P,l) -> halt-free;
end;

definition
 let P be programmed FinPartState of SCM+FSA;
 cluster Directed P -> halt-free;
end;

theorem :: SCMFSA8A:19  ::T21
 for P being programmed FinPartState of SCM+FSA,
 l being Instruction-Location of SCM+FSA holds
     dom Directed(P,l) = dom P;

theorem :: SCMFSA8A:20  ::T72'
 for P being programmed FinPartState of SCM+FSA,
 l being Instruction-Location of SCM+FSA holds
     Directed(P,l) = P +* ((halt SCM+FSA .--> goto l) * P);

theorem :: SCMFSA8A:21  ::T39'
 for P being programmed FinPartState of SCM+FSA,
 l being Instruction-Location of SCM+FSA, x being set
 st x in dom P holds
     (P.x = halt SCM+FSA implies Directed(P,l).x = goto l) &
     (P.x <> halt SCM+FSA implies Directed(P,l).x = P.x);

theorem :: SCMFSA8A:22  ::TQ60 <> T4
 for i being Instruction of SCM+FSA, a being Int-Location, n being Nat holds
     i does_not_destroy a implies IncAddr(i,n) does_not_destroy a;

theorem :: SCMFSA8A:23  ::TQ59'
 for P being programmed FinPartState of SCM+FSA, n being Nat,
 a being Int-Location holds
     P does_not_destroy a implies ProgramPart Relocated(P,n) does_not_destroy a
;

theorem :: SCMFSA8A:24  ::TQ59 <> T7
 for P being good programmed FinPartState of SCM+FSA, n being Nat holds
     ProgramPart Relocated(P,n) is good;

theorem :: SCMFSA8A:25  ::TQ58'
 for I,J being programmed FinPartState of SCM+FSA, a being Int-Location holds
     I does_not_destroy a & J does_not_destroy a implies
         I +* J does_not_destroy a;

theorem :: SCMFSA8A:26  ::TQ58
 for I,J being good programmed FinPartState of SCM+FSA holds
     I +* J is good;

theorem :: SCMFSA8A:27  ::TG8
 for I being programmed FinPartState of SCM+FSA,
 l being Instruction-Location of SCM+FSA, a being Int-Location holds
     I does_not_destroy a implies Directed(I,l) does_not_destroy a;

definition
 let I be good programmed FinPartState of SCM+FSA;
 let l be Instruction-Location of SCM+FSA;
 cluster Directed(I,l) -> good;
end;

definition
 let I be good Macro-Instruction;
 cluster Directed I -> good;
end;

definition
 let I be Macro-Instruction, l be Instruction-Location of SCM+FSA;
 cluster Directed(I,l) -> initial;
end;

definition
 let I,J be good Macro-Instruction;
 cluster I ';' J -> good;
end;

definition
 let l be Instruction-Location of SCM+FSA;
 func Goto l -> halt-free good Macro-Instruction equals
:: SCMFSA8A:def 2
 ::D1
  insloc 0 .--> goto l;
end;

definition
 let s be State of SCM+FSA;
 let P be initial FinPartState of SCM+FSA;
 pred P is_pseudo-closed_on s means
:: SCMFSA8A:def 3
 ::DQ1
 ex k being Nat st
     IC (Computation (s +* (P +* Start-At insloc 0))).k =
         insloc card ProgramPart P &
     for n being Nat st n < k holds
         IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P;
end;

definition let P be initial FinPartState of SCM+FSA;
 attr P is pseudo-paraclosed means
:: SCMFSA8A:def 4
 ::D2
 for s being State of SCM+FSA holds P is_pseudo-closed_on s;
end;

definition
 cluster pseudo-paraclosed Macro-Instruction;
end;

definition
 let s be State of SCM+FSA,
 P be initial FinPartState of SCM+FSA such that  P is_pseudo-closed_on s;
 func pseudo-LifeSpan(s,P) -> Nat means
:: SCMFSA8A:def 5
 ::DQ3
 IC (Computation (s +* (P +* Start-At insloc 0))).it =
     insloc card ProgramPart P &
 for n being Nat
 st not IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P
     holds it <= n;
end;

theorem :: SCMFSA8A:28  ::TQ51
 for I,J being Macro-Instruction, x being set holds
     x in dom I implies (I ';' J).x = (Directed I).x;

theorem :: SCMFSA8A:29  ::T31(@BBB8)
 for l being Instruction-Location of SCM+FSA holds
     card Goto l = 1;

theorem :: SCMFSA8A:30  ::T39
 for P being programmed FinPartState of SCM+FSA, x being set
 st x in dom P holds
     (P.x = halt SCM+FSA implies (Directed P).x = goto insloc card P) &
     (P.x <> halt SCM+FSA implies (Directed P).x = P.x);

theorem :: SCMFSA8A:31  ::TQ3
 for s being State of SCM+FSA, P being initial FinPartState of SCM+FSA st
 P is_pseudo-closed_on s holds
     for n being Nat st n < pseudo-LifeSpan(s,P) holds
         IC ((Computation (s +* (P +* Start-At insloc 0))).n) in dom P &
         CurInstr ((Computation (s +* (P +* Start-At insloc 0))).n) <>
             halt SCM+FSA;

theorem :: SCMFSA8A:32  ::BBBB'54'
 for s being State of SCM+FSA, I,J being Macro-Instruction
 st I is_pseudo-closed_on s
     for k being Nat st k <= pseudo-LifeSpan(s,I) holds
         (Computation (s +* (I +* Start-At insloc 0))).k,
         (Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
             equal_outside the Instruction-Locations of SCM+FSA;

theorem :: SCMFSA8A:33  ::TT4
 for I being programmed FinPartState of SCM+FSA,
 l being Instruction-Location of SCM+FSA holds
     card Directed(I,l) = card I;

theorem :: SCMFSA8A:34  ::TQ1
 for I being Macro-Instruction holds
     card Directed I = card I;

theorem :: SCMFSA8A:35  ::TQ21'
 for s being State of SCM+FSA, I being Macro-Instruction
 st I is_closed_on s & I is_halting_on s holds
     for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) holds
         ((Computation (s +* (I +* Start-At insloc 0))).k,
             (Computation (s +* (Directed I +* Start-At insloc 0))).k
             equal_outside the Instruction-Locations of SCM+FSA &
         CurInstr (Computation (s +* (Directed I +* Start-At insloc 0))).k <>
             halt SCM+FSA);

theorem :: SCMFSA8A:36  ::TQ4''(Lemma0)''
 for s being State of SCM+FSA, I being Macro-Instruction
 st I is_closed_on s & I is_halting_on s holds
     IC (Computation (s +* (Directed I +* Start-At insloc 0))).
         (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) = insloc card I &
     (Computation (s +* (I +* Start-At insloc 0))).
         (LifeSpan (s +* (I +* Start-At insloc 0))) |
         (Int-Locations \/ FinSeq-Locations) =
     (Computation (s +* (Directed I +* Start-At insloc 0))).
         (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) |
         (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8A:37  ::TQ18
  for s being State of SCM+FSA, I being Macro-Instruction holds
     I is_closed_on s & I is_halting_on s implies
         Directed I is_pseudo-closed_on s;

theorem :: SCMFSA8A:38  ::TQ18'
  for s being State of SCM+FSA, I being Macro-Instruction holds
     I is_closed_on s & I is_halting_on s implies
         pseudo-LifeSpan(s,Directed I) =
             LifeSpan (s +* (I +* Start-At insloc 0)) + 1;

theorem :: SCMFSA8A:39  ::T35'
 for I being programmed FinPartState of SCM+FSA,
 l being Instruction-Location of SCM+FSA holds
     I is halt-free implies Directed(I,l) = I;

theorem :: SCMFSA8A:40  ::T35
 for I being Macro-Instruction holds
     I is halt-free implies Directed I = I;

theorem :: SCMFSA8A:41  ::TT8'
 for I,J being Macro-Instruction holds
     Directed I ';' J = I ';' J;

theorem :: SCMFSA8A:42  ::TR1'
 for s being State of SCM+FSA, I,J being Macro-Instruction
 st I is_closed_on s & I is_halting_on s holds
 (for k being Nat st k <= LifeSpan (s +* (I +* Start-At insloc 0)) holds
     IC (Computation (s +* (Directed I +* Start-At insloc 0))).k =
         IC (Computation (s +* ((I ';' J) +* Start-At insloc 0))).k &
     CurInstr (Computation (s +* (Directed I +* Start-At insloc 0))).k =
         CurInstr (Computation (s +* ((I ';' J) +* Start-At insloc 0))).k) &
 (Computation (s +* (Directed I +* Start-At insloc 0))).
     (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) |
         (Int-Locations \/ FinSeq-Locations) =
     (Computation (s +* ((I ';' J) +* Start-At insloc 0))).
         (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) |
         (Int-Locations \/ FinSeq-Locations) &
 IC (Computation (s +* (Directed I +* Start-At insloc 0))).
     (LifeSpan (s +* (I +* Start-At insloc 0)) + 1) =
     IC (Computation (s +* ((I ';' J) +* Start-At insloc 0))).
         (LifeSpan (s +* (I +* Start-At insloc 0)) + 1);

theorem :: SCMFSA8A:43  ::TR1
 for s being State of SCM+FSA, I,J being Macro-Instruction
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
 (for k being Nat st k <= LifeSpan (s +* Initialized I) holds
     IC (Computation (s +* Initialized Directed I)).k =
         IC (Computation (s +* Initialized (I ';' J))).k &
     CurInstr (Computation (s +* Initialized Directed I)).k =
         CurInstr (Computation (s +* Initialized (I ';' J))).k) &
 (Computation (s +* Initialized Directed I)).
     (LifeSpan (s +* Initialized I) + 1) | (Int-Locations \/
 FinSeq-Locations) =
     (Computation (s +* Initialized (I ';' J))).
         (LifeSpan (s +* Initialized I) + 1) |
         (Int-Locations \/ FinSeq-Locations) &
 IC (Computation (s +* Initialized Directed I)).
     (LifeSpan (s +* Initialized I) + 1) =
     IC (Computation (s +* Initialized (I ';' J))).
         (LifeSpan (s +* Initialized I) + 1);

theorem :: SCMFSA8A:44  ::TQ21
 for s being State of SCM+FSA, I being Macro-Instruction
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
     for k being Nat st k <= LifeSpan (s +* Initialized I) holds
         ((Computation (s +* Initialized I)).k,
             (Computation (s +* Initialized Directed I)).k
             equal_outside the Instruction-Locations of SCM+FSA &
         CurInstr (Computation (s +* Initialized Directed I)).k <>
             halt SCM+FSA);

theorem :: SCMFSA8A:45  ::TQ4'(Lemma0)'
 for s being State of SCM+FSA, I being Macro-Instruction
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
     IC (Computation (s +* Initialized Directed I)).
         (LifeSpan (s +* Initialized I) + 1) = insloc card I &
     (Computation (s +* Initialized I)).(LifeSpan (s +* Initialized I)) |
         (Int-Locations \/ FinSeq-Locations) =
     (Computation (s +* Initialized Directed I)).
         (LifeSpan (s +* Initialized I) + 1) |
         (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8A:46  ::TI9' <> _T22''
   for I being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on s & I is_halting_on s holds
     I ';' SCM+FSA-Stop is_closed_on s &
     I ';' SCM+FSA-Stop is_halting_on s;

theorem :: SCMFSA8A:47  ::TB61'(TB61'@BBB8)
 for l being Instruction-Location of SCM+FSA holds
     insloc 0 in dom Goto l & (Goto l).insloc 0 = goto l;

theorem :: SCMFSA8A:48  ::T70
  for N being with_non-empty_elements set,
      S being definite (non empty non void AMI-Struct over N),
      I being programmed FinPartState of S, x being set holds
       x in dom I implies I.x is Instruction of S;

theorem :: SCMFSA8A:49  ::T71
 for I being programmed FinPartState of SCM+FSA, x being set, k being Nat holds
     x in dom ProgramPart Relocated(I,k) implies
         (ProgramPart Relocated(I,k)).x = Relocated(I,k).x;

theorem :: SCMFSA8A:50  ::T12
 for I being programmed FinPartState of SCM+FSA, k being Nat holds
     ProgramPart Relocated(Directed I,k) =
         Directed(ProgramPart Relocated(I,k),insloc (card I + k));

theorem :: SCMFSA8A:51  ::T37
 for I,J being programmed FinPartState of SCM+FSA,
 l being Instruction-Location of SCM+FSA holds
     Directed(I +* J,l) = Directed(I,l) +* Directed(J,l);

theorem :: SCMFSA8A:52  ::TQ52
 for I,J being Macro-Instruction holds
     Directed (I ';' J) = I ';' Directed J;

theorem :: SCMFSA8A:53
   for I being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
     IC (Computation (s +* Initialized (I ';' SCM+FSA-Stop))).
         (LifeSpan (s +* Initialized I) + 1) = insloc card I;

theorem :: SCMFSA8A:54
   for I being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
     (Computation (s +* Initialized I)).(LifeSpan (s +* Initialized I)) |
         (Int-Locations \/ FinSeq-Locations) =
     (Computation (s +* Initialized (I ';' SCM+FSA-Stop))).
         (LifeSpan (s +* Initialized I) + 1) |
         (Int-Locations \/ FinSeq-Locations);

theorem :: SCMFSA8A:55  ::TI9 <> _T22'
   for I being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
     s +* Initialized (I ';' SCM+FSA-Stop) is halting;

theorem :: SCMFSA8A:56
   for I being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
     LifeSpan (s +* Initialized (I ';' SCM+FSA-Stop)) =
         LifeSpan (s +* Initialized I) + 1;

theorem :: SCMFSA8A:57  ::TA24'(@BBB8)
   for s being State of SCM+FSA, I being Macro-Instruction
 st I is_closed_on Initialize s & I is_halting_on Initialize s
 holds IExec(I ';' SCM+FSA-Stop,s) = IExec(I,s) +* Start-At insloc card I;

theorem :: SCMFSA8A:58  ::TI10 <> T62''(@BBB8)
   for I,J being Macro-Instruction,s being State of SCM+FSA
 st I is_closed_on s & I is_halting_on s
 holds
     I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop is_closed_on s &
     I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop is_halting_on s;

theorem :: SCMFSA8A:59
   for I,J being Macro-Instruction, s being State of SCM+FSA st
 I is_closed_on s & I is_halting_on s holds
     s +* (I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop +*
         Start-At insloc 0) is halting;

theorem :: SCMFSA8A:60
   for I,J being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
     s +* Initialized (I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop)
         is halting;

theorem :: SCMFSA8A:61  ::T63'(@BBB8)
   for I,J being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
 IC IExec(I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop,s) =
     insloc (card I + card J + 1);

theorem :: SCMFSA8A:62  ::T64'(@BBB8)
   for I,J being Macro-Instruction, s being State of SCM+FSA
 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
 IExec(I ';' Goto insloc (card J + 1) ';' J ';' SCM+FSA-Stop,s) =
     IExec(I,s) +* Start-At insloc (card I + card J + 1);
The abstract of the Mizar article:

Conditional Branch Macro Instructions of \SCMFSA. Part I
