:: ARMSTRNG semantic presentation

E1: now
let c1 be Nat;
let c2 be non empty set ;
let c3 be Tuple of c1,c2;
len c3 = c1 by FINSEQ_2:109;
hence dom c3 = Seg c1 by FINSEQ_1:def 3;
end;

theorem E2: :: ARMSTRNG:1
for b1 being set holds
( b1 is (B2) implies for b2 being set
for b3 being finite Subset-Family of b2 holds
( ( b2 in b1 & b3 c= b1 ) implies ( Intersect b3 in b1 ) ) )
proof
let c1 be set ;
assume E3: c1 is (B2) ;
let c2 be set ;
let c3 be finite Subset-Family of c2;
assume that E4: c2 in c1
and E5: c3 c= c1 ;
defpred S1[ set ] means for b1 being Subset-Family of c2 holds
( b1 = a1 implies Intersect b1 in c1 );
E6: c3 is finite ;
E7: S1[ {} ] by E4, SETFAM_1:def 10;
E8: now
let c4, c5 be set ;
assume that E9: c4 in c3
and E10: c5 c= c3
and E11: S1[c5] ;
thus S1[c5 \/ {c4}]
proof
let c6 be Subset-Family of c2;
assume E12: c6 = c5 \/ {c4} ;
reconsider c7 = c4 as Subset of c2 by E9;
c5 c= bool c2 by E10, XBOOLE_1:1;
then reconsider c8 = c5 as Subset-Family of c2 ;
{c4} c= bool c2 by E9, ZFMISC_1:37;
then reconsider c9 = {c4} as Subset-Family of c2 ;
E13: Intersect c8 in c1 by E11;
Intersect (c8 \/ c9) = (Intersect c8) /\ (Intersect c9) by MSSUBFAM:8
.= (Intersect c8) /\ c7 by MSSUBFAM:9 ;
hence Intersect c6 in c1 by E3, E5, E9, E12, E13, FINSUB_1:def 2;
end;
end;
S1[c3] from FINSET_1:sch 2(E6, E7, E8);
 hence Intersect c3 in c1 ;
end;

registration
cluster non empty reflexive antisymmetric transitive set ;
existence
ex b1 being Relation st
( b1 is reflexive & b1 is antisymmetric & b1 is (F2) & b1 is (C1) )
proof
set c1 = {[{} ,{} ]};
reconsider c2 = {[{} ,{} ]} as Relation by RELAT_1:4;
E3: field c2 = {{} ,{} } by RELAT_1:32
.= {{} } by ENUMSET1:69 ;
take c2 ;
thus c2 is reflexive
proof
let c3 be set ; :: uses RELAT_2:def 1,RELAT_2:def 9
assume c3 in field c2 ;
then c3 = {} by E3, TARSKI:def 1;
hence [c3,c3] in c2 by TARSKI:def 1;
end;
thus c2 is antisymmetric
proof
let c3, c4 be set ; :: uses RELAT_2:def 4,RELAT_2:def 12
assume ( c3 in field c2 & c4 in field c2 & [c3,c4] in c2 & [c4,c3] in c2 ) ;
then ( c3 = {} & c4 = {} ) by E3, TARSKI:def 1;
hence c3 = c4 ;
end;
thus c2 is (F2)
proof
let c3, c4, c5 be set ; :: uses RELAT_2:def 8,RELAT_2:def 16
assume ( c3 in field c2 & c4 in field c2 & c5 in field c2 & [c3,c4] in c2 & [c4,c5] in c2 ) ;
then ( c3 = {} & c5 = {} ) by E3, TARSKI:def 1;
hence [c3,c5] in c2 by TARSKI:def 1;
end;
thus c2 is (C1) ;
end;
end;

theorem E3: :: ARMSTRNG:2
for b1 being non empty antisymmetric transitive Relation
for b2 being finite Subset of (field b1) holds
not ( b2 <> {} & for b3 being Element of b2 holds
not b3 is_maximal_wrt b2,b1 )
proof
let c1 be non empty antisymmetric transitive Relation;
let c2 be finite Subset of (field c1);
assume E4: c2 <> {} ;
reconsider c3 = c1 as Relation of field c1 by POLYNOM1:4;
set c4 = RelStr (field c1),c3;
set c5 = the carrier of (RelStr (field c1),c3);
set c6 = the InternalRel of (RelStr (field c1),c3);
E5: the carrier of (RelStr (field c1),c3) is (C1) by E4, XBOOLE_1:3;
E6: c1 is_antisymmetric_in field c1 by RELAT_2:def 12;
E7: RelStr (field c1),c3 is antisymmetric
proof
let c7, c8 be Element of (RelStr (field c1),c3); :: uses YELLOW_0:def 3
assume ( c7 <= c8 & c8 <= c7 ) ;
then ( [c7,c8] in the InternalRel of (RelStr (field c1),c3) & [c8,c7] in the InternalRel of (RelStr (field c1),c3) ) by ORDERS_2:def 9;
hence c7 = c8 by E5, E6, RELAT_2:def 4;
end;
E8: c1 is_transitive_in field c1 by RELAT_2:def 16;
RelStr (field c1),c3 is transitive
proof
let c7, c8, c9 be Element of (RelStr (field c1),c3); :: uses YELLOW_0:def 2
assume ( c7 <= c8 & c8 <= c9 ) ;
then ( [c7,c8] in the InternalRel of (RelStr (field c1),c3) & [c8,c9] in the InternalRel of (RelStr (field c1),c3) ) by ORDERS_2:def 9;
then [c7,c9] in the InternalRel of (RelStr (field c1),c3) by E5, E8, RELAT_2:def 8;
hence c7 <= c9 by ORDERS_2:def 9;
end;
then reconsider c7 = RelStr (field c1),c3 as non empty transitive antisymmetric RelStr by E5, E7, STRUCT_0:def 1;
reconsider c8 = c2 as finite Subset of the carrier of (RelStr (field c1),c3) ;
consider c9 being Element of c7 such that
E9: ( c9 in c8 & c9 is_maximal_wrt c8,the InternalRel of c7 ) by E4, BAGORDER:7;
reconsider c10 = c9 as Element of c2 by E9;
take c10 ;
thus c10 in c2 by E9; :: uses WAYBEL_4:def 24
given c11 being set such that E10: ( c11 in c2 & c11 <> c10 & [c10,c11] in c1 ) ;
thus not verum by E9, E10, WAYBEL_4:def 24;
end;

