Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Noriko Asamoto
- Received August 27, 1996
- MML identifier: SCMFSA8B
- [
Mizar article,
MML identifier index
]
environ
vocabulary AMI_1, SCMFSA_2, BOOLE, AMI_3, SCMFSA6A, AMI_5, RELOC, CARD_1,
FUNCT_4, RELAT_1, UNIALG_2, FUNCT_1, SCMFSA6C, SF_MASTR, FUNCT_7,
SCMFSA7B, SCMFSA6B, SCMFSA8A, SCMFSA_4, SCM_1, AMI_2, ARYTM_1, NAT_1,
ABSVALUE, FINSEQ_1, FINSEQ_2, SCMFSA8B, FINSEQ_4;
notation TARSKI, XBOOLE_0, XCMPLX_0, XREAL_0, NAT_1, INT_1, RELAT_1, FUNCT_1,
FUNCT_4, FUNCT_7, CARD_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, STRUCT_0, AMI_1,
AMI_3, AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCM_1, SCMFSA6A, SF_MASTR,
SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, GROUP_1;
constructors NAT_1, AMI_5, SCMFSA_5, SCM_1, SCMFSA6A, SCMFSA6B, SCMFSA6C,
SCMFSA8A, SF_MASTR, FINSEQ_4;
clusters RELSET_1, FUNCT_1, AMI_1, SCMFSA_2, SCMFSA_4, SF_MASTR, SCMFSA6B,
SCMFSA6C, INT_1, FRAENKEL, XREAL_0, NUMBERS;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
theorem :: SCMFSA8B:1 ::TA7(@BBB8)
for s being State of SCM+FSA holds
IC SCM+FSA in dom s;
theorem :: SCMFSA8B:2 ::TA8(@BBB8)
for s being State of SCM+FSA, l being Instruction-Location of SCM+FSA holds
l in dom s;
theorem :: SCMFSA8B:3 ::BBBB'53
for I being Macro-Instruction, s being State of SCM+FSA st I is_closed_on s
holds insloc 0 in dom I;
theorem :: SCMFSA8B:4 ::T15(@BBB8)
for s being State of SCM+FSA, l1,l2 being Instruction-Location of SCM+FSA
holds s +* Start-At l1 +* Start-At l2 = s +* Start-At l2;
theorem :: SCMFSA8B:5 ::TI1 <> PRE8'82'
for s being State of SCM+FSA, I being Macro-Instruction holds
(Initialize s) | (Int-Locations \/ FinSeq-Locations) =
(s +* Initialized I) | (Int-Locations \/ FinSeq-Locations);
theorem :: SCMFSA8B:6 ::T8'
for s1,s2 being State of SCM+FSA, I being Macro-Instruction st
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations) holds
I is_closed_on s1 implies I is_closed_on s2;
theorem :: SCMFSA8B:7 ::TQ40'
for s1,s2 being State of SCM+FSA, I,J being Macro-Instruction holds
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations) implies
s1 +* (I +* Start-At insloc 0),s2 +* (J +* Start-At insloc 0)
equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCMFSA8B:8 ::TQ38' <> T8'
for s1,s2 being State of SCM+FSA, I being Macro-Instruction
st s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations) holds
I is_closed_on s1 & I is_halting_on s1 implies
I is_closed_on s2 & I is_halting_on s2;
theorem :: SCMFSA8B:9 ::T61''
for s being State of SCM+FSA, I,J being Macro-Instruction holds
I is_closed_on Initialize s iff I is_closed_on s +* Initialized J;
theorem :: SCMFSA8B:10 ::TI11 <> T61
for s being State of SCM+FSA, I,J being Macro-Instruction,
l being Instruction-Location of SCM+FSA holds
I is_closed_on s iff I is_closed_on s +* (I +* Start-At l);
theorem :: SCMFSA8B:11 ::PRE8'115'(@AAAA)
for s1,s2 being State of SCM+FSA, I being Macro-Instruction
st I +* Start-At insloc 0 c= s1 & I is_closed_on s1
for n being Nat st ProgramPart Relocated(I,n) c= s2 &
IC s2 = insloc n &
s1 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations)
for i being Nat holds
IC (Computation s1).i + n = IC (Computation s2).i &
IncAddr(CurInstr ((Computation s1).i),n) = CurInstr ((Computation s2).i) &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations)
= (Computation s2).i | (Int-Locations \/ FinSeq-Locations);
theorem :: SCMFSA8B:12 ::TG25
for s being State of SCM+FSA,
i being keeping_0 parahalting Instruction of SCM+FSA,
J being parahalting Macro-Instruction, a being Int-Location
holds IExec(i ';' J,s).a = IExec(J,Exec(i,Initialize s)).a;
theorem :: SCMFSA8B:13 ::TG26
for s being State of SCM+FSA,
i being keeping_0 parahalting Instruction of SCM+FSA,
J being parahalting Macro-Instruction, f being FinSeq-Location
holds IExec(i ';' J,s).f = IExec(J,Exec(i,Initialize s)).f;
definition
let a be Int-Location;
let I,J be Macro-Instruction;
func if=0(a,I,J) -> Macro-Instruction equals
:: SCMFSA8B:def 1
::Di2
a =0_goto insloc (card J + 3) ';' J ';' Goto insloc (card I + 1) ';'
I ';' SCM+FSA-Stop;
func if>0(a,I,J) -> Macro-Instruction equals
:: SCMFSA8B:def 2
::Di3
a >0_goto insloc (card J + 3) ';' J ';' Goto insloc (card I + 1) ';'
I ';' SCM+FSA-Stop;
end;
definition
let a be Int-Location;
let I,J be Macro-Instruction;
func if<0(a,I,J) -> Macro-Instruction equals
:: SCMFSA8B:def 3
::Di4
if=0(a,J,if>0(a,J,I));
end;
theorem :: SCMFSA8B:14 ::T17
for I,J being Macro-Instruction, a being Int-Location holds
card if=0(a,I,J) = card I + card J + 4;
theorem :: SCMFSA8B:15 ::T18
for I,J being Macro-Instruction, a being Int-Location holds
card if>0(a,I,J) = card I + card J + 4;
theorem :: SCMFSA8B:16 ::ThIF0_1'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & I is_closed_on s & I is_halting_on s holds
if=0(a,I,J) is_closed_on s & if=0(a,I,J) is_halting_on s;
theorem :: SCMFSA8B:17 ::ThIF0_1(@BBB8)
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec(if=0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3)
;
theorem :: SCMFSA8B:18 ::ThIF0_2'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a <> 0 & J is_closed_on s & J is_halting_on s holds
if=0(a,I,J) is_closed_on s & if=0(a,I,J) is_halting_on s;
theorem :: SCMFSA8B:19 ::ThIF0_2(@BBB8)
for I,J being Macro-Instruction, a being read-write Int-Location holds
for s being State of SCM+FSA
st s.a <> 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec(if=0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3)
;
theorem :: SCMFSA8B:20 ::ThIF0(@BBB8)
for s being State of SCM+FSA, I,J being parahalting Macro-Instruction,
a being read-write Int-Location holds
if=0(a,I,J) is parahalting &
(s.a = 0 implies IExec(if=0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + 3)) &
(s.a <> 0 implies IExec(if=0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + 3));
theorem :: SCMFSA8B:21 ::ThIF0'
for s being State of SCM+FSA, I,J being parahalting Macro-Instruction,
a being read-write Int-Location holds
IC IExec(if=0(a,I,J),s) = insloc (card I + card J + 3) &
(s.a = 0 implies
((for d being Int-Location holds
IExec(if=0(a,I,J),s).d = IExec(I,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,I,J),s).f = IExec(I,s).f)) &
(s.a <> 0 implies
((for d being Int-Location holds
IExec(if=0(a,I,J),s).d = IExec(J,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,I,J),s).f = IExec(J,s).f));
theorem :: SCMFSA8B:22 ::ThIFg0_1'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a > 0 & I is_closed_on s & I is_halting_on s holds
if>0(a,I,J) is_closed_on s & if>0(a,I,J) is_halting_on s;
theorem :: SCMFSA8B:23 ::ThIFg0_1(@BBB8)
for I,J being Macro-Instruction, a being read-write Int-Location holds
for s being State of SCM+FSA
st s.a > 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec(if>0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3)
;
theorem :: SCMFSA8B:24 ::ThIFg0_2'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a <= 0 & J is_closed_on s & J is_halting_on s holds
if>0(a,I,J) is_closed_on s & if>0(a,I,J) is_halting_on s;
theorem :: SCMFSA8B:25 ::ThIFg0_2(@BBB8)
for I,J being Macro-Instruction, a being read-write Int-Location holds
for s being State of SCM+FSA
st s.a <= 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec(if>0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3)
;
theorem :: SCMFSA8B:26 ::ThIFg0(@BBB8)
for s being State of SCM+FSA, I,J being parahalting Macro-Instruction,
a being read-write Int-Location holds
if>0(a,I,J) is parahalting &
(s.a > 0 implies IExec(if>0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + 3)) &
(s.a <= 0 implies IExec(if>0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + 3));
theorem :: SCMFSA8B:27 ::ThIFg0'
for s being State of SCM+FSA, I,J being parahalting Macro-Instruction,
a being read-write Int-Location holds
IC IExec(if>0(a,I,J),s) = insloc (card I + card J + 3) &
(s.a > 0 implies
((for d being Int-Location holds
IExec(if>0(a,I,J),s).d = IExec(I,s).d) &
for f being FinSeq-Location holds
IExec(if>0(a,I,J),s).f = IExec(I,s).f)) &
(s.a <= 0 implies
((for d being Int-Location holds
IExec(if>0(a,I,J),s).d = IExec(J,s).d) &
for f being FinSeq-Location holds
IExec(if>0(a,I,J),s).f = IExec(J,s).f));
theorem :: SCMFSA8B:28 ::ThIFl0_1' -- ???
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a < 0 & I is_closed_on s & I is_halting_on s holds
if<0(a,I,J) is_closed_on s & if<0(a,I,J) is_halting_on s;
theorem :: SCMFSA8B:29 ::ThIFl0_1(@BBB8)
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a < 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec(if<0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + card J + 7);
theorem :: SCMFSA8B:30 ::ThIFl0_2' --- ??
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & J is_closed_on s & J is_halting_on s holds
if<0(a,I,J) is_closed_on s & if<0(a,I,J) is_halting_on s;
theorem :: SCMFSA8B:31 ::ThIFl0_2(@BBB8)
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec(if<0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + card J + 7);
theorem :: SCMFSA8B:32 ::ThIFl0_3' --- ???
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a > 0 & J is_closed_on s & J is_halting_on s holds
if<0(a,I,J) is_closed_on s & if<0(a,I,J) is_halting_on s;
theorem :: SCMFSA8B:33 ::ThIFl0_3(@BBB8)
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a > 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec(if<0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + card J + 7);
theorem :: SCMFSA8B:34 ::ThIFl0(@BBB8)
for s being State of SCM+FSA, I,J being parahalting Macro-Instruction,
a being read-write Int-Location holds
(if<0(a,I,J) is parahalting &
(s.a < 0 implies IExec(if<0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + card J + 7)) &
(s.a >= 0 implies IExec(if<0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + card J + 7)));
definition
let I,J be parahalting Macro-Instruction;
let a be read-write Int-Location;
cluster if=0(a,I,J) -> parahalting;
cluster if>0(a,I,J) -> parahalting;
end;
definition
let a,b be Int-Location;
let I,J be Macro-Instruction;
func if=0(a,b,I,J) -> Macro-Instruction equals
:: SCMFSA8B:def 4
SubFrom(a,b) ';' if=0(a,I,J);
func if>0(a,b,I,J) -> Macro-Instruction equals
:: SCMFSA8B:def 5
SubFrom(a,b) ';' if>0(a,I,J);
synonym if<0(b,a,I,J);
end;
definition
let I,J be parahalting Macro-Instruction;
let a,b be read-write Int-Location;
cluster if=0(a,b,I,J) -> parahalting;
cluster if>0(a,b,I,J) -> parahalting;
end;
theorem :: SCMFSA8B:35 ::PRE8'90'(@AAAA)
for s being State of SCM+FSA, I being Macro-Instruction holds
(Result (s +* Initialized I)) | (Int-Locations \/ FinSeq-Locations) =
IExec(I,s) | (Int-Locations \/ FinSeq-Locations);
theorem :: SCMFSA8B:36 ::PRE8'91(@AAAA)
for s being State of SCM+FSA, I being Macro-Instruction,
a being Int-Location holds
Result (s +* Initialized I),IExec(I,s) equal_outside
the Instruction-Locations of SCM+FSA;
theorem :: SCMFSA8B:37 ::T81'
for s1,s2 being State of SCM+FSA, i being Instruction of SCM+FSA,
a being Int-Location holds
(for b being Int-Location st a <> b holds s1.b = s2.b) &
(for f being FinSeq-Location holds s1.f = s2.f) &
i does_not_refer a & IC s1 = IC s2 implies
(for b being Int-Location st a <> b holds Exec(i,s1).b = Exec(i,s2).b) &
(for f being FinSeq-Location holds Exec(i,s1).f = Exec(i,s2).f) &
IC Exec(i,s1) = IC Exec(i,s2);
theorem :: SCMFSA8B:38 ::TT11 <> AAAA'01
for s1,s2 being State of SCM+FSA, I being Macro-Instruction,
a being Int-Location
st I does_not_refer a &
(for b being Int-Location st a <> b holds s1.b = s2.b) &
(for f being FinSeq-Location holds s1.f = s2.f) &
I is_closed_on s1 & I is_halting_on s1 holds
for k being Nat holds
(for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* Start-At insloc 0))).k.b =
(Computation (s2 +* (I +* Start-At insloc 0))).k.b) &
(for f being FinSeq-Location holds
(Computation (s1 +* (I +* Start-At insloc 0))).k.f =
(Computation (s2 +* (I +* Start-At insloc 0))).k.f) &
IC (Computation (s1 +* (I +* Start-At insloc 0))).k =
IC (Computation (s2 +* (I +* Start-At insloc 0))).k &
CurInstr (Computation (s1 +* (I +* Start-At insloc 0))).k =
CurInstr (Computation (s2 +* (I +* Start-At insloc 0))).k;
theorem :: SCMFSA8B:39 ::TI11'
for s being State of SCM+FSA, I,J being Macro-Instruction,
l being Instruction-Location of SCM+FSA holds
I is_closed_on s & I is_halting_on s
iff I is_closed_on s +* (I +* Start-At l) &
I is_halting_on s +* (I +* Start-At l);
theorem :: SCMFSA8B:40 ::TT10 <> PRE8'79
for s1,s2 being State of SCM+FSA, I being Macro-Instruction,
a being Int-Location
st I does_not_refer a &
(for b being Int-Location st a <> b holds s1.b = s2.b) &
(for f being FinSeq-Location holds s1.f = s2.f) &
I is_closed_on s1 & I is_halting_on s1 holds
I is_closed_on s2 & I is_halting_on s2;
theorem :: SCMFSA8B:41 ::TT12 <> AAAA'86
for s1,s2 being State of SCM+FSA, I being Macro-Instruction,
a being Int-Location holds
(for d being read-write Int-Location st a <> d holds s1.d = s2.d) &
(for f being FinSeq-Location holds s1.f = s2.f) &
I does_not_refer a &
I is_closed_on Initialize s1 & I is_halting_on Initialize s1
implies
(for d being Int-Location st a <> d holds IExec(I,s1).d = IExec(I,s2).d) &
(for f being FinSeq-Location holds IExec(I,s1).f = IExec(I,s2).f) &
IC IExec(I,s1) = IC IExec(I,s2);
theorem :: SCMFSA8B:42 ::ThIFab0
for s being State of SCM+FSA,
I,J being parahalting Macro-Instruction, a,b being read-write Int-Location
st I does_not_refer a & J does_not_refer a holds
IC IExec(if=0(a,b,I,J),s) = insloc (card I + card J + 5) &
(s.a = s.b implies
((for d being Int-Location st a <> d holds
IExec(if=0(a,b,I,J),s).d = IExec(I,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,b,I,J),s).f = IExec(I,s).f)) &
(s.a <> s.b implies
((for d being Int-Location st a <> d holds
IExec(if=0(a,b,I,J),s).d = IExec(J,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,b,I,J),s).f = IExec(J,s).f));
theorem :: SCMFSA8B:43 ::ThIFabg0
for s being State of SCM+FSA,
I,J being parahalting Macro-Instruction, a,b being read-write Int-Location
st I does_not_refer a & J does_not_refer a holds
IC IExec(if>0(a,b,I,J),s) = insloc (card I + card J + 5) &
(s.a > s.b implies
(for d being Int-Location st a <> d holds
IExec(if>0(a,b,I,J),s).d = IExec(I,s).d) &
for f being FinSeq-Location holds
IExec(if>0(a,b,I,J),s).f = IExec(I,s).f) &
(s.a <= s.b implies
(for d being Int-Location st a <> d holds
IExec(if>0(a,b,I,J),s).d = IExec(J,s).d) &
for f being FinSeq-Location holds
IExec(if>0(a,b,I,J),s).f = IExec(J,s).f);
Back to top