Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Czeslaw Bylinski,
and
- Grzegorz Bancerek
- Received November 23, 1989
- MML identifier: QC_LANG3
- [
Mizar article,
MML identifier index
]
environ
vocabulary QC_LANG1, FINSEQ_1, FUNCT_1, ZF_LANG, BOOLE, QC_LANG2, PRE_TOPC,
ZF_MODEL, QC_LANG3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
FUNCT_1, FUNCT_2, FINSEQ_1, QC_LANG1, QC_LANG2;
constructors FUNCT_2, QC_LANG2, XREAL_0, XCMPLX_0, MEMBERED, XBOOLE_0;
clusters SUBSET_1, RELSET_1, QC_LANG1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS,
ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET;
begin
reserve i,j,k for Nat;
reserve x for bound_QC-variable;
reserve a for free_QC-variable;
reserve p,q for Element of QC-WFF;
reserve l for FinSequence of QC-variables;
reserve P,Q for QC-pred_symbol;
reserve V for non empty Subset of QC-variables;
scheme QC_Func_Uniq { D() -> non empty set,
F1() -> (Function of QC-WFF, D()),
F2() -> (Function of QC-WFF, D()),
V() -> (Element of D()),
A(set) -> (Element of D()),
N(set) -> (Element of D()),
C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()} :
F1() = F2() provided
for p for d1,d2 being Element of D() holds
(p = VERUM implies F1().p = V()) &
(p is atomic implies F1().p = A(p)) &
(p is negative & d1 = F1().the_argument_of p implies F1().p = N(d1)) &
(p is conjunctive &
d1 = F1().the_left_argument_of p & d2 = F1().the_right_argument_of p
implies F1().p = C(d1, d2)) &
(p is universal & d1 = F1().the_scope_of p implies F1().p = Q(p, d1)) and
for p for d1,d2 being Element of D() holds
(p = VERUM implies F2().p = V()) &
(p is atomic implies F2().p = A(p)) &
(p is negative & d1 = F2().the_argument_of p implies F2().p = N(d1)) &
(p is conjunctive &
d1 = F2().the_left_argument_of p & d2 = F2().the_right_argument_of p
implies F2().p = C(d1, d2)) &
(p is universal & d1 = F2().the_scope_of p implies F2().p = Q(p, d1));
scheme QC_Def_D
{ D() -> non empty set, V() -> (Element of D()),
p() -> (Element of QC-WFF),
A(Element of QC-WFF) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()), Element of D()) -> (Element of D()),
Q((Element of QC-WFF), Element of D()) -> Element of D()} :
(ex d being (Element of D()), F being Function of QC-WFF, D() st
d = F.p() &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) &
for x1,x2 being Element of D() st
(ex F being Function of QC-WFF, D() st
x1 = F.p() &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) &
(ex F being Function of QC-WFF, D() st
x2 = F.p() &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) )
holds x1 = x2;
scheme QC_D_Result'VERUM
{ D() -> non empty set,
F(Element of QC-WFF) -> (Element of D()),
V() -> (Element of D()),
A(Element of QC-WFF) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()), Element of D()) -> (Element of D()),
Q((Element of QC-WFF), Element of D()) -> Element of D()} :
F(VERUM) = V()
provided
for p being QC-formula, d being Element of D() holds
d = F(p) iff
ex F being Function of QC-WFF, D() st
d = F.p &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1));
scheme QC_D_Result'atomic
{ D() -> non empty set, V() -> (Element of D()),
F(Element of QC-WFF) -> (Element of D()),
p() -> QC-formula,
A(Element of QC-WFF) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()), Element of D()) -> (Element of D()),
Q((Element of QC-WFF), Element of D()) -> Element of D()} :
F(p()) = A(p())
provided
for p being QC-formula, d being Element of D() holds
d = F(p) iff
ex F being Function of QC-WFF, D() st
d = F.p &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and
p() is atomic;
scheme QC_D_Result'negative
{ D() -> non empty set, V() -> (Element of D()),
p() -> QC-formula,
A(Element of QC-WFF) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()), Element of D()) -> (Element of D()),
Q((Element of QC-WFF), Element of D()) -> (Element of D()),
F(Element of QC-WFF) -> (Element of D()) } :
F(p()) = N(F(the_argument_of p()))
provided
for p being QC-formula, d being Element of D() holds
d = F(p) iff
ex F being Function of QC-WFF, D() st
d = F.p &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and
p() is negative;
scheme QC_D_Result'conjunctive
{ D() -> non empty set,
V() -> (Element of D()),
A(Element of QC-WFF) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()), Element of D()) -> (Element of D()),
Q((Element of QC-WFF), Element of D()) -> (Element of D()),
F(Element of QC-WFF) -> (Element of D()),
p() -> QC-formula } :
for d1,d2 being Element of D() st
d1 = F(the_left_argument_of p()) & d2 = F(the_right_argument_of p()) holds
F(p()) = C(d1,d2)
provided
for p being QC-formula, d being Element of D() holds
d = F(p) iff
ex F being Function of QC-WFF, D() st
d = F.p &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and
p() is conjunctive;
scheme QC_D_Result'universal
{ D() -> non empty set,
V() -> (Element of D()),
p() -> QC-formula,
A(Element of QC-WFF) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()), Element of D()) -> (Element of D()),
Q((Element of QC-WFF), Element of D()) -> (Element of D()),
F(Element of QC-WFF) -> (Element of D()) } :
F(p()) = Q(p(),F(the_scope_of p()))
provided
for p being QC-formula, d being Element of D() holds
d = F(p) iff
ex F being Function of QC-WFF, D() st
d = F.p &
for p being Element of QC-WFF
for d1,d2 being Element of D() holds
(p = VERUM implies F.p = V()) &
(p is atomic implies F.p = A(p)) &
(p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) &
(p is conjunctive &
d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p
implies F.p = C(d1, d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and
p() is universal;
canceled 2;
theorem :: QC_LANG3:3
P is QC-pred_symbol of the_arity_of P;
definition let l; let V;
canceled;
func variables_in(l,V) -> Element of bool V equals
:: QC_LANG3:def 2
{ l.k : 1 <= k & k <= len l & l.k in V };
end;
canceled 2;
theorem :: QC_LANG3:6
still_not-bound_in l = variables_in(l,bound_QC-variables);
theorem :: QC_LANG3:7
still_not-bound_in VERUM = {};
theorem :: QC_LANG3:8
for p being QC-formula st p is atomic holds
still_not-bound_in p = still_not-bound_in the_arguments_of p;
theorem :: QC_LANG3:9
for P being QC-pred_symbol of k for l being QC-variable_list of k
holds still_not-bound_in (P!l) = still_not-bound_in l;
theorem :: QC_LANG3:10
for p being QC-formula st p is negative holds
still_not-bound_in p = still_not-bound_in the_argument_of p;
theorem :: QC_LANG3:11
for p being QC-formula holds
still_not-bound_in 'not' p = still_not-bound_in p;
theorem :: QC_LANG3:12
still_not-bound_in FALSUM = {};
theorem :: QC_LANG3:13
for p being QC-formula st p is conjunctive holds
still_not-bound_in p = (still_not-bound_in the_left_argument_of p) \/
(still_not-bound_in the_right_argument_of p);
theorem :: QC_LANG3:14
for p,q being QC-formula holds
still_not-bound_in(p '&' q) =
(still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:15
for p being QC-formula st p is universal holds
still_not-bound_in p =
(still_not-bound_in the_scope_of p) \ {bound_in p};
theorem :: QC_LANG3:16
for p being QC-formula
holds still_not-bound_in All(x,p) = (still_not-bound_in p) \ {x};
theorem :: QC_LANG3:17
for p being QC-formula st p is disjunctive holds
still_not-bound_in p = (still_not-bound_in the_left_disjunct_of p) \/
(still_not-bound_in the_right_disjunct_of p);
theorem :: QC_LANG3:18
for p,q being QC-formula holds still_not-bound_in p 'or' q
= (still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:19
for p being QC-formula st p is conditional holds
still_not-bound_in p = (still_not-bound_in the_antecedent_of p) \/
(still_not-bound_in the_consequent_of p);
theorem :: QC_LANG3:20
for p,q being QC-formula holds still_not-bound_in p => q
= (still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:21
for p being QC-formula st p is biconditional holds
still_not-bound_in p = (still_not-bound_in the_left_side_of p) \/
(still_not-bound_in the_right_side_of p);
theorem :: QC_LANG3:22
for p,q being QC-formula holds still_not-bound_in p <=> q
= (still_not-bound_in p) \/ (still_not-bound_in q);
theorem :: QC_LANG3:23
for p being QC-formula holds
still_not-bound_in Ex(x,p) = (still_not-bound_in p) \ {x};
theorem :: QC_LANG3:24
VERUM is closed & FALSUM is closed;
theorem :: QC_LANG3:25
for p being QC-formula holds p is closed iff 'not' p is closed;
theorem :: QC_LANG3:26
for p,q being QC-formula holds
p is closed & q is closed iff p '&' q is closed;
theorem :: QC_LANG3:27
for p being QC-formula holds
All(x,p) is closed iff still_not-bound_in p c= {x};
theorem :: QC_LANG3:28
for p being QC-formula st p is closed holds All(x,p) is closed;
theorem :: QC_LANG3:29
for p,q being QC-formula holds
p is closed & q is closed iff p 'or' q is closed;
theorem :: QC_LANG3:30
for p,q being QC-formula holds
p is closed & q is closed iff p => q is closed;
theorem :: QC_LANG3:31
for p,q being QC-formula holds
p is closed & q is closed iff p <=> q is closed;
theorem :: QC_LANG3:32
for p being QC-formula holds
Ex(x,p) is closed iff still_not-bound_in p c= {x};
theorem :: QC_LANG3:33
for p being QC-formula st p is closed holds Ex(x,p) is closed;
definition let k;
func x.k -> bound_QC-variable equals
:: QC_LANG3:def 3
[4,k];
end;
canceled;
theorem :: QC_LANG3:35
x.i = x.j implies i = j;
theorem :: QC_LANG3:36
ex i st x.i = x;
definition let k;
func a.k -> free_QC-variable equals
:: QC_LANG3:def 4
[6,k];
end;
canceled;
theorem :: QC_LANG3:38
a.i = a.j implies i = j;
theorem :: QC_LANG3:39
ex i st a.i = a;
theorem :: QC_LANG3:40
for c being Element of fixed_QC-variables
for a being Element of free_QC-variables holds c <> a;
theorem :: QC_LANG3:41
for c being Element of fixed_QC-variables
for x being Element of bound_QC-variables holds c <> x;
theorem :: QC_LANG3:42
for a being Element of free_QC-variables
for x being Element of bound_QC-variables holds a <> x;
definition let V; let V1,V2 be Element of bool V;
redefine func V1 \/ V2 -> Element of bool V;
end;
definition let V; let p;
func Vars(p,V) -> Element of bool V means
:: QC_LANG3:def 5
ex F being Function of QC-WFF, bool V st
it = F.p &
for p being Element of QC-WFF
for d1,d2 being Element of bool V holds
(p = VERUM implies F.p = {}(V)) &
(p is atomic implies F.p = variables_in(the_arguments_of p,V)) &
(p is negative & d1 = F.the_argument_of p implies F.p = d1) &
(p is conjunctive & d1 = F.the_left_argument_of p &
d2 = F.the_right_argument_of p implies F.p = d1 \/ d2) &
(p is universal & d1 = F.the_scope_of p implies F.p = d1);
end;
canceled 3;
theorem :: QC_LANG3:46
Vars(VERUM,V) = {};
theorem :: QC_LANG3:47
p is atomic implies Vars(p,V) = variables_in(the_arguments_of p, V) &
Vars(p,V) = { (the_arguments_of p).k :
1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p).k in V };
theorem :: QC_LANG3:48
for P being QC-pred_symbol of k for l being QC-variable_list of k
holds Vars(P!l,V) = variables_in(l, V) &
Vars((P!l),V) = { l.i : 1 <= i & i <= len l & l.i in V };
theorem :: QC_LANG3:49
p is negative implies Vars(p,V) = Vars(the_argument_of p,V);
theorem :: QC_LANG3:50
Vars('not' p,V) = Vars(p,V);
theorem :: QC_LANG3:51
Vars(FALSUM,V) = {};
theorem :: QC_LANG3:52
p is conjunctive implies Vars(p,V) =
Vars(the_left_argument_of p,V) \/ Vars(the_right_argument_of p,V);
theorem :: QC_LANG3:53
Vars(p '&' q,V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:54
p is universal implies Vars(p,V) = Vars(the_scope_of p,V);
theorem :: QC_LANG3:55
Vars(All(x,p),V) = Vars(p,V);
theorem :: QC_LANG3:56
p is disjunctive implies Vars(p,V) =
Vars(the_left_disjunct_of p,V) \/ Vars(the_right_disjunct_of p,V);
theorem :: QC_LANG3:57
Vars(p 'or' q, V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:58
p is conditional implies Vars(p,V) =
Vars(the_antecedent_of p,V) \/ Vars(the_consequent_of p,V);
theorem :: QC_LANG3:59
Vars(p => q,V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:60
p is biconditional implies Vars(p,V) =
Vars(the_left_side_of p,V) \/ Vars(the_right_side_of p,V);
theorem :: QC_LANG3:61
Vars(p <=> q,V) = Vars(p,V) \/ Vars(q,V);
theorem :: QC_LANG3:62
p is existential implies Vars(p,V) =
Vars(the_argument_of the_scope_of the_argument_of p, V);
theorem :: QC_LANG3:63
Vars(Ex(x,p), V) = Vars(p,V);
definition let p;
func Free p -> Element of bool free_QC-variables equals
:: QC_LANG3:def 6
Vars(p,free_QC-variables);
end;
canceled;
theorem :: QC_LANG3:65
Free VERUM = {};
theorem :: QC_LANG3:66
for P being QC-pred_symbol of k for l being QC-variable_list of k
holds Free(P!l) = { l.i : 1 <= i & i <= len l & l.i in free_QC-variables };
theorem :: QC_LANG3:67
Free 'not' p = Free p;
theorem :: QC_LANG3:68
Free FALSUM = {};
theorem :: QC_LANG3:69
Free(p '&' q) = Free p \/ Free q;
theorem :: QC_LANG3:70
Free(All(x,p)) = Free(p);
theorem :: QC_LANG3:71
Free(p 'or' q) = Free p \/ Free q;
theorem :: QC_LANG3:72
Free(p => q) = Free p \/ Free q;
theorem :: QC_LANG3:73
Free(p <=> q) = Free p \/ Free q;
theorem :: QC_LANG3:74
Free Ex(x,p) = Free p;
definition let p;
func Fixed p -> Element of bool fixed_QC-variables equals
:: QC_LANG3:def 7
Vars(p,fixed_QC-variables);
end;
canceled;
theorem :: QC_LANG3:76
Fixed VERUM = {};
theorem :: QC_LANG3:77
for P being QC-pred_symbol of k for l being QC-variable_list of k
holds Fixed(P!l) = { l.i : 1 <= i & i <= len l & l.i in
fixed_QC-variables };
theorem :: QC_LANG3:78
Fixed 'not' p = Fixed p;
theorem :: QC_LANG3:79
Fixed FALSUM = {};
theorem :: QC_LANG3:80
Fixed(p '&' q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:81
Fixed(All(x,p)) = Fixed(p);
theorem :: QC_LANG3:82
Fixed(p 'or' q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:83
Fixed(p => q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:84
Fixed(p <=> q) = Fixed p \/ Fixed q;
theorem :: QC_LANG3:85
Fixed Ex(x,p) = Fixed p;
Back to top