scheme :: ARMSTRNG:sch 1
s1{ F1() -> set , P1[ set ] } :
for b1, b2 being Subset of F1() holds
( ( for b3 being set holds
( b3 in b1 iff P1[b3] ) & for b3 being set holds
( b3 in b2 iff P1[b3] ) ) implies ( b1 = b2 ) )
provided
proof
let c1, c2 be Subset of F1();
assume that E4: for b1 being set holds
( b1 in c1 iff P1[b1] )
and E5: for b1 being set holds
( b1 in c2 iff P1[b1] ) ;
for b1 being set holds
( b1 in c1 iff b1 in c2 )
proof
let c3 be set ;
hereby
assume c3 in c1 ;
then P1[c3] by E4;
hence c3 in c2 by E5;
end; assume c3 in c2 ;
then P1[c3] by E5;
hence c3 in c1 by E4;
end;
hence c1 = c2 by TARSKI:2;
end;

definition
let c1 be set ;
let c2 be Relation;
func a2 Maximal_in a1 -> Subset of a1 means :E4: :: ARMSTRNG:def 1
for b1 being set holds
( b1 in a3 iff b1 is_maximal_wrt a1,a2 );
existence
ex b1 being Subset of c1 st
for b2 being set holds
( b2 in b1 iff b2 is_maximal_wrt c1,c2 )
proof
defpred S1[ set ] means a1 is_maximal_wrt c1,c2;
consider c3 being set such that
E4: for b1 being set holds
( b1 in c3 iff ( b1 in c1 & S1[b1] ) ) from XBOOLE_0:sch 1();
 for b1 being set holds
( b1 in c3 implies b1 in c1 ) by E4;
then reconsider c4 = c3 as Subset of c1 by TARSKI:def 3;
take c4 ;
let c5 be set ;
thus ( c5 in c4 implies c5 is_maximal_wrt c1,c2 ) by E4;
assume E5: c5 is_maximal_wrt c1,c2 ;
then c5 in c1 by WAYBEL_4:def 24;
hence c5 in c4 by E4, E5;
end;
uniqueness
for b1, b2 being Subset of c1 holds
( ( for b3 being set holds
( b3 in b1 iff b3 is_maximal_wrt c1,c2 ) & for b3 being set holds
( b3 in b2 iff b3 is_maximal_wrt c1,c2 ) ) implies ( b1 = b2 ) )
proof
defpred S1[ set ] means a1 is_maximal_wrt c1,c2;
thus for b1, b2 being Subset of c1 holds
( ( for b3 being set holds
( b3 in b1 iff S1[b3] ) & for b3 being set holds
( b3 in b2 iff S1[b3] ) ) implies ( b1 = b2 ) ) from ARMSTRNG:sch 1();
end;
end;

:: deftheorem E4 defines Maximal_in ARMSTRNG:def 1 :
for b1 being set
for b2 being Relation
for b3 being Subset of b1 holds
( b3 = b2 Maximal_in b1 iff for b4 being set holds
( b4 in b3 iff b4 is_maximal_wrt b1,b2 ) );

definition
let c1, c2 be set ;
pred a1 is_/\-irreducible_in a2 means :E5: :: ARMSTRNG:def 2
( a1 in a2 & for b1, b2 being set holds
not ( b1 in a2 & b2 in a2 & a1 = b1 /\ b2 & not a1 = b1 & not a1 = b2 ) );
end;

:: deftheorem E5 defines is_/\-irreducible_in ARMSTRNG:def 2 :
for b1, b2 being set holds
( b1 is_/\-irreducible_in b2 iff ( b1 in b2 & for b3, b4 being set holds
not ( b3 in b2 & b4 in b2 & b1 = b3 /\ b4 & not b1 = b3 & not b1 = b4 ) ) );

notation
let c1, c2 be set ;
end;

