:: Some Multi-instructions defined by sequence of instructions of SCM+FSA
:: by Noriko Asamoto
::
:: Received April 24, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users


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 H1( Nat) -> Element of NAT = $1 -' 1;

definition
let a be Int-Location;
let k be Integer;
func a := k -> NAT -defined the InstructionsF of SCM+FSA -valued finite Function means :Def1: :: SCMFSA_7:def 1
 ex k1 being Nat st
( k1 + 1 = k & it = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) if k > 0
otherwise ex k1 being Nat st
( k1 + k = 1 & it = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) );
existence
( ( k > 0 implies ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + 1 = k & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) & ( not k > 0 implies ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) )
proof end;
uniqueness
for b1, b2 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds
( ( k > 0 & ex k1 being Nat st
( k1 + 1 = k & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) & ex k1 being Nat st
( k1 + 1 = k & b2 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) implies b1 = b2 ) & ( not k > 0 & ex k1 being Nat st
( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) & ex k1 being Nat st
( k1 + k = 1 & b2 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop 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 Nat st
( k1 + 1 = k & b3 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) ) & ( not k > 0 implies ( b3 = a := k iff ex k1 being Nat st
( k1 + k = 1 & b3 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) ) );

definition
let a be Int-Location;
let k be Integer;
func aSeq (a,k) -> XFinSequence of the InstructionsF of SCM+FSA means :Def2: :: SCMFSA_7:def 2
 ex k1 being Nat st
( k1 + 1 = k & it = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) if k > 0
otherwise ex k1 being Nat st
( k1 + k = 1 & it = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) );
existence
( ( k > 0 implies ex b1 being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + 1 = k & b1 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) & ( not k > 0 implies ex b1 being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) )
proof end;
uniqueness
for b1, b2 being XFinSequence of the InstructionsF of SCM+FSA holds
( ( k > 0 & ex k1 being Nat st
( k1 + 1 = k & b1 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) & ex k1 being Nat st
( k1 + 1 = k & b2 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) implies b1 = b2 ) & ( not k > 0 & ex k1 being Nat st
( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) & ex k1 being Nat st
( k1 + k = 1 & b2 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) implies b1 = b2 ) ) ;
correctness
consistency
for b1 being XFinSequence of the InstructionsF of SCM+FSA 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 the InstructionsF of SCM+FSA holds
( ( k > 0 implies ( b3 = aSeq (a,k) iff ex k1 being 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 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)) ^ (Stop SCM+FSA)
proof end;

definition
let f be FinSeq-Location ;
let p be FinSequence of INT ;
func aSeq (f,p) -> XFinSequence of the InstructionsF of SCM+FSA means :Def3: :: SCMFSA_7:def 3
 ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being 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 the InstructionsF of SCM+FSA ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being 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 )
proof end;
uniqueness
for b1, b2 being XFinSequence of the InstructionsF of SCM+FSA st ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being 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 the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being 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
proof end;
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 the InstructionsF of SCM+FSA holds
( b3 = aSeq (f,p) iff ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being 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 ;
func f := 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))) ^ (Stop SCM+FSA);
correctness
coherence
(((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ (Stop 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))) ^ (Stop SCM+FSA);

theorem :: SCMFSA_7:2
for a being Int-Location holds a := 1 = <%(a := (intloc 0))%> ^ (Stop SCM+FSA)
proof end;

theorem :: SCMFSA_7:3
for a being Int-Location holds a := 0 = (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ (Stop SCM+FSA)
proof end;

theorem Th4: :: SCMFSA_7:4
for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT
for c0 being 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 Nat st c in dom (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
( ( for i being 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 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 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;

:: 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 ) )
proof end;

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 ) )
proof end;