:: An Extension of { \bf SCM }
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Copyright (c) 1996-2019 Association of Mizar Users

notation end;

definition
::$CD coherence ; end; :: deftheorem SCMFSA_1:def 1 : canceled; :: deftheorem defines SCM+FSA-Memory SCMFSA_1:def 2 : registration coherence not SCM+FSA-Memory is empty ; end; theorem Th1: :: SCMFSA_1:1 definition :: original: SCM+FSA-Data-Loc redefine func SCM+FSA-Data-Loc -> Subset of SCM+FSA-Memory; coherence proof end; end; definition :: original: SCM+FSA-Data*-Loc redefine func SCM+FSA-Data*-Loc -> Subset of SCM+FSA-Memory; coherence by XBOOLE_1:7; end; registration coherence ; end; definition ::$CD
func SCM+FSA-OK -> Function of SCM+FSA-Memory,(Segm 3) equals :: SCMFSA_1:def 4
() +* SCM-OK;
coherence
() +* SCM-OK is Function of SCM+FSA-Memory,(Segm 3)
proof end;
end;

:: deftheorem SCMFSA_1:def 3 :
canceled;

:: deftheorem defines SCM+FSA-OK SCMFSA_1:def 4 :

theorem :: SCMFSA_1:2
canceled;

theorem :: SCMFSA_1:3
canceled;

theorem :: SCMFSA_1:4
canceled;

::$CT 3 theorem Th2: :: SCMFSA_1:5 proof end; theorem :: SCMFSA_1:6 canceled; theorem :: SCMFSA_1:7 canceled; ::$CT 2
theorem :: SCMFSA_1:8

definition
func SCM*-VAL -> ManySortedSet of Segm 3 equals :: SCMFSA_1:def 5
<%NAT,INT,()%>;
coherence
<%NAT,INT,()%> is ManySortedSet of Segm 3
;
end;

:: deftheorem defines SCM*-VAL SCMFSA_1:def 5 :
SCM*-VAL = <%NAT,INT,()%>;

Lm1:
proof end;

Lm2:
proof end;

Lm3:
proof end;

Lm4:
proof end;

theorem Th4: :: SCMFSA_1:9
proof end;

Lm5: for b being Element of SCM+FSA-Data-Loc holds SCM+FSA-OK . b = 1
proof end;

theorem Th5: :: SCMFSA_1:10
for b being Element of SCM+FSA-Data-Loc holds . b = INT
proof end;

Lm6: for f being Element of SCM+FSA-Data*-Loc holds SCM+FSA-OK . f = 2
proof end;

theorem Th6: :: SCMFSA_1:11
for f being Element of SCM+FSA-Data*-Loc holds . f = INT *
proof end;

Lm7:
by PARTFUN1:def 2;

len <%NAT,INT,()%> = 3
by AFINSQ_1:39;

then
by RELAT_1:def 19;

then Lm8:
by ;

registration
coherence
proof end;
end;

definition end;

theorem :: SCMFSA_1:12
canceled;

theorem :: SCMFSA_1:13
canceled;

theorem :: SCMFSA_1:14
canceled;

theorem :: SCMFSA_1:15
canceled;

theorem :: SCMFSA_1:16
canceled;

::$CT 5 theorem Th7: :: SCMFSA_1:17 for s being SCM+FSA-State for I being Element of SCM-Instr holds s | SCM-Memory is SCM-State proof end; theorem Th8: :: SCMFSA_1:18 for s being SCM+FSA-State for s1 being SCM-State holds s +* s1 is SCM+FSA-State proof end; definition let s be SCM+FSA-State; let u be Nat; func SCM+FSA-Chg (s,u) -> SCM+FSA-State equals :: SCMFSA_1:def 6 s +* (); coherence s +* () is SCM+FSA-State proof end; end; :: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 6 : for s being SCM+FSA-State for u being Nat holds SCM+FSA-Chg (s,u) = s +* (); definition let s be SCM+FSA-State; let t be Element of SCM+FSA-Data-Loc ; let u be Integer; func SCM+FSA-Chg (s,t,u) -> SCM+FSA-State equals :: SCMFSA_1:def 7 s +* (t .--> u); coherence s +* (t .--> u) is SCM+FSA-State proof end; end; :: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 7 : for s being SCM+FSA-State for t being Element of SCM+FSA-Data-Loc for u being Integer holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u); definition let s be SCM+FSA-State; let t be Element of SCM+FSA-Data*-Loc ; let u be FinSequence of INT ; func SCM+FSA-Chg (s,t,u) -> SCM+FSA-State equals :: SCMFSA_1:def 8 s +* (t .--> u); coherence s +* (t .--> u) is SCM+FSA-State proof end; end; :: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 8 : for s being SCM+FSA-State for t being Element of SCM+FSA-Data*-Loc for u being FinSequence of INT holds SCM+FSA-Chg (s,t,u) = s +* (t .--> u); registration let s be SCM+FSA-State; let a be Element of SCM+FSA-Data-Loc ; cluster s . a -> integer ; coherence s . a is integer proof end; end; definition let s be SCM+FSA-State; let a be Element of SCM+FSA-Data*-Loc ; :: original: . redefine func s . a -> FinSequence of INT ; coherence s . a is FinSequence of INT proof end; end; definition let s be SCM+FSA-State; func IC s -> Element of NAT equals :: SCMFSA_1:def 15 s . NAT; coherence s . NAT is Element of NAT proof end; end; :: deftheorem SCMFSA_1:def 9 : canceled; :: deftheorem SCMFSA_1:def 10 : canceled; :: deftheorem SCMFSA_1:def 11 : canceled; :: deftheorem SCMFSA_1:def 12 : canceled; :: deftheorem SCMFSA_1:def 13 : canceled; :: deftheorem SCMFSA_1:def 14 : canceled; :: deftheorem defines IC SCMFSA_1:def 15 : for s being SCM+FSA-State holds IC s = s . NAT; definition let x be Element of SCM+FSA-Instr ; let s be SCM+FSA-State; func SCM+FSA-Exec-Res (x,s) -> SCM+FSA-State means :: SCMFSA_1:def 16 ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & it = s +* (SCM-Exec-Res (x9,s9)) ) if x 1_3 <= 8 ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) if x 1_3 = 9 ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) if x 1_3 = 10 it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) if x 1_3 = 11 ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) if x 1_3 = 12 ex i being Integer st ( i = 1 & it = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) if x 1_3 = 13 otherwise it = s; existence ( ( x 1_3 <= 8 implies ex b1 being SCM+FSA-State ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) ) & ( x 1_3 = 9 implies ex b1 being SCM+FSA-State ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) & ( x 1_3 = 10 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) & ( x 1_3 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) ) & ( x 1_3 = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) & ( x 1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st ( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) & ( not x 1_3 <= 8 & not x 1_3 = 9 & not x 1_3 = 10 & not x 1_3 = 11 & not x 1_3 = 12 & not x 1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) ) proof end; uniqueness for b1, b2 being SCM+FSA-State holds ( ( x 1_3 <= 8 & ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) & ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b2 = s +* (SCM-Exec-Res (x9,s9)) ) implies b1 = b2 ) & ( x 1_3 = 9 & ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) & ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b2 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) implies b1 = b2 ) & ( x 1_3 = 10 & ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) & ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b2 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) implies b1 = b2 ) & ( x 1_3 = 11 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) & b2 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) implies b1 = b2 ) & ( x 1_3 = 12 & ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) & ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b2 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) implies b1 = b2 ) & ( x 1_3 = 13 & ex i being Integer st ( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) & ex i being Integer st ( i = 1 & b2 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) implies b1 = b2 ) & ( not x 1_3 <= 8 & not x 1_3 = 9 & not x 1_3 = 10 & not x 1_3 = 11 & not x 1_3 = 12 & not x 1_3 = 13 & b1 = s & b2 = s implies b1 = b2 ) ) ; consistency for b1 being SCM+FSA-State holds ( ( x 1_3 <= 8 & x 1_3 = 9 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) iff ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) & ( x 1_3 <= 8 & x 1_3 = 10 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 <= 8 & x 1_3 = 11 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) iff b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) ) ) & ( x 1_3 <= 8 & x 1_3 = 12 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 <= 8 & x 1_3 = 13 implies ( ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b1 = s +* (SCM-Exec-Res (x9,s9)) ) iff ex i being Integer st ( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) & ( x 1_3 = 9 & x 1_3 = 10 implies ( ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 = 9 & x 1_3 = 11 implies ( ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) iff b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) ) ) & ( x 1_3 = 9 & x 1_3 = 12 implies ( ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 = 9 & x 1_3 = 13 implies ( ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) iff ex i being Integer st ( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) & ( x 1_3 = 10 & x 1_3 = 11 implies ( ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) iff b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) ) ) & ( x 1_3 = 10 & x 1_3 = 12 implies ( ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 = 10 & x 1_3 = 13 implies ( ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) iff ex i being Integer st ( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) & ( x 1_3 = 11 & x 1_3 = 12 implies ( b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 = 11 & x 1_3 = 13 implies ( b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) iff ex i being Integer st ( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) & ( x 1_3 = 12 & x 1_3 = 13 implies ( ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) iff ex i being Integer st ( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) ) ; end; :: deftheorem defines SCM+FSA-Exec-Res SCMFSA_1:def 16 : for x being Element of SCM+FSA-Instr for s, b3 being SCM+FSA-State holds ( ( x 1_3 <= 8 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff ex x9 being Element of SCM-Instr ex s9 being SCM-State st ( x = x9 & s9 = s | SCM-Memory & b3 = s +* (SCM-Exec-Res (x9,s9)) ) ) ) & ( x 1_3 = 9 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff ex i being Integer ex k being Nat st ( k = |.(s . ()).| & i = (s . ()) /. k & b3 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) & ( x 1_3 = 10 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b3 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 = 11 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff b3 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((IC s) + 1)) ) ) & ( x 1_3 = 12 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff ex f being FinSequence of INT ex k being Nat st ( k = |.(s . ()).| & f = k |-> 0 & b3 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) ) & ( x 1_3 = 13 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff ex i being Integer st ( i = 1 & b3 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ) ) & ( not x 1_3 <= 8 & not x 1_3 = 9 & not x 1_3 = 10 & not x 1_3 = 11 & not x 1_3 = 12 & not x 1_3 = 13 implies ( b3 = SCM+FSA-Exec-Res (x,s) iff b3 = s ) ) ); definition func SCM+FSA-Exec -> Action of SCM+FSA-Instr,() means :: SCMFSA_1:def 17 for x being Element of SCM+FSA-Instr for y being SCM+FSA-State holds (it . x) . y = SCM+FSA-Exec-Res (x,y); existence ex b1 being Action of SCM+FSA-Instr,() st for x being Element of SCM+FSA-Instr for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res (x,y) proof end; uniqueness for b1, b2 being Action of SCM+FSA-Instr,() st ( for x being Element of SCM+FSA-Instr for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res (x,y) ) & ( for x being Element of SCM+FSA-Instr for y being SCM+FSA-State holds (b2 . x) . y = SCM+FSA-Exec-Res (x,y) ) holds b1 = b2 proof end; end; :: deftheorem defines SCM+FSA-Exec SCMFSA_1:def 17 : for b1 being Action of SCM+FSA-Instr,() holds ( b1 = SCM+FSA-Exec iff for x being Element of SCM+FSA-Instr for y being SCM+FSA-State holds (b1 . x) . y = SCM+FSA-Exec-Res (x,y) ); theorem :: SCMFSA_1:19 for s being SCM+FSA-State for u being Nat holds (SCM+FSA-Chg (s,u)) . NAT = u proof end; theorem :: SCMFSA_1:20 for s being SCM+FSA-State for u being Nat for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,u)) . mk = s . mk proof end; theorem :: SCMFSA_1:21 for s being SCM+FSA-State for u being Nat for p being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,u)) . p = s . p proof end; theorem :: SCMFSA_1:22 for s being SCM+FSA-State for u, v being Nat holds (SCM+FSA-Chg (s,u)) . v = s . v proof end; theorem :: SCMFSA_1:23 for s being SCM+FSA-State for t being Element of SCM+FSA-Data-Loc for u being Integer holds (SCM+FSA-Chg (s,t,u)) . NAT = s . NAT proof end; theorem :: SCMFSA_1:24 for s being SCM+FSA-State for t being Element of SCM+FSA-Data-Loc for u being Integer holds (SCM+FSA-Chg (s,t,u)) . t = u proof end; theorem :: SCMFSA_1:25 for s being SCM+FSA-State for t being Element of SCM+FSA-Data-Loc for u being Integer for mk being Element of SCM+FSA-Data-Loc st mk <> t holds (SCM+FSA-Chg (s,t,u)) . mk = s . mk proof end; theorem :: SCMFSA_1:26 for s being SCM+FSA-State for t being Element of SCM+FSA-Data-Loc for u being Integer for f being Element of SCM+FSA-Data*-Loc holds (SCM+FSA-Chg (s,t,u)) . f = s . f proof end; theorem :: SCMFSA_1:27 for s being SCM+FSA-State for t being Element of SCM+FSA-Data*-Loc for u being FinSequence of INT holds (SCM+FSA-Chg (s,t,u)) . t = u proof end; theorem :: SCMFSA_1:28 for s being SCM+FSA-State for t being Element of SCM+FSA-Data*-Loc for u being FinSequence of INT for mk being Element of SCM+FSA-Data*-Loc st mk <> t holds (SCM+FSA-Chg (s,t,u)) . mk = s . mk proof end; theorem :: SCMFSA_1:29 for s being SCM+FSA-State for t being Element of SCM+FSA-Data*-Loc for u being FinSequence of INT for a being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,t,u)) . a = s . a proof end; theorem :: SCMFSA_1:30 theorem :: SCMFSA_1:31 canceled; ::$CT
theorem :: SCMFSA_1:32

theorem :: SCMFSA_1:33
for s being SCM+FSA-State holds dom s = SCM+FSA-Memory by ;