definition
let c1 be non empty set ;
func /\-IRR a1 -> Subset of a1 means :E6: :: ARMSTRNG:def 3
for b1 being set holds
( b1 in a2 iff b1 is_/\-irreducible_in a1 );
existence
ex b1 being Subset of c1 st
for b2 being set holds
( b2 in b1 iff b2 is_/\-irreducible_in c1 )
proof
set c2 = { b1 where B is Element of c1 : b1 is_/\-irreducible_in c1 } ;
{ b1 where B is Element of c1 : b1 is_/\-irreducible_in c1 } c= c1
proof
let c3 be set ; :: uses TARSKI:def 3
assume c3 in { b1 where B is Element of c1 : b1 is_/\-irreducible_in c1 } ;
then consider c4 being Element of c1 such that
E6: ( c3 = c4 & c4 is_/\-irreducible_in c1 ) ;
thus c3 in c1 by E6;
end;
then reconsider c3 = { b1 where B is Element of c1 : b1 is_/\-irreducible_in c1 } as Subset of c1 ;
take c3 ;
let c4 be set ;
hereby
assume c4 in c3 ;
then consider c5 being Element of c1 such that
E6: ( c4 = c5 & c5 is_/\-irreducible_in c1 ) ;
thus c4 is_/\-irreducible_in c1 by E6;
end; assume E6: c4 is_/\-irreducible_in c1 ;
then c4 in c1 by E5;
hence c4 in c3 by E6;
end;
uniqueness
for b1, b2 being Subset of c1 holds
( ( for b3 being set holds
( b3 in b1 iff b3 is_/\-irreducible_in c1 ) & for b3 being set holds
( b3 in b2 iff b3 is_/\-irreducible_in c1 ) ) implies ( b1 = b2 ) )
proof
defpred S1[ set ] means a1 is_/\-irreducible_in c1;
thus for b1, b2 being Subset of c1 holds
( ( for b3 being set holds
( b3 in b1 iff S1[b3] ) & for b3 being set holds
( b3 in b2 iff S1[b3] ) ) implies ( b1 = b2 ) ) from ARMSTRNG:sch 1();
end;
end;

:: deftheorem E6 defines /\-IRR ARMSTRNG:def 3 :
for b1 being non empty set
for b2 being Subset of b1 holds
( b2 = /\-IRR b1 iff for b3 being set holds
( b3 in b2 iff b3 is_/\-irreducible_in b1 ) );

scheme :: ARMSTRNG:sch 2
s2{ F1() -> non empty finite set , P1[ set ] } :
for b1 being set holds
( b1 in F1() implies P1[b1] )
provided
E7: for b1 being set holds
( b1 is_/\-irreducible_in F1() implies P1[b1] ) and E8: for b1, b2 being set holds
( ( b1 in F1() & b2 in F1() & P1[b1] & P1[b2] ) implies ( P1[b1 /\ b2] ) )
proof
deffunc H1( set ) -> set = { b1 where B is Element of F1() : a1 c= b1 } ;
given c1 being set such that E9: c1 in F1()
and E10: not P1[c1] ;
defpred S1[ Nat] means ex b1 being Element of F1() st
( Card H1(b1) = a1 & not P1[b1] );
H1(c1) c= F1()
proof
let c2 be set ; :: uses TARSKI:def 3
assume c2 in H1(c1) ;
then ex b1 being Element of F1() st
( c2 = b1 & c1 c= b1 ) ;
hence c2 in F1() ;
end;
then reconsider c2 = H1(c1) as finite set by FINSET_1:13;
E11: ex b1 being Nat st
S1[b1]
proof
take c3 = card c2;
reconsider c4 = c1 as Element of F1() by E9;
take c4 ;
thus Card H1(c4) = c3 ;
thus not P1[c4] by E10;
end;
consider c3 being Nat such that
E12: S1[c3]
and E13: for b1 being Nat holds
( S1[b1] implies c3 <= b1 ) from NAT_1:sch 5(E11);
 consider c4 being Element of F1() such that
