:: Some Multi-instructions defined by sequence of instructions of SCM+FSA :: by Noriko Asamoto :: :: Received April 24, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin Lm1: for p1, p2, p3, p4 being XFinSequence holds ( ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ p2) ^ (p3 ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 ) proofend; Lm2: for p1, p2, p3, p4, p5 being XFinSequence holds ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) proofend; deffunc H1( Element of NAT ) -> Element of NAT = $1 -' 1; definition let a be Int-Location; let k be Integer; funca := k -> NAT -defined the InstructionsF of SCM+FSA -valued finite Function means :Def1: :: SCMFSA_7:def 1 ex k1 being Element of NAT st ( k1 + 1 = k & it = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) if k > 0 otherwise ex k1 being Element of NAT st ( k1 + k = 1 & it = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ); existence ( ( k > 0 implies ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + 1 = k & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) & ( not k > 0 implies ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ) proofend; uniqueness for b1, b2 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds ( ( k > 0 & ex k1 being Element of NAT st ( k1 + 1 = k & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) & ex k1 being Element of NAT st ( k1 + 1 = k & b2 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) implies b1 = b2 ) & ( not k > 0 & ex k1 being Element of NAT st ( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) & ex k1 being Element of NAT st ( k1 + k = 1 & b2 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) implies b1 = b2 ) ) ; correctness consistency for b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds verum; ; end; :: deftheorem Def1 defines := SCMFSA_7:def_1_:_ for a being Int-Location for k being Integer for b3 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds ( ( k > 0 implies ( b3 = a := k iff ex k1 being Element of NAT st ( k1 + 1 = k & b3 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ) & ( not k > 0 implies ( b3 = a := k iff ex k1 being Element of NAT st ( k1 + k = 1 & b3 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ) ); definition let a be Int-Location; let k be Integer; func aSeq (a,k) -> XFinSequence of means :Def2: :: SCMFSA_7:def 2 ex k1 being Element of NAT st ( k1 + 1 = k & it = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) if k > 0 otherwise ex k1 being Element of NAT st ( k1 + k = 1 & it = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ); existence ( ( k > 0 implies ex b1 being XFinSequence of ex k1 being Element of NAT st ( k1 + 1 = k & b1 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) & ( not k > 0 implies ex b1 being XFinSequence of ex k1 being Element of NAT st ( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) ) proofend; uniqueness for b1, b2 being XFinSequence of holds ( ( k > 0 & ex k1 being Element of NAT st ( k1 + 1 = k & b1 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) & ex k1 being Element of NAT st ( k1 + 1 = k & b2 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) implies b1 = b2 ) & ( not k > 0 & ex k1 being Element of NAT st ( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) & ex k1 being Element of NAT st ( k1 + k = 1 & b2 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) implies b1 = b2 ) ) ; correctness consistency for b1 being XFinSequence of holds verum; ; end; :: deftheorem Def2 defines aSeq SCMFSA_7:def_2_:_ for a being Int-Location for k being Integer for b3 being XFinSequence of holds ( ( k > 0 implies ( b3 = aSeq (a,k) iff ex k1 being Element of NAT st ( k1 + 1 = k & b3 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) ) & ( not k > 0 implies ( b3 = aSeq (a,k) iff ex k1 being Element of NAT st ( k1 + k = 1 & b3 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) ) ); theorem :: SCMFSA_7:1 for a being Int-Location for k being Integer holds a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> proofend; definition let f be FinSeq-Location ; let p be FinSequence of INT ; func aSeq (f,p) -> XFinSequence of means :Def3: :: SCMFSA_7:def 3 ex pp being XFinSequence of st ( len pp = len p & ( for k being Element of NAT st k < len pp holds ex i being Integer st ( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & it = FlattenSeq pp ); existence ex b1 being XFinSequence of ex pp being XFinSequence of st ( len pp = len p & ( for k being Element of NAT st k < len pp holds ex i being Integer st ( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b1 = FlattenSeq pp ) proofend; uniqueness for b1, b2 being XFinSequence of st ex pp being XFinSequence of st ( len pp = len p & ( for k being Element of NAT st k < len pp holds ex i being Integer st ( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b1 = FlattenSeq pp ) & ex pp being XFinSequence of st ( len pp = len p & ( for k being Element of NAT st k < len pp holds ex i being Integer st ( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b2 = FlattenSeq pp ) holds b1 = b2 proofend; correctness ; end; :: deftheorem Def3 defines aSeq SCMFSA_7:def_3_:_ for f being FinSeq-Location for p being FinSequence of INT for b3 being XFinSequence of holds ( b3 = aSeq (f,p) iff ex pp being XFinSequence of st ( len pp = len p & ( for k being Element of NAT st k < len pp holds ex i being Integer st ( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & b3 = FlattenSeq pp ) ); definition let f be FinSeq-Location ; let p be FinSequence of INT ; funcf := p -> NAT -defined the InstructionsF of SCM+FSA -valued finite Function equals :: SCMFSA_7:def 4 (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>; correctness coherence (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> is NAT -defined the InstructionsF of SCM+FSA -valued finite Function; ; end; :: deftheorem defines := SCMFSA_7:def_4_:_ for f being FinSeq-Location for p being FinSequence of INT holds f := p = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>; theorem :: SCMFSA_7:2 for a being Int-Location holds a := 1 = <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%> proofend; theorem :: SCMFSA_7:3 for a being Int-Location holds a := 0 = (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ <%(halt SCM+FSA)%> proofend; theorem Th4: :: SCMFSA_7:4 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for c0 being Element of NAT for s being b2 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ) holds ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = c0 + i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) proofend; theorem Th5: :: SCMFSA_7:5 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) proofend; :: Users' guide theorem :: SCMFSA_7:6 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st a := k c= P & a <> intloc 0 holds ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) proofend; theorem :: SCMFSA_7:7 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) proofend;