:: MARGREL1 semantic presentation

definition

let c₁, c₂ be non empty set ;
let c₃ be Element of c₁;
redefine func --> as c₂ --> c₃ -> Element of Funcs a₂,a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
attr a₁ is relation-like means :Def1: :: MARGREL1:def 1
( ( for b₁ being set st b₁ in a₁ holds
b₁ is FinSequence ) & ( for b₁, b₂ being FinSequence st b₁ in a₁ & b₂ in a₁ holds
len b₁ = len b₂ ) );

end;

:: deftheorem Def1 defines relation-like MARGREL1:def 1 :

registration

cluster relation-like set ;
existence

proof end;

end;

definition

mode relation is relation-like set ;

end;

theorem Th1: :: MARGREL1:1

canceled;

theorem Th2: :: MARGREL1:2

canceled;

theorem Th3: :: MARGREL1:3

canceled;

theorem Th4: :: MARGREL1:4

canceled;

theorem Th5: :: MARGREL1:5

canceled;

theorem Th6: :: MARGREL1:6

canceled;

theorem Th7: :: MARGREL1:7

for b₁ being set
for b₂ being relation st b₁ c= b₂ holds
b₁ is relation-like

proof end;

theorem Th8: :: MARGREL1:8

for b₁ being FinSequence holds {b₁} is relation-like

proof end;

scheme :: MARGREL1:sch 1
s1{ F₁() -> set , P₁[ FinSequence] } :

ex b₁ being relation st
for b₂ being FinSequence holds
( b₂ in b₁ iff ( b₂ in F₁() & P₁[b₂] ) )

provided

E2: for b₁, b₂ being FinSequence st P₁[b₁] & P₁[b₂] holds
len b₁ = len b₂

proof end;

definition

let c₁, c₂ be relation;
redefine pred c₁ = c₂ means :: MARGREL1:def 2
for b₁ being FinSequence holds
( b₁ in a₁ iff b₁ in a₂ );
compatibility

proof end;

end;

:: deftheorem Def2 defines = MARGREL1:def 2 :

registration

cluster {} -> relation-like ;
coherence

proof end;

end;

theorem Th9: :: MARGREL1:9

for b₁ being relation st ( for b₂ being FinSequence holds not b₂ in b₁ ) holds
b₁ = {}

proof end;

definition

let c₁ be relation;
assume E3: c₁ <> {} ;
canceled;
func the_arity_of c₁ -> Nat means :: MARGREL1:def 4
for b₁ being FinSequence st b₁ in a₁ holds
a₂ = len b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 MARGREL1:def 3 :

:: deftheorem Def4 defines the_arity_of MARGREL1:def 4 :

definition

let c₁ be Nat;
mode relation_length of c₁ -> relation means :: MARGREL1:def 5
for b₁ being FinSequence st b₁ in a₂ holds
len b₁ = a₁;
existence

proof end;

end;

:: deftheorem Def5 defines relation_length MARGREL1:def 5 :

definition

let c₁ be set ;
mode relation of c₁ -> relation means :: MARGREL1:def 6
for b₁ being FinSequence st b₁ in a₂ holds
rng b₁ c= a₁;
existence

proof end;

end;

:: deftheorem Def6 defines relation MARGREL1:def 6 :

theorem Th10: :: MARGREL1:10

canceled;

theorem Th11: :: MARGREL1:11

canceled;

theorem Th12: :: MARGREL1:12

canceled;

theorem Th13: :: MARGREL1:13

canceled;

theorem Th14: :: MARGREL1:14

canceled;

theorem Th15: :: MARGREL1:15

canceled;

theorem Th16: :: MARGREL1:16

canceled;

theorem Th17: :: MARGREL1:17

canceled;

theorem Th18: :: MARGREL1:18

canceled;

theorem Th19: :: MARGREL1:19

canceled;

theorem Th20: :: MARGREL1:20

for b₁ being set holds {} is relation of b₁

proof end;

theorem Th21: :: MARGREL1:21

for b₁ being Nat holds {} is relation_length of b₁

proof end;

definition

let c₁ be set ;
let c₂ be Nat;
mode relation of c₁,c₂ -> relation means :: MARGREL1:def 7
( a₃ is relation of a₁ & a₃ is relation_length of a₂ );
existence

proof end;

end;

:: deftheorem Def7 defines relation MARGREL1:def 7 :

definition