E14: Card H1(c4) = c3
and E15: not P1[c4] by E12;
per cases not ( not c4 is_/\-irreducible_in F1() & not c4 is_/\-reducible_in F1() ) ;
suppose c4 is_/\-irreducible_in F1() ;
hence not verum by E7, E15;
end;
suppose c4 is_/\-reducible_in F1() ;
then consider c5, c6 being set such that
E16: ( c5 in F1() & c6 in F1() )
and E17: c4 = c5 /\ c6
and E18: ( c4 <> c5 & c4 <> c6 ) by E5;
E19: ( c4 c= c5 & c4 c= c6 ) by E17, XBOOLE_1:17;
H1(c4) c= F1()
proof
let c7 be set ; :: uses TARSKI:def 3
assume c7 in H1(c4) ;
then ex b1 being Element of F1() st
( c7 = b1 & c4 c= b1 ) ;
hence c7 in F1() ;
end;
then reconsider c7 = H1(c4) as finite set by FINSET_1:13;
H1(c6) c= F1()
proof
let c8 be set ; :: uses TARSKI:def 3
assume c8 in H1(c6) ;
then ex b1 being Element of F1() st
( c8 = b1 & c6 c= b1 ) ;
hence c8 in F1() ;
end;
then reconsider c8 = H1(c6) as finite set by FINSET_1:13;
H1(c5) c= F1()
proof
let c9 be set ; :: uses TARSKI:def 3
assume c9 in H1(c5) ;
then ex b1 being Element of F1() st
( c9 = b1 & c5 c= b1 ) ;
hence c9 in F1() ;
end;
then reconsider c9 = H1(c5) as finite set by FINSET_1:13;
reconsider c10 = c6, c11 = c5 as Element of F1() by E16;
E20: now
assume c4 in c9 ;
then ex b1 being Element of F1() st
( c4 = b1 & c11 c= b1 ) ;
hence not verum by E18, E19, XBOOLE_0:def 10;
end;
now
assume c4 in c8 ;
then ex b1 being Element of F1() st
( c4 = b1 & c10 c= b1 ) ;
hence not verum by E18, E19, XBOOLE_0:def 10;
end;
then E21: ( c9 <> c7 & c8 <> c7 ) by E20;
E22: c9 c= c7
proof
let c12 be set ; :: uses TARSKI:def 3
assume c12 in c9 ;
then consider c13 being Element of F1() such that
E23: c12 = c13
and E24: c11 c= c13 ;
c4 c= c13 by E19, E24, XBOOLE_1:1;
hence c12 in c7 by E23;
end;
c8 c= c7
proof
let c12 be set ; :: uses TARSKI:def 3
assume c12 in c8 ;
then consider c13 being Element of F1() such that
E23: c12 = c13
and E24: c10 c= c13 ;
c4 c= c13 by E19, E24, XBOOLE_1:1;
hence c12 in c7 by E23;
end;
then ( c9 c< c7 & c8 c< c7 ) by E21, E22, XBOOLE_0:def 8;
then ( card c7 > card c9 & card c7 > card c8 ) by TREES_1:24;
then ( P1[c11] & P1[c10] ) by E13, E14;
hence not verum by E8, E15, E17;
end;
end;
end;

theorem E7: :: ARMSTRNG:3
for b1 being non empty finite set
for b2 being Element of b1 holds
ex b3 being non empty Subset of b1 st
( b2 = meet b3 & for b4 being set holds
( b4 in b3 implies b4 is_/\-irreducible_in b1 ) )
proof
let c1 be non empty finite set ;
let c2 be Element of c1;
defpred S1[ set ] means ex b1 being non empty Subset of c1 st
( a1 = meet b1 & for b2 being set holds
( b2 in b1 implies b2 is_/\-irreducible_in c1 ) );
E8: now
let c3 be set ;
assume E9: c3 is_/\-irreducible_in c1 ;
thus S1[c3]
proof
c3 in c1 by E9, E5;
then reconsider c4 = {c3} as non empty Subset of c1 by ZFMISC_1:37;
take c4 ;
thus c3 = meet c4 by SETFAM_1:11;
let c5 be set ;
assume c5 in c4 ;
hence c5 is_/\-irreducible_in c1 by E9, TARSKI:def 1;
end;
end;
E9: now
let c3, c4 be set ;
assume that ( c3 in c1 & c4 in c1 )
and E10: S1[c3]
and E11: S1[c4] ;
consider c5 being non empty Subset of c1 such that
E12: c3 = meet c5
and E13: for b1 being set holds
( b1 in c5 implies b1 is_/\-irreducible_in c1 ) by E10;
consider c6 being non empty Subset of c1 such that
E14: c4 = meet c6
and E15: for b1 being set holds
( b1 in c6 implies b1 is_/\-irreducible_in c1 ) by E11;
reconsider c7 = c5 \/ c6 as non empty Subset of c1 ;
now
take c8 = c7;
thus c3 /\ c4 = meet c8 by E12, E14, SETFAM_1:10;
let c9 be set ;
assume E16: c9 in c8 ;
per cases ( c9 in c5 or c9 in c6 ) by E16, XBOOLE_0:def 2;
suppose c9 in c5 ;
hence c9 is_/\-irreducible_in c1 by E13;
end;
suppose c9 in c6 ;
hence c9 is_/\-irreducible_in c1 by E15;
end;
end;
end;
hence S1[c3 /\ c4] ;
end;
for b1 being set holds
( b1 in c1 implies S1[b1] ) from ARMSTRNG:sch 2(E8, E9);
 hence ex b1 being non empty Subset of c1 st
( c2 = meet b1 & for b2 being set holds
( b2 in b1 implies b2 is_/\-irreducible_in c1 ) ) ;
end;

definition
let c1 be set ;
let c2 be Subset-Family of c1;
attr a2 is (B1) means :E8: :: ARMSTRNG:def 4
a1 in a2;
end;

:: deftheorem E8 defines (B1) ARMSTRNG:def 4 :
for b1 being set
for b2 being Subset-Family of b1 holds
( b2 is (B1) iff b1 in b2 );

notation
let c1 be set ;
end;

registration
let c1 be set ;
cluster (B2) (B1) Element of bool (bool a1);
existence
ex b1 being Subset-Family of c1 st
( b1 is (B1) & b1 is (B2) )
proof
set c2 = {c1};
{c1} c= bool c1 by ZFMISC_1:80;
then reconsider c3 = {c1} as Subset-Family of c1 ;
take c3 ;
c1 in c3 by TARSKI:def 1;
hence c3 is (B1) by E8;
thus c3 is (B2)
proof
let c4, c5 be set ; :: uses FINSUB_1:def 2
assume ( c4 in c3 & c5 in c3 ) ;
then ( c4 = c1 & c5 = c1 ) by TARSKI:def 1;
hence c4 /\ c5 in c3 by TARSKI:def 1;
end;
end;
end;

theorem E9: :: ARMSTRNG:4
for b1 being set
for b2 being non empty Subset-Family of b1 holds
( b2 is (B2) implies for b3 being Element of b2 holds
( ( b3 is_/\-irreducible_in b2 ) implies ( not b3 <> b1 or for b4 being finite Subset-Family of b1 holds
( ( b4 c= b2 & b3 = Intersect b4 ) implies ( b3 in b4 ) ) ) ) )
proof
let c1 be set ;
let c2 be non empty Subset-Family of c1;
assume E10: c2 is (B2) ;
let c3 be Element of c2;
assume that E11: c3 is_/\-irreducible_in c2
and E12: c3 <> c1 ;
let c4 be finite Subset-Family of c1;
assume that E13: c4 c= c2
and E14: c3 = Intersect c4
and E15: not c3 in c4 ;
defpred S1[ set ] means not ( for b1, b2 being Element of c2 holds
not ( c3 <> b1 & c3 <> b2 & c3 = b1 /\ b2 ) & for b1 being Subset-Family of c1 holds
( not a1 = {} & not ( a1 <> {} & a1 = b1 & Intersect b1 <> c3 & Intersect b1 in c2 ) ) );
E16: c4 is finite ;
E17: S1[ {} ] ;
E18: now
let c5, c6 be set ;
assume that E19: c5 in c4
and c6 c= c4
and E20: S1[c6] ;
per cases not ( for b1, b2 being Element of c2 holds
not ( c3 <> b1 & c3 <> b2 & c3 = b1 /\ b2 ) & for b1 being Subset-Family of c1 holds
( not c6 = {} & not ( c6 = b1 & Intersect b1 <> c3 & Intersect b1 in c2 ) ) ) by E20;
suppose ex b1, b2 being Element of c2 st
( c3 <> b1 & c3 <> b2 & c3 = b1 /\ b2 ) ;
hence S1[c6 \/ {c5}] ;
end;
suppose not for b1 being Subset-Family of c1 holds
( not c6 = {} & not ( c6 = b1 & Intersect b1 <> c3 & Intersect b1 in c2 ) ) ;
then consider c7 being Subset-Family of c1 such that
E21: ( c6 = {} or ( c6 <> {} & c6 = c7 & Intersect c7 <> c3 & Intersect c7 in c2 ) ) ;
thus S1[c6 \/ {c5}]
proof
{c5} c= bool c1 by E19, ZFMISC_1:37;
then reconsider c8 = {c5} as Subset-Family of c1 ;
E22: Intersect c8 = meet c8 by SETFAM_1:def 10;
then E23: Intersect c8 = c5 by SETFAM_1:11;
per cases ( c6 = {} or ( c6 <> {} & c6 = c7 & Intersect c7 <> c3 & Intersect c7 in c2 ) ) by E21;
suppose c6 = {} ;
hence S1[c6 \/ {c5}] by E13, E15, E19, E23;
end;
suppose E24: ( c6 <> {} & c6 = c7 & Intersect c7 <> c3 & Intersect c7 in c2 ) ;
then c6 \/ c8 c= bool c1 by XBOOLE_1:8;
then reconsider c9 = c6 \/ c8 as non empty Subset-Family of c1 by XBOOLE_1:15;
E25: Intersect c7 = meet c7 by E24, SETFAM_1:def 10;
E26: Intersect c9 = meet c9 by SETFAM_1:def 10
.= (meet c6) /\ (meet c8) by E24, SETFAM_1:10 ;
thus S1[c6 \/ {c5}]
proof
per cases not ( not Intersect c9 <> c3 & not Intersect c9 = c3 ) ;
suppose E27: Intersect c9 <> c3 ;
Intersect c9 in c2 by E10, E13, E19, E22, E23, E24, E25, E26, FINSUB_1:def 2;
hence S1[c6 \/ {c5}] by E27;
end;
suppose Intersect c9 = c3 ;
hence S1[c6 \/ {c5}] by E13, E15, E19, E22, E23, E24, E25, E26;
end;
end;
end;
end;
end;
end;
end;
end;
end;
S1[c4] from FINSET_1:sch 2(E16, E17, E18);
 then consider c5 being Subset-Family of c1 such that
E19: ( c4 = {} or ( c4 = c5 & Intersect c5 <> c3 ) ) by E11, E5;
thus not verum by E12, E14, E19, SETFAM_1:def 10;
end;

registration
let c1, c2 be non empty set ;
let c3 be Nat;
cluster -> FinSequence-yielding Relation of a1,a3 -tuples_on a2;
coherence
for b1 being Function of c1,c3 -tuples_on c2 holds b1 is FinSequence-yielding
proof
let c4 be Function of c1,c3 -tuples_on c2;
let c5 be set ; :: uses MATRLIN:def 1
assume c5 in dom c4 ;
then reconsider c6 = c4 . c5 as Element of c3 -tuples_on c2 by FUNCT_2:7;
c6 = c4 . c5 ;
hence c4 . c5 is FinSequence ;
end;
end;

registration
let c1 be FinSequence-yielding Function;
let c2 be set ;
cluster a1 . a2 -> FinSequence-like ;
coherence
c1 . c2 is FinSequence-like
proof
per cases not ( not c2 in dom c1 & c2 in dom c1 ) ;
suppose c2 in dom c1 ;
hence c1 . c2 is FinSequence-like by MATRLIN:def 1;
end;
suppose not c2 in dom c1 ;
hence c1 . c2 is FinSequence-like by FUNCT_1:def 4;
end;
end;
end;
end;

definition
let c1 be Nat;
let c2, c3 be Tuple of c1,BOOLEAN ;
func a2 '&' a3 -> Tuple of a1,BOOLEAN means :E10: :: ARMSTRNG:def 5
for b1 being set holds
( b1 in Seg a1 implies a4 . b1 = (a2 /. b1) '&' (a3 /. b1) );
existence
ex b1 being Tuple of c1,BOOLEAN st
for b2 being set holds
( b2 in Seg c1 implies b1 . b2 = (c2 /. b2) '&' (c3 /. b2) )
proof
deffunc H1( set ) -> Element of BOOLEAN = (c2 /. a1) '&' (c3 /. a1);
consider c4 being FinSequence of BOOLEAN such that
E10: len c4 = c1
and E11: for b1 being Nat holds
( b1 in Seg c1 implies c4 . b1 = H1(b1) ) from FINSEQ_2:sch 1();
 E12: c1 -tuples_on BOOLEAN = { b1 where B is Element of BOOLEAN * : len b1 = c1 } by FINSEQ_2:def 4;
c4 in BOOLEAN * by FINSEQ_1:def 11;
then c4 in c1 -tuples_on BOOLEAN by E10, E12;
then reconsider c5 = c4 as Element of c1 -tuples_on BOOLEAN ;
take c5 ;
thus for b1 being set holds
( b1 in Seg c1 implies c5 . b1 = (c2 /. b1) '&' (c3 /. b1) ) by E11;
end;
uniqueness
for b1, b2 being Tuple of c1,BOOLEAN holds
( ( for b3 being set holds
( b3 in Seg c1 implies b1 . b3 = (c2 /. b3) '&' (c3 /. b3) ) & for b3 being set holds
( b3 in Seg c1 implies b2 . b3 = (c2 /. b3) '&' (c3 /. b3) ) ) implies ( b1 = b2 ) )
proof
let c4, c5 be Element of c1 -tuples_on BOOLEAN ;
assume that E10: for b1 being set holds
( b1 in Seg c1 implies c4 . b1 = (c2 /. b1) '&' (c3 /. b1) )
and E11: for b1 being set holds
( b1 in Seg c1 implies c5 . b1 = (c2 /. b1) '&' (c3 /. b1) ) ;
now
E12: dom c4 = Seg c1 by E1;
hence dom c4 = dom c5 by E1;
let c6 be set ;
assume E13: c6 in dom c4 ;
hence c4 . c6 = (c2 /. c6) '&' (c3 /. c6) by E10, E12
.= c5 . c6 by E11, E12, E13 ;

end;
hence c4 = c5 by FUNCT_1:9;
end;
commutativity
for b1, b2, b3 being Tuple of c1,BOOLEAN holds
( for b4 being set holds
( b4 in Seg c1 implies b1 . b4 = (b2 /. b4) '&' (b3 /. b4) ) implies for b4 being set holds
( b4 in Seg c1 implies b1 . b4 = (b3 /. b4) '&' (b2 /. b4) ) ) ;
end;

:: deftheorem E10 defines '&' ARMSTRNG:def 5 :
for b1 being Nat
for b2, b3, b4 being Tuple of b1,BOOLEAN holds
( b4 = b2 '&' b3 iff for b5 being set holds
( b5 in Seg b1 implies b4 . b5 = (b2 /. b5) '&' (b3 /. b5) ) );

theorem E11: :: ARMSTRNG:5
for b1 being Nat
for b2 being Tuple of b1,BOOLEAN holds (b1 -BinarySequence 0) '&' b2 = b1 -BinarySequence 0
proof
let c1 be Nat;
let c2 be Tuple of c1,BOOLEAN ;
set c3 = c1 -BinarySequence 0;
now
let c4 be set ;
E12: dom ((c1 -BinarySequence 0) '&' c2) = Seg c1 by E1;
hence dom ((c1 -BinarySequence 0) '&' c2) = dom (c1 -BinarySequence 0) by E1;
let c5 be set ;
assume E13: c5 in dom ((c1 -BinarySequence 0) '&' c2) ;
E14: dom (c1 -BinarySequence 0) = Seg c1 by E1;
E15: c1 -BinarySequence 0 = 0* c1 by BINARI_3:26
.= c1 |-> 0 by EUCLID:def 4 ;
then (c1 -BinarySequence 0) . c5 = 0 by E12, E13, FINSEQ_2:70;
then (c1 -BinarySequence 0) /. c5 = FALSE by E12, E13, E14, FINSEQ_4:def 4, MARGREL1:def 13;
hence ((c1 -BinarySequence 0) '&' c2) . c5 = FALSE '&' (c2 /. c5) by E12, E13, E10
.= FALSE by MARGREL1:49
.= (c1 -BinarySequence 0) . c5 by E12, E13, E15, FINSEQ_2:70, MARGREL1:def 13 ;

end;
hence (c1 -BinarySequence 0) '&' c2 = c1 -BinarySequence 0 by FUNCT_1:9;
end;

theorem :: ARMSTRNG:6
for b1 being Nat
for b2 being Tuple of b1,BOOLEAN holds ('not' (b1 -BinarySequence 0)) '&' b2 = b2
proof
let c1 be Nat;
let c2 be Tuple of c1,BOOLEAN ;
set c3 = c1 -BinarySequence 0;
set c4 = 'not' (c1 -BinarySequence 0);
now
let c5 be set ;
E12: dom (('not' (c1 -BinarySequence 0)) '&' c2) = Seg c1 by E1;
hence E13: dom (('not' (c1 -BinarySequence 0)) '&' c2) = dom c2 by E1;
let c6 be set ;
assume E14: c6 in dom (('not' (c1 -BinarySequence 0)) '&' c2) ;
E15: c1 -BinarySequence 0 = 0* c1 by BINARI_3:26
.= c1 |-> 0 by EUCLID:def 4 ;
E16: dom (c1 -BinarySequence 0) = Seg c1 by E1;
(c1 -BinarySequence 0) . c6 = 0 by E12, E14, E15, FINSEQ_2:70;
then E17: (c1 -BinarySequence 0) /. c6 = FALSE by E12, E14, E16, FINSEQ_4:def 4, MARGREL1:def 13;
('not' (c1 -BinarySequence 0)) /. c6 = 'not' ((c1 -BinarySequence 0) /. c6) by E12, E14, BINARITH:def 4
.= TRUE by E17, MARGREL1:def 16 ;
hence (('not' (c1 -BinarySequence 0)) '&' c2) . c6 = TRUE '&' (c2 /. c6) by E12, E14, E10
.= c2 /. c6 by MARGREL1:50
.= c2 . c6 by E13, E14, FINSEQ_4:def 4 ;

end;
hence ('not' (c1 -BinarySequence 0)) '&' c2 = c2 by FUNCT_1:9;
end;

theorem :: ARMSTRNG:7
canceled;

theorem E12: :: ARMSTRNG:8
for b1, b2 being Nat holds
( b2 < b1 implies ( (b1 -BinarySequence (2 to_power b2)) . (b2 + 1) = 1 & for b3 being Nat holds
( ( b3 in Seg b1 ) implies ( not b3 <> b2 + 1 or (b1 -BinarySequence (2 to_power b2)) . b3 = 0 ) ) ) )
proof
let c1, c2 be Nat;
assume E13: c2 < c1 ;
set c3 = c1 -BinarySequence (2 to_power c2);
deffunc H1( Nat) -> Element of a1 -tuples_on BOOLEAN = a1 -BinarySequence (2 to_power c2);
defpred S1[ Nat] means ( c2 < a1 implies H1(a1) . (c2 + 1) = TRUE );
E14: S1[0] ;
E15: now
let c4 be Nat;
assume E16: S1[c4] ;
now
assume c2 < c4 + 1 ;
then E17: c2 <= c4 by NAT_1:38;
per cases not ( not c4 = 0 & not ( c4 > 0 & c4 = c2 ) & not ( c4 > 0 & c4 > c2 ) ) by E17, REAL_1:def 5;
suppose E18: c4 = 0 ;
then E19: c2 = 0 by E17;
0* c4 = c4 |-> 0 by EUCLID:def 4;
then dom (0* c4) = Seg c4 by FINSEQ_2:68;
then E20: len (0* c4) = c4 by FINSEQ_1:def 3;
dom <*TRUE *> = Seg 1 by FINSEQ_1:55;
then E21: 1 in dom <*TRUE *> by FINSEQ_1:3;
thus H1(c4 + 1) . (c2 + 1) = ((0* c4) ^ <*TRUE *>) . (c2 + 1) by E18, E19, BINARI_3:29, MARGREL1:def 14
.= <*TRUE *> . 1 by E18, E19, E20, E21, FINSEQ_1:def 7
.= TRUE by FINSEQ_1:57 ;
end;
suppose E18: ( c4 > 0 & c4 = c2 ) ;
0* c4 = c4 |-> 0 by EUCLID:def 4;
then dom (0* c4) = Seg c4 by FINSEQ_2:68;
then E19: len (0* c4) = c4 by FINSEQ_1:def 3;
dom <*TRUE *> = Seg 1 by FINSEQ_1:55;
then E20: 1 in dom <*TRUE *> by FINSEQ_1:3;
thus H1(c4 + 1) . (c2 + 1) = ((0* c4) ^ <*TRUE *>) . (c2 + 1) by E18, BINARI_3:29, MARGREL1:def 14
.= <*TRUE *> . 1 by E18, E19, E20, FINSEQ_1:def 7
.= TRUE by FINSEQ_1:57 ;
end;
suppose E18: ( c4 > 0 & c4 > c2 ) ;
then reconsider c5 = c4 as non empty Nat ;
E19: 2 to_power c2 < 2 to_power c4 by E18, POWER:44;
E20: 0 + 1 <= c2 + 1 by XREAL_1:8;
c2 + 1 <= c4 by E18, NAT_1:38;
then c2 + 1 in Seg c4 by E20, FINSEQ_1:3;
then E21: c2 + 1 in dom H1(c4) by E1;
thus H1(c4 + 1) . (c2 + 1) = (H1(c5) ^ <*FALSE *>) . (c2 + 1) by E19, BINARI_3:28
.= TRUE by E16, E18, E21, FINSEQ_1:def 7 ;
end;
end;
end;
hence S1[c4 + 1] ;
end;
E16: for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E14, E15);
 defpred S2[ Nat] means ( c2 < a1 implies for b1 being Nat holds
( ( c2 + 1 <= b1 & b1 <= a1 ) implies ( H1(a1) . (b1 + 1) = FALSE ) ) );
E17: S2[0] ;
E18: now
let c4 be Nat;
assume E19: S2[c4] ;
now
assume E20: c2 < c4 + 1 ;
let c5 be Nat;
assume E21: ( c2 + 1 <= c5 & c5 <= c4 + 1 ) ;
E22: c2 <= c4 by E20, NAT_1:38;
E23: 0 + 1 <= c2 + 1 by XREAL_1:8;
per cases not ( not c4 = 0 & not ( c4 > 0 & c4 = c2 ) & not ( c4 > 0 & c4 > c2 ) ) by E22, REAL_1:def 5;
suppose E24: c4 = 0 ;
E25: dom H1(c4 + 1) = Seg (c4 + 1) by E1;
1 <= c5 by E21, E23, XREAL_1:2;
then c5 = 1 by E21, E24, XREAL_1:1;
then not c5 + 1 in dom H1(c4 + 1) by E24, E25, FINSEQ_1:3;
hence H1(c4 + 1) . (c5 + 1) = FALSE by FUNCT_1:def 4, MARGREL1:def 13;
end;
suppose E24: ( c4 > 0 & c4 = c2 ) ;
E25: dom H1(c4 + 1) = Seg (c4 + 1) by E1;
c5 + 1 > c4 + 1 by E21, E24, NAT_1:38;
then not c5 + 1 in dom H1(c4 + 1) by E25, FINSEQ_1:3;
hence H1(c4 + 1) . (c5 + 1) = FALSE by FUNCT_1:def 4, MARGREL1:def 13;
end;
suppose E24: ( c4 > 0 & c4 > c2 ) ;
then reconsider c6 = c4 as non empty Nat ;
E25: 2 to_power c2 < 2 to_power c4 by E24, POWER:44;
thus H1(c4 + 1) . (c5 + 1) = FALSE
proof
not ( not c5 < c4 + 1 & not c5 = c4 + 1 ) by E21, REAL_1:def 5;
then E26: ( c5 <= c4 or c5 = c4 + 1 ) by NAT_1:38;
per cases not ( not c5 = c4 + 1 & not c5 = c4 & not c5 < c4 ) by E26, REAL_1:def 5;
suppose E27: c5 = c4 + 1 ;
E28: dom H1(c4 + 1) = Seg (c4 + 1) by E1;
c5 + 1 > c4 + 1 by E27, NAT_1:38;
then not c5 + 1 in dom H1(c4 + 1) by E28, FINSEQ_1:3;
hence H1(c4 + 1) . (c5 + 1) = FALSE by FUNCT_1:def 4, MARGREL1:def 13;
end;
suppose E27: c5 = c4 ;
dom H1(c4) = Seg c4 by E1;
then E28: c5 = len H1(c4) by E27, FINSEQ_1:def 3;
dom <*FALSE *> = Seg 1 by FINSEQ_1:55;
then E29: 1 in dom <*FALSE *> by FINSEQ_1:3;
thus H1(c4 + 1) . (c5 + 1) = (H1(c6) ^ <*FALSE *>) . (c5 + 1) by E25, BINARI_3:28
.= <*FALSE *> . 1 by E28, E29, FINSEQ_1:def 7
.= FALSE by FINSEQ_1:57 ;
end;
suppose E27: c5 < c4 ;
E28: 1 <= c5 + 1 by NAT_1:37;
c5 + 1 <= c4 by E27, NAT_1:38;
then c5 + 1 in Seg c4 by E28, FINSEQ_1:3;
then E29: c5 + 1 in dom H1(c4) by E1;
thus H1(c4 + 1) . (c5 + 1) = (H1(c6) ^ <*FALSE *>) . (c5 + 1) by E25, BINARI_3:28
.= H1(c4) . (c5