:: A Classical First Order Language
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1990
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, QC_LANG1, FINSEQ_1, PARTFUN1, XXREAL_0,
FUNCT_1, RELAT_1, TARSKI, FUNCOP_1, QC_LANG3, XBOOLE_0, ZF_MODEL,
FINSEQ_2, ZF_LANG, CARD_1, REALSET1, XBOOLEAN, BVFUNC_2, MARGREL1,
CLASSES2, CQC_LANG, ZFMISC_1, NAT_1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCOP_1, FUNCT_4,
FINSEQ_1, FINSEQ_2, QC_LANG1, QC_LANG2, QC_LANG3, XXREAL_0, NAT_1,
ZFMISC_1;
constructors ENUMSET1, PARTFUN1, BINOP_1, FUNCOP_1, FUNCT_4, XXREAL_0,
MEMBERED, QC_LANG2, QC_LANG3, FINSEQ_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELSET_1, FUNCOP_1, MEMBERED, QC_LANG1, XXREAL_0,
FINSEQ_2, CARD_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, RELAT_1;
equalities FUNCOP_1, FINSEQ_2;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FINSEQ_1, PARTFUN1, FUNCOP_1,
QC_LANG1, QC_LANG2, QC_LANG3, FINSEQ_2, RELSET_1, FINSEQ_3, RELAT_1,
CARD_1, XBOOLE_0, XTUPLE_0;
schemes FINSEQ_1, QC_LANG1, QC_LANG3;
begin
reserve A for QC-alphabet;
reserve i,j,k for Nat;
Lm1: for x being bound_QC-variable of A holds not x in fixed_QC-variables(A)
proof
let x be bound_QC-variable of A;
x in bound_QC-variables(A);
then x in [: {4},QC-symbols(A) :] by QC_LANG1:def 4;
then consider x1,x2 being object such that
A1: x1 in {4} and
x2 in QC-symbols(A) and
A2: x = [x1,x2] by ZFMISC_1:def 2;
A3: x1 = 4 by A1,TARSKI:def 1;
assume x in fixed_QC-variables(A);
then x in [: {5},QC-symbols(A) :] by QC_LANG1:def 5;
then consider c1,c2 being object such that
A4: c1 in {5} and
c2 in QC-symbols(A) and
A5: x = [c1,c2] by ZFMISC_1:def 2;
c1 = 5 by A4,TARSKI:def 1;
hence contradiction by A2,A5,A3,XTUPLE_0:1;
end;
theorem Th1:
for x being set holds x in QC-variables(A) iff x in
fixed_QC-variables(A) or x in free_QC-variables(A) or
x in bound_QC-variables(A)
proof
let x be set;
thus x in QC-variables(A) implies x in fixed_QC-variables(A) or x in
free_QC-variables(A) or x in bound_QC-variables(A)
proof
assume x in QC-variables(A);
then x in [: {6}, NAT :] \/ [: {4,5}, QC-symbols(A) :] by QC_LANG1:def 3;
then x in [: {6}, NAT :] or x in [: {4,5}, QC-symbols(A) :]
by XBOOLE_0:def 3;
then consider x1,x2 being object such that
A1: (x1 in {6} & x2 in NAT & x = [x1,x2]) or
(x1 in {4,5} & x2 in QC-symbols(A) & x = [x1,x2]) by ZFMISC_1:def 2;
(x1 in {6} & x2 in NAT & x = [x1,x2]) or
((x1 = 4 or x1 = 5) & x2 in QC-symbols(A) & x = [x1,x2])
by A1,TARSKI:def 2;
then ((x1 in {4} & x2 in QC-symbols(A)) or (x1 in {5} & x2 in QC-symbols(A))
or (x1 in {6} & x2 in NAT)) & x = [x1,x2] by TARSKI:def 1;
then x in [:{4},QC-symbols(A):] or x in [:{5}, QC-symbols(A):] or
x in [:{6},NAT:] by ZFMISC_1:def 2;
hence thesis by QC_LANG1:def 4,def 5,def 6;
end;
thus thesis;
end;
definition
let A;
mode Substitution of A is PartFunc of free_QC-variables(A),QC-variables(A);
end;
reserve f for Substitution of A;
definition
let A;
let l be FinSequence of QC-variables(A);
let f;
func Subst(l,f) -> FinSequence of QC-variables(A) means
:Def1:
len it = len l &
for k st 1 <= k & k <= len l holds (l.k in dom f implies it.k = f.(l.k)) & (not
l.k in dom f implies it.k = l.k);
existence
proof
defpred P[set,object] means
(l.$1 in dom f implies $2 = f.(l.$1)) & (not l.$1
in dom f implies $2 = l.$1);
A1: for k be Nat st k in Seg len l ex y being object st P[k,y]
proof
let k be Nat;
assume k in Seg len l;
l.k in dom f implies thesis;
hence thesis;
end;
consider s being FinSequence such that
A2: dom s = Seg len l and
A3: for k be Nat st k in Seg len l holds P[k,s.k]
from FINSEQ_1:sch 1(
A1);
rng s c= QC-variables(A)
proof
let y be object;
assume y in rng s;
then consider x being object such that
A4: x in dom s and
A5: s.x = y by FUNCT_1:def 3;
reconsider x as Nat by A4;
A6: now
per cases;
case
l.x in dom f;
hence s.x = f.(l.x) & f.(l.x) in QC-variables(A)
by A2,A3,A4,PARTFUN1:4;
end;
case
not l.x in dom f;
hence s.x = l.x by A2,A3,A4;
end;
end;
dom l = Seg len l by FINSEQ_1:def 3;
hence thesis by A2,A4,A5,A6,FINSEQ_2:11;
end;
then reconsider s as FinSequence of QC-variables(A) by FINSEQ_1:def 4;
take s;
thus len s = len l by A2,FINSEQ_1:def 3;
let k;
assume 1 <= k & k <= len l;
then k in dom l by FINSEQ_3:25;
then k in Seg len l by FINSEQ_1:def 3;
hence thesis by A3;
end;
uniqueness
proof
let l1,l2 be FinSequence of QC-variables(A) such that
A7: len l1 = len l and
A8: for k st 1 <= k & k <= len l holds (l.k in dom f implies l1.k = f
.(l.k)) & (not l.k in dom f implies l1.k = l.k) and
A9: len l2 = len l and
A10: for k st 1 <= k & k <= len l holds (l.k in dom f implies l2.k = f
.(l.k)) & (not l.k in dom f implies l2.k = l.k);
now
let k be Nat;
assume
A11: 1 <= k & k <= len l;
A12: not l.k in dom f implies l1.k = l.k by A8,A11;
l.k in dom f implies l1.k = f.(l.k) by A8,A11;
hence l1.k = l2.k by A10,A11,A12;
end;
hence thesis by A7,A9,FINSEQ_1:14;
end;
end;
registration
let A,k;
let l be QC-variable_list of k, A;
let f;
cluster Subst(l,f) -> k-element;
coherence
proof
len Subst(l,f) = len l & len l = k by Def1,CARD_1:def 7;
hence thesis by CARD_1:def 7;
end;
end;
theorem Th2:
for x being bound_QC-variable of A, a being free_QC-variable of A holds
a .--> x is Substitution of A
proof
let x be bound_QC-variable of A;
let a be free_QC-variable of A;
set f = a .--> x;
rng f = {x} by FUNCOP_1:8;
then
A1: rng f c= QC-variables(A) by ZFMISC_1:31;
dom f = {a} by FUNCOP_1:13;
then dom f c= free_QC-variables(A) by ZFMISC_1:31;
hence thesis by A1,RELSET_1:4;
end;
definition
let A;
let a be free_QC-variable of A, x be bound_QC-variable of A;
redefine func a .--> x -> Substitution of A;
coherence by Th2;
end;
theorem Th3:
for x being bound_QC-variable of A, a being free_QC-variable of A,
l, ll being FinSequence of QC-variables(A)
holds
f = a .--> x & ll = Subst(l,f) & 1 <= k & k <= len l implies (l.
k = a implies ll.k = x) & (l.k <> a implies ll.k = l.k)
proof
let x be bound_QC-variable of A, a be free_QC-variable of A,
l, ll be FinSequence of QC-variables(A);
set f9 = a .--> x;
assume
A1: f = a .--> x & ll = Subst(l,f) & 1 <= k & k <= len l;
thus l.k = a implies ll.k = x
proof
A2: f9.a = x by FUNCOP_1:72;
assume
A3: l.k = a;
then l.k in { a } by TARSKI:def 1;
then l.k in dom(f9) by FUNCOP_1:13;
hence thesis by A1,A3,A2,Def1;
end;
assume l.k <> a;
then not l.k in { a } by TARSKI:def 1;
then not l.k in dom(f9) by FUNCOP_1:13;
hence thesis by A1,Def1;
end;
definition
let A;
func CQC-WFF(A) -> Subset of QC-WFF(A) equals
{s where s is QC-formula of A: Fixed s = {} & Free s = {} };
coherence
proof
set F = {s where s is QC-formula of A: Fixed s = {} & Free s = {} };
F c= QC-WFF(A)
proof
let x be object;
assume x in F;
then ex s being QC-formula of A st s = x & Fixed s = {} & Free s = {};
hence thesis;
end;
hence thesis;
end;
end;
registration
let A;
cluster CQC-WFF(A) -> non empty;
coherence
proof
Fixed VERUM(A) = {} & Free VERUM(A) = {} by QC_LANG3:53,63;
then VERUM(A) in
{s where s is QC-formula of A: Fixed s = {} & Free s = {} };
hence thesis;
end;
end;
theorem Th4:
for p being Element of QC-WFF(A) holds
p is Element of CQC-WFF(A) iff Fixed p = {} & Free p = {}
proof
let p be Element of QC-WFF(A);
thus p is Element of CQC-WFF(A) implies Fixed p = {} & Free p = {}
proof
assume p is Element of CQC-WFF(A);
then p in CQC-WFF(A);
then ex s being QC-formula of A st s = p & Fixed s = {} & Free s = {};
hence thesis;
end;
assume Fixed p = {} & Free p = {};
then p in CQC-WFF(A);
hence thesis;
end;
registration
let A;
let k be Nat;
cluster bound_QC-variables(A)-valued for QC-variable_list of k, A;
existence
proof
set null = 0;
reconsider null as QC-symbol of A by QC_LANG1:3;
set l = k |-> x.null;
A1: dom l = Seg k by FUNCOP_1:13;
rng l c= QC-variables(A)
proof
let y be object;
assume y in rng l;
then consider x being object such that
A2: x in dom l and
A3: l.x = y by FUNCT_1:def 3;
y = x.null by A1,A2,A3,FINSEQ_2:57;
hence thesis;
end;
then reconsider l as QC-variable_list of k, A by FINSEQ_1:def 4;
take l;
let x be object;
assume x in rng l;
then consider i being object such that
A4: i in dom l and
A5: x = l.i by FUNCT_1:def 3;
reconsider i as Nat by A4;
l.i = x.null by A1,A4,FINSEQ_2:57;
hence thesis by A5;
end;
end;
definition
let A; let k be Nat;
mode CQC-variable_list of k,
A is bound_QC-variables(A)-valued QC-variable_list of k,A;
end;
theorem Th5:
for l being QC-variable_list of k, A holds l is CQC-variable_list
of k,A iff { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A) }
= {} & { l.j
: 1 <= j & j <= len l & l.j in fixed_QC-variables(A) } = {}
proof
let l be QC-variable_list of k, A;
set FR = { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A) };
set FI = { l.j : 1 <= j & j <= len l & l.j in fixed_QC-variables(A) };
thus l is CQC-variable_list of k, A implies FR = {} & FI = {}
proof
assume l is CQC-variable_list of k, A;
then reconsider l as CQC-variable_list of k, A;
now
set x =the Element of FR;
assume FR <> {};
then x in FR;
then consider i such that
x = l.i and
A1: 1 <= i & i <= len l and
A2: l.i in free_QC-variables(A);
i in dom l by A1,FINSEQ_3:25;
then rng l c= bound_QC-variables(A) & l.i in rng l by FUNCT_1:def 3
,RELAT_1:def 19;
hence contradiction by A2,QC_LANG3:34;
end;
hence FR = {};
now
set x =the Element of FI;
assume FI <> {};
then x in FI;
then consider i such that
x = l.i and
A3: 1 <= i & i <= len l and
A4: l.i in fixed_QC-variables(A);
i in dom l by A3,FINSEQ_3:25;
then rng l c= bound_QC-variables(A) & l.i in rng l by FUNCT_1:def 3
,RELAT_1:def 19;
hence contradiction by A4,QC_LANG3:33;
end;
hence thesis;
end;
assume that
A5: FR = {} and
A6: FI = {};
l is bound_QC-variables(A)-valued
proof
let x be object;
A7: rng l c= QC-variables(A) by FINSEQ_1:def 4;
assume x in rng l;
then consider i being object such that
A8: i in dom l and
A9: l.i = x by FUNCT_1:def 3;
reconsider i as Nat by A8;
A10: 1 <= i & i <= len l by A8,FINSEQ_3:25;
A11: now
assume x in fixed_QC-variables(A);
then x in FI by A9,A10;
hence contradiction by A6;
end;
A12: now
assume x in free_QC-variables(A);
then x in FR by A9,A10;
hence contradiction by A5;
end;
l.i in rng l by A8,FUNCT_1:def 3;
hence thesis by A9,A7,A11,A12,Th1;
end;
hence thesis;
end;
theorem Th6:
VERUM(A) is Element of CQC-WFF(A)
proof
Fixed VERUM(A) = {} & Free VERUM(A) = {} by QC_LANG3:53,63;
hence thesis by Th4;
end;
theorem Th7:
for P being QC-pred_symbol of k,A for l being QC-variable_list of
k,A holds P!l is Element of CQC-WFF(A) iff
{ l.i : 1 <= i & i <= len l & l.i in
free_QC-variables(A) } = {} & { l.j : 1 <= j & j <= len l & l.j in
fixed_QC-variables(A) } = {}
proof
let P be QC-pred_symbol of k,A;
let l be QC-variable_list of k, A;
A1: Free(P!l) = { l.j : 1 <= j & j <= len l & l.j in free_QC-variables(A) } by
QC_LANG3:54;
Fixed(P!l) = { l.i : 1 <= i & i <= len l & l.i in fixed_QC-variables(A) }
by QC_LANG3:64;
hence thesis by A1,Th4;
end;
definition
let k,A;
let P be QC-pred_symbol of k,A;
let l be CQC-variable_list of k,A;
redefine func P!l -> Element of CQC-WFF(A);
coherence
proof
A1: { l.j : 1 <= j & j <= len l & l.j in fixed_QC-variables(A) } = {} by Th5;
{ l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A) } = {} by Th5;
hence thesis by A1,Th7;
end;
end;
theorem Th8:
for p being Element of QC-WFF(A) holds
'not' p is Element of CQC-WFF(A) iff p is Element of CQC-WFF(A)
proof
let p be Element of QC-WFF(A);
thus 'not' p is Element of CQC-WFF(A) implies p is Element of CQC-WFF(A)
proof
assume
A1: 'not' p is Element of CQC-WFF(A);
then Free 'not' p = {} by Th4;
then
A2: Free p = {} by QC_LANG3:55;
Fixed 'not' p = {} by A1,Th4;
then Fixed p = {} by QC_LANG3:65;
hence thesis by A2,Th4;
end;
assume p is Element of CQC-WFF(A);
then reconsider r = p as Element of CQC-WFF(A);
Fixed r = {} by Th4;
then
A3: Fixed 'not' r = {} by QC_LANG3:65;
Free r = {} by Th4;
then Free 'not' r = {} by QC_LANG3:55;
hence thesis by A3,Th4;
end;
theorem Th9:
for p,q being Element of QC-WFF(A) holds
p '&' q is Element of CQC-WFF(A) iff p is Element of CQC-WFF(A) & q is
Element of CQC-WFF(A)
proof
let p,q being Element of QC-WFF(A);
thus p '&' q is Element of CQC-WFF(A) implies
p is Element of CQC-WFF(A) & q is
Element of CQC-WFF(A)
proof
assume
A1: p '&' q is Element of CQC-WFF(A);
then Fixed(p '&' q) = {} by Th4;
then
A2: Fixed p \/ Fixed q = {} by QC_LANG3:67;
then
A3: Fixed p = {};
Free(p '&' q) = {} by A1,Th4;
then
A4: Free p \/ Free q = {} by QC_LANG3:57;
then Free p = {};
hence thesis by A4,A2,A3,Th4;
end;
assume p is Element of CQC-WFF(A) & q is Element of CQC-WFF(A);
then reconsider r = p, s = q as Element of CQC-WFF(A);
Fixed r = {} by Th4;
then Fixed r \/ Fixed s = {} by Th4;
then
A5: Fixed(r '&' s) = {} by QC_LANG3:67;
Free r = {} by Th4;
then Free r \/ Free s = {} by Th4;
then Free (r '&' s) = {} by QC_LANG3:57;
hence thesis by A5,Th4;
end;
definition
let A;
redefine func VERUM(A) -> Element of CQC-WFF(A);
coherence by Th6;
let r be Element of CQC-WFF(A);
redefine func 'not' r -> Element of CQC-WFF(A);
coherence by Th8;
let s be Element of CQC-WFF(A);
redefine func r '&' s -> Element of CQC-WFF(A);
coherence by Th9;
end;
theorem Th10:
for r,s being Element of CQC-WFF(A) holds
r => s is Element of CQC-WFF(A)
proof
let r,s be Element of CQC-WFF(A);
r => s = 'not' (r '&' 'not' s) by QC_LANG2:def 2;
hence thesis;
end;
theorem Th11:
for r,s being Element of CQC-WFF(A) holds
r 'or' s is Element of CQC-WFF(A)
proof
let r,s be Element of CQC-WFF(A);
r 'or' s = 'not' ('not' r '&' 'not' s) by QC_LANG2:def 3;
hence thesis;
end;
theorem Th12:
for r,s being Element of CQC-WFF(A) holds
r <=> s is Element of CQC-WFF(A)
proof
let r,s be Element of CQC-WFF(A);
r <=> s = (r => s) '&' (s => r) by QC_LANG2:def 4
.= ( 'not' (r '&' 'not' s) ) '&' (s => r) by QC_LANG2:def 2
.= ( 'not' (r '&' 'not' s) ) '&' ( 'not' (s '&' 'not' r) ) by
QC_LANG2:def 2;
hence thesis;
end;
definition
let A;
let r,s be Element of CQC-WFF(A);
redefine func r => s -> Element of CQC-WFF(A);
coherence by Th10;
redefine func r 'or' s -> Element of CQC-WFF(A);
coherence by Th11;
redefine func r <=> s -> Element of CQC-WFF(A);
coherence by Th12;
end;
theorem Th13:
for x being bound_QC-variable of A, p being Element of QC-WFF(A) holds
All(x,p) is Element of CQC-WFF(A) iff p is Element of CQC-WFF(A)
proof
let x be bound_QC-variable of A, p be Element of QC-WFF(A);
thus All(x,p) is Element of CQC-WFF(A) implies p is Element of CQC-WFF(A)
proof
assume
A1: All(x,p) is Element of CQC-WFF(A);
then Fixed All(x,p) = {} by Th4;
then
A2: Fixed p = {} by QC_LANG3:68;
Free All(x,p) = {} by A1,Th4;
then Free p = {} by QC_LANG3:58;
hence thesis by A2,Th4;
end;
assume
A3: p is Element of CQC-WFF(A);
then Fixed p = {} by Th4;
then
A4: Fixed All(x,p) = {} by QC_LANG3:68;
Free p = {} by A3,Th4;
then Free All(x,p) = {} by QC_LANG3:58;
hence thesis by A4,Th4;
end;
definition
let A;
let x be bound_QC-variable of A,r be Element of CQC-WFF(A);
redefine func All(x,r) -> Element of CQC-WFF(A);
coherence by Th13;
end;
theorem Th14:
for x being bound_QC-variable of A,r being Element of CQC-WFF(A) holds
Ex(x,r) is Element of CQC-WFF(A)
proof
let x be bound_QC-variable of A,r be Element of CQC-WFF(A);
Ex(x,r) = 'not' All(x,'not' r) by QC_LANG2:def 5;
hence thesis;
end;
definition
let A;
let x be bound_QC-variable of A,r be Element of CQC-WFF(A);
redefine func Ex(x,r) -> Element of CQC-WFF(A);
coherence by Th14;
end;
scheme
CQCInd { A() -> QC-alphabet, P[set] }
:
for r being Element of CQC-WFF(A()) holds P[r]
provided
A1: for r,s being Element of CQC-WFF(A())
for x being bound_QC-variable of A() for k
for l being CQC-variable_list of k, A() for P being
QC-pred_symbol of k,A() holds P[VERUM(A())] & P[P!l] &
(P[r] implies P['not' r]) & (P[r]
& P[s] implies P[r '&' s]) & (P[r] implies P[All(x, r)])
proof
defpred Prop[Element of QC-WFF(A())] means $1 is Element of CQC-WFF(A())
implies P[ $1 ];
A2: for p being Element of QC-WFF(A()) st Prop[p] holds Prop['not' p]
proof
let p be Element of QC-WFF(A());
assume
A3: Prop[p];
assume 'not' p is Element of CQC-WFF(A());
then p is Element of CQC-WFF(A()) by Th8;
hence thesis by A1,A3;
end;
A4: for p,q being Element of QC-WFF(A()) st Prop[p]
& Prop[q] holds Prop[p '&' q ]
proof
let p,q be Element of QC-WFF(A());
assume
A5: ( Prop[p])& Prop[q];
assume p '&' q is Element of CQC-WFF(A());
then p is Element of CQC-WFF(A()) & q is Element of CQC-WFF(A()) by Th9;
hence thesis by A1,A5;
end;
A6: for k being Nat, P being (QC-pred_symbol of k,A()), l being
QC-variable_list of k, A() holds Prop[P!l]
proof
let k be Nat, P be (QC-pred_symbol of k,A()),
l be QC-variable_list of k, A();
assume
A7: P!l is Element of CQC-WFF(A());
reconsider k as Nat;
reconsider l as QC-variable_list of k, A();
A8: { l.j :1 <= j & j <= len l & l.j in fixed_QC-variables(A()) } = {}
by Th7,A7;
{ l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A()) }
= {} by A7,Th7;
then l is CQC-variable_list of k, A() by A8,Th5;
hence thesis by A1;
end;
A9: for x being bound_QC-variable of A(), p being Element of QC-WFF(A())
st Prop[p] holds Prop[All(x, p)]
proof
let x be bound_QC-variable of A(), p be Element of QC-WFF(A());
assume
A10: Prop[p];
assume All(x,p) is Element of CQC-WFF(A());
then p is Element of CQC-WFF(A()) by Th13;
hence thesis by A1,A10;
end;
A11: Prop[VERUM(A())] by A1;
for p being Element of QC-WFF(A()) holds Prop[p]
from QC_LANG1:sch 1 (A6,A11,A2,A4,A9);
hence thesis;
end;
scheme
CQCFuncEx { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), A(set,set,set) -> (Element of D()),
N(set) -> (Element of D()), C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()} : ex F being Function of CQC-WFF(Al()),
D() st F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s)& F.All(x,r) = Q(x,F.r)
proof
deffunc q((Element of QC-WFF(Al())), Element of D()) = Q(bound_in $1,$2);
deffunc a(Element of QC-WFF(Al())) = A(the_arity_of the_pred_symbol_of $1,
the_pred_symbol_of $1,the_arguments_of $1);
consider F being Function of QC-WFF(Al()), D() such that
A1: F.VERUM(Al()) = V() & for p being Element of QC-WFF(Al())
holds (p is atomic implies F.p = a(p)) &
(p is negative implies F.p = N(F.the_argument_of p)) &
(p is conjunctive implies F.p = C(F.the_left_argument_of p, F.
the_right_argument_of p)) & (p is universal implies
F.p = q(p, F.the_scope_of p)) from QC_LANG1:sch 3;
reconsider G = F|CQC-WFF(Al()) as Function of CQC-WFF(Al()),D()
by FUNCT_2:32;
take G;
thus G.VERUM(Al()) = V() by A1,FUNCT_1:49;
let r,s being Element of CQC-WFF(Al());
let x being bound_QC-variable of Al();
let k;
let l be CQC-variable_list of k, Al();
let P be QC-pred_symbol of k,Al();
A2: the_arity_of P = k by QC_LANG1:11;
A3: P!l is atomic by QC_LANG1:def 18;
then
A4: the_arguments_of (P!l) = l & the_pred_symbol_of (P!l) = P by
QC_LANG1:def 22,def 23;
thus G.(P!l) = F.(P!l) by FUNCT_1:49
.= A(k,P,l) by A1,A3,A4,A2;
set r9 = G.r, s9 = G.s;
A5: r9 = F.r by FUNCT_1:49;
A6: r '&' s is conjunctive by QC_LANG1:def 20;
then
A7: the_left_argument_of(r '&' s) = r & the_right_argument_of(r '&' s) = s
by QC_LANG1:def 25,def 26;
A8: 'not' r is negative by QC_LANG1:def 19;
then
A9: the_argument_of 'not' r = r by QC_LANG1:def 24;
thus G.('not' r) = F.('not' r) by FUNCT_1:49
.= N(r9) by A1,A5,A8,A9;
A10: s9 = F.s by FUNCT_1:49;
thus G.(r '&' s) = F.(r '&' s) by FUNCT_1:49
.= C(r9,s9) by A1,A5,A10,A6,A7;
A11: All(x,r) is universal by QC_LANG1:def 21;
then
A12: bound_in All(x,r) = x & the_scope_of All(x,r)=r by QC_LANG1:def 27,def 28;
thus G.All(x,r) = F.All(x,r) by FUNCT_1:49
.= Q(x,r9) by A1,A5,A11,A12;
end;
scheme
CQCFuncUniq { Al() -> QC-alphabet, D() -> non empty set,
F1() -> (Function of CQC-WFF(Al()), D()),
F2()-> (Function of CQC-WFF(Al()), D()),
V() -> (Element of D()), A(set,set,set) -> (Element of D()),
N(set) -> (Element of D()), C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()} : F1() = F2()
provided
A1: F1().VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F1().(P!l) = A(k,P,l) &
F1().('not' r) = N(F1().r) & F1().(r '&' s) = C(F1().r,F1().s) &
F1().All(x,r) = Q(x,F1().r) and
A2: F2().VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F2().(P!l) =
A(k,P,l) & F2().('not' r) =
N(F2().r) & F2().(r '&' s) = C(F2().r,F2().s) & F2().All(x,r) = Q(x,F2().r)
proof
defpred P[set] means F1().$1 = F2().$1;
A3:for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P being
QC-pred_symbol of k,Al() holds P[VERUM(Al())] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]) &
(P[r] implies P[All(x, r)])
proof
let r,s be Element of CQC-WFF(Al());
let x be bound_QC-variable of Al();
let k;
let l be CQC-variable_list of k, Al();
let P be QC-pred_symbol of k,Al();
thus F1().VERUM(Al()) = F2().VERUM(Al()) by A1,A2;
F1().(P!l) = A(k,P,l) by A1;
hence F1().(P!l) = F2().(P!l) by A2;
F1().('not' r) = N(F1().r) by A1;
hence F1().r = F2().r implies F1().('not' r) = F2().('not' r) by A2;
F1().(r '&' s) = C(F1().r,F1().s) by A1;
hence F1().r = F2().r & F1().s = F2().s implies F1().(r '&' s) = F2().(r
'&' s) by A2;
F1().All(x,r) = Q(x,F1().r) by A1;
hence thesis by A2;
end;
for r being Element of CQC-WFF(Al()) holds P[r] from CQCInd(A3);
hence thesis by FUNCT_2:63;
end;
scheme
CQCDefcorrectness { Al() -> QC-alphabet, D() -> non empty set,
p() -> (Element of CQC-WFF(Al())), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), Q(set,set) -> Element of D()}
:
(ex d being Element of D() st ex F being Function of CQC-WFF(Al()),
D() st d = F.p() & F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P being
QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) ) &
for d1,d2 being Element of D() st (ex F being Function of CQC-WFF(Al()),
D() st d1 = F.p() & F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al()
holds F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) ) &
(ex F being Function of CQC-WFF(Al()), D() st d2 = F.p() &
F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) ) holds d1 = d2
proof
thus ex d being Element of D() st ex F being Function of CQC-WFF(Al()), D()
st d = F.p() & F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P being QC-pred_symbol of k,Al()
holds F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r)
proof
consider F being Function of CQC-WFF(Al()), D() such that
A1: F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r)
from CQCFuncEx;
take F.p(),F;
thus thesis by A1;
end;
let d1,d2 be Element of D();
given F1 being Function of CQC-WFF(Al()), D() such that
A2: d1 = F1.p() and
A3: F1.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F1.(P!l) = A(k,P,l) &
F1.('not' r) = N(F1.r) & F1.(r '&' s) = C(F1.r,F1.s) & F1.All(x,r) = Q(x,F1.r);
given F2 being Function of CQC-WFF(Al()), D() such that
A4: d2 = F2.p() and
A5: F2.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F2.(P!l) = A(k,P,l) &
F2.('not' r) = N(F2.r) & F2.(r '&' s) = C(F2.r,F2.s) &
F2.All(x,r) = Q(x,F2.r);
F1 = F2 from CQCFuncUniq(A3,A5);
hence thesis by A2,A4;
end;
scheme
CQCDefVERUM { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), Q(set,set) -> Element of D()} :
F(VERUM(Al())) = V()
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds
d = F (p) iff ex F being Function of CQC-WFF(Al()), D() st
d = F.p & F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r)
proof
ex F being Function of CQC-WFF(Al()), D() st F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r)
from CQCFuncEx;
hence thesis by A1;
end;
scheme
CQCDefatomic { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), F(set) -> (Element of D()),
A(set,set,set) -> (Element of D()), k() -> Nat, P()
-> (QC-pred_symbol of k(),Al()), l() -> (CQC-variable_list of k(), Al()),
N(set) -> (Element of D()), C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()}
: F(P()!l()) = A(k(),P(),l())
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds d = F
(p) iff ex F being Function of CQC-WFF(Al()), D()
st d = F.p & F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds
F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r)
proof
consider F being Function of CQC-WFF(Al()), D() such that
A2: F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) from CQCFuncEx;
A(k(),P(),l()) = F.(P()!l()) by A2;
hence thesis by A1,A2;
end;
scheme
CQCDefnegative { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
r() -> (Element of CQC-WFF(Al())), C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()}
:
F('not' r()) = N(F(r()))
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds
d = F (p) iff ex F being Function of CQC-WFF(Al()), D() st
d = F.p & F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds
F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r)
proof
consider G being Function of CQC-WFF(Al()), D() such that
A2: F(r()) = G.r() and
A3: G.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds G.(P!l) = A(k,P,l) &
G.('not' r) = N(G.r) &
G.(r '&' s) = C(G.r,G.s) & G.All(x,r) = Q(x,G.r) by A1;
consider F being Function of CQC-WFF(Al()), D() such that
A4: F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r)
from CQCFuncEx;
A5: F.('not' r()) = N(F.r()) by A4;
F = G from CQCFuncUniq(A4,A3);
hence thesis by A1,A4,A5,A2;
end;
scheme
QCDefconjunctive { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), r() -> (Element of CQC-WFF(Al())),
s() -> (Element of CQC-WFF(Al())), Q(set,set) -> Element of D()}
:
F(r() '&' s()) = C(F(r()), F(s()))
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds d = F
(p) iff ex F being Function of CQC-WFF(Al()), D() st d = F.p &
F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds
F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r)
proof
consider F2 being Function of CQC-WFF(Al()), D() such that
A2: F(s()) = F2.s() and
A3: F2.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F2.(P!l) = A(k,P,l) &
F2.('not' r) = N(F2.r)
& F2.(r '&' s) = C(F2.r,F2.s) & F2.All(x,r) = Q(x,F2.r) by A1;
consider F1 being Function of CQC-WFF(Al()), D() such that
A4: F(r()) = F1.r() and
A5: F1.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for
P being QC-pred_symbol of k,Al() holds F1.(P!l) = A(k,P,l) &
F1.('not' r) = N(F1.r)
& F1.(r '&' s) = C(F1.r,F1.s) & F1.All(x,r) = Q(x,F1.r) by A1;
consider F being Function of CQC-WFF(Al()), D() such that
A6: F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r)
from CQCFuncEx;
A7: F.(r() '&' s()) = C(F.r(),F.s()) by A6;
A8: F = F2 from CQCFuncUniq(A6,A3);
F = F1 from CQCFuncUniq(A6,A5);
hence thesis by A1,A6,A7,A4,A2,A8;
end;
scheme
QCDefuniversal { Al() -> QC-alphabet, D() -> non empty set,
F(set) -> (Element of D()), V() -> (Element of D()),
A(set,set,set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), Q(set,set) -> (Element of D()),
x() -> bound_QC-variable of Al(), r() -> Element of CQC-WFF(Al())}
:
F(All(x(),r())) = Q(x(),F(r()))
provided
A1: for p being (Element of CQC-WFF(Al())), d being Element of D() holds d = F
(p) iff ex F being Function of CQC-WFF(Al()), D() st
d = F.p & F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al()
for P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r)
proof
consider G being Function of CQC-WFF(Al()), D() such that
A2: F(r()) = G.r() and
A3: G.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds
G.(P!l) = A(k,P,l) & G.('not' r) = N(G.r) &
G.(r '&' s) = C(G.r,G.s) & G.All(x,r) = Q(x,G.r) by A1;
consider F being Function of CQC-WFF(Al()), D() such that
A4: F.VERUM(Al()) = V() &
for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k, Al() for P
being QC-pred_symbol of k,Al() holds
F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) from CQCFuncEx;
A5: F.All(x(),r()) = Q(x(),F.r()) by A4;
F = G from CQCFuncUniq(A4,A3);
hence thesis by A1,A4,A5,A2;
end;
reserve x,y for bound_QC-variable of A;
reserve a for free_QC-variable of A;
reserve p,q for Element of QC-WFF(A);
reserve l,l1,l2,ll for FinSequence of QC-variables(A);
reserve r,s for Element of CQC-WFF(A);
Lm2: for F1,F2 being Function of QC-WFF(A),QC-WFF(A) st
( for q holds F1.VERUM(A) = VERUM(A) & (q is atomic implies F1.q =
(the_pred_symbol_of q)!Subst( the_arguments_of q,(A)a.0.-->x)) &
(q is negative implies F1.q = 'not' (F1.
the_argument_of q) ) & (q is conjunctive implies F1.q = (F1.
the_left_argument_of q) '&' (F1.the_right_argument_of q)) & (q is universal
implies F1.q = IFEQ(bound_in q,x,q,All(bound_in q,F1.the_scope_of q)))) & ( for
q holds F2.VERUM(A) = VERUM(A) & (q is atomic implies F2.q =
(the_pred_symbol_of q)!
Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative implies
F2.q = 'not' (F2.the_argument_of q) ) & (q is conjunctive implies F2.q = (F2.
the_left_argument_of q) '&' (F2.the_right_argument_of q)) & (q is universal
implies F2.q = IFEQ(bound_in q,x,q,All(bound_in q,F2.the_scope_of q)))) holds
F1 = F2
proof
deffunc c((Element of QC-WFF(A)), Element of QC-WFF(A)) = $1 '&' $2;
deffunc n(Element of QC-WFF(A)) = 'not' ($1);
let F1,F2 be Function of QC-WFF(A),QC-WFF(A);
deffunc a(Element of QC-WFF(A)) = (the_pred_symbol_of $1)!Subst(
the_arguments_of $1,(A)a.0.-->x);
deffunc q((Element of QC-WFF(A)), Element of QC-WFF(A)) =
IFEQ(bound_in $1,x,$1,All(bound_in $1,$2));
assume for q holds F1.VERUM(A) = VERUM(A) &
(q is atomic implies F1.q = a(q)) & (q is negative implies
F1.q = 'not' (F1.the_argument_of q) ) & (q is conjunctive
implies F1.q = (F1.the_left_argument_of q) '&' (F1.the_right_argument_of q)) &
(q is universal implies F1.q = IFEQ(bound_in q,x,q,All(bound_in q,F1.
the_scope_of q)));
then
A1: for p being Element of QC-WFF(A) for d1,d2 being Element of QC-WFF(A)
holds (p = VERUM(A) implies F1.p = VERUM(A)) &
(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));
assume for q holds F2.VERUM(A) = VERUM(A) & (q is atomic implies F2.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F2.q = 'not' (F2.the_argument_of q) ) & (q is conjunctive implies F2.q
= (F2.the_left_argument_of q) '&' (F2.the_right_argument_of q)) & (q is
universal implies F2.q = IFEQ(bound_in q,x,q,All(bound_in q,F2.the_scope_of q))
);
then
A2: for p being Element of QC-WFF(A) for d1,d2 being Element of QC-WFF(A)
holds (p = VERUM(A) implies F2.p = VERUM(A)) &
(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));
thus F1 = F2 from QC_LANG3:sch 1(A1,A2);
end;
definition
let A,p,x;
func p.x -> Element of QC-WFF(A) means
:Def3:
ex F being Function of QC-WFF(A),
QC-WFF(A) st it = F.p & for q holds F.VERUM(A) = VERUM(A) &
(q is atomic implies F.q =
(the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) &
(q is negative implies F.q = 'not' (F.the_argument_of q) ) &
(q is conjunctive implies F.q = (F.the_left_argument_of q) '&'
(F.the_right_argument_of q)) & (q is universal implies F.q =
IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q)));
existence
proof
deffunc q((Element of QC-WFF(A)), Element of QC-WFF(A)) =
IFEQ(bound_in $1,x,$1,
All(bound_in $1,$2));
deffunc c((Element of QC-WFF(A)), Element of QC-WFF(A)) = $1 '&' $2;
deffunc n(Element of QC-WFF(A)) = 'not' ($1);
deffunc a(Element of QC-WFF(A)) = (the_pred_symbol_of $1)!Subst(
the_arguments_of $1,(A)a.0.-->x);
consider F being Function of QC-WFF(A), QC-WFF(A) such that
A1: F.VERUM(A) = VERUM(A) & for p being Element of QC-WFF(A) holds (p is atomic
implies F.p = a(p)) & (p is negative implies F.p = n(F.the_argument_of p)) & (p
is conjunctive implies F.p = c(F.the_left_argument_of p,F.the_right_argument_of
p)) & (p is universal implies F.p = q(p,F.the_scope_of p)) from QC_LANG1:sch 3;
take F.p,F;
thus F.p = F.p;
thus thesis by A1;
end;
uniqueness by Lm2;
end;
theorem Th15:
VERUM(A).x = VERUM(A)
proof
ex F being Function of QC-WFF(A),QC-WFF(A) st VERUM(A).x = F.VERUM(A) &
for q holds F.VERUM(A) = VERUM(A) &
(q is atomic implies F.q =
(the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) &
(q is negative implies F.q = 'not' (F.the_argument_of q) ) &
(q is conjunctive implies F.q = (F.the_left_argument_of
q) '&' (F.the_right_argument_of q)) & (q is universal implies F.q = IFEQ(
bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
hence thesis;
end;
theorem Th16:
p is atomic implies p.x = (the_pred_symbol_of p)!Subst(
the_arguments_of p,(A)a.0.-->x)
proof
ex F being Function of QC-WFF(A),QC-WFF(A) st p.x = F.p &
for q holds F.VERUM(A)= VERUM(A) &
(q is atomic implies F.q = (the_pred_symbol_of q)!Subst(
the_arguments_of q,(A)a.0.-->x)) & (q is negative implies F.q = 'not' (F.
the_argument_of q) ) & (q is conjunctive implies F.q = (F.the_left_argument_of
q) '&' (F.the_right_argument_of q)) & (q is universal implies F.q = IFEQ(
bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
hence thesis;
end;
theorem Th17:
for k being Nat
for P being QC-pred_symbol of k,A for l being QC-variable_list of
k,A holds (P!l).x = P!Subst(l,(A)a.0.-->x)
proof let k be Nat;
let P be QC-pred_symbol of k,A;
let l be QC-variable_list of k, A;
reconsider P9 = P as QC-pred_symbol of A;
A1: P!l is atomic by QC_LANG1:def 18;
then the_arguments_of (P!l) = l & the_pred_symbol_of (P!l) = P9 by
QC_LANG1:def 22,def 23;
hence thesis by A1,Th16;
end;
theorem Th18:
p is negative implies p.x = 'not'((the_argument_of p).x)
proof
consider F being Function of QC-WFF(A),QC-WFF(A) such that
A1: p.x = F.p and
A2: for q holds F.VERUM(A) = VERUM(A) & (q is atomic implies F.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F.q = 'not' (F.the_argument_of q) ) & (q is conjunctive implies F.q = (
F.the_left_argument_of q) '&' (F.the_right_argument_of q)) & (q is universal
implies F.q = IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
consider G being Function of QC-WFF(A),QC-WFF(A) such that
A3: (the_argument_of p).x = G.(the_argument_of p) and
A4: for q holds G.VERUM(A) = VERUM(A) & (q is atomic implies G.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies G.q = 'not' (G.the_argument_of q) ) & (q is conjunctive implies G.q = (
G.the_left_argument_of q) '&' (G.the_right_argument_of q)) & (q is universal
implies G.q = IFEQ(bound_in q,x,q,All(bound_in q,G.the_scope_of q))) by Def3;
F = G by A2,A4,Lm2;
hence thesis by A1,A2,A3;
end;
theorem Th19:
('not' p).x = 'not'(p.x)
proof
set 9p = 'not' p;
A1: 9p is negative by QC_LANG1:def 19;
then the_argument_of 9p = p by QC_LANG1:def 24;
hence thesis by A1,Th18;
end;
theorem Th20:
p is conjunctive implies p.x = ((the_left_argument_of p).x) '&'
((the_right_argument_of p).x)
proof
consider F being Function of QC-WFF(A),QC-WFF(A) such that
A1: p.x = F.p and
A2: for q holds F.VERUM(A) = VERUM(A) & (q is atomic implies F.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F.q = 'not' (F.the_argument_of q) ) & (q is conjunctive implies F.q = (
F.the_left_argument_of q) '&' (F.the_right_argument_of q)) & (q is universal
implies F.q = IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
consider F2 being Function of QC-WFF(A),QC-WFF(A) such that
A3: (the_right_argument_of p).x = F2.(the_right_argument_of p) and
A4: for q holds F2.VERUM(A) = VERUM(A) & (q is atomic implies F2.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F2.q = 'not' (F2.the_argument_of q) ) & (q is conjunctive implies F2.q
= (F2.the_left_argument_of q) '&' (F2.the_right_argument_of q)) & (q is
universal implies F2.q = IFEQ(bound_in q,x,q,All(bound_in q,F2.the_scope_of q))
) by Def3;
A5: F2 = F by A2,A4,Lm2;
consider F1 being Function of QC-WFF(A),QC-WFF(A) such that
A6: (the_left_argument_of p).x = F1.(the_left_argument_of p) and
A7: for q holds F1.VERUM(A) = VERUM(A) & (q is atomic implies F1.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F1.q = 'not' (F1.the_argument_of q) ) & (q is conjunctive implies F1.q
= (F1.the_left_argument_of q) '&' (F1.the_right_argument_of q)) & (q is
universal implies F1.q = IFEQ(bound_in q,x,q,All(bound_in q,F1.the_scope_of q))
) by Def3;
F1 = F by A2,A7,Lm2;
hence thesis by A1,A2,A6,A3,A5;
end;
theorem Th21:
(p '&' q).x = (p.x) '&' (q.x)
proof
set pq = p '&' q;
A1: p '&' q is conjunctive by QC_LANG1:def 20;
then the_left_argument_of pq = p & the_right_argument_of pq = q by
QC_LANG1:def 25,def 26;
hence thesis by A1,Th20;
end;
Lm3: p is universal implies p.x = IFEQ(bound_in p,x,p,All(bound_in p,(
the_scope_of p).x))
proof
consider F being Function of QC-WFF(A),QC-WFF(A) such that
A1: p.x = F.p and
A2: for q holds F.VERUM(A) = VERUM(A) & (q is atomic implies F.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies F.q = 'not' (F.the_argument_of q) ) & (q is conjunctive implies F.q = (
F.the_left_argument_of q) '&' (F.the_right_argument_of q)) & (q is universal
implies F.q = IFEQ(bound_in q,x,q,All(bound_in q,F.the_scope_of q))) by Def3;
consider G being Function of QC-WFF(A),QC-WFF(A) such that
A3: (the_scope_of p).x = G.(the_scope_of p) and
A4: for q holds G.VERUM(A) = VERUM(A) & (q is atomic implies G.q = (
the_pred_symbol_of q)!Subst(the_arguments_of q,(A)a.0.-->x)) & (q is negative
implies G.q = 'not' (G.the_argument_of q) ) & (q is conjunctive implies G.q = (
G.the_left_argument_of q) '&' (G.the_right_argument_of q)) & (q is universal
implies G.q = IFEQ(bound_in q,x,q,All(bound_in q,G.the_scope_of q))) by Def3;
F = G by A2,A4,Lm2;
hence thesis by A1,A2,A3;
end;
theorem Th22:
p is universal & bound_in p = x implies p.x = p
proof
assume p is universal;
then (p.x) = IFEQ(bound_in p,x,p,All(bound_in p,(the_scope_of p).x)) by Lm3;
hence thesis by FUNCOP_1:def 8;
end;
theorem Th23:
p is universal & bound_in p <> x implies p.x = All(bound_in p,(
the_scope_of p).x)
proof
assume p is universal;
then (p.x) = IFEQ(bound_in p,x,p,All(bound_in p,(the_scope_of p).x)) by Lm3;
hence thesis by FUNCOP_1:def 8;
end;
theorem Th24:
(All(x,p)).x = All(x,p)
proof
set q = All(x,p);
A1: q is universal by QC_LANG1:def 21;
then bound_in q = x by QC_LANG1:def 27;
hence thesis by A1,Th22;
end;
theorem Th25:
x<>y implies (All(x,p)).y = All(x,p.y)
proof
set q = All(x,p);
A1: q is universal by QC_LANG1:def 21;
then the_scope_of q = p & bound_in q = x by QC_LANG1:def 27,def 28;
hence thesis by A1,Th23;
end;
theorem Th26:
Free p = {} implies p.x = p
proof
defpred P[Element of QC-WFF(A)] means Free $1 = {} implies $1.x = $1;
A1: for p st P[p] holds P['not' p] by Th19,QC_LANG3:55;
A2: for p,q st P[p] & P[q] holds P[p '&' q]
proof
let p,q;
assume
A3: ( Free p = {} implies p.x = p)&( Free q = {} implies q.x = q);
assume Free(p '&' q) = {};
then (Free p) \/ (Free q) = {} by QC_LANG3:57;
hence thesis by A3,Th21;
end;
A4: for k being Nat
for P being (QC-pred_symbol of k,A),l being QC-variable_list of k, A
holds P[P!l]
proof
let k be Nat;
let P be (QC-pred_symbol of k,A),l be QC-variable_list of k, A;
assume
A5: Free(P!l) = {};
A6: now
let j be Nat;
assume
A7: 1 <= j & j <= len l;
now
assume l.j = (A)a.0;
then (A)a.0 in { l.i where i is Nat : 1 <= i &
i <= len l & l.i in free_QC-variables(A) }
by A7;
hence contradiction by A5,QC_LANG3:54;
end;
hence Subst(l,(A)a.0.-->x).j = l.j by A7,Th3;
end;
len Subst(l,(A)a.0.-->x) = len l by Def1;
then Subst(l,(A)a.0.-->x) = l by A6,FINSEQ_1:14;
hence thesis by Th17;
end;
A8: for y,p st P[p] holds P[All(y, p)]
proof
let y,p;
assume
A9: Free p = {} implies p.x = p;
A10: x = y implies All(y, p).x = All(y, p) by Th24;
assume Free All(y,p) = {};
hence thesis by A9,A10,Th25,QC_LANG3:58;
end;
A11: P[VERUM(A)] by Th15;
for p holds P[p] from QC_LANG1:sch 1(A4,A11,A1,A2,A8);
hence thesis;
end;
theorem
r.x = r
proof
Free r = {} by Th4;
hence thesis by Th26;
end;
theorem
Fixed(p.x) = Fixed p
proof
defpred P[Element of QC-WFF(A)] means Fixed($1.x) = Fixed $1;
A1: for p st P[p] holds P['not' p]
proof
let p such that
A2: Fixed (p.x) = Fixed p;
thus Fixed(('not' p).x) = Fixed('not' (p.x)) by Th19
.= Fixed p by A2,QC_LANG3:65
.= Fixed 'not' p by QC_LANG3:65;
end;
A3: for p,q st P[p] & P[q] holds P[p '&' q]
proof
let p,q such that
A4: Fixed(p.x) = Fixed(p) & Fixed(q.x) = Fixed q;
thus Fixed((p '&' q).x) = Fixed((p.x) '&' (q.x)) by Th21
.= Fixed(p) \/ Fixed(q) by A4,QC_LANG3:67
.= Fixed (p '&' q) by QC_LANG3:67;
end;
A5: for k for P being (QC-pred_symbol of k,A),l being QC-variable_list of k, A
holds P[P!l]
proof
let k;
let P be (QC-pred_symbol of k,A),l be QC-variable_list of k, A;
set F1 = { l.i : 1 <= i & i <= len l & l.i in fixed_QC-variables(A) };
set ll = Subst(l,(A)a.0.-->x);
set F2 = { ll.i : 1 <= i & i <= len ll & ll.i in fixed_QC-variables(A) };
A6: len l = len ll by Def1;
now
let y be object;
thus y in F1 implies y in F2
proof
assume y in F1;
then consider i such that
A7: y = l.i and
A8: 1 <= i & i <= len l and
A9: l.i in fixed_QC-variables(A);
l.i <> (A)a.0 by A9,QC_LANG3:32;
then ll.i = l.i by A8,Th3;
hence thesis by A6,A7,A8,A9;
end;
assume y in F2;
then consider i such that
A10: y = ll.i and
A11: 1 <= i & i <= len ll and
A12: ll.i in fixed_QC-variables(A);
now
assume l.i = (A)a.0;
then ll.i = x by A6,A11,Th3;
hence contradiction by A12,Lm1;
end;
then ll.i = l.i by A6,A11,Th3;
hence y in F1 by A6,A10,A11,A12;
end;
then
A13: F1 = F2 by TARSKI:2;
Fixed(P!l) = F1 & Fixed(P!ll) = F2 by QC_LANG3:64;
hence thesis by A13,Th17;
end;
A14: for y,p st P[p] holds P[All(y,p)]
proof
let y,p such that
A15: Fixed(p.x) = Fixed p;
now
assume x <> y;
hence Fixed(All(y,p).x) = Fixed(All(y,p.x)) by Th25
.= Fixed(p) by A15,QC_LANG3:68
.= Fixed(All(y,p)) by QC_LANG3:68;
end;
hence thesis by Th24;
end;
A16: P[VERUM(A)] by Th15;
for p holds P[p] from QC_LANG1:sch 1(A5,A16,A1,A3,A14);
hence thesis;
end;