let c₁ be non empty set ;
func relations_on c₁ -> set means :Def8: :: MARGREL1:def 8
for b₁ being set holds
( b₁ in a₂ iff ( b₁ c= a₁ * & ( for b₂, b₃ being FinSequence of a₁ st b₂ in b₁ & b₃ in b₁ holds
len b₂ = len b₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines relations_on MARGREL1:def 8 :

registration

let c₁ be non empty set ;
cluster relations_on a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
mode relation of a₁ is Element of relations_on a₁;

end;

theorem Th22: :: MARGREL1:22

canceled;

theorem Th23: :: MARGREL1:23

canceled;

theorem Th24: :: MARGREL1:24

canceled;

theorem Th25: :: MARGREL1:25

canceled;

theorem Th26: :: MARGREL1:26

for b₁ being non empty set
for b₂ being set
for b₃ being Element of relations_on b₁ st b₂ c= b₃ holds
b₂ is Element of relations_on b₁

proof end;

theorem Th27: :: MARGREL1:27

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds {b₂} is Element of relations_on b₁

proof end;

theorem Th28: :: MARGREL1:28

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds {<*b₂,b₃*>} is Element of relations_on b₁

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of relations_on c₁;
redefine pred = as c₂ = c₃ means :Def9: :: MARGREL1:def 9
for b₁ being FinSequence of a₁ holds
( b₁ in a₂ iff b₁ in a₃ );
compatibility

proof end;

end;

:: deftheorem Def9 defines = MARGREL1:def 9 :

scheme :: MARGREL1:sch 2
s2{ F₁() -> non empty set , P₁[ FinSequence of F₁()] } :

ex b₁ being Element of relations_on F₁() st
for b₂ being FinSequence of F₁() holds
( b₂ in b₁ iff P₁[b₂] )

provided

E7: for b₁, b₂ being FinSequence of F₁() st P₁[b₁] & P₁[b₂] holds
len b₁ = len b₂

proof end;

definition

let c₁ be non empty set ;
func empty_rel c₁ -> Element of relations_on a₁ means :Def10: :: MARGREL1:def 10
for b₁ being FinSequence of a₁ holds not b₁ in a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines empty_rel MARGREL1:def 10 :

theorem Th29: :: MARGREL1:29

canceled;

theorem Th30: :: MARGREL1:30

canceled;

theorem Th31: :: MARGREL1:31

canceled;

theorem Th32: :: MARGREL1:32

for b₁ being non empty set holds empty_rel b₁ = {}

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of relations_on c₁;
assume E8: c₂ <> empty_rel c₁ ;
func the_arity_of c₂ -> Nat means :: MARGREL1:def 11
for b₁ being FinSequence of a₁ st b₁ in a₂ holds
a₃ = len b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines the_arity_of MARGREL1:def 11 :

scheme :: MARGREL1:sch 3
s3{ F₁() -> non empty set , F₂() -> Nat, P₁[ FinSequence of F₁()] } :

ex b₁ being Element of relations_on F₁() st
for b₂ being FinSequence of F₁() st len b₂ = F₂() holds
( b₂ in b₁ iff P₁[b₂] )

proof end;

definition

func BOOLEAN -> set equals :: MARGREL1:def 12
{0,1};
coherence ;

end;

:: deftheorem Def12 defines BOOLEAN MARGREL1:def 12 :

registration

cluster BOOLEAN -> non empty ;
coherence ;

end;

definition

func FALSE -> Element of BOOLEAN equals :: MARGREL1:def 13
0;
coherence by TARSKI:def 2;
func TRUE -> Element of BOOLEAN equals :: MARGREL1:def 14
1;
coherence by TARSKI:def 2;

end;

:: deftheorem Def13 defines FALSE MARGREL1:def 13 :

:: deftheorem Def14 defines TRUE MARGREL1:def 14 :

theorem Th33: :: MARGREL1:33

canceled;

theorem Th34: :: MARGREL1:34

canceled;

theorem Th35: :: MARGREL1:35

canceled;

theorem Th36: :: MARGREL1:36

( FALSE = 0 & TRUE = 1 ) ;

theorem Th37: :: MARGREL1:37

BOOLEAN = {FALSE ,TRUE } ;

theorem Th38: :: MARGREL1:38

FALSE <> TRUE ;

definition

let c₁ be set ;
attr a₁ is boolean means :Def15: :: MARGREL1:def 15
a₁ in BOOLEAN ;

end;

:: deftheorem Def15 defines boolean MARGREL1:def 15 :

registration

cluster boolean set ;
existence

proof end;

cluster -> boolean Element of BOOLEAN ;
coherence by Def15;

end;

theorem Th39: :: MARGREL1:39

for b₁ being boolean set holds
( b₁ = FALSE or b₁ = TRUE )

proof end;

definition

let c₁ be boolean set ;
func 'not' c₁ -> boolean set equals :Def16: :: MARGREL1:def 16
TRUE if a₁ = FALSE
otherwise FALSE ;
correctness ;
involutiveness by Th39;
let c₂ be boolean set ;
func c₁ '&' c₂ -> set equals :Def17: :: MARGREL1:def 17
TRUE if ( a₁ = TRUE & a₂ = TRUE )
otherwise FALSE ;
correctness ;
commutativity ;

end;

:: deftheorem Def16 defines 'not' MARGREL1:def 16 :

:: deftheorem Def17 defines '&' MARGREL1:def 17 :

registration

let c₁ be boolean set ;
cluster 'not' a₁ -> boolean ;
coherence ;
let c₂ be boolean set ;
cluster a₁ '&' a₂ -> boolean ;
correctness

proof end;

end;

definition

let c₁ be Element of BOOLEAN ;
redefine func 'not' as 'not' c₁ -> Element of BOOLEAN ;
correctness by Def15;
let c₂ be Element of BOOLEAN ;
redefine func '&' as c₁ '&' c₂ -> Element of BOOLEAN ;
correctness by Def15;

end;

theorem Th40: :: MARGREL1:40

for b₁ being boolean set holds 'not' ('not' b₁) = b₁ ;

theorem Th41: :: MARGREL1:41

for b₁ being boolean set holds
( ( b₁ = FALSE implies 'not' b₁ = TRUE ) & ( 'not' b₁ = TRUE implies b₁ = FALSE ) & ( b₁ = TRUE implies 'not' b₁ = FALSE ) & ( 'not' b₁ = FALSE implies b₁ = TRUE ) )

proof end;

theorem Th42: :: MARGREL1:42

canceled;

theorem Th43: :: MARGREL1:43

for b₁ being boolean set holds
( b₁ <> TRUE iff b₁ = FALSE ) by Th39;

theorem Th44: :: MARGREL1:44

canceled;

theorem Th45: :: MARGREL1:45

for b₁, b₂ being boolean set holds
( ( b₁ '&' b₂ = TRUE implies ( b₁ = TRUE & b₂ = TRUE ) ) & ( b₁ = TRUE & b₂ = TRUE implies b₁ '&' b₂ = TRUE ) & ( not b₁ '&' b₂ = FALSE or b₁ = FALSE or b₂ = FALSE ) & ( ( b₁ = FALSE or b₂ = FALSE ) implies b₁ '&' b₂ = FALSE ) )

proof end;

theorem Th46: :: MARGREL1:46

for b₁ being boolean set holds b₁ '&' ('not' b₁) = FALSE

proof end;

theorem Th47: :: MARGREL1:47

for b₁ being boolean set holds 'not' (b₁ '&' ('not' b₁)) = TRUE

proof end;

theorem Th48: :: MARGREL1:48

canceled;

theorem Th49: :: MARGREL1:49

for b₁ being boolean set holds FALSE '&' b₁ = FALSE by Th45;

theorem Th50: :: MARGREL1:50

for b₁ being boolean set holds TRUE '&' b₁ = b₁

proof end;

theorem Th51: :: MARGREL1:51

for b₁ being boolean set st b₁ '&' b₁ = FALSE holds
b₁ = FALSE by Th45;

theorem Th52: :: MARGREL1:52

for b₁, b₂, b₃ being boolean set holds b₁ '&' (b₂ '&' b₃) = (b₁ '&' b₂) '&' b₃

proof end;

definition

let c₁ be set ;
func ALL c₁ -> set equals :Def18: :: MARGREL1:def 18
TRUE if not FALSE in a₁
otherwise FALSE ;
correctness ;

end;

:: deftheorem Def18 defines ALL MARGREL1:def 18 :

registration

let c₁ be set ;
cluster ALL a₁ -> boolean ;
correctness

proof end;

end;

definition

let c₁ be set ;
redefine func ALL as ALL c₁ -> Element of BOOLEAN ;
correctness by Def15;

end;

theorem Th53: :: MARGREL1:53

for b₁ being set holds
( ( not FALSE in b₁ implies ALL b₁ = TRUE ) & ( ALL b₁ = TRUE implies not FALSE in b₁ ) & ( FALSE in b₁ implies ALL b₁ = FALSE ) & ( ALL b₁ = FALSE implies FALSE in b₁ ) ) by Def18;