A1:
SCM-Memory c= (union {INT }) \/ SCM-Memory
by XBOOLE_1:7;
A2:
{ [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } or x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] )
assume
x in { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} }
;
:: thesis: x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
then consider I being
Element of
Segm 9,
b,
c being
Element of
SCM-Data-Loc such that A3:
(
x = [I,<*b,c*>] &
I in {1,2,3,4,5} )
;
reconsider b =
b,
c =
c as
Element of
(union {INT }) \/ SCM-Memory by A1, TARSKI:def 3;
<*b,c*> in ((union {INT }) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A3, ZFMISC_1:106;
:: thesis: verum
end;
A4:
{ [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } or x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] )
assume
x in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 }
;
:: thesis: x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
then consider J being
Element of
Segm 9,
a being
Element of
NAT such that A5:
(
x = [J,<*a*>] &
J = 6 )
;
reconsider a =
a as
Element of
(union {INT }) \/ SCM-Memory by A1, TARSKI:def 3;
<*a*> in ((union {INT }) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A5, ZFMISC_1:106;
:: thesis: verum
end;
A6:
{ [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] )
assume
x in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} }
;
:: thesis: x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
then consider K being
Element of
Segm 9,
a1 being
Element of
NAT ,
b1 being
Element of
SCM-Data-Loc such that A7:
(
x = [K,<*a1,b1*>] &
K in {7,8} )
;
reconsider b1 =
b1,
a1 =
a1 as
Element of
(union {INT }) \/ SCM-Memory by A1, TARSKI:def 3;
<*a1,b1*> in ((union {INT }) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A7, ZFMISC_1:106;
:: thesis: verum
end;
( SCM-Halt in Segm 9 & {} in ((union {INT }) \/ SCM-Memory ) * )
by FINSEQ_1:66;
then
[SCM-Halt ,{} ] in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by ZFMISC_1:106;
then
{[SCM-Halt ,{} ]} c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by ZFMISC_1:37;
then
{[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A4, XBOOLE_1:8;
then
({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A6, XBOOLE_1:8;
hence
(({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } is Subset of [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A2, XBOOLE_1:8; :: thesis: verum