let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being non-empty b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds
vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds
vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis: for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds
vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds
vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)
let I be integer SortSymbol of S; :: thesis: for i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds
vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)
let i be pure Element of the generators of G . I; :: thesis: for M being pure Element of the generators of G . (the_array_sort_of S) st not T is array-degenerated holds
vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)
let M be pure Element of the generators of G . (the_array_sort_of S); :: thesis: ( not T is array-degenerated implies vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M) )
set t = (@ M) . (@ i);
assume A1: not T is array-degenerated ; :: thesis: vf ((@ M) . (@ i)) = (I -singleton i) (\/) ((the_array_sort_of S) -singleton M)
reconsider N = M as Element of (FreeGen T) . (the_array_sort_of S) by Def4;
@ N = @ M ;
then A2: (@ M) . (@ i) = (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,i*> by A1;
A3: ( <*M,i*> . (0 + 1) = M & <*M,i*> . (1 + 1) = i & len <*M,i*> = 2 ) by FINSEQ_1:44;
then A4: ( ((@ M) . (@ i)) | <*0*> = M & ((@ M) . (@ i)) | <*1*> = i ) by A2, TREES_4:def 4;
M in (FreeGen T) . (the_array_sort_of S) by Def4;
then M in FreeGen ((the_array_sort_of S),X) by MSAFREE:def 16;
then consider m being set such that
A5: ( m in X . (the_array_sort_of S) & M = root-tree [m,(the_array_sort_of S)] ) by MSAFREE:def 15;
i in (FreeGen T) . I by Def4;
then i in FreeGen (I,X) by MSAFREE:def 16;
then consider j being set such that
A6: ( j in X . I & i = root-tree [j,I] ) by MSAFREE:def 15;
( (((@ M) . (@ i)) | <*0*>) . {} = [m,(the_array_sort_of S)] & (((@ M) . (@ i)) | <*1*>) . {} = [j,I] ) by A4, A5, A6, TREES_4:3;
then A7: ( ((((@ M) . (@ i)) | <*0*>) . {}) `2 = the_array_sort_of S & ((((@ M) . (@ i)) | <*1*>) . {}) `2 = I ) ;
( {} in dom (root-tree [m,(the_array_sort_of S)]) & {} in dom (root-tree [j,I]) ) by TREES_1:22;
then ( <*0*> ^ {} in dom ((@ M) . (@ i)) & <*1*> ^ {} in dom ((@ M) . (@ i)) ) by A2, A5, A6, A3, TREES_4:11;
then A8: ( <*0*> in dom ((@ M) . (@ i)) & <*1*> in dom ((@ M) . (@ i)) ) by FINSEQ_1:34;
A9: the_array_sort_of S <> I by Th73;
A10: {M} = (vf ((@ M) . (@ i))) . (the_array_sort_of S)

proof

set A = { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = the_array_sort_of S } ;
A11: ( M in { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = the_array_sort_of S } & { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = the_array_sort_of S } = (vf ((@ M) . (@ i))) . (the_array_sort_of S) ) by A4, A7, A8, AOFA_A00:def 12;
hence {M} c= (vf ((@ M) . (@ i))) . (the_array_sort_of S) by ZFMISC_1:31; :: according to XBOOLE_0:def 10 :: thesis: (vf ((@ M) . (@ i))) . (the_array_sort_of S) c= {M}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (vf ((@ M) . (@ i))) . (the_array_sort_of S) or x in {M} )
assume x in (vf ((@ M) . (@ i))) . (the_array_sort_of S) ; :: thesis: x in {M}
then consider p being Element of dom ((@ M) . (@ i)) such that
A12: ( x = ((@ M) . (@ i)) | p & ((((@ M) . (@ i)) | p) . {}) `2 = the_array_sort_of S ) by A11;

per cases ( p = {} or ex k being Nat ex T being DecoratedTree ex q being Node of T st
( k < len <*M,i*> & T = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ) by A2, TREES_4:11;

suppose p = {} ; :: thesis: x in {M}

then ((@ M) . (@ i)) | p = (@ M) . (@ i) by TREES_9:1;
then (((@ M) . (@ i)) | p) . {} = Sym ((In (( the connectives of S . 11), the carrier' of S)),X) by A2, TREES_4:def 4
.= [(In (( the connectives of S . 11), the carrier' of S)), the carrier of S] by MSAFREE:def 9 ;
then ( ((((@ M) . (@ i)) | p) . {}) `2 = the carrier of S & the_array_sort_of S in the carrier of S ) ;
hence x in {M} by A12; :: thesis: verum

