:: Conditional branch macro instructions of SCM+FSA, Part II :: by Noriko Asamoto :: :: Received August 27, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SCMFSA_2, AMI_1, AMISTD_2, CARD_1, TARSKI, SCMFSA6A, FUNCT_4, FSM_1, RELAT_1, CIRCUIT2, FUNCT_1, SF_MASTR, SUBSET_1, ARYTM_3, SCMFSA7B, SCMFSA6B, SCMFSA6C, AMI_3, SCMFSA8A, NAT_1, GRAPHSP, XXREAL_0, MSUALG_1, STRUCT_0, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, SCMFSA8B, EXTPRO_1, RELOC, FUNCOP_1, COMPOS_1, AMISTD_1, FRECHET; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, CARD_3, VALUED_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_4, PBOOLE, FUNCT_7, FINSEQ_1, FINSEQ_2, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, INT_2, SCMFSA_M; constructors DOMAIN_1, XXREAL_0, NAT_1, INT_2, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, AMISTD_2, RELSET_1, SCMFSA7B, PRE_POLY, AMISTD_1, PBOOLE, FUNCOP_1, FUNCT_4, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X, NAT_D, AMI_3, COMPOS_2; registrations XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6B, SCMFSA6C, ORDINAL1, MEMSTR_0, RELSET_1, SCMFSA10, AMISTD_2, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, STRUCT_0, COMPOS_0, SCMFSA_M, SCMFSA6A, CARD_1; requirements NUMERALS, REAL, SUBSET, ARITHM; begin reserve P,P1,P2 for Instruction-Sequence of SCM+FSA; ::$CT 4 theorem :: SCMFSA8B:5 for s1,s2 being State of SCM+FSA, I being really-closed Program of SCM+FSA st DataPart s1 = DataPart s2 holds :::I is_closed_on s1,P1 & I is_halting_on s1,P1 implies ::: I is_closed_on s2,P2 & I is_halting_on s2,P2; :: theorem Th5: :: for s being State of SCM+FSA, I,J being Program of SCM+FSA holds :: I is_closed_on Initialized s,P iff :: I is_closed_on s +* Initialize((intloc 0).-->1),P+*J :: proof :: let s be State of SCM+FSA; :: let I,J be Program of SCM+FSA; :: DataPart Initialized s = DataPart(s +* Initialize((intloc 0).-->1)); :: hence thesis by Th2; :: end; :: theorem Th6: :: for s being State of SCM+FSA, I,J being Program of SCM+FSA, l :: being Element of NAT holds I is_closed_on s,P iff I is_closed_on :: s +* (Start-At(0,SCM+FSA)),P+*I :: proof :: let s be State of SCM+FSA; :: let I,J be Program of SCM+FSA; :: let l be Element of NAT; :: DataPart s = DataPart(Initialize s) by MEMSTR_0:79; :: hence thesis by Th2; :: end; ::$CT 2 theorem :: SCMFSA8B:8 for s1 being 0-started State of SCM+FSA, s2 being State of SCM+FSA, I being really-closed Program of SCM+FSA st :::I is_closed_on s1,P1 & I c= P1 for n being Nat st IC s2 = n & DataPart s1 = DataPart s2 & Reloc(I,n) c= P2 for i being Nat holds IC Comput(P1, s1,i) + n = IC Comput(P2, s2,i) & IncAddr(CurInstr(P1,Comput( P1,s1,i)),n) = CurInstr(P2,Comput(P2,s2,i)) & DataPart Comput(P1, s1,i) = DataPart Comput(P2,s2,i); theorem :: SCMFSA8B:9 for s being State of SCM+FSA, i being keeping_0 sequential Instruction of SCM+FSA, J being parahalting really-closed Program of SCM+FSA, a being Int-Location holds IExec(i ";" J,P,s).a = IExec(J,P,Exec(i,Initialized s)).a; theorem :: SCMFSA8B:10 for s being State of SCM+FSA, i being keeping_0 sequential Instruction of SCM+FSA, J being parahalting really-closed Program of SCM+FSA, f being FinSeq-Location holds IExec(i ";" J,P,s).f = IExec(J,P,Exec(i,Initialized s)).f; definition let a be Int-Location; let I,J be MacroInstruction of SCM+FSA; func if=0(a,I,J) -> Program of SCM+FSA equals :: SCMFSA8B:def 1 a =0_goto (card J + 3) ";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA; func if>0(a,I,J) -> Program of SCM+FSA equals :: SCMFSA8B:def 2 a >0_goto (card J + 3) ";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA; end; :: definition :: let a be Int-Location; :: let I,J be Program of SCM+FSA; :: func if<0(a,I,J) -> Program of SCM+FSA equals :: if=0(a,J,if>0(a,J,I)); :: coherence; :: end; :: definicjas w tym sensie jest niepoporawna, ze powtarza instrukcje J ::$CD theorem :: SCMFSA8B:11 for I,J being MacroInstruction of SCM+FSA, a being Int-Location holds card if=0(a,I,J) = card I + card J + 4; theorem :: SCMFSA8B:12 for I,J being MacroInstruction of SCM+FSA, a being Int-Location holds card if>0(a,I,J) = card I + card J + 4; theorem :: SCMFSA8B:13 for s being State of SCM+FSA, I being really-closed MacroInstruction of SCM+FSA, J being MacroInstruction of SCM+FSA, a being read-write Int-Location st s.a = 0 & :::I is_closed_on s,P & I is_halting_on s,P holds :::if=0(a,I,J) is_closed_on s,P & if=0(a,I,J) is_halting_on s,P; theorem :: SCMFSA8B:14 for s being State of SCM+FSA, I being really-closed MacroInstruction of SCM+FSA, J being MacroInstruction of SCM+FSA, a being read-write Int-Location st s.a = 0 ::: & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds IExec(if=0(a,I,J),P,s) = IExec(I,P,s) +* Start-At((card I + card J + 3),SCM+FSA); registration let I,J be really-closed MacroInstruction of SCM+FSA, a be Int-Location; cluster if=0(a,I,J) -> really-closed; cluster if>0(a,I,J) -> really-closed; end; theorem :: SCMFSA8B:15 for s being State of SCM+FSA, ::: I being Program of SCM+FSA, I,J being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location st s.a <> 0 & :::J is_closed_on s,P & J is_halting_on s,P holds :::if=0(a,I,J) is_closed_on s,P & if=0(a,I,J) is_halting_on s,P; theorem :: SCMFSA8B:16 for I,J being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location holds for s being State of SCM+FSA st s.a <> 0 & ::: J is_closed_on Initialized s,P & J is_halting_on Initialized s,P holds IExec(if=0(a,I,J),P,s) = IExec(J,P,s) +* Start-At((card I+card J+3),SCM+FSA); theorem :: SCMFSA8B:17 for s being State of SCM+FSA, I,J being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location holds if=0(a,I,J) is parahalting & (s.a = 0 implies IExec(if=0(a,I,J),P,s) = IExec(I,P,s) +* Start-At( (card I + card J + 3),SCM+FSA)) & (s.a <> 0 implies IExec(if=0(a,I,J),P,s) = IExec(J,P,s) +* Start-At((card I + card J + 3),SCM+FSA)); theorem :: SCMFSA8B:18 for s being State of SCM+FSA, I,J being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location holds IC IExec(if=0(a,I,J),P,s) = (card I + card J + 3) & (s.a = 0 implies ((for d being Int-Location holds IExec(if=0(a,I,J),P,s).d = IExec(I,P,s).d) & for f being FinSeq-Location holds IExec(if=0(a,I,J),P,s).f = IExec(I,P,s).f)) & (s.a <> 0 implies ((for d being Int-Location holds IExec(if=0(a,I,J),P,s).d = IExec(J,P,s).d) & for f being FinSeq-Location holds IExec(if=0(a,I,J),P,s).f = IExec(J,P,s).f)); theorem :: SCMFSA8B:19 for s being State of SCM+FSA, I,J being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location st s.a > 0 & ::: I is_closed_on s,P& I is_halting_on s,P holds :::if>0(a,I,J) is_closed_on s,P & if>0(a,I,J) is_halting_on s,P; theorem :: SCMFSA8B:20 for I,J being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location holds for s being State of SCM+FSA st s.a > 0 & ::: I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds IExec(if>0(a,I,J),P,s) = IExec(I,P,s) +* Start-At((card I+card J+3),SCM+FSA); theorem :: SCMFSA8B:21 for s being State of SCM+FSA, I,J being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location st s.a <= 0 & :::J is_closed_on s,P & J is_halting_on s,P holds :::if>0(a,I,J) is_closed_on s,P & if>0(a,I,J) is_halting_on s,P; theorem :: SCMFSA8B:22 for I,J being really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location holds for s being State of SCM+FSA st s.a <= 0 & ::: J is_closed_on Initialized s,P & J is_halting_on Initialized s,P holds IExec(if>0(a,I,J),P,s) = IExec(J,P,s) +* Start-At((card I+card J+3),SCM+FSA); theorem :: SCMFSA8B:23 for s being State of SCM+FSA, I,J being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location holds if>0(a,I,J) is parahalting & (s. a > 0 implies IExec(if>0(a,I,J),P,s) = IExec(I,P,s) +* Start-At( (card I + card J + 3),SCM+FSA)) & (s.a <= 0 implies IExec(if>0(a,I,J),P,s) = IExec(J,P,s) +* Start-At((card I + card J + 3),SCM+FSA)); theorem :: SCMFSA8B:24 for s being State of SCM+FSA, I,J being parahalting really-closed MacroInstruction of SCM+FSA, a being read-write Int-Location holds IC IExec(if>0(a,I,J),P,s) = (card I + card J + 3) & (s.a > 0 implies ((for d being Int-Location holds IExec(if>0(a,I,J),P,s).d = IExec(I,P,s).d) & for f being FinSeq-Location holds IExec(if>0(a,I,J),P,s).f = IExec(I,P,s).f)) & (s.a <= 0 implies ((for d being Int-Location holds IExec(if>0(a,I,J),P,s).d = IExec(J,P,s).d) & for f being FinSeq-Location holds IExec(if>0(a,I,J),P,s).f = IExec(J,P,s).f)); ::$CT 7 registration let I,J be parahalting really-closed MacroInstruction of SCM+FSA; 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 MacroInstruction of SCM+FSA; func if=0(a,b,I,J) -> Program of SCM+FSA equals :: SCMFSA8B:def 4 SubFrom(a,b) ";" if=0(a,I,J); func if>0(a,b,I,J) -> Program of SCM+FSA equals :: SCMFSA8B:def 5 SubFrom(a,b) ";" if>0(a,I,J); end; registration let a be Int-Location; let I,J be MacroInstruction of SCM+FSA; cluster if=0(a,I,J) -> halt-ending unique-halt; cluster if>0(a,I,J) -> halt-ending unique-halt; end; registration let a,b be Int-Location; let I,J be really-closed MacroInstruction of SCM+FSA; cluster if=0(a,b,I,J) -> really-closed; cluster if>0(a,b,I,J) -> really-closed; end; registration let a,b be Int-Location; let I,J be MacroInstruction of SCM+FSA; cluster if=0(a,b,I,J) -> halt-ending unique-halt; cluster if>0(a,b,I,J) -> halt-ending unique-halt; end; registration let I,J be parahalting really-closed MacroInstruction of SCM+FSA; 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; registration let I,J be really-closed MacroInstruction of SCM+FSA; let a,b be read-write Int-Location; cluster if=0(a,b,I,J) -> really-closed; cluster if>0(a,b,I,J) -> really-closed; end; theorem :: SCMFSA8B:32 for s being State of SCM+FSA, I being Program of SCM+FSA holds DataPart Result(P+*I,Initialized s) = DataPart IExec(I,P,s); theorem :: SCMFSA8B:33 for s being State of SCM+FSA, I being Program of SCM+FSA holds Result(P+*I,Initialized s) = IExec(I,P,s); theorem :: SCMFSA8B:34 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:35 for s1,s2 being State of SCM+FSA, I being really-closed Program of SCM+FSA, 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,P1 holds for k being Nat holds (for b being Int-Location st a <> b holds Comput(P1+*I,(Initialize s1),k).b = Comput(P2+*I, (Initialize s2),k).b) & (for f being FinSeq-Location holds Comput(P1+*I,(Initialize s1),k).f = Comput(P2+*I, (Initialize s2),k).f) & IC Comput(P1+*I, (Initialize s1),k) = IC Comput(P2+*I, (Initialize s2),k) & CurInstr(P1+*I,Comput(P1+*I, (Initialize s1),k)) = CurInstr(P2+*I,Comput(P2+*I, (Initialize s2),k)); theorem :: SCMFSA8B:36 for s being State of SCM+FSA, I being really-closed Program of SCM+FSA, l being Nat holds :::I is_closed_on s,P & I is_halting_on s,P iff :::I is_closed_on s +* Start-At(l,SCM+FSA),P+*I & I is_halting_on s +* Start-At(l,SCM+FSA),P+*I; theorem :: SCMFSA8B:37 for s1,s2 being State of SCM+FSA, I being really-closed Program of SCM+FSA, 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) & :::& Iis_closed_on s1,P1 & I is_halting_on s1,P1 holds :::I is_closed_on s2,P2 & I is_halting_on s2,P2; theorem :: SCMFSA8B:38 for s1,s2 being State of SCM+FSA, I being really-closed Program of SCM+FSA, 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 Initialized s1,P1 & I is_halting_on Initialized s1,P1 implies (for d being Int-Location st a <> d holds IExec(I,P1,s1).d = IExec(I,P2,s2).d) & (for f being FinSeq-Location holds IExec(I,P1,s1).f = IExec(I,P2,s2).f) & IC IExec(I,P1,s1) = IC IExec(I,P2,s2); theorem :: SCMFSA8B:39 for s being State of SCM+FSA, I,J being parahalting really-closed MacroInstruction of SCM+FSA, 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),P,s) = (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),P,s).d = IExec(I,P,s).d) & for f being FinSeq-Location holds IExec(if=0(a,b,I,J),P,s).f = IExec(I,P,s).f)) & (s.a <> s.b implies ((for d being Int-Location st a <> d holds IExec(if=0(a,b,I,J),P,s).d = IExec(J,P,s).d) & for f being FinSeq-Location holds IExec(if=0(a,b,I,J),P,s).f = IExec(J,P,s).f)); theorem :: SCMFSA8B:40 for s being State of SCM+FSA, I,J being parahalting really-closed MacroInstruction of SCM+FSA , 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),P,s) = (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),P,s).d = IExec(I,P,s).d) & for f being FinSeq-Location holds IExec(if>0(a,b,I,J),P,s).f = IExec(I,P,s).f) & (s.a <= s.b implies (for d being Int-Location st a <> d holds IExec(if>0(a,b,I,J),P,s).d = IExec(J,P,s).d) & for f being FinSeq-Location holds IExec(if>0(a,b,I,J),P,s).f = IExec(J,P,s).f); reserve s for State of SCM+FSA, I for Program of SCM+FSA, p for Instruction-Sequence of SCM+FSA; :: theorem :: s.intloc 0 = 1 implies (I is_closed_on s,p iff I is_closed_on :: Initialized s,p) :: proof :: assume s.intloc 0 = 1; :: then DataPart Initialized s = DataPart s by SCMFSA_M:19; :: hence thesis by Th2; :: end; ::$CT theorem :: SCMFSA8B:42 for I being really-closed Program of SCM+FSA st s.intloc 0 = 1 holds I is_halting_on s,p iff I is_halting_on Initialized s,p;