:: AMI_2 semantic presentation

definition
func SCM-Halt -> Element of Segm 9 equals :: AMI_2:def 1
0;
correctness
coherence
0 is Element of Segm 9;
by GR_CY_1:12;
end;

:: deftheorem defines SCM-Halt AMI_2:def 1 :
SCM-Halt = 0;

definition
func SCM-Data-Loc -> Subset of NAT equals :: AMI_2:def 2
{ ((2 * b1) + 1) where B is Nat : verum } ;
coherence
{ ((2 * b1) + 1) where B is Nat : verum } is Subset of NAT
proof
{ ((2 * b1) + 1) where B is Nat : verum } c= NAT
proof
let c1 be set ; :: uses TARSKI:def 3
assume c1 in { ((2 * b1) + 1) where B is Nat : verum } ;
then ex b1 being Nat st c1 = (2 * b1) + 1 ;
hence c1 in NAT ;
end;
hence { ((2 * b1) + 1) where B is Nat : verum } is Subset of NAT ;
end;
func SCM-Instr-Loc -> Subset of NAT equals :: AMI_2:def 3
{ (2 * b1) where B is Nat : b1 > 0 } ;
coherence
{ (2 * b1) where B is Nat : b1 > 0 } is Subset of NAT
proof
{ (2 * b1) where B is Nat : b1 > 0 } c= NAT
proof
let c1 be set ; :: uses TARSKI:def 3
assume c1 in { (2 * b1) where B is Nat : b1 > 0 } ;
then ex b1 being Nat st
( c1 = 2 * b1 & b1 > 0 ) ;
hence c1 in NAT ;
end;
hence { (2 * b1) where B is Nat : b1 > 0 } is Subset of NAT ;
end;
end;

:: deftheorem defines SCM-Data-Loc AMI_2:def 2 :
SCM-Data-Loc = { ((2 * b1) + 1) where B is Nat : verum } ;

:: deftheorem defines SCM-Instr-Loc AMI_2:def 3 :
SCM-Instr-Loc = { (2 * b1) where B is Nat : b1 > 0 } ;

registration
cluster SCM-Data-Loc -> non empty ;
coherence
not SCM-Data-Loc is empty
proof
(2 * 0) + 1 in { ((2 * b1) + 1) where B is Nat : verum } ;
hence not SCM-Data-Loc is empty ;
end;
cluster SCM-Instr-Loc -> non empty ;
coherence
not SCM-Instr-Loc is empty
proof
2 * 1 in { (2 * b1) where B is Nat : b1 > 0 } ;
hence not SCM-Instr-Loc is empty ;
end;
end;

