let S be non empty 1-sorted ; :: thesis: SCM-Instr S c= [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
set X = proj2 (SCM-Instr S);
let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in SCM-Instr S or u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):] )
assume Z: u in SCM-Instr S ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
X: {} in NAT * by FINSEQ_1:66;
per cases ( u in (({[0 ,{} ,{} ]} \/ { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{} ] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or u in { [5,{} ,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by Z, XBOOLE_0:def 3;
suppose S: u in (({[0 ,{} ,{} ]} \/ { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{} ] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
per cases ( u in ({[0 ,{} ,{} ]} \/ { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{} ] where i is Element of NAT : verum } or u in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) by S, XBOOLE_0:def 3;
suppose S: u in ({[0 ,{} ,{} ]} \/ { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{} ] where i is Element of NAT : verum } ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
per cases ( u in {[0 ,{} ,{} ]} \/ { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or u in { [6,<*i*>,{} ] where i is Element of NAT : verum } ) by S, XBOOLE_0:def 3;
suppose S: u in {[0 ,{} ,{} ]} \/ { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
per cases ( u in {[0 ,{} ,{} ]} or u in { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) by S, XBOOLE_0:def 3;
suppose u in { [I,{} ,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that
W: ( u = [I,{} ,<*a,b*>] & I in {1,2,3,4} ) ;
( I in NAT & <*a,b*> in proj2 (SCM-Instr S) ) by W, Z, RELAT_1:def 5;
hence u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):] by W, MCART_1:73, X; :: thesis: verum
end;
end;
end;
suppose u in { [6,<*i*>,{} ] where i is Element of NAT : verum } ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
then consider i being Element of NAT such that
W: u = [6,<*i*>,{} ] ;
X: <*i*> in NAT * by FUNCT_7:20;
( 6 in NAT & {} in proj2 (SCM-Instr S) ) by W, Z, RELAT_1:def 5;
hence u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):] by W, MCART_1:73, X; :: thesis: verum
end;
end;
end;
suppose u in { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
then consider i being Element of NAT , a being Element of SCM-Data-Loc such that
W: u = [7,<*i*>,<*a*>] ;
X: <*i*> in NAT * by FUNCT_7:20;
( 7 in NAT & <*a*> in proj2 (SCM-Instr S) ) by W, Z, RELAT_1:def 5;
hence u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):] by W, MCART_1:73, X; :: thesis: verum
end;
end;
end;
suppose u in { [5,{} ,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ; :: thesis: u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):]
then consider a being Element of SCM-Data-Loc , r being Element of S such that
W: u = [5,{} ,<*a,r*>] ;
( 5 in NAT & <*a,r*> in proj2 (SCM-Instr S) ) by W, Z, RELAT_1:def 5;
hence u in [:NAT ,(NAT * ),(proj2 (SCM-Instr S)):] by W, MCART_1:73, X; :: thesis: verum
end;
end;