---- MODULE MeolicVaja2 ----

\* Predviden cas za to vajo je 45 minut

\* Stevilske mnozice

EXTENDS
  TLC,             (* Operator Print *)
  FiniteSets,      (* Operatorji za mnozice *)  
  Naturals         (* Operatorji za aritmetiko *)

U == 1..20

S == {1, 2, 3, 4, 5, 6, 7, 8, 9, 10}
S1 == {x \in U : x <= 10}
S2 == {x \in U : (x > 5) /\ (x < 15)}

T == {x \in S : (\E y \in S : x = y * 2)}
T1 == {x \in S : (x % 2 = 0)} (* pred dvopicjem obvezno brez oklepajev *)
T2 == {(2 * x): x \in S} (* za dvopicjem obvezno brez oklepajev *)

ASSUME
  T1 = T

ASSUME
  ~(T2 = T)

ASSUME
  {} \subseteq U

ASSUME
  T \subseteq S

ASSUME
  UNION{{1},{1,2},{1,3}} = {1,2,3}

ASSUME LET V == SUBSET S
       IN Cardinality(V) = 1024

ASSUME
  \E x \in U : (x \in S /\ x \in T)

ASSUME
  ~ \A x \in U : (x \in S /\ x \in T)

ASSUME
  \A x \in (U \ S) : (x > 10)

\* NALOGA 1
\* Pokazi, da v mnozici SUBSET S obstaja taka mnozica X,
\* ki ima enako stevilo elementov kot mnozica S

\* NALOGA 2
\* Pokazi, da v mnozici SUBSET S obstaja taka mnozica X,
\* ki ni prazna in vsebuje samo soda stevila

\* Izpisovanje rezultatov

ASSUME 
  Print("MNOZICA T", TRUE) /\ Print(T, TRUE)

ASSUME 
  Print("KOMPLEMENT MNOZICE T", TRUE) /\ Print(U \ T, TRUE)

ASSUME
  Print("STEVILO ELEMENTOV MNOZICE PODMNOZIC", TRUE) /\ Print(Cardinality(SUBSET S), TRUE)

ASSUME 
  \E x \in U : 
    /\ (x > 5 /\ x < 9)
    /\ Print("VECJI OD 5 in MANJSI OD 9 (PRVIC)", TRUE) /\ Print(x, TRUE)

ASSUME 
  \E x \in SUBSET U :
    /\ Cardinality(x) = 2
    /\ \A y \in x : (y > 5 /\ y < 9)
    /\ Print("VECJI OD 5 in MANJSI OD 9 (DRUGIC)", TRUE) /\ Print(x, TRUE)

====