end;

suppose ex k being Nat ex T being DecoratedTree ex q being Node of T st
( k < len <*M,i*> & T = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ; :: thesis: x in {M}

then consider k being Nat, Q being DecoratedTree, q being Element of dom Q such that
A13: ( k < len <*M,i*> & Q = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ;
A14: ( k = 0 or k = 1 ) by A3, A13, NAT_1:23;
then ( q in dom (root-tree [m,(the_array_sort_of S)]) or q in dom (root-tree [j,I]) ) by A13, A5, A6;
then q in {{}} by TREES_4:3, TREES_1:29;
then q = {} by TARSKI:def 1;
then p = <*0*> by A12, A14, A9, A7, A13, FINSEQ_1:34;
hence x in {M} by A12, A4, TARSKI:def 1; :: thesis: verum

end;

end;

end;

A15: {i} = (vf ((@ M) . (@ i))) . I

proof

set A = { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = I } ;
A16: ( i in { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = I } & { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = I } = (vf ((@ M) . (@ i))) . I ) by A4, A7, A8, AOFA_A00:def 12;
hence {i} c= (vf ((@ M) . (@ i))) . I by ZFMISC_1:31; :: according to XBOOLE_0:def 10 :: thesis: (vf ((@ M) . (@ i))) . I c= {i}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (vf ((@ M) . (@ i))) . I or x in {i} )
assume x in (vf ((@ M) . (@ i))) . I ; :: thesis: x in {i}
then consider p being Element of dom ((@ M) . (@ i)) such that
A17: ( x = ((@ M) . (@ i)) | p & ((((@ M) . (@ i)) | p) . {}) `2 = I ) by A16;

per cases ( p = {} or ex k being Nat ex T being DecoratedTree ex q being Node of T st
( k < len <*M,i*> & T = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ) by A2, TREES_4:11;

suppose p = {} ; :: thesis: x in {i}

then ((@ M) . (@ i)) | p = (@ M) . (@ i) by TREES_9:1;
then (((@ M) . (@ i)) | p) . {} = Sym ((In (( the connectives of S . 11), the carrier' of S)),X) by A2, TREES_4:def 4
.= [(In (( the connectives of S . 11), the carrier' of S)), the carrier of S] by MSAFREE:def 9 ;
then ( ((((@ M) . (@ i)) | p) . {}) `2 = the carrier of S & I in the carrier of S ) ;
hence x in {i} by A17; :: thesis: verum

end;

suppose ex k being Nat ex T being DecoratedTree ex q being Node of T st
( k < len <*M,i*> & T = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ; :: thesis: x in {i}

then consider k being Nat, Q being DecoratedTree, q being Element of dom Q such that
A18: ( k < len <*M,i*> & Q = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ;
A19: ( k = 0 or k = 1 ) by A3, A18, NAT_1:23;
then ( q in dom (root-tree [m,(the_array_sort_of S)]) or q in dom (root-tree [j,I]) ) by A18, A5, A6;
then q in {{}} by TREES_4:3, TREES_1:29;
then q = {} by TARSKI:def 1;
then p = <*1*> by A17, A19, A9, A7, A18, FINSEQ_1:34;
hence x in {i} by A17, A4, TARSKI:def 1; :: thesis: verum

end;

end;

end;

A20: for s being SortSymbol of S st s <> the_array_sort_of S & s <> I holds
{} = (vf ((@ M) . (@ i))) . s

proof

let s be SortSymbol of S; :: thesis: ( s <> the_array_sort_of S & s <> I implies {} = (vf ((@ M) . (@ i))) . s )
assume A21: s <> the_array_sort_of S ; :: thesis: ( not s <> I or {} = (vf ((@ M) . (@ i))) . s )
assume A22: s <> I ; :: thesis: {} = (vf ((@ M) . (@ i))) . s
set A = { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = s } ;
A23: { (((@ M) . (@ i)) | p) where p is Element of dom ((@ M) . (@ i)) : ((((@ M) . (@ i)) | p) . {}) `2 = s } = (vf ((@ M) . (@ i))) . s by AOFA_A00:def 12;
thus {} c= (vf ((@ M) . (@ i))) . s ; :: according to XBOOLE_0:def 10 :: thesis: (vf ((@ M) . (@ i))) . s c= {}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (vf ((@ M) . (@ i))) . s or x in {} )
assume x in (vf ((@ M) . (@ i))) . s ; :: thesis: x in {}
then consider p being Element of dom ((@ M) . (@ i)) such that
A24: ( x = ((@ M) . (@ i)) | p & ((((@ M) . (@ i)) | p) . {}) `2 = s ) by A23;

per cases ( p = {} or ex k being Nat ex T being DecoratedTree ex q being Node of T st
( k < len <*M,i*> & T = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ) by A2, TREES_4:11;

suppose p = {} ; :: thesis: x in {}

then ((@ M) . (@ i)) | p = (@ M) . (@ i) by TREES_9:1;
then (((@ M) . (@ i)) | p) . {} = Sym ((In (( the connectives of S . 11), the carrier' of S)),X) by A2, TREES_4:def 4
.= [(In (( the connectives of S . 11), the carrier' of S)), the carrier of S] by MSAFREE:def 9 ;
then ( ((((@ M) . (@ i)) | p) . {}) `2 = the carrier of S & s in the carrier of S ) ;
hence x in {} by A24; :: thesis: verum

end;

suppose ex k being Nat ex T being DecoratedTree ex q being Node of T st
( k < len <*M,i*> & T = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ; :: thesis: x in {}

then consider k being Nat, Q being DecoratedTree, q being Element of dom Q such that
A25: ( k < len <*M,i*> & Q = <*M,i*> . (k + 1) & p = <*k*> ^ q ) ;
A26: ( k = 0 or k = 1 ) by A3, A25, NAT_1:23;
then ( q in dom (root-tree [m,(the_array_sort_of S)]) or q in dom (root-tree [j,I]) ) by A25, A5, A6;
then q in {{}} by TREES_4:3, TREES_1:29;
then q = {} by TARSKI:def 1;
hence x in {} by A24, A26, A7, A21, A22, A25, FINSEQ_1:34; :: thesis: verum

end;

end;

end;

let a be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: (vf ((@ M) . (@ i))) . a = ((I -singleton i) (\/) ((the_array_sort_of S) -singleton M)) . a

per cases ( a = the_array_sort_of S or a = I or ( a <> the_array_sort_of S & a <> I ) ) ;

suppose A27: a = the_array_sort_of S ; :: thesis: (vf ((@ M) . (@ i))) . a = ((I -singleton i) (\/) ((the_array_sort_of S) -singleton M)) . a

thus (vf ((@ M) . (@ i))) . a = {} \/ (((the_array_sort_of S) -singleton M) . a) by A10, A27, AOFA_A00:6
.= ((I -singleton i) . a) \/ (((the_array_sort_of S) -singleton M) . a) by A27, A9, AOFA_A00:6
.= ((I -singleton i) (\/) ((the_array_sort_of S) -singleton M)) . a by PBOOLE:def 4 ; :: thesis: verum

end;

suppose A28: a = I ; :: thesis: (vf ((@ M) . (@ i))) . a = ((I -singleton i) (\/) ((the_array_sort_of S) -singleton M)) . a

hence (vf ((@ M) . (@ i))) . a = ((I -singleton i) . a) \/ {} by A15, AOFA_A00:6
.= ((I -singleton i) . a) \/ (((the_array_sort_of S) -singleton M) . a) by A28, Th73, AOFA_A00:6
.= ((I -singleton i) (\/) ((the_array_sort_of S) -singleton M)) . a by PBOOLE:def 4 ;
:: thesis: verum

end;

suppose A29: ( a <> the_array_sort_of S & a <> I ) ; :: thesis: (vf ((@ M) . (@ i))) . a = ((I -singleton i) (\/) ((the_array_sort_of S) -singleton M)) . a

hence (vf ((@ M) . (@ i))) . a = {} by A20
.= ((I -singleton i) . a) \/ {} by A29, AOFA_A00:6
.= ((I -singleton i) . a) \/ (((the_array_sort_of S) -singleton M) . a) by A29, AOFA_A00:6
.= ((I -singleton i) (\/) ((the_array_sort_of S) -singleton M)) . a by PBOOLE:def 4 ;
:: thesis: verum

end;

end;