definition
func SCM-Instr -> Subset of [:(Segm 9),(((union {INT }) \/ NAT ) * ):] equals :: AMI_2:def 4
(({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ;
coherence
(({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } is Subset of [:(Segm 9),(((union {INT }) \/ NAT ) * ):]
proof
E1: NAT c= (union {INT }) \/ NAT by XBOOLE_1:7;
E2: { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } c= [:(Segm 9),(((union {INT }) \/ NAT ) * ):]
proof
let c1 be set ; :: uses TARSKI:def 3
assume c1 in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ;
then consider c2 being Element of Segm 9, c3, c4 being Element of SCM-Data-Loc such that
E3: ( c1 = [c2,<*c3,c4*>] & c2 in {1,2,3,4,5} ) ;
reconsider c5 = c3, c6 = c4 as Element of (union {INT }) \/ NAT by E1, TARSKI:def 3;
<*c5,c6*> in ((union {INT }) \/ NAT ) * by FINSEQ_1:def 11;
hence c1 in [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by E3, ZFMISC_1:106;
end;
E3: { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } c= [:(Segm 9),(((union {INT }) \/ NAT ) * ):]
proof
let c1 be set ; :: uses TARSKI:def 3
assume c1 in { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ;
then consider c2 being Element of Segm 9, c3 being Element of SCM-Instr-Loc such that
E4: ( c1 = [c2,<*c3*>] & c2 = 6 ) ;
reconsider c4 = c3 as Element of (union {INT }) \/ NAT by E1, TARSKI:def 3;
<*c4*> in ((union {INT }) \/ NAT ) * by FINSEQ_1:def 11;
hence c1 in [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by E4, ZFMISC_1:106;
end;
E4: { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } c= [:(Segm 9),(((union {INT }) \/ NAT ) * ):]
proof
let c1 be set ; :: uses TARSKI:def 3
assume c1 in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ;
then consider c2 being Element of Segm 9, c3 being Element of SCM-Instr-Loc , c4 being Element of SCM-Data-Loc such that
E5: ( c1 = [c2,<*c3,c4*>] & c2 in {7,8} ) ;
reconsider c5 = c4, c6 = c3 as Element of (union {INT }) \/ NAT by E1, TARSKI:def 3;
<*c6,c5*> in ((union {INT }) \/ NAT ) * by FINSEQ_1:def 11;
hence c1 in [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by E5, ZFMISC_1:106;
end;
( SCM-Halt in Segm 9 & {} in ((union {INT }) \/ NAT ) * ) by FINSEQ_1:66;
then [SCM-Halt ,{} ] in [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by ZFMISC_1:106;
then {[SCM-Halt ,{} ]} c= [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by ZFMISC_1:37;
then {[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } c= [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by E3, XBOOLE_1:8;
then ({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } c= [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by E4, XBOOLE_1:8;
hence (({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } is Subset of [:(Segm 9),(((union {INT }) \/ NAT ) * ):] by E2, XBOOLE_1:8;
end;
end;

:: deftheorem defines SCM-Instr AMI_2:def 4 :
SCM-Instr = (({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ;

theorem :: AMI_2:1
canceled;

theorem :: AMI_2:2
[0,{} ] in SCM-Instr
proof
[0,{} ] in {[SCM-Halt ,{} ]} by TARSKI:def 1;
then [0,{} ] in {[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } by XBOOLE_0:def 2;
then [0,{} ] in ({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } by XBOOLE_0:def 2;
hence [0,{} ] in SCM-Instr by XBOOLE_0:def 2;
end;

registration
cluster SCM-Instr -> non empty ;
coherence
not SCM-Instr is empty ;
end;

theorem :: AMI_2:3
for b1 being Element of SCM-Instr-Loc holds [6,<*b1*>] in SCM-Instr
proof
let c1 be Element of SCM-Instr-Loc ;
reconsider c2 = 6 as Element of Segm 9 by GR_CY_1:10;
[c2,<*c1*>] in { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ;
then [c2,<*c1*>] in {[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } by XBOOLE_0:def 2;
then [c2,<*c1*>] in ({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } by XBOOLE_0:def 2;
hence [6,<*c1*>] in SCM-Instr by XBOOLE_0:def 2;
end;

theorem :: AMI_2:4
for b1 being set
for b2 being Element of SCM-Instr-Loc
for b3 being Element of SCM-Data-Loc holds
( b1 in {7,8} implies [b1,<*b2,b3*>] in SCM-Instr )
proof
let c1 be set ;
let c2 be Element of SCM-Instr-Loc ;
let c3 be Element of SCM-Data-Loc ;
assume E1: c1 in {7,8} ;
then ( ( c1 = 7 or c1 = 8 ) & 9 > 0 & 7 < 9 & 8 < 9 ) by TARSKI:def 2;
then reconsider c4 = c1 as Element of Segm 9 by GR_CY_1:10;
[c4,<*c2,c3*>] in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } by E1;
then [c4,<*c2,c3*>] in ({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } by XBOOLE_0:def 2;
hence [c1,<*c2,c3*>] in SCM-Instr by XBOOLE_0:def 2;
end;

theorem :: AMI_2:5
for b1 being set
for b2, b3 being Element of SCM-Data-Loc holds
( b1 in {1,2,3,4,5} implies [b1,<*b2,b3*>] in SCM-Instr )
proof
let c1 be set ;
let c2, c3 be Element of SCM-Data-Loc ;
assume E1: c1 in {1,2,3,4,5} ;
then not ( not c1 = 1 & not c1 = 2 & not c1 = 3 & not c1 = 4 & not c1 = 5 ) by ENUMSET1:def 3;
then reconsider c4 = c1 as Element of Segm 9 by GR_CY_1:10;
[c4,<*c2,c3*>] in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } by E1;
hence [c1,<*c2,c3*>] in SCM-Instr by XBOOLE_0:def 2;
end;

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

E2: 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 E3: c1 = (2 * c2) + 1 ;
thus c1 <> 0 by E3;
given c3 being Nat such that E4: c1 = (2 * c3) + 2 ;
E5: (2 * c3) + (2 * 1) = (2 * (c3 + 1)) + 0 ;
1 = ((2 * c3) + 2) mod 2 by E3, E4, NAT_1:def 2
.= 0 by E5, NAT_1:def 2 ;
hence not verum ;
end;
given c2 being Nat such that E3: c1 = (2 * c2) + (1 + 1) ;
thus c1 <> 0 by E3;
given c3 being Nat such that E4: c1 = (2 * c3) + 1 ;
E5: (2 * c2) + (2 * 1) = (2 * (c2 + 1)) + 0 ;
1 = ((2 * c2) + 2) mod 2 by E3, E4, NAT_1:def 2
.= 0 by E5, NAT_1:def 2 ;
hence not verum ;
end;

definition
func SCM-OK -> Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } means :E3: :: AMI_2:def 5
( a1 . 0 = SCM-Instr-Loc & for b1 being Nat holds
( a1 . ((2 * b1) + 1) = INT & a1 . ((2 * b1) + 2) = SCM-Instr ) );
existence
ex b1 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } st
( b1 . 0 = SCM-Instr-Loc & for b2 being Nat holds
( b1 . ((2 * b2) + 1) = INT & b1 . ((2 * b2) + 2) = SCM-Instr ) )
proof
defpred S1[ set , set ] means not ( not ( a1 = 0 & a2 = SCM-Instr-Loc ) & not ( ex b1 being Nat st a1 = (2 * b1) + 1 & a2 = INT ) & not ( ex b1 being Nat st a1 = (2 * b1) + 2 & a2 = SCM-Instr ) );
E3: now
let c1 be Nat;
{INT } \/ {SCM-Instr ,SCM-Instr-Loc } = {INT ,SCM-Instr ,SCM-Instr-Loc } by ENUMSET1:42;
then E4: ( INT in {INT } \/ {SCM-Instr ,SCM-Instr-Loc } & SCM-Instr in {INT } \/ {SCM-Instr ,SCM-Instr-Loc } & SCM-Instr-Loc in {INT } \/ {SCM-Instr ,SCM-Instr-Loc } ) by ENUMSET1:def 1;
not ( not S1[c1, SCM-Instr-Loc ] & not S1[c1, INT ] & not S1[c1, SCM-Instr ] ) by E1;
hence ex b1 being Element of {INT } \/ {SCM-Instr ,SCM-Instr-Loc } st
S1[c1,b1] by E4;
end;
consider c1 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } such that
E4: for b1 being Element of NAT holds
S1[b1,c1 . b1] from FUNCT_2:sch 3(E3);
 take c1 ;
S1[0,c1 . 0] by E4;
hence c1 . 0 = SCM-Instr-Loc ;
let c2 be Nat;
( S1[(2 * c2) + 1,c1 . ((2 * c2) + 1)] & S1[(2 * c2) + 2,c1 . ((2 * c2) + 2)] ) by E4;
hence ( c1 . ((2 * c2) + 1) = INT & c1 . ((2 * c2) + 2) = SCM-Instr ) by E2;
end;
uniqueness
for b1, b2 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } holds
( ( b1 . 0 = SCM-Instr-Loc & for b3 being Nat holds
( b1 . ((2 * b3) + 1) = INT & b1 . ((2 * b3) + 2) = SCM-Instr ) & b2 . 0 = SCM-Instr-Loc & for b3 being Nat holds
( b2 . ((2 * b3) + 1) = INT & b2 . ((2 * b3) + 2) = SCM-Instr ) ) implies ( b1 = b2 ) )
proof
let c1, c2 be Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc };
assume that E3: ( c1 . 0 = SCM-Instr-Loc & for b1 being Nat holds
( c1 . ((2 * b1) + 1) = INT & c1 . ((2 * b1) + 2) = SCM-Instr ) )
and E4: ( c2 . 0 = SCM-Instr-Loc & for b1 being Nat holds
( c2 . ((2 * b1) + 1) = INT & c2 . ((2 * b1) + 2) = SCM-Instr ) ) ;
now
let c3 be Nat;
now
per cases not ( not c3 = 0 & for b1 being Nat holds
not c3 = (2 * b1) + 1 & for b1 being Nat holds
not c3 = (2 * b1) + 2 ) by E1;
suppose c3 = 0 ;
hence c1 . c3 = c2 . c3 by E3, E4;
end;
suppose E5: ex b1 being Nat st c3 = (2 * b1) + 1 ;
hence c1 . c3 = INT by E3
.= c2 . c3 by E4, E5 ;

end;
suppose E5: ex b1 being Nat st c3 = (2 * b1) + 2 ;
hence c1 . c3 = SCM-Instr by E3
.= c2 . c3 by E4, E5 ;

end;
end;
end;
hence c1 . c3 = c2 . c3 ;
end;
hence c1 = c2 by FUNCT_2:113;
end;
end;

:: deftheorem E3 defines SCM-OK AMI_2:def 5 :
for b1 being Function of NAT ,{INT } \/ {SCM-Instr ,SCM-Instr-Loc } holds
( b1 = SCM-OK iff ( b1 . 0 = SCM-Instr-Loc & for b2 being Nat holds
( b1 . ((2 * b2) + 1) = INT & b1 . ((2 * b2) + 2) = SCM-Instr ) ) );

theorem E4: :: AMI_2:6
( SCM-Instr-Loc <> INT & SCM-Instr <> INT & SCM-Instr-Loc <> SCM-Instr )
proof
thus SCM-Instr-Loc <> INT by NUMBERS:17, NUMBERS:27, XBOOLE_0:def 10;
E5: 2 * 1 in { (2 * b1) where B is Nat : b1 > 0 } ;
now
assume 2 in SCM-Instr ;
then ( 2 in ({[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } ) \/ { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } or 2 in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ) by XBOOLE_0:def 2;
then not ( not 2 in {[SCM-Halt ,{} ]} \/ { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } & not 2 in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } & not 2 in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ) by XBOOLE_0:def 2;
then not ( not 2 in {[SCM-Halt ,{} ]} & not 2 in { [b1,<*b2*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b1 = 6 } & not 2 in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b1 in {7,8} } & not 2 in { [b1,<*b2,b3*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b1 in {1,2,3,4,5} } ) by XBOOLE_0:def 2;
then not ( not 2 = [SCM-Halt ,{} ] & for b1 being Element of Segm 9
for b2 being Element of SCM-Instr-Loc holds
not ( 2 = [b1,<*b2*>] & b1 = 6 ) & for b1 being Element of Segm 9
for b2 being Element of SCM-Instr-Loc
for b3 being Element of SCM-Data-Loc holds
not ( 2 = [b1,<*b2,b3*>] & b1 in {7,8} ) & for b1 being Element of Segm 9
for b2, b3 being Element of SCM-Data-Loc holds
not ( 2 = [b1,<*b2,b3*>] & b1 in {1,2,3,4,5} ) ) by TARSKI:def 1;
hence not verum by AMI_1:3;
end;
hence ( SCM-Instr <> INT & SCM-Instr-Loc <> SCM-Instr ) by E5, INT_1:def 2;
end;

theorem E5: :: AMI_2:7
for b1 being Nat holds
( SCM-OK . b1 = SCM-Instr-Loc iff b1 = 0 )
proof
let c1 be Nat;
thus ( SCM-OK . c1 = SCM-Instr-Loc implies c1 = 0 )
proof
assume E6: SCM-OK . c1 = SCM-Instr-Loc ;
assume c1 <> 0 ;
then not ( for b1 being Nat holds
not c1 = (2 * b1) + 1 & for b1 being Nat holds
not c1 = (2 * b1) + 2 ) by E1;
hence not verum by E6, E3, E4;
end;
thus ( c1 = 0 implies SCM-OK . c1 = SCM-Instr-Loc ) by E3;
end;

theorem E6: :: AMI_2:8
for b1 being Nat holds
( SCM-OK . b1 = INT iff ex b2 being Nat st b1 = (2 * b2) + 1 )
proof
let c1 be Nat;
thus not ( SCM-OK . c1 = INT & for b1 being Nat holds
not c1 = (2 * b1) + 1 )
proof
assume E7: SCM-OK . c1 = INT ;
assume for b1 being Nat holds
not c1 = (2 * b1) + 1 ;
then not ( not c1 = 0 & for b1 being Nat holds
not c1 = (2 * b1) + 2 ) by E1;
hence not verum by E7, E3, E4;
end;
thus ( ex b1 being Nat st c1 = (2 * b1) + 1 implies SCM-OK . c1 = INT ) by E3;
end;

theorem E7: :: AMI_2:9
for b1 being Nat holds
( SCM-OK . b1 = SCM-Instr iff ex b2 being Nat st b1 = (2 * b2) + 2 )
proof
let c1 be Nat;
thus not ( SCM-OK . c1 = SCM-Instr & for b1 being Nat holds
not c1 = (2 * b1) + 2 )
proof
assume E8: SCM-OK . c1 = SCM-Instr ;
assume for b1 being Nat holds
not c1 = (2 * b1) + 2 ;
then not ( not c1 = 0 & for b1 being Nat holds
not c1 = (2 * b1) + 1 ) by E1;
hence not verum by E8, E3, E4;
end;
thus ( ex b1 being Nat st c1 = (2 * b1) + 2 implies SCM-OK . c1 = SCM-Instr ) by E3;
end;

definition
mode SCM-State is Element of product SCM-OK ;
end;

theorem E8: :: AMI_2:10
for b1 being Element of SCM-Data-Loc holds SCM-OK . b1 = INT
proof
let c1 be Element of SCM-Data-Loc ;
c1 in { ((2 * b1) + 1) where B is Nat : verum } ;
then ex b1 being Nat st c1 = (2 * b1) + 1 ;
hence SCM-OK . c1 = INT by E6;
end;

theorem E9: :: AMI_2:11
for b1 being Element of SCM-Instr-Loc holds SCM-OK . b1 = SCM-Instr
proof
let c1 be Element of SCM-Instr-Loc ;
c1 in { (2 * b1) where B is Nat : b1 > 0 } ;
then consider c2 being Nat such that
E10: ( c1 = 2 * c2 & c2 > 0 ) ;
consider c3 being Nat such that
E11: c2 = c3 + 1 by E10, NAT_1:22;
c1 = (2 * c3) + (2 * 1) by E10, E11;
hence SCM-OK . c1 = SCM-Instr by E7;
end;

theorem :: AMI_2:12
for b1 being Element of SCM-Instr-Loc
for b2 being Element of SCM-Data-Loc holds
b1 <> b2
proof
let c1 be Element of SCM-Instr-Loc ;
let c2 be Element of SCM-Data-Loc ;
( SCM-OK . c1 = SCM-Instr & SCM-OK . c2 = INT ) by E8, E9;
hence c1 <> c2 by E4;
end;

theorem E10: :: AMI_2:13
pi (product SCM-OK ),0 = SCM-Instr-Loc
proof
dom SCM-OK = NAT by FUNCT_2:def 1;
hence pi (product SCM-OK ),0 = SCM-OK . 0 by CARD_3:22
.= SCM-Instr-Loc by E5 ;

end;

theorem E11: :: AMI_2:14
for b1 being Element of SCM-Data-Loc holds pi (product SCM-OK ),b1 = INT
proof
let c1 be Element of SCM-Data-Loc ;
dom SCM-OK = NAT by FUNCT_2:def 1;
hence pi (product SCM-OK ),c1 = SCM-OK . c1 by CARD_3:22
.= INT by E8 ;

end;

theorem :: AMI_2:15
for b1 being Element of SCM-Instr-Loc holds pi (product SCM-OK ),b1 = SCM-Instr
proof
let c1 be Element of SCM-Instr-Loc ;
dom SCM-OK = NAT by FUNCT_2:def 1;
hence pi (product SCM-OK ),c1 = SCM-OK . c1 by CARD_3:22
.= SCM-Instr by E9 ;

end;

definition
let c1 be SCM-State;
func IC a1 -> Element of SCM-Instr-Loc equals :: AMI_2:def 6
a1 . 0;
coherence
c1 . 0 is Element of SCM-Instr-Loc by E10, CARD_3:def 6;
end;

:: deftheorem defines IC AMI_2:def 6 :
for b1 being SCM-State holds IC b1 = b1 . 0;

definition
let c1 be SCM-State;
let c2 be Element of SCM-Instr-Loc ;
func SCM-Chg a1,a2 -> SCM-State equals :: AMI_2:def 7
a1 +* (0 .--> a2);
coherence
c1 +* (0 .--> c2) is SCM-State
proof
E12: dom SCM-OK = NAT by FUNCT_2:def 1;
then dom c1 = NAT by CARD_3:18;
then E13: dom (c1 +* (0 .--> c2)) = NAT \/ (dom (0 .--> c2)) by FUNCT_4:def 1
.= NAT \/ {0} by CQC_LANG:5
.= dom SCM-OK by E12, ZFMISC_1:46 ;
now
let c3 be set ;
assume E14: c3 in