:: MARGREL1 semantic presentation

definition

let B, A be non empty set ;
let b be Element of B;
:: original: -->
redefine func A --> b -> Element of Funcs A,B;
coherence

proof end;

end;

definition

let IT be set ;
attr IT is relation-like means :Def1: :: MARGREL1:def 1
( ( for x being set st x in IT holds
x is FinSequence ) & ( for a, b being FinSequence st a in IT & b in IT holds
len a = 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 :: MARGREL1:1

canceled;

theorem :: MARGREL1:2

canceled;

theorem :: MARGREL1:3

canceled;

theorem :: MARGREL1:4

canceled;

theorem :: MARGREL1:5

canceled;

theorem :: MARGREL1:6

canceled;

theorem :: MARGREL1:7

for X being set
for p being relation st X c= p holds
X is relation-like

proof end;

theorem :: MARGREL1:8

for a being FinSequence holds {a} is relation-like

proof end;

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

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

provided

A1: for a, b being FinSequence st P₁[a] & P₁[b] holds
len a = len b

proof end;

definition

let p, r be relation;
redefine pred p = r means :: MARGREL1:def 2
for a being FinSequence holds
( a in p iff a in r );
compatibility

proof end;

end;

:: deftheorem defines = MARGREL1:def 2 :

registration

cluster {} -> relation-like ;
coherence

proof end;

end;

theorem Th9: :: MARGREL1:9

for p being relation st ( for a being FinSequence holds not a in p ) holds
p = {}

proof end;

definition

let p be relation;
assume A1: p <> {} ;
canceled;
func the_arity_of p -> Nat means :: MARGREL1:def 4
for a being FinSequence st a in p holds
it = len a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem MARGREL1:def 3 :

:: deftheorem defines the_arity_of MARGREL1:def 4 :

definition

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

proof end;

end;

:: deftheorem defines relation_length MARGREL1:def 5 :

definition

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

proof end;

end;

:: deftheorem defines relation MARGREL1:def 6 :

theorem :: MARGREL1:10

canceled;

theorem :: MARGREL1:11

canceled;

theorem :: MARGREL1:12

canceled;

theorem :: MARGREL1:13

canceled;

theorem :: MARGREL1:14

canceled;

theorem :: MARGREL1:15

canceled;

theorem :: MARGREL1:16

canceled;

theorem :: MARGREL1:17

canceled;

theorem :: MARGREL1:18

canceled;

theorem :: MARGREL1:19

canceled;

theorem Th20: :: MARGREL1:20

for X being set holds {} is relation of X

proof end;

theorem Th21: :: MARGREL1:21

for k being Nat holds {} is relation_length of k

proof end;

definition

let X be set ;
let k be Nat;
mode relation of X,k -> relation means :: MARGREL1:def 7
( it is relation of X & it is relation_length of k );
existence

proof end;

end;

:: deftheorem defines relation MARGREL1:def 7 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines relations_on MARGREL1:def 8 :

registration

let D be non empty set ;
cluster relations_on D -> non empty ;
coherence

proof end;

end;

definition

let D be non empty set ;
mode relation of D is Element of relations_on D;

end;

theorem :: MARGREL1:22

canceled;

theorem :: MARGREL1:23

canceled;

theorem :: MARGREL1:24

canceled;

theorem :: MARGREL1:25

canceled;

theorem :: MARGREL1:26

for D being non empty set
for X being set
for r being Element of relations_on D st X c= r holds
X is Element of relations_on D

proof end;

theorem :: MARGREL1:27

for D being non empty set
for a being FinSequence of D holds {a} is Element of relations_on D

proof end;

theorem :: MARGREL1:28

for D being non empty set
for x, y being Element of D holds {<*x,y*>} is Element of relations_on D

proof end;

definition

let D be non empty set ;
let p, r be Element of relations_on D;
:: original: =
redefine pred p = r means :Def9: :: MARGREL1:def 9
for a being FinSequence of D holds
( a in p iff a in r );
compatibility

proof end;

end;

:: deftheorem Def9 defines = MARGREL1:def 9 :

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

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

provided

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

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines empty_rel MARGREL1:def 10 :

theorem :: MARGREL1:29

canceled;

theorem :: MARGREL1:30

canceled;

theorem :: MARGREL1:31

canceled;

theorem :: MARGREL1:32

for D being non empty set holds empty_rel D = {}

proof end;

definition

let D be non empty set ;
let p be Element of relations_on D;
assume A1: p <> empty_rel D ;
func the_arity_of p -> Nat means :: MARGREL1:def 11
for a being FinSequence of D st a in p holds
it = len a;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines the_arity_of MARGREL1:def 11 :

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

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

proof end;

definition

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

end;

:: deftheorem 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 defines FALSE MARGREL1:def 13 :

:: deftheorem defines TRUE MARGREL1:def 14 :

theorem :: MARGREL1:33

canceled;

theorem :: MARGREL1:34

canceled;

theorem :: MARGREL1:35

canceled;

theorem :: MARGREL1:36

( FALSE = 0 & TRUE = 1 ) ;

theorem :: MARGREL1:37

BOOLEAN = {FALSE ,TRUE } ;

theorem :: MARGREL1:38

FALSE <> TRUE ;

definition

let x be set ;
attr x is boolean means :Def15: :: MARGREL1:def 15
x 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 v being boolean set holds
( v = FALSE or v = TRUE )

proof end;

definition

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

end;

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

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

registration

let v be boolean set ;
cluster 'not' v -> boolean ;
coherence ;
let w be boolean set ;
cluster v '&' w -> boolean ;
correctness

proof end;

end;

definition

let v be Element of BOOLEAN ;
:: original: 'not'
redefine func 'not' v -> Element of BOOLEAN ;
correctness by Def15;
let w be Element of BOOLEAN ;
:: original: '&'
redefine func v '&' w -> Element of BOOLEAN ;
correctness by Def15;

end;

theorem :: MARGREL1:40

for v being boolean set holds 'not' ('not' v) = v ;

theorem Th41: :: MARGREL1:41

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

proof end;

theorem :: MARGREL1:42

canceled;

theorem :: MARGREL1:43

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

theorem :: MARGREL1:44

canceled;

theorem Th45: :: MARGREL1:45

for v, w being boolean set holds
( ( v '&' w = TRUE implies ( v = TRUE & w = TRUE ) ) & ( v = TRUE & w = TRUE implies v '&' w = TRUE ) & ( not v '&' w = FALSE or v = FALSE or w = FALSE ) & ( ( v = FALSE or w = FALSE ) implies v '&' w = FALSE ) )

proof end;

theorem Th46: :: MARGREL1:46

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

proof end;

theorem :: MARGREL1:47

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

proof end;

theorem :: MARGREL1:48

canceled;

theorem :: MARGREL1:49

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

theorem :: MARGREL1:50

for v being boolean set holds TRUE '&' v = v

proof end;

theorem :: MARGREL1:51

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

theorem :: MARGREL1:52

for v, w, u being boolean set holds v '&' (w '&' u) = (v '&' w) '&' u

proof end;

definition

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

end;

:: deftheorem Def18 defines ALL MARGREL1:def 18 :

registration

let X be set ;
cluster ALL X -> boolean ;
correctness

proof end;

end;

definition

let X be set ;
:: original: ALL
redefine func ALL X -> Element of BOOLEAN ;
correctness by Def15;

end;

theorem :: MARGREL1:53

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