let S be non empty 1-sorted ; SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
set X = proj2 (SCM-Instr S);
let u be object ; TARSKI:def 3 ( not u in SCM-Instr S or u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):] )
assume A1:
u in SCM-Instr S
; u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
A2:
{} in NAT *
by FINSEQ_1:49;
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 Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is 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 A1, XBOOLE_0:def 3;
suppose A3:
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 Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum }
;
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 Nat : verum } or u in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } )
by A3, XBOOLE_0:def 3;
suppose A4:
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 Nat : verum }
;
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 Nat : verum } )
by A4, XBOOLE_0:def 3;
suppose A5:
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} }
;
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 A5, 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} }
;
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 A7:
(
u = [I,{},<*a,b*>] &
I in {1,2,3,4} )
;
(
I in NAT &
<*a,b*> in proj2 (SCM-Instr S) )
by A7, A1, XTUPLE_0:def 13;
hence
u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
by A7, A2, MCART_1:69;
verum end; end; end; end; end; end; end; suppose
u in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum }
;
u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]then consider a being
Element of
SCM-Data-Loc ,
r being
Element of
S such that A12:
u = [5,{},<*a,r*>]
;
( 5
in NAT &
<*a,r*> in proj2 (SCM-Instr S) )
by A12, A1, XTUPLE_0:def 13;
hence
u in [:NAT,(NAT *),(proj2 (SCM-Instr S)):]
by A12, A2, MCART_1:69;
verum end; end;