:: Some Multi-instructions defined by sequence of instructions of SCM+FSA
:: by Noriko Asamoto
::
:: Received April 24, 1996
:: Copyright (c) 1996 Association of Mizar Users
Lm1:
for p1, p2, p3 being FinSequence holds
( ((len p1) + (len p2)) + (len p3) = len ((p1 ^ p2) ^ p3) & ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )
Lm2:
for p1, p2, p3, p4 being FinSequence 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 )
Lm3:
for p1, p2, p3, p4, p5 being FinSequence 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) )
deffunc H1( Element of NAT ) -> Element of NAT = $1 -' 1;
:: deftheorem Def1 defines Load SCMFSA_7:def 1 :
theorem :: SCMFSA_7:1
canceled;
theorem :: SCMFSA_7:2
canceled;
theorem :: SCMFSA_7:3
canceled;
theorem :: SCMFSA_7:4
canceled;
theorem :: SCMFSA_7:5
canceled;
theorem :: SCMFSA_7:6
canceled;
theorem :: SCMFSA_7:7
canceled;
theorem :: SCMFSA_7:8
canceled;
theorem :: SCMFSA_7:9
canceled;
theorem :: SCMFSA_7:10
canceled;
theorem :: SCMFSA_7:11
canceled;
theorem :: SCMFSA_7:12
canceled;
theorem :: SCMFSA_7:13
canceled;
theorem :: SCMFSA_7:14
canceled;
theorem :: SCMFSA_7:15
canceled;
theorem :: SCMFSA_7:16
canceled;
theorem :: SCMFSA_7:17
canceled;
theorem :: SCMFSA_7:18
canceled;
theorem :: SCMFSA_7:19
canceled;
theorem :: SCMFSA_7:20
canceled;
theorem :: SCMFSA_7:21
canceled;
theorem :: SCMFSA_7:22
canceled;
theorem :: SCMFSA_7:23
canceled;
theorem :: SCMFSA_7:24
canceled;
theorem :: SCMFSA_7:25
theorem Th26: :: SCMFSA_7:26
theorem :: SCMFSA_7:27
canceled;
theorem :: SCMFSA_7:28
canceled;
theorem Th29: :: SCMFSA_7:29
theorem :: SCMFSA_7:30
theorem Th31: :: SCMFSA_7:31
theorem :: SCMFSA_7:32
:: deftheorem Def2 defines := SCMFSA_7:def 2 :
definition
let a be
Int-Location ;
let k be
Integer;
func aSeq a,
k -> FinSequence of the
Instructions of
SCM+FSA means :
Def3:
:: SCMFSA_7:def 3
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 FinSequence of the Instructions of SCM+FSA 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 FinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b1 = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) ) ) )
uniqueness
for b1, b2 being FinSequence of the Instructions of SCM+FSA 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 FinSequence of the Instructions of SCM+FSA holds verum;
;
end;
:: deftheorem Def3 defines aSeq SCMFSA_7:def 3 :
theorem :: SCMFSA_7:33
definition
let f be
FinSeq-Location ;
let p be
FinSequence of
INT ;
func aSeq f,
p -> FinSequence of the
Instructions of
SCM+FSA means :
Def4:
:: SCMFSA_7:def 4
ex
pp being
FinSequence of the
Instructions of
SCM+FSA * st
(
len pp = len p & ( for
k being
Element of
NAT st 1
<= k &
k <= len p holds
ex
i being
Integer st
(
i = p . k &
pp . k = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> ) ) &
it = FlattenSeq pp );
existence
ex b1 being FinSequence of the Instructions of SCM+FSA ex pp being FinSequence of the Instructions of SCM+FSA * st
( len pp = len p & ( for k being Element of NAT st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> ) ) & b1 = FlattenSeq pp )
uniqueness
for b1, b2 being FinSequence of the Instructions of SCM+FSA st ex pp being FinSequence of the Instructions of SCM+FSA * st
( len pp = len p & ( for k being Element of NAT st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> ) ) & b1 = FlattenSeq pp ) & ex pp being FinSequence of the Instructions of SCM+FSA * st
( len pp = len p & ( for k being Element of NAT st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> ) ) & b2 = FlattenSeq pp ) holds
b1 = b2
correctness
;
end;
:: deftheorem Def4 defines aSeq SCMFSA_7:def 4 :
:: deftheorem defines := SCMFSA_7:def 5 :
theorem :: SCMFSA_7:34
theorem :: SCMFSA_7:35
theorem Th36: :: SCMFSA_7:36
theorem Th37: :: SCMFSA_7:37
theorem :: SCMFSA_7:38
theorem :: SCMFSA_7:39