:: NAT_LAT semantic presentation

definition
canceled;
canceled;
func hcflat -> BinOp of NAT means :Def3: :: NAT_LAT:def 3
for b1, b2 being Nat holds a1 . b1,b2 = b1 hcf b2;
existence
ex b1 being BinOp of NAT st
for b2, b3 being Nat holds b1 . b2,b3 = b2 hcf b3
proof end;
uniqueness
for b1, b2 being BinOp of NAT st ( for b3, b4 being Nat holds b1 . b3,b4 = b3 hcf b4 ) & ( for b3, b4 being Nat holds b2 . b3,b4 = b3 hcf b4 ) holds
b1 = b2
proof end;
func lcmlat -> BinOp of NAT means :Def4: :: NAT_LAT:def 4
for b1, b2 being Nat holds a1 . b1,b2 = b1 lcm b2;
existence
ex b1 being BinOp of NAT st
for b2, b3 being Nat holds b1 . b2,b3 = b2 lcm b3
proof end;
uniqueness
for b1, b2 being BinOp of NAT st ( for b3, b4 being Nat holds b1 . b3,b4 = b3 lcm b4 ) & ( for b3, b4 being Nat holds b2 . b3,b4 = b3 lcm b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 NAT_LAT:def 1 :
canceled;

:: deftheorem Def2 NAT_LAT:def 2 :
canceled;

:: deftheorem Def3 defines hcflat NAT_LAT:def 3 :
for b1 being BinOp of NAT holds
( b1 = hcflat iff for b2, b3 being Nat holds b1 . b2,b3 = b2 hcf b3 );

:: deftheorem Def4 defines lcmlat NAT_LAT:def 4 :
for b1 being BinOp of NAT holds
( b1 = lcmlat iff for b2, b3 being Nat holds b1 . b2,b3 = b2 lcm b3 );

definition
let c1 be Element of LattStr(# NAT ,lcmlat ,hcflat #);
func @ c1 -> Nat equals :: NAT_LAT:def 5
a1;
coherence
c1 is Nat ;
end;

:: deftheorem Def5 defines @ NAT_LAT:def 5 :
for b1 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds @ b1 = b1;

theorem Th1: :: NAT_LAT:1
canceled;

theorem Th2: :: NAT_LAT:2
canceled;

theorem Th3: :: NAT_LAT:3
canceled;

theorem Th4: :: NAT_LAT:4
canceled;

theorem Th5: :: NAT_LAT:5
canceled;

theorem Th6: :: NAT_LAT:6
canceled;

theorem Th7: :: NAT_LAT:7
canceled;

theorem Th8: :: NAT_LAT:8
canceled;

theorem Th9: :: NAT_LAT:9
canceled;

theorem Th10: :: NAT_LAT:10
canceled;

theorem Th11: :: NAT_LAT:11
canceled;

theorem Th12: :: NAT_LAT:12
canceled;

theorem Th13: :: NAT_LAT:13
canceled;

theorem Th14: :: NAT_LAT:14
canceled;

theorem Th15: :: NAT_LAT:15
canceled;

theorem Th16: :: NAT_LAT:16
canceled;

theorem Th17: :: NAT_LAT:17
canceled;

theorem Th18: :: NAT_LAT:18
canceled;

theorem Th19: :: NAT_LAT:19
canceled;

theorem Th20: :: NAT_LAT:20
canceled;

theorem Th21: :: NAT_LAT:21
canceled;

theorem Th22: :: NAT_LAT:22
canceled;

theorem Th23: :: NAT_LAT:23
canceled;

theorem Th24: :: NAT_LAT:24
canceled;

theorem Th25: :: NAT_LAT:25
canceled;

theorem Th26: :: NAT_LAT:26
canceled;

theorem Th27: :: NAT_LAT:27
canceled;

theorem Th28: :: NAT_LAT:28
canceled;

theorem Th29: :: NAT_LAT:29
canceled;

theorem Th30: :: NAT_LAT:30
canceled;

theorem Th31: :: NAT_LAT:31
canceled;

theorem Th32: :: NAT_LAT:32
canceled;

theorem Th33: :: NAT_LAT:33
canceled;

theorem Th34: :: NAT_LAT:34
canceled;

theorem Th35: :: NAT_LAT:35
canceled;

theorem Th36: :: NAT_LAT:36
canceled;

theorem Th37: :: NAT_LAT:37
canceled;

theorem Th38: :: NAT_LAT:38
canceled;

theorem Th39: :: NAT_LAT:39
canceled;

theorem Th40: :: NAT_LAT:40
canceled;

theorem Th41: :: NAT_LAT:41
canceled;

theorem Th42: :: NAT_LAT:42
canceled;

theorem Th43: :: NAT_LAT:43
canceled;

theorem Th44: :: NAT_LAT:44
canceled;

theorem Th45: :: NAT_LAT:45
canceled;

theorem Th46: :: NAT_LAT:46
canceled;

theorem Th47: :: NAT_LAT:47
canceled;

theorem Th48: :: NAT_LAT:48
for b1, b2 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds b1 "\/" b2 = (@ b1) lcm (@ b2) by Def4;

theorem Th49: :: NAT_LAT:49
for b1, b2 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds b1 "/\" b2 = (@ b1) hcf (@ b2) by Def3;

Lemma5: for b1, b2 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds b1 "\/" b2 = b2 "\/" b1
proof end;

Lemma6: for b1, b2 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds b1 "/\" b2 = b2 "/\" b1
proof end;

Lemma7: for b1, b2, b3 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds b1 "/\" (b2 "/\" b3) = (b1 "/\" b2) "/\" b3
proof end;

Lemma8: for b1, b2, b3 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds b1 "\/" (b2 "\/" b3) = (b1 "\/" b2) "\/" b3
proof end;

Lemma9: for b1, b2 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds (b1 "/\" b2) "\/" b2 = b2
proof end;

Lemma10: for b1, b2 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds b1 "/\" (b1 "\/" b2) = b1
proof end;

theorem Th50: :: NAT_LAT:50
canceled;

theorem Th51: :: NAT_LAT:51
canceled;

theorem Th52: :: NAT_LAT:52
for b1, b2 being Element of LattStr(# NAT ,lcmlat ,hcflat #) st b1 [= b2 holds
@ b1 divides @ b2
proof end;

definition
func 0_NN -> Element of LattStr(# NAT ,lcmlat ,hcflat #) equals :: NAT_LAT:def 6
1;
coherence
1 is Element of LattStr(# NAT ,lcmlat ,hcflat #) ;
func 1_NN -> Element of LattStr(# NAT ,lcmlat ,hcflat #) equals :: NAT_LAT:def 7
0;
coherence
0 is Element of LattStr(# NAT ,lcmlat ,hcflat #) ;
end;

:: deftheorem Def6 defines 0_NN NAT_LAT:def 6 :
0_NN = 1;

:: deftheorem Def7 defines 1_NN NAT_LAT:def 7 :
1_NN = 0;

theorem Th53: :: NAT_LAT:53
canceled;

theorem Th54: :: NAT_LAT:54
canceled;

theorem Th55: :: NAT_LAT:55
@ 0_NN = 1 ;

theorem Th56: :: NAT_LAT:56
for b1 being Element of LattStr(# NAT ,lcmlat ,hcflat #) holds
( 0_NN "/\" b1 = 0_NN & b1 "/\" 0_NN = 0_NN )
proof end;

definition
func Nat_Lattice -> Lattice equals :: NAT_LAT:def 8
 LattStr(# NAT ,lcmlat ,hcflat #);
coherence
LattStr(# NAT ,lcmlat ,hcflat #) is Lattice
proof end;
end;

:: deftheorem Def8 defines Nat_Lattice NAT_LAT:def 8 :
Nat_Lattice = LattStr(# NAT ,lcmlat ,hcflat #);

registration
cluster Nat_Lattice -> strict ;
coherence
Nat_Lattice is strict ;
end;

theorem Th57: :: NAT_LAT:57
canceled;

theorem Th58: :: NAT_LAT:58
canceled;

theorem Th59: :: NAT_LAT:59
canceled;

theorem Th60: :: NAT_LAT:60
Nat_Lattice is 0_Lattice by Th56, LATTICES:def 13;

theorem Th61: :: NAT_LAT:61
for b1, b2 being Element of Nat_Lattice holds lcmlat . b1,b2 = lcmlat . b2,b1
proof end;

theorem Th62: :: NAT_LAT:62
for b1, b2 being Element of Nat_Lattice holds hcflat . b1,b2 = hcflat . b2,b1
proof end;

theorem Th63: :: NAT_LAT:63
for b1, b2, b3 being Element of Nat_Lattice holds lcmlat . b1,(lcmlat . b2,b3) = lcmlat . (lcmlat . b1,b2),b3
proof end;

theorem Th64: :: NAT_LAT:64
for b1, b2, b3 being Element of Nat_Lattice holds
( lcmlat . b1,(lcmlat . b2,b3) = lcmlat . (lcmlat . b2,b1),b3 & lcmlat . b1,(lcmlat . b2,b3) = lcmlat . (lcmlat . b1,b3),b2 & lcmlat . b1,(lcmlat . b2,b3) = lcmlat . (lcmlat . b3,b2),b1 & lcmlat . b1,(lcmlat . b2,b3) = lcmlat . (lcmlat . b3,b1),b2 )
proof end;

theorem Th65: :: NAT_LAT:65
for b1, b2, b3 being Element of Nat_Lattice holds hcflat . b1,(hcflat . b2,b3) = hcflat . (hcflat . b1,b2),b3
proof end;

theorem Th66: :: NAT_LAT:66
for b1, b2, b3 being Element of Nat_Lattice holds
( hcflat . b1,(hcflat . b2,b3) = hcflat . (hcflat . b2,b1),b3 & hcflat . b1,(hcflat . b2,b3) = hcflat . (hcflat . b1,b3),b2 & hcflat . b1,(hcflat . b2,b3) = hcflat . (hcflat . b3,b2),b1 & hcflat . b1,(hcflat . b2,b3) = hcflat . (hcflat . b3,b1),b2 )
proof end;

theorem Th67: :: NAT_LAT:67
for b1, b2 being Element of Nat_Lattice holds
( hcflat . b1,(lcmlat . b1,b2) = b1 & hcflat . (lcmlat . b2,b1),b1 = b1 & hcflat . b1,(lcmlat . b2,b1) = b1 & hcflat . (lcmlat . b1,b2),b1 = b1 )
proof end;

theorem Th68: :: NAT_LAT:68
for b1, b2 being Element of Nat_Lattice holds
( lcmlat . b1,(hcflat . b1,b2) = b1 & lcmlat . (hcflat . b2,b1),b1 = b1 & lcmlat . b1,(hcflat . b2,b1) = b1 & lcmlat . (hcflat . b1,b2),b1 = b1 )
proof end;

definition
func NATPLUS -> Subset of NAT means :Def9: :: NAT_LAT:def 9
for b1 being Nat holds
( b1 in a1 iff 0 < b1 );
existence
ex b1 being Subset of NAT st
for b2 being Nat holds
( b2 in b1 iff 0 < b2 )
proof end;
uniqueness
for b1, b2 being Subset of NAT st ( for b3 being Nat holds
( b3 in b1 iff 0 < b3 ) ) & ( for b3 being Nat holds
( b3 in b2 iff 0 < b3 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines NATPLUS NAT_LAT:def 9 :
for b1 being Subset of NAT holds
( b1 = NATPLUS iff for b2 being Nat holds
( b2 in b1 iff 0 < b2 ) );

registration
cluster NATPLUS -> non empty ;
coherence
not NATPLUS is empty
proof end;
end;

definition
let c1 be non empty set ;
let c2 be non empty Subset of c1;
let c3 be non empty Subset of c2;
redefine mode Element as Element of c3 -> Element of a2;
coherence
for b1 being Element of c3 holds b1 is Element of c2
proof end;
end;

registration
let c1 be Subset of REAL ;
cluster -> real Element of a1;
coherence
for b1 being Element of c1 holds b1 is real ;
end;

registration
let c1 be Subset of NAT ;
cluster -> real Element of a1;
coherence
for b1 being Element of c1 holds b1 is real ;
end;

definition
mode NatPlus is Element of NATPLUS ;
end;

definition
let c1 be Nat;
assume E18: c1 > 0 ;
func @ c1 -> Element of NATPLUS equals :Def10: :: NAT_LAT:def 10
a1;
coherence
c1 is Element of NATPLUS by E18, Def9;
end;

:: deftheorem Def10 defines @ NAT_LAT:def 10 :
for b1 being Nat st b1 > 0 holds
@ b1 = b1;

definition
let c1 be Element of NATPLUS ;
func @ c1 -> NatPlus equals :: NAT_LAT:def 11
a1;
coherence
c1 is NatPlus ;
end;

:: deftheorem Def11 defines @ NAT_LAT:def 11 :
for b1 being Element of NATPLUS holds @ b1 = b1;

definition
func hcflatplus -> BinOp of NATPLUS means :Def12: :: NAT_LAT:def 12
for b1, b2 being NatPlus holds a1 . b1,b2 = b1 hcf b2;
existence
ex b1 being BinOp of NATPLUS st
for b2, b3 being NatPlus holds b1 . b2,b3 = b2 hcf b3
proof end;
uniqueness
for b1, b2 being BinOp of NATPLUS st ( for b3, b4 being NatPlus holds b1 . b3,b4 = b3 hcf b4 ) & ( for b3, b4 being NatPlus holds b2 . b3,b4 = b3 hcf b4 ) holds
b1 = b2
proof end;
func lcmlatplus -> BinOp of NATPLUS means :Def13: :: NAT_LAT:def 13
for b1, b2 being NatPlus holds a1 . b1,b2 = b1 lcm b2;
existence
ex b1 being BinOp of NATPLUS st
for b2, b3 being NatPlus holds b1 . b2,b3 = b2 lcm b3
proof end;
uniqueness
for b1, b2 being BinOp of NATPLUS st ( for b3, b4 being NatPlus holds b1 . b3,b4 = b3 lcm b4 ) & ( for b3, b4 being NatPlus holds b2 . b3,b4 = b3 lcm b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines hcflatplus NAT_LAT:def 12 :
for b1 being BinOp of NATPLUS holds
( b1 = hcflatplus iff for b2, b3 being NatPlus holds b1 . b2,b3 = b2 hcf b3 );

:: deftheorem Def13 defines lcmlatplus NAT_LAT:def 13 :
for b1 being BinOp of NATPLUS holds
( b1 = lcmlatplus iff for b2, b3 being NatPlus holds b1 . b2,b3 = b2 lcm b3 );

definition
let c1 be Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #);
func @ c1 -> NatPlus equals :: NAT_LAT:def 14
a1;
coherence
c1 is NatPlus ;
end;

:: deftheorem Def14 defines @ NAT_LAT:def 14 :
for b1 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds @ b1 = b1;

theorem Th69: :: NAT_LAT:69
for b1, b2 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds b1 "\/" b2 = (@ b1) lcm (@ b2) by Def13;

theorem Th70: :: NAT_LAT:70
for b1, b2 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds b1 "/\" b2 = (@ b1) hcf (@ b2) by Def12;

Lemma23: for b1, b2 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds b1 "\/" b2 = b2 "\/" b1
proof end;

Lemma24: for b1, b2, b3 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds b1 "\/" (b2 "\/" b3) = (b1 "\/" b2) "\/" b3
proof end;

Lemma25: for b1, b2 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds (b1 "/\" b2) "\/" b2 = b2
proof end;

Lemma26: for b1, b2 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds b1 "/\" b2 = b2 "/\" b1
proof end;

Lemma27: for b1, b2, b3 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds b1 "/\" (b2 "/\" b3) = (b1 "/\" b2) "/\" b3
proof end;

Lemma28: for b1, b2 being Element of LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) holds b1 "/\" (b1 "\/" b2) = b1
proof end;

definition
func NatPlus_Lattice -> Lattice equals :: NAT_LAT:def 15
 LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #);
coherence
LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #) is Lattice
proof end;
end;

:: deftheorem Def15 defines NatPlus_Lattice NAT_LAT:def 15 :
NatPlus_Lattice = LattStr(# NATPLUS ,lcmlatplus ,hcflatplus #);

registration
cluster NatPlus_Lattice -> strict ;
coherence
NatPlus_Lattice is strict ;
end;

E29: now
let c1 be Lattice;
thus the L_join of c1 = the L_join of c1 || the carrier of c1
proof
[:the carrier of c1,the carrier of c1:] = dom the L_join of c1 by FUNCT_2:def 1;
hence the L_join of c1 = the L_join of c1 || the carrier of c1 by RELAT_1:97;
end;
thus the L_meet of c1 = the L_meet of c1 || the carrier of c1
proof
[:the carrier of c1,the carrier of c1:] = dom the L_meet of c1 by FUNCT_2:def 1;
hence the L_meet of c1 = the L_meet of c1 || the carrier of c1 by RELAT_1:97;
end;
end;

definition
let c1 be Lattice;
mode SubLattice of c1 -> Lattice means :Def16: :: NAT_LAT:def 16
( the carrier of a2 c= the carrier of a1 & the L_join of a2 = the L_join of a1 || the carrier of a2 & the L_meet of a2 = the L_meet of a1 || the carrier of a2 );
existence
ex b1 being Lattice st
( the carrier of b1 c= the carrier of c1 & the L_join of b1 = the L_join of c1 || the carrier of b1 & the L_meet of b1 = the L_meet of c1 || the carrier of b1 )
proof end;
end;

:: deftheorem Def16 defines SubLattice NAT_LAT:def 16 :
for b1, b2 being Lattice holds
( b2 is SubLattice of b1 iff ( the carrier of b2 c= the carrier of b1 & the L_join of b2 = the L_join of b1 || the carrier of b2 & the L_meet of b2 = the L_meet of b1 || the carrier of b2 ) );

registration
let c1 be Lattice;
cluster strict SubLattice of a1;
existence
ex b1 being SubLattice of c1 st b1 is strict
proof end;
end;

theorem Th71: :: NAT_LAT:71
canceled;

theorem Th72: :: NAT_LAT:72
canceled;

theorem Th73: :: NAT_LAT:73
canceled;

theorem Th74: :: NAT_LAT:74
canceled;

theorem Th75: :: NAT_LAT:75
for b1 being Lattice holds b1 is SubLattice of b1
proof end;

theorem Th76: :: NAT_LAT:76
NatPlus_Lattice is SubLattice of Nat_Lattice
proof end;