:: SCMRING1 semantic presentation

registration
cluster infinite -> non trivial set ;
coherence
for b1 being set st not b1 is finite holds
not b1 is trivial
proof end;
cluster infinite -> non trivial 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is finite holds
not b1 is trivial
proof end;
end;

registration
cluster non empty trivial -> non empty Abelian add-associative right_zeroed right_complementable LoopStr ;
coherence
for b1 being non empty LoopStr st b1 is trivial holds
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof end;
cluster non empty trivial -> non empty right-distributive right_unital doubleLoopStr ;
coherence
for b1 being non empty doubleLoopStr st b1 is trivial holds
( b1 is right_unital & b1 is right-distributive )
proof end;
end;

registration
cluster -> natural Element of SCM-Data-Loc ;
coherence
for b1 being Element of SCM-Data-Loc holds b1 is natural by ORDINAL2:def 21;
end;

registration
cluster SCM-Instr -> non trivial ;
coherence
not SCM-Instr is trivial
proof end;
cluster SCM-Instr-Loc -> infinite non trivial ;
coherence
not SCM-Instr-Loc is finite
proof end;
end;

definition
let c1 be non empty 1-sorted ;
func SCM-Instr c1 -> Subset of [:(Segm 8),(((union {the carrier of a1}) \/ NAT ) * ):] equals :: SCMRING1:def 1
((({[0,{} ]} \/ { [b1,<*b2,b3*>] where B is Element of Segm 8, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4} } ) \/ { [6,<*b1*>] where B is Element of SCM-Instr-Loc : verum } ) \/ { [7,<*b1,b2*>] where B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : verum } ) \/ { [5,<*b1,b2*>] where B is Element of SCM-Data-Loc , B is Element of a1 : verum } ;
coherence
((({[0,{} ]} \/ { [b1,<*b2,b3*>] where B is Element of Segm 8, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4} } ) \/ { [6,<*b1*>] where B is Element of SCM-Instr-Loc : verum } ) \/ { [7,<*b1,b2*>] where B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : verum } ) \/ { [5,<*b1,b2*>] where B is Element of SCM-Data-Loc , B is Element of c1 : verum } is Subset of [:(Segm 8),(((union {the carrier of c1}) \/ NAT ) * ):]
proof end;
end;

:: deftheorem Def1 defines SCM-Instr SCMRING1:def 1 :
for b1 being non empty 1-sorted holds SCM-Instr b1 = ((({[0,{} ]} \/ { [b2,<*b3,b4*>] where B is Element of Segm 8, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b2 in {1,2,3,4} } ) \/ { [6,<*b2*>] where B is Element of SCM-Instr-Loc : verum } ) \/ { [7,<*b2,b3*>] where B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : verum } ) \/ { [5,<*b2,b3*>] where B is Element of SCM-Data-Loc , B is Element of b1 : verum } ;

registration
let c1 be non empty 1-sorted ;
cluster SCM-Instr a1 -> non trivial ;
coherence
not SCM-Instr c1 is trivial
proof end;
end;

definition
let c1 be non empty 1-sorted ;
attr a1 is good means :Def2: :: SCMRING1:def 2
( the carrier of a1 <> SCM-Instr-Loc & the carrier of a1 <> SCM-Instr a1 );
end;

:: deftheorem Def2 defines good SCMRING1:def 2 :
for b1 being non empty 1-sorted holds
( b1 is good iff ( the carrier of b1 <> SCM-Instr-Loc & the carrier of b1 <> SCM-Instr b1 ) );

registration
cluster non empty trivial -> non empty good 1-sorted ;
coherence
for b1 being non empty 1-sorted st b1 is trivial holds
b1 is good
proof end;
end;

registration
cluster strict non empty trivial good 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & b1 is trivial & not b1 is empty )
proof end;
end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable strict right-distributive right_unital trivial good doubleLoopStr ;
existence
ex b1 being doubleLoopStr st
( b1 is strict & b1 is trivial & not b1 is empty )
proof end;
end;

registration
cluster strict trivial good doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is strict & b1 is trivial )
proof end;
end;

E2: now
let c1 be Nat;
consider c2 being Nat such that
E3: ( c1 = 2 * c2 or c1 = (2 * c2) + 1 ) by SCHEME1:1;
now
assume E4: c1 = 2 * c2 ;
E5: ( c2 = 0 or ex b1 being Nat st c2 = b1 + 1 ) by NAT_1:22;
now
given c3 being Nat such that E6: c2 = c3 + 1 ;
take c4 = c3;
thus c1 = (2 * c4) + (2 * 1) by E4, E6;
end;
hence ( c1 = 0 or ex b1 being Nat st c1 = (2 * b1) + 2 ) by E4, E5;
end;
hence ( c1 = 0 or ex b1 being Nat st c1 = (2 * b1) + 1 or ex b1 being Nat st c1 = (2 * b1) + 2 ) by E3;
end;

E3: now
let c1 be Nat;
thus ( ex b1 being Nat st c1 = (2 * b1) + 1 implies ( c1 <> 0 & ( for b1 being Nat holds not c1 = (2 * b1) + 2 ) ) )
proof
given c2 being Nat such that E4: c1 = (2 * c2) + 1 ;
thus c1 <> 0 by E4;
given c3 being Nat such that E5: c1 = (2 * c3) + 2 ;
E6: (2 * c3) + (2 * 1) = (2 * (c3 + 1)) + 0 ;
1 = ((2 * c3) + 2) mod 2 by E4, E5, NAT_1:def 2
.= 0 by E6, NAT_1:def 2 ;
hence contradiction ;
end;
given c2 being Nat such that E4: c1 = (2 * c2) + (1 + 1) ;
thus c1 <> 0 by E4;
given c3 being Nat such that E5: c1 = (2 * c3) + 1 ;
E6: (2 * c2) + (2 * 1) = (2 * (c2 + 1)) + 0 ;
1 = ((2 * c2) + 2) mod 2 by E4, E5, NAT_1:def 2
.= 0 by E6, NAT_1:def 2 ;
hence contradiction ;
end;

definition
let c1 be non empty 1-sorted ;
func SCM-OK c1 -> Function of NAT ,{the carrier of a1} \/ {(SCM-Instr a1),SCM-Instr-Loc } means :Def3: :: SCMRING1:def 3
( a2 . 0 = SCM-Instr-Loc & ( for b1 being Nat holds
( a2 . ((2 * b1) + 1) = the carrier of a1 & a2 . ((2 * b1) + 2) = SCM-Instr a1 ) ) );
existence
ex b1 being Function of NAT ,{the carrier of c1} \/ {(SCM-Instr c1),SCM-Instr-Loc } st
( b1 . 0 = SCM-Instr-Loc & ( for b2 being Nat holds
( b1 . ((2 * b2) + 1) = the carrier of c1 & b1 . ((2 * b2) + 2) = SCM-Instr c1 ) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT ,{the carrier of c1} \/ {(SCM-Instr c1),SCM-Instr-Loc } st b1 . 0 = SCM-Instr-Loc & ( for b3 being Nat holds
( b1 . ((2 * b3) + 1) = the carrier of c1 & b1 . ((2 * b3) + 2) = SCM-Instr c1 ) ) & b2 . 0 = SCM-Instr-Loc & ( for b3 being Nat holds
( b2 . ((2 * b3) + 1) = the carrier of c1 & b2 . ((2 * b3) + 2) = SCM-Instr c1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines SCM-OK SCMRING1:def 3 :
for b1 being non empty 1-sorted
for b2 being Function of NAT ,{the carrier of b1} \/ {(SCM-Instr b1),SCM-Instr-Loc } holds
( b2 = SCM-OK b1 iff ( b2 . 0 = SCM-Instr-Loc & ( for b3 being Nat holds
( b2 . ((2 * b3) + 1) = the carrier of b1 & b2 . ((2 * b3) + 2) = SCM-Instr b1 ) ) ) );

definition
let c1 be non empty 1-sorted ;
mode SCM-State of a1 is Element of product (SCM-OK a1);
end;

theorem Th1: :: SCMRING1:1
for b1 being non empty 1-sorted holds SCM-Instr-Loc <> SCM-Instr b1
proof end;

theorem Th2: :: SCMRING1:2
for b1 being Nat
for b2 being non empty good 1-sorted holds
( (SCM-OK b2) . b1 = SCM-Instr-Loc iff b1 = 0 )
proof end;

theorem Th3: :: SCMRING1:3
for b1 being Nat
for b2 being non empty good 1-sorted holds
( (SCM-OK b2) . b1 = the carrier of b2 iff ex b3 being Nat st b1 = (2 * b3) + 1 )
proof end;

theorem Th4: :: SCMRING1:4
for b1 being Nat
for b2 being non empty good 1-sorted holds
( (SCM-OK b2) . b1 = SCM-Instr b2 iff ex b3 being Nat st b1 = (2 * b3) + 2 )
proof end;

theorem Th5: :: SCMRING1:5
for b1 being Element of SCM-Data-Loc
for b2 being non empty good 1-sorted holds (SCM-OK b2) . b1 = the carrier of b2
proof end;

theorem Th6: :: SCMRING1:6
for b1 being Element of SCM-Instr-Loc
for b2 being non empty good 1-sorted holds (SCM-OK b2) . b1 = SCM-Instr b2
proof end;

theorem Th7: :: SCMRING1:7
for b1 being non empty 1-sorted holds pi (product (SCM-OK b1)),0 = SCM-Instr-Loc
proof end;

theorem Th8: :: SCMRING1:8
for b1 being Element of SCM-Data-Loc
for b2 being non empty good 1-sorted holds pi (product (SCM-OK b2)),b1 = the carrier of b2
proof end;

theorem Th9: :: SCMRING1:9
for b1 being Element of SCM-Instr-Loc
for b2 being non empty good 1-sorted holds pi (product (SCM-OK b2)),b1 = SCM-Instr b2
proof end;

definition
let c1 be non empty 1-sorted ;
let c2 be SCM-State of c1;
func IC c2 -> Element of SCM-Instr-Loc equals :: SCMRING1:def 4
a2 . 0;
coherence
c2 . 0 is Element of SCM-Instr-Loc
proof end;
end;

:: deftheorem Def4 defines IC SCMRING1:def 4 :
for b1 being non empty 1-sorted
for b2 being SCM-State of b1 holds IC b2 = b2 . 0;

definition
let c1 be non empty good 1-sorted ;
let c2 be SCM-State of c1;
let c3 be Element of SCM-Instr-Loc ;
func SCM-Chg c2,c3 -> SCM-State of a1 equals :: SCMRING1:def 5
a2 +* (0 .--> a3);
coherence
c2 +* (0 .--> c3) is SCM-State of c1
proof end;
end;

:: deftheorem Def5 defines SCM-Chg SCMRING1:def 5 :
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Instr-Loc holds SCM-Chg b2,b3 = b2 +* (0 .--> b3);

theorem Th10: :: SCMRING1:10
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Instr-Loc holds (SCM-Chg b2,b3) . 0 = b3
proof end;

theorem Th11: :: SCMRING1:11
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Instr-Loc
for b4 being Element of SCM-Data-Loc holds (SCM-Chg b2,b3) . b4 = b2 . b4
proof end;

theorem Th12: :: SCMRING1:12
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3, b4 being Element of SCM-Instr-Loc holds (SCM-Chg b2,b3) . b4 = b2 . b4
proof end;

definition
let c1 be non empty good 1-sorted ;
let c2 be SCM-State of c1;
let c3 be Element of SCM-Data-Loc ;
let c4 be Element of c1;
func SCM-Chg c2,c3,c4 -> SCM-State of a1 equals :: SCMRING1:def 6
a2 +* (a3 .--> a4);
coherence
c2 +* (c3 .--> c4) is SCM-State of c1
proof end;
end;

:: deftheorem Def6 defines SCM-Chg SCMRING1:def 6 :
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Data-Loc
for b4 being Element of b1 holds SCM-Chg b2,b3,b4 = b2 +* (b3 .--> b4);

theorem Th13: :: SCMRING1:13
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Data-Loc
for b4 being Element of b1 holds (SCM-Chg b2,b3,b4) . 0 = b2 . 0
proof end;

theorem Th14: :: SCMRING1:14
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Data-Loc
for b4 being Element of b1 holds (SCM-Chg b2,b3,b4) . b3 = b4
proof end;

theorem Th15: :: SCMRING1:15
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Data-Loc
for b4 being Element of b1
for b5 being Element of SCM-Data-Loc st b5 <> b3 holds
(SCM-Chg b2,b3,b4) . b5 = b2 . b5
proof end;

theorem Th16: :: SCMRING1:16
for b1 being non empty good 1-sorted
for b2 being SCM-State of b1
for b3 being Element of SCM-Data-Loc
for b4 being Element of b1
for b5 being Element of SCM-Instr-Loc holds (SCM-Chg b2,b3,b4) . b5 = b2 . b5
proof end;

definition
let c1 be non empty good 1-sorted ;
let c2 be SCM-State of c1;
let c3 be Element of SCM-Data-Loc ;
redefine func . as c2 . c3 -> Element of a1;
coherence
c2 . c3 is Element of c1
proof end;
end;

definition
let c1 be non empty 1-sorted ;
let c2 be Element of SCM-Instr c1;
given c3, c4 being Element of SCM-Data-Loc , c5 being Element of Segm 8 such that E13: c2 = [c5,<*c3,c4*>] ;
func c2 address_1 -> Element of SCM-Data-Loc means :Def7: :: SCMRING1:def 7
ex b1 being FinSequence of SCM-Data-Loc st
( b1 = a2 `2 & a3 = b1 /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc st
( b2 = c2 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c2 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c2 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
func c2 address_2 -> Element of SCM-Data-Loc means :Def8: :: SCMRING1:def 8
ex b1 being FinSequence of SCM-Data-Loc st
( b1 = a2 `2 & a3 = b1 /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc st
( b2 = c2 `2 & b1 = b2 /. 2 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c2 `2 & b1 = b3 /. 2 ) & ex b3 being FinSequence of SCM-Data-Loc st
( b3 = c2 `2 & b2 = b3 /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def7 defines address_1 SCMRING1:def 7 :
for b1 being non empty 1-sorted
for b2 being Element of SCM-Instr b1 st ex b3, b4 being Element of SCM-Data-Loc ex b5 being Element of Segm 8 st b2 = [b5,<*b3,b4*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = b2 address_1 iff ex b4 being FinSequence of SCM-Data-Loc st
( b4 = b2 `2 & b3 = b4 /. 1 ) );

:: deftheorem Def8 defines address_2 SCMRING1:def 8 :
for b1 being non empty 1-sorted
for b2 being Element of SCM-Instr b1 st ex b3, b4 being Element of SCM-Data-Loc ex b5 being Element of Segm 8 st b2 = [b5,<*b3,b4*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = b2 address_2 iff ex b4 being FinSequence of SCM-Data-Loc st
( b4 = b2 `2 & b3 = b4 /. 2 ) );

theorem Th17: :: SCMRING1:17
for b1 being Element of Segm 8
for b2 being non empty 1-sorted
for b3 being Element of SCM-Instr b2
for b4, b5 being Element of SCM-Data-Loc st b3 = [b1,<*b4,b5*>] holds
( b3 address_1 = b4 & b3 address_2 = b5 )
proof end;

definition
let c1 be non empty 1-sorted ;
let c2 be Element of SCM-Instr c1;
given c3 being Element of SCM-Instr-Loc , c4 being Element of Segm 8 such that E15: c2 = [c4,<*c3*>] ;
func c2 jump_address -> Element of SCM-Instr-Loc means :Def9: :: SCMRING1:def 9
ex b1 being FinSequence of SCM-Instr-Loc st
( b1 = a2 `2 & a3 = b1 /. 1 );
existence
ex b1 being Element of SCM-Instr-Loc ex b2 being FinSequence of SCM-Instr-Loc st
( b2 = c2 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex b3 being FinSequence of SCM-Instr-Loc st
( b3 = c2 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Instr-Loc st
( b3 = c2 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
end;

:: deftheorem Def9 defines jump_address SCMRING1:def 9 :
for b1 being non empty 1-sorted
for b2 being Element of SCM-Instr b1 st ex b3 being Element of SCM-Instr-Loc ex b4 being Element of Segm 8 st b2 = [b4,<*b3*>] holds
for b3 being Element of SCM-Instr-Loc holds
( b3 = b2 jump_address iff ex b4 being FinSequence of SCM-Instr-Loc st
( b4 = b2 `2 & b3 = b4 /. 1 ) );

theorem Th18: :: SCMRING1:18
for b1 being Element of Segm 8
for b2 being non empty 1-sorted
for b3 being Element of SCM-Instr b2
for b4 being Element of SCM-Instr-Loc st b3 = [b1,<*b4*>] holds
b3 jump_address = b4
proof end;

definition
let c1 be non empty 1-sorted ;
let c2 be Element of SCM-Instr c1;
given c3 being Element of SCM-Instr-Loc , c4 being Element of SCM-Data-Loc , c5 being Element of Segm 8 such that E16: c2 = [c5,<*c3,c4*>] ;
func c2 cjump_address -> Element of SCM-Instr-Loc means :Def10: :: SCMRING1:def 10
ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st
( <*b1,b2*> = a2 `2 & a3 = <*b1,b2*> /. 1 );
existence
ex b1, b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st
( <*b2,b3*> = c2 `2 & b1 = <*b2,b3*> /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Instr-Loc st ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c2 `2 & b1 = <*b3,b4*> /. 1 ) & ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c2 `2 & b2 = <*b3,b4*> /. 1 ) holds
b1 = b2 ;
func c2 cond_address -> Element of SCM-Data-Loc means :Def11: :: SCMRING1:def 11
ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st
( <*b1,b2*> = a2 `2 & a3 = <*b1,b2*> /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st
( <*b2,b3*> = c2 `2 & b1 = <*b2,b3*> /. 2 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c2 `2 & b1 = <*b3,b4*> /. 2 ) & ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc st
( <*b3,b4*> = c2 `2 & b2 = <*b3,b4*> /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def10 defines cjump_address SCMRING1:def 10 :
for b1 being non empty 1-sorted
for b2 being Element of SCM-Instr b1 st ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc ex b5 being Element of Segm 8 st b2 = [b5,<*b3,b4*>] holds
for b3 being Element of SCM-Instr-Loc holds
( b3 = b2 cjump_address iff ex b4 being Element of SCM-Instr-Loc ex b5 being Element of SCM-Data-Loc st
( <*b4,b5*> = b2 `2 & b3 = <*b4,b5*> /. 1 ) );

:: deftheorem Def11 defines cond_address SCMRING1:def 11 :
for b1 being non empty 1-sorted
for b2 being Element of SCM-Instr b1 st ex b3 being Element of SCM-Instr-Loc ex b4 being Element of SCM-Data-Loc ex b5 being Element of Segm 8 st b2 = [b5,<*b3,b4*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = b2 cond_address iff ex b4 being Element of SCM-Instr-Loc ex b5 being Element of SCM-Data-Loc st
( <*b4,b5*> = b2 `2 & b3 = <*b4,b5*> /. 2 ) );

theorem Th19: :: SCMRING1:19
for b1 being Element of Segm 8
for b2 being non empty 1-sorted
for b3 being Element of SCM-Instr b2
for b4 being Element of SCM-Instr-Loc
for b5 being Element of SCM-Data-Loc st b3 = [b1,<*b4,b5*>] holds
( b3 cjump_address = b4 & b3 cond_address = b5 )
proof end;

definition
let c1 be non empty 1-sorted ;
let c2 be Element of SCM-Data-Loc ;
let c3 be Element of c1;
redefine func <* as <*c2,c3*> -> FinSequence of SCM-Data-Loc \/ the carrier of a1;
coherence
<*c2,c3*> is FinSequence of SCM-Data-Loc \/ the carrier of c1
proof end;
end;

definition
let c1 be non empty 1-sorted ;
let c2 be Element of SCM-Instr c1;
given c3 being Element of SCM-Data-Loc , c4 being Element of c1, c5 being Element of Segm 8 such that E18: c2 = [c5,<*c3,c4*>] ;
func c2 const_address -> Element of SCM-Data-Loc means :Def12: :: SCMRING1:def 12
ex b1 being FinSequence of SCM-Data-Loc \/ the carrier of a1 st
( b1 = a2 `2 & a3 = b1 /. 1 );
existence
ex b1 being Element of SCM-Data-Loc ex b2 being FinSequence of SCM-Data-Loc \/ the carrier of c1 st
( b2 = c2 `2 & b1 = b2 /. 1 )
proof end;
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex b3 being FinSequence of SCM-Data-Loc \/ the carrier of c1 st
( b3 = c2 `2 & b1 = b3 /. 1 ) & ex b3 being FinSequence of SCM-Data-Loc \/ the carrier of c1 st
( b3 = c2 `2 & b2 = b3 /. 1 ) holds
b1 = b2 ;
func c2 const_value -> Element of a1 means :Def13: :: SCMRING1:def 13
ex b1 being FinSequence of SCM-Data-Loc \/ the carrier of a1 st
( b1 = a2 `2 & a3 = b1 /. 2 );
existence
ex b1 being Element of c1ex b2 being FinSequence of SCM-Data-Loc \/ the carrier of c1 st
( b2 = c2 `2 & b1 = b2 /. 2 )
proof end;
uniqueness
for b1, b2 being Element of c1 st ex b3 being FinSequence of SCM-Data-Loc \/ the carrier of c1 st
( b3 = c2 `2 & b1 = b3 /. 2 ) & ex b3 being FinSequence of SCM-Data-Loc \/ the carrier of c1 st
( b3 = c2 `2 & b2 = b3 /. 2 ) holds
b1 = b2 ;
end;

:: deftheorem Def12 defines const_address SCMRING1:def 12 :
for b1 being non empty 1-sorted
for b2 being Element of SCM-Instr b1 st ex b3 being Element of SCM-Data-Loc ex b4 being Element of b1ex b5 being Element of Segm 8 st b2 = [b5,<*b3,b4*>] holds
for b3 being Element of SCM-Data-Loc holds
( b3 = b2 const_address iff ex b4 being FinSequence of SCM-Data-Loc \/ the carrier of b1 st
( b4 = b2 `2 & b3 = b4 /. 1 ) );

:: deftheorem Def13 defines const_value SCMRING1:def 13 :
for b1 being non empty 1-sorted
for b2 being Element of SCM-Instr b1 st ex b3 being Element of SCM-Data-Loc ex b4 being Element of b1ex b5 being Element of Segm 8 st b2 = [b5,<*b3,b4*>] holds
for b3 being Element of b1 holds
( b3 = b2 const_value iff ex b4 being FinSequence of SCM-Data-Loc \/ the carrier of b1 st
( b4 = b2 `2 & b3 = b4 /. 2 ) );

theorem Th20: :: SCMRING1:20
for b1 being Element of Segm 8
for b2 being non empty 1-sorted
for b3 being Element of SCM-Instr b2
for b4 being Element of SCM-Data-Loc
for b5 being Element of b2 st b3 = [b1,<*b4,b5*>] holds
( b3 const_address = b4 & b3 const_value = b5 )
proof end;

definition
let c1 be good Ring;
let c2 be Element of SCM-Instr c1;
let c3 be SCM-State of c1;
func SCM-Exec-Res c2,c3 -> SCM-State of a1 equals :: SCMRING1:def 14
 SCM-Chg (SCM-Chg a3,(a2 address_1 ),(a3 . (a2 address_2 ))),(Next (IC a3)) if ex b1, b2 being Element of SCM-Data-Loc st a2 = [1,<*b1,b2*>]
SCM-Chg (SCM-Chg a3,(a2 address_1 ),((a3 . (a2 address_1 )) + (a3 . (a2 address_2 )))),(Next (IC a3)) if ex b1, b2 being Element of SCM-Data-Loc st a2 = [2,<*b1,b2*>]
SCM-Chg (SCM-Chg a3,(a2 address_1 ),((a3 . (a2 address_1 )) - (a3 . (a2 address_2 )))),(Next (IC a3)) if ex b1, b2 being Element of SCM-Data-Loc st a2 = [3,<*b1,b2*>]
SCM-Chg (SCM-Chg a3,(a2 address_1 ),((a3 . (a2 address_1 )) * (a3 . (a2 address_2 )))),(Next (IC a3)) if ex b1, b2 being Element of SCM-Data-Loc st a2 = [4,<*b1,b2*>]
SCM-Chg a3,(a2 jump_address ) if ex b1 being Element of SCM-Instr-Loc st a2 = [6,<*b1*>]
SCM-Chg a3,(IFEQ (a3 . (a2 cond_address )),(0. a1),(a2 cjump_address ),(Next (IC a3))) if ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st a2 = [7,<*b1,b2*>]
SCM-Chg (SCM-Chg a3,(a2 const_address ),(a2 const_value )),(Next (IC a3)) if ex b1 being Element of SCM-Data-Loc ex b2 being Element of a1 st a2 = [5,<*b1,b2*>]
otherwise a3;
coherence
( ( ex b1, b2 being Element of SCM-Data-Loc st c2 = [1,<*b1,b2*>] implies SCM-Chg (SCM-Chg c3,(c2 address_1 ),(c3 . (c2 address_2 ))),(Next (IC c3)) is SCM-State of c1 ) & ( ex b1, b2 being Element of SCM-Data-Loc st c2 = [2,<*b1,b2*>] implies SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) + (c3 . (c2 address_2 )))),(Next (IC c3)) is SCM-State of c1 ) & ( ex b1, b2 being Element of SCM-Data-Loc st c2 = [3,<*b1,b2*>] implies SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) - (c3 . (c2 address_2 )))),(Next (IC c3)) is SCM-State of c1 ) & ( ex b1, b2 being Element of SCM-Data-Loc st c2 = [4,<*b1,b2*>] implies SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) * (c3 . (c2 address_2 )))),(Next (IC c3)) is SCM-State of c1 ) & ( ex b1 being Element of SCM-Instr-Loc st c2 = [6,<*b1*>] implies SCM-Chg c3,(c2 jump_address ) is SCM-State of c1 ) & ( ex b1 being Element of SCM-Instr-Loc ex b2 being Element of SCM-Data-Loc st c2 = [7,<*b1,b2*>] implies SCM-Chg c3,(IFEQ (c3 . (c2 cond_address )),(0. c1),(c2 cjump_address ),(Next (IC c3))) is SCM-State of c1 ) & ( ex b1 being Element of SCM-Data-Loc ex b2 being Element of c1 st c2 = [5,<*b1,b2*>] implies SCM-Chg (SCM-Chg c3,(c2 const_address ),(c2 const_value )),(Next (IC c3)) is SCM-State of c1 ) & ( ( for b1, b2 being Element of SCM-Data-Loc holds not c2 = [1,<*b1,b2*>] ) & ( for b1, b2 being Element of SCM-Data-Loc holds not c2 = [2,<*b1,b2*>] ) & ( for b1, b2 being Element of SCM-Data-Loc holds not c2 = [3,<*b1,b2*>] ) & ( for b1, b2 being Element of SCM-Data-Loc holds not c2 = [4,<*b1,b2*>] ) & ( for b1 being Element of SCM-Instr-Loc holds not c2 = [6,<*b1*>] ) & ( for b1 being Element of SCM-Instr-Loc
for b2 being Element of SCM-Data-Loc holds not c2 = [7,<*b1,b2*>] ) & ( for b1 being Element of SCM-Data-Loc
for b2 being Element of c1 holds not c2 = [5,<*b1,b2*>] ) implies c3 is SCM-State of c1 ) ) ;
consistency
for b1 being SCM-State of c1 holds
( ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [1,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c2 = [2,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),(c3 . (c2 address_2 ))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) + (c3 . (c2 address_2 )))),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [1,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c2 = [3,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),(c3 . (c2 address_2 ))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) - (c3 . (c2 address_2 )))),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [1,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c2 = [4,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),(c3 . (c2 address_2 ))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) * (c3 . (c2 address_2 )))),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [1,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c2 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),(c3 . (c2 address_2 ))),(Next (IC c3)) iff b1 = SCM-Chg c3,(c2 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [1,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c2 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),(c3 . (c2 address_2 ))),(Next (IC c3)) iff b1 = SCM-Chg c3,(IFEQ (c3 . (c2 cond_address )),(0. c1),(c2 cjump_address ),(Next (IC c3))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [1,<*b2,b3*>] & ex b2 being Element of SCM-Data-Loc ex b3 being Element of c1 st c2 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),(c3 . (c2 address_2 ))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 const_address ),(c2 const_value )),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [2,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c2 = [3,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) + (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) - (c3 . (c2 address_2 )))),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [2,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c2 = [4,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) + (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) * (c3 . (c2 address_2 )))),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [2,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c2 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) + (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg c3,(c2 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [2,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c2 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) + (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg c3,(IFEQ (c3 . (c2 cond_address )),(0. c1),(c2 cjump_address ),(Next (IC c3))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [2,<*b2,b3*>] & ex b2 being Element of SCM-Data-Loc ex b3 being Element of c1 st c2 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) + (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 const_address ),(c2 const_value )),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [3,<*b2,b3*>] & ex b2, b3 being Element of SCM-Data-Loc st c2 = [4,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) - (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) * (c3 . (c2 address_2 )))),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [3,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c2 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) - (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg c3,(c2 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [3,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c2 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) - (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg c3,(IFEQ (c3 . (c2 cond_address )),(0. c1),(c2 cjump_address ),(Next (IC c3))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [3,<*b2,b3*>] & ex b2 being Element of SCM-Data-Loc ex b3 being Element of c1 st c2 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) - (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 const_address ),(c2 const_value )),(Next (IC c3)) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [4,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc st c2 = [6,<*b2*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) * (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg c3,(c2 jump_address ) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [4,<*b2,b3*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c2 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) * (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg c3,(IFEQ (c3 . (c2 cond_address )),(0. c1),(c2 cjump_address ),(Next (IC c3))) ) ) & ( ex b2, b3 being Element of SCM-Data-Loc st c2 = [4,<*b2,b3*>] & ex b2 being Element of SCM-Data-Loc ex b3 being Element of c1 st c2 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg (SCM-Chg c3,(c2 address_1 ),((c3 . (c2 address_1 )) * (c3 . (c2 address_2 )))),(Next (IC c3)) iff b1 = SCM-Chg (SCM-Chg c3,(c2 const_address ),(c2 const_value )),(Next (IC c3)) ) ) & ( ex b2 being Element of SCM-Instr-Loc st c2 = [6,<*b2*>] & ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c2 = [7,<*b2,b3*>] implies ( b1 = SCM-Chg c3,(c2 jump_address ) iff b1 = SCM-Chg c3,(IFEQ (c3 . (c2 cond_address )),(0. c1),(c2 cjump_address ),(Next (IC c3))) ) ) & ( ex b2 being Element of SCM-Instr-Loc st c2 = [6,<*b2*>] & ex b2 being Element of SCM-Data-Loc ex b3 being Element of c1 st c2 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg c3,(c2 jump_address ) iff b1 = SCM-Chg (SCM-Chg c3,(c2 const_address ),(c2 const_value )),(Next (IC c3)) ) ) & ( ex b2 being Element of SCM-Instr-Loc ex b3 being Element of SCM-Data-Loc st c2 = [7,<*b2,b3*>] & ex b2 being Element of SCM-Data-Loc ex b3 being Element of c1 st c2 = [5,<*b2,b3*>] implies ( b1 = SCM-Chg c3,(IFEQ (c3 . (c2 cond_address )),(0. c1),(c2 cjump_address ),(Next (IC c3))) iff b1 = SCM-Chg (SCM-Chg c3,(c2 const_address ),(c2 const_value )),(Next (IC c3)) ) ) ) by ZFMISC_1:33;
end;

:: deftheorem Def14 defines SCM-Exec-Res SCMRING1:def 14 :
for b1 being good Ring
for b2 being Element of SCM-Instr b1
for b3 being SCM-State of b1 holds
( ( ex b4, b5 being Element of SCM-Data-Loc st b2 = [1,<*b4,b5*>] implies SCM-Exec-Res b2,b3 = SCM-Chg (SCM-Chg b3,(b2 address_1 ),(b3 . (b2 address_2 ))),(Next (IC b3)) ) & ( ex b4, b5 being Element of SCM-Data-Loc st b2 = [2,<*b4,b5*>] implies SCM-Exec-Res b2,b3 = SCM-Chg (SCM-Chg b3,(b2 address_1 ),((b3 . (b2 address_1 )) + (b3 . (b2 address_2 )))),(Next (IC b3)) ) & ( ex b4, b5 being Element of SCM-Data-Loc st b2 = [3,<*b4,b5*>] implies SCM-Exec-Res b2,b3 = SCM-Chg (SCM-Chg b3,(b2 address_1 ),((b3 . (b2 address_1 )) - (b3 . (b2 address_2 )))),(Next (IC b3)) ) & ( ex b4, b5 being Element of SCM-Data-Loc st b2 = [4,<*b4,b5*>] implies SCM-Exec-Res b2,b3 = SCM-Chg (SCM-Chg b3,(b2 address_1 ),((b3 . (b2 address_1 )) * (b3 . (b2 address_2 )))),(Next (IC b3)) ) & ( ex b4 being Element of SCM-Instr-Loc st b2 = [6,<*b4*>] implies SCM-Exec-Res b2,b3 = SCM-Chg b3,(b2 jump_address ) ) & ( ex b4 being Element of SCM-Instr-Loc ex b5 being Element of SCM-Data-Loc st b2 = [7,<*b4,b5*>] implies SCM-Exec-Res b2,b3 = SCM-Chg b3,(IFEQ (b3 . (b2 cond_address )),(0. b1),(b2 cjump_address ),(Next (IC b3))) ) & ( ex b4 being Element of SCM-Data-Loc ex b5 being Element of b1 st b2 = [5,<*b4,b5*>] implies SCM-Exec-Res b2,b3 = SCM-Chg (SCM-Chg b3,(b2 const_address ),(b2 const_value )),(Next (IC b3)) ) & ( ( for b4, b5 being Element of SCM-Data-Loc holds not b2 = [1,<*b4,b5*>] ) & ( for b4, b5 being Element of SCM-Data-Loc holds not b2 = [2,<*b4,b5*>] ) & ( for b4, b5 being Element of SCM-Data-Loc holds not b2 = [3,<*b4,b5*>] ) & ( for b4, b5 being Element of SCM-Data-Loc holds not b2 = [4,<*b4,b5*>] ) & ( for b4 being Element of SCM-Instr-Loc holds not b2 = [6,<*b4*>] ) & ( for b4 being Element of SCM-Instr-Loc
for b5 being Element of SCM-Data-Loc holds not b2 = [7,<*b4,b5*>] ) & ( for b4 being Element of SCM-Data-Loc
for b5 being Element of b1 holds not b2 = [5,<*b4,b5*>] ) implies SCM-Exec-Res b2,b3 = b3 ) );

registration
let c1 be non empty 1-sorted ;
let c2 be Function of SCM-Instr c1, Funcs (product (SCM-OK c1)),(product (SCM-OK c1));
let c3 be Element of SCM-Instr c1;
cluster a2 . a3 -> Relation-like Function-like ;
coherence
( c2 . c3 is Function-like & c2 . c3 is Relation-like ) ;
end;

definition
let c1 be good Ring;
func SCM-Exec c1 -> Function of SCM-Instr a1, Funcs (product (SCM-OK a1)),(product (SCM-OK a1)) means :: SCMRING1:def 15
for b1 being Element of SCM-Instr a1
for b2 being SCM-State of a1 holds (a2 . b1) . b2 = SCM-Exec-Res b1,b2;
existence
ex b1 being Function of SCM-Instr c1, Funcs (product (SCM-OK c1)),(product (SCM-OK c1)) st
for b2 being Element of SCM-Instr c1
for b3 being SCM-State of c1 holds (b1 . b2) . b3 = SCM-Exec-Res b2,b3
proof end;
uniqueness
for b1, b2 being Function of SCM-Instr c1, Funcs (product (SCM-OK c1)),(product (SCM-OK c1)) st ( for b3 being Element of SCM-Instr c1
for b4 being SCM-State of c1 holds (b1 . b3) . b4 = SCM-Exec-Res b3,b4 ) & ( for b3 being Element of SCM-Instr c1
for b4 being SCM-State of c1 holds (b2 . b3) . b4 = SCM-Exec-Res b3,b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines SCM-Exec SCMRING1:def 15 :
for b1 being good Ring
for b2 being Function of SCM-Instr b1, Funcs (product (SCM-OK b1)),(product (SCM-OK b1)) holds
( b2 = SCM-Exec b1 iff for b3 being Element of SCM-Instr b1
for b4 being SCM-State of b1 holds (b2 . b3) . b4 = SCM-Exec-Res b3,b4 );