:: Some Multi-instructions defined by sequence of instructions of SCM+FSA
:: by Noriko Asamoto
::
:: Received April 24, 1996
:: Copyright (c) 1996-2011 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 )

proof end;

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) )

proof end;

deffunc H₁( Element of NAT ) -> Element of NAT = $1 -' 1;

definition

canceled;
let a be Int-Location ;
let k be Integer;
func a := k -> FinPartState of SCM+FSA 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))))) ^ <%(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 b₁ being FinPartState of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) & ( not k > 0 implies ex b₁ being FinPartState of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) )

proof end;

uniqueness
for b₁, b₂ being FinPartState of SCM+FSA holds
( ( k > 0 & ex k1 being Element of NAT st
( k1 + 1 = k & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) & ex k1 being Element of NAT st
( k1 + 1 = k & b₂ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) implies b₁ = b₂ ) & ( not k > 0 & ex k1 being Element of NAT st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) & ex k1 being Element of NAT st
( k1 + k = 1 & b₂ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) implies b₁ = b₂ ) ) ;
correctness
consistency
for b₁ being FinPartState of SCM+FSA holds verum;
;

end;

:: deftheorem SCMFSA_7:def 1 :
canceled;

:: deftheorem Def2 defines := SCMFSA_7:def 2 :
for a being Int-Location
for k being Integer
for b₃ being FinPartState of SCM+FSA holds
( ( k > 0 implies ( b₃ = a := k iff ex k1 being Element of NAT st
( k1 + 1 = k & b₃ = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ) & ( not k > 0 implies ( b₃ = a := k iff ex k1 being Element of NAT st
( k1 + k = 1 & b₃ = (<%(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 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 b₁ being XFinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) & ( not k > 0 implies ex b₁ being XFinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of the Instructions of SCM+FSA holds
( ( k > 0 & ex k1 being Element of NAT st
( k1 + 1 = k & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) & ex k1 being Element of NAT st
( k1 + 1 = k & b₂ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) implies b₁ = b₂ ) & ( not k > 0 & ex k1 being Element of NAT st
( k1 + k = 1 & b₁ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) & ex k1 being Element of NAT st
( k1 + k = 1 & b₂ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) implies b₁ = b₂ ) ) ;
correctness
consistency
for b₁ being XFinSequence of the Instructions of SCM+FSA holds verum;
;

end;

:: deftheorem Def3 defines aSeq SCMFSA_7:def 3 :
for a being Int-Location
for k being Integer
for b₃ being XFinSequence of the Instructions of SCM+FSA holds
( ( k > 0 implies ( b₃ = aSeq (a,k) iff ex k1 being Element of NAT st
( k1 + 1 = k & b₃ = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) ) & ( not k > 0 implies ( b₃ = aSeq (a,k) iff ex k1 being Element of NAT st
( k1 + k = 1 & b₃ = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) ) );

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

canceled;

theorem :: SCMFSA_7:26

canceled;

theorem :: SCMFSA_7:27

canceled;

theorem :: SCMFSA_7:28

canceled;

theorem :: SCMFSA_7:29

canceled;

theorem :: SCMFSA_7:30

canceled;

theorem :: SCMFSA_7:31

canceled;

theorem :: SCMFSA_7:32

canceled;

theorem :: SCMFSA_7:33

for a being Int-Location
for k being Integer holds a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%>

proof end;

definition

let f be FinSeq-Location ;
let p be FinSequence of INT ;
func aSeq (f,p) -> XFinSequence of the Instructions of SCM+FSA means :Def4: :: SCMFSA_7:def 4
ex pp being XFinSequence of the Instructions of SCM+FSA ^omega 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 b₁ being XFinSequence of the Instructions of SCM+FSA ex pp being XFinSequence of the Instructions of SCM+FSA ^omega 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))%> ) ) & b₁ = FlattenSeq pp )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of the Instructions of SCM+FSA st ex pp being XFinSequence of the Instructions of SCM+FSA ^omega 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))%> ) ) & b₁ = FlattenSeq pp ) & ex pp being XFinSequence of the Instructions of SCM+FSA ^omega 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))%> ) ) & b₂ = FlattenSeq pp ) holds
b₁ = b₂

proof end;

correctness
;

end;

:: deftheorem Def4 defines aSeq SCMFSA_7:def 4 :
for f being FinSeq-Location
for p being FinSequence of INT
for b₃ being XFinSequence of the Instructions of SCM+FSA holds
( b₃ = aSeq (f,p) iff ex pp being XFinSequence of the Instructions of SCM+FSA ^omega 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))%> ) ) & b₃ = FlattenSeq pp ) );

definition

let f be FinSeq-Location ;
let p be FinSequence of INT ;
func f := p -> FinPartState of SCM+FSA equals :: SCMFSA_7:def 5
(((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 FinPartState of SCM+FSA;
;

end;

:: deftheorem defines := SCMFSA_7:def 5 :
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:34

for a being Int-Location holds a := 1 = <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%>

proof end;

theorem :: SCMFSA_7:35

for a being Int-Location holds a := 0 = (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ <%(halt SCM+FSA)%>

proof end;

theorem Th36: :: SCMFSA_7:36

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for c0 being Element of NAT
for s being b₂ -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 )

proof end;

theorem Th37: :: SCMFSA_7:37

for P being the Instructions 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 )

proof end;

theorem :: SCMFSA_7:38

for P being the Instructions 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 ) )

proof end;

theorem :: SCMFSA_7:39

for P being the Instructions 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 ) )

proof end;