:: A First-Order Predicate Calculus. Axiomatics, the Consequence Operation and a Concept of Proof :: by Agata Darmochwa{\l} :: :: Received May 25, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem Th1: :: CQC_THE1:1 for n being Element of NAT holds { k where k is Element of NAT : k <= n + 1 } = { i where i is Element of NAT : i <= n } \/ {(n + 1)} proofend; theorem Th2: :: CQC_THE1:2 for n being Element of NAT holds { k where k is Element of NAT : k <= n } is finite proofend; theorem :: CQC_THE1:3 for X, Y, Z being set st X is finite & X c= [:Y,Z:] holds ex A, B being set st ( A is finite & A c= Y & B is finite & B c= Z & X c= [:A,B:] ) by FINSET_1:13; theorem :: CQC_THE1:4 for X, Z, Y being set st X is finite & Z is finite & X c= [:Y,Z:] holds ex A being set st ( A is finite & A c= Y & X c= [:A,Z:] ) by FINSET_1:14; definition let Al be QC-alphabet ; let T be Subset of (CQC-WFF Al); attrT is being_a_theory means :Def1: :: CQC_THE1:def 1 ( VERUM Al in T & ( for p, q, r being Element of CQC-WFF Al for s being QC-formula of Al for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) ); end; :: deftheorem Def1 defines being_a_theory CQC_THE1:def_1_:_ for Al being QC-alphabet for T being Subset of (CQC-WFF Al) holds ( T is being_a_theory iff ( VERUM Al in T & ( for p, q, r being Element of CQC-WFF Al for s being QC-formula of Al for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in T & p => (('not' p) => q) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p '&' q) => (q '&' p) in T & ( p in T & p => q in T implies q in T ) & (All (x,p)) => p in T & ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T implies s . y in T ) ) ) ) ); theorem :: CQC_THE1:5 for Al being QC-alphabet for T, S being Subset of (CQC-WFF Al) st T is being_a_theory & S is being_a_theory holds T /\ S is being_a_theory proofend; :: --------- The consequence operation definition let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); func Cn X -> Subset of (CQC-WFF Al) means :Def2: :: CQC_THE1:def 2 for t being Element of CQC-WFF Al holds ( t in it iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ); existence ex b1 being Subset of (CQC-WFF Al) st for t being Element of CQC-WFF Al holds ( t in b1 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) proofend; uniqueness for b1, b2 being Subset of (CQC-WFF Al) st ( for t being Element of CQC-WFF Al holds ( t in b1 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) ) & ( for t being Element of CQC-WFF Al holds ( t in b2 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Cn CQC_THE1:def_2_:_ for Al being QC-alphabet for X, b3 being Subset of (CQC-WFF Al) holds ( b3 = Cn X iff for t being Element of CQC-WFF Al holds ( t in b3 iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) ); theorem Th6: :: CQC_THE1:6 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds VERUM Al in Cn X proofend; theorem Th7: :: CQC_THE1:7 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds (('not' p) => p) => p in Cn X proofend; theorem Th8: :: CQC_THE1:8 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in Cn X proofend; theorem Th9: :: CQC_THE1:9 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X proofend; theorem Th10: :: CQC_THE1:10 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in Cn X proofend; theorem Th11: :: CQC_THE1:11 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al st p in Cn X & p => q in Cn X holds q in Cn X proofend; theorem Th12: :: CQC_THE1:12 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al for x being bound_QC-variable of Al holds (All (x,p)) => p in Cn X proofend; theorem Th13: :: CQC_THE1:13 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al st p => q in Cn X & not x in still_not-bound_in p holds p => (All (x,q)) in Cn X proofend; theorem Th14: :: CQC_THE1:14 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for s being QC-formula of Al for x, y being bound_QC-variable of Al st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Cn X holds s . y in Cn X proofend; theorem Th15: :: CQC_THE1:15 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds Cn X is being_a_theory proofend; theorem Th16: :: CQC_THE1:16 for Al being QC-alphabet for T, X being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds Cn X c= T proofend; theorem Th17: :: CQC_THE1:17 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds X c= Cn X proofend; theorem Th18: :: CQC_THE1:18 for Al being QC-alphabet for X, Y being Subset of (CQC-WFF Al) st X c= Y holds Cn X c= Cn Y proofend; Lm1: for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds Cn (Cn X) c= Cn X proofend; theorem :: CQC_THE1:19 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds Cn (Cn X) = Cn X proofend; theorem Th20: :: CQC_THE1:20 for Al being QC-alphabet for T being Subset of (CQC-WFF Al) holds ( T is being_a_theory iff Cn T = T ) proofend; :: ---------- The notion of proof definition func Proof_Step_Kinds -> set equals :: CQC_THE1:def 3 { k where k is Element of NAT : k <= 9 } ; coherence { k where k is Element of NAT : k <= 9 } is set ; end; :: deftheorem defines Proof_Step_Kinds CQC_THE1:def_3_:_ Proof_Step_Kinds = { k where k is Element of NAT : k <= 9 } ; registration cluster Proof_Step_Kinds -> non empty ; coherence not Proof_Step_Kinds is empty proofend; end; theorem Th21: :: CQC_THE1:21 ( 0 in Proof_Step_Kinds & 1 in Proof_Step_Kinds & 2 in Proof_Step_Kinds & 3 in Proof_Step_Kinds & 4 in Proof_Step_Kinds & 5 in Proof_Step_Kinds & 6 in Proof_Step_Kinds & 7 in Proof_Step_Kinds & 8 in Proof_Step_Kinds & 9 in Proof_Step_Kinds ) ; theorem :: CQC_THE1:22 Proof_Step_Kinds is finite by Th2; theorem Th23: :: CQC_THE1:23 for Al being QC-alphabet for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] for n being Nat st 1 <= n & n <= len f & not (f . n) `2 = 0 & not (f . n) `2 = 1 & not (f . n) `2 = 2 & not (f . n) `2 = 3 & not (f . n) `2 = 4 & not (f . n) `2 = 5 & not (f . n) `2 = 6 & not (f . n) `2 = 7 & not (f . n) `2 = 8 holds (f . n) `2 = 9 proofend; definition let Al be QC-alphabet ; let PR be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; let n be Nat; let X be Subset of (CQC-WFF Al); predPR,n is_a_correct_step_wrt X means :Def4: :: CQC_THE1:def 4 (PR . n) `1 in X if (PR . n) `2 = 0 (PR . n) `1 = VERUM Al if (PR . n) `2 = 1 ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p if (PR . n) `2 = 2 ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) if (PR . n) `2 = 3 ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) if (PR . n) `2 = 4 ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) if (PR . n) `2 = 5 ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p if (PR . n) `2 = 6 ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) if (PR . n) `2 = 7 ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) if (PR . n) `2 = 8 ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) if (PR . n) `2 = 9 ; consistency ( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( (PR . n) `1 in X iff (PR . n) `1 = VERUM Al ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 3 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 4 implies ( (PR . n) `1 in X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 5 implies ( (PR . n) `1 in X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 6 implies ( (PR . n) `1 in X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 7 implies ( (PR . n) `1 in X iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( (PR . n) `1 in X iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( (PR . n) `1 in X iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( (PR . n) `1 = VERUM Al iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( (PR . n) `1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( (PR . n) `1 = VERUM Al iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 5 implies ( (PR . n) `1 = VERUM Al iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( (PR . n) `1 = VERUM Al iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( (PR . n) `1 = VERUM Al iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( (PR . n) `1 = VERUM Al iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( (PR . n) `1 = VERUM Al iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 5 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 5 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 6 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 7 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 7 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) ) ; end; :: deftheorem Def4 defines is_a_correct_step_wrt CQC_THE1:def_4_:_ for Al being QC-alphabet for PR being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] for n being Nat for X being Subset of (CQC-WFF Al) holds ( ( (PR . n) `2 = 0 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) `1 in X ) ) & ( (PR . n) `2 = 1 implies ( PR,n is_a_correct_step_wrt X iff (PR . n) `1 = VERUM Al ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al st (PR . n) `1 = (('not' p) => p) => p ) ) & ( (PR . n) `2 = 3 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = p => (('not' p) => q) ) ) & ( (PR . n) `2 = 4 implies ( PR,n is_a_correct_step_wrt X iff ex p, q, r being Element of CQC-WFF Al st (PR . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) ) ) & ( (PR . n) `2 = 5 implies ( PR,n is_a_correct_step_wrt X iff ex p, q being Element of CQC-WFF Al st (PR . n) `1 = (p '&' q) => (q '&' p) ) ) & ( (PR . n) `2 = 6 implies ( PR,n is_a_correct_step_wrt X iff ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (PR . n) `1 = (All (x,p)) => p ) ) & ( (PR . n) `2 = 7 implies ( PR,n is_a_correct_step_wrt X iff ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) ) ) & ( (PR . n) `2 = 8 implies ( PR,n is_a_correct_step_wrt X iff ex i being Element of NAT ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ( 1 <= i & i < n & (PR . i) `1 = p => q & not x in still_not-bound_in p & (PR . n) `1 = p => (All (x,q)) ) ) ) & ( (PR . n) `2 = 9 implies ( PR,n is_a_correct_step_wrt X iff ex i being Element of NAT ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st ( 1 <= i & i < n & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (PR . i) `1 & s . y = (PR . n) `1 ) ) ) ); definition let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; predf is_a_proof_wrt X means :Def5: :: CQC_THE1:def 5 ( f <> {} & ( for n being Element of NAT st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt X ) ); end; :: deftheorem Def5 defines is_a_proof_wrt CQC_THE1:def_5_:_ for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] holds ( f is_a_proof_wrt X iff ( f <> {} & ( for n being Element of NAT st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt X ) ) ); theorem :: CQC_THE1:24 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds rng f <> {} proofend; theorem Th25: :: CQC_THE1:25 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds 1 <= len f proofend; theorem :: CQC_THE1:26 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] holds ( not f is_a_proof_wrt X or (f . 1) `2 = 0 or (f . 1) `2 = 1 or (f . 1) `2 = 2 or (f . 1) `2 = 3 or (f . 1) `2 = 4 or (f . 1) `2 = 5 or (f . 1) `2 = 6 ) proofend; theorem Th27: :: CQC_THE1:27 for Al being QC-alphabet for n being Element of NAT for X being Subset of (CQC-WFF Al) for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len f holds ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X ) proofend; theorem Th28: :: CQC_THE1:28 for Al being QC-alphabet for n being Element of NAT for X being Subset of (CQC-WFF Al) for g, f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt X holds f ^ g,n + (len f) is_a_correct_step_wrt X proofend; theorem Th29: :: CQC_THE1:29 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for f, g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & g is_a_proof_wrt X holds f ^ g is_a_proof_wrt X proofend; theorem :: CQC_THE1:30 for Al being QC-alphabet for X, Y being Subset of (CQC-WFF Al) for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & X c= Y holds f is_a_proof_wrt Y proofend; theorem Th31: :: CQC_THE1:31 for Al being QC-alphabet for l being Element of NAT for X being Subset of (CQC-WFF Al) for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X & 1 <= l & l <= len f holds (f . l) `1 in Cn X proofend; definition let Al be QC-alphabet ; let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; assume A1: f <> {} ; func Effect f -> Element of CQC-WFF Al equals :Def6: :: CQC_THE1:def 6 (f . (len f)) `1 ; coherence (f . (len f)) `1 is Element of CQC-WFF Al proofend; end; :: deftheorem Def6 defines Effect CQC_THE1:def_6_:_ for Al being QC-alphabet for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f <> {} holds Effect f = (f . (len f)) `1 ; theorem Th32: :: CQC_THE1:32 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds Effect f in Cn X proofend; Lm2: for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) } c= CQC-WFF Al proofend; theorem Th33: :: CQC_THE1:33 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds X c= { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } proofend; Lm3: for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds VERUM Al in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } proofend; Lm4: for Al being QC-alphabet for p being Element of CQC-WFF Al for X being Subset of (CQC-WFF Al) holds (('not' p) => p) => p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } proofend; Lm5: for Al being QC-alphabet for p, q being Element of CQC-WFF Al for X being Subset of (CQC-WFF Al) holds p => (('not' p) => q) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } proofend; Lm6: for Al being QC-alphabet for p, q, r being Element of CQC-WFF Al for X being Subset of (CQC-WFF Al) holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } proofend; Lm7: for Al being QC-alphabet for p, q being Element of CQC-WFF Al for X being Subset of (CQC-WFF Al) holds (p '&' q) => (q '&' p) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } proofend; Lm8: for Al being QC-alphabet for p, q being Element of CQC-WFF Al for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } & p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = G ) } holds q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = H ) } proofend; Lm9: for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for X being Subset of (CQC-WFF Al) holds (All (x,p)) => p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } proofend; Lm10: for Al being QC-alphabet for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for X being Subset of (CQC-WFF Al) st p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } & not x in still_not-bound_in p holds p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = G ) } proofend; Lm11: for Al being QC-alphabet for s being QC-formula of Al for x, y being bound_QC-variable of Al for X being Subset of (CQC-WFF Al) st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) } holds s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = G ) } proofend; theorem Th34: :: CQC_THE1:34 for Al being QC-alphabet for Y, X being Subset of (CQC-WFF Al) st Y = { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) } holds Y is being_a_theory proofend; Lm12: for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) } c= Cn X proofend; theorem Th35: :: CQC_THE1:35 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds { p where p is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) } = Cn X proofend; theorem Th36: :: CQC_THE1:36 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds ( p in Cn X iff ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) ) proofend; theorem :: CQC_THE1:37 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al st p in Cn X holds ex Y being Subset of (CQC-WFF Al) st ( Y c= X & Y is finite & p in Cn Y ) proofend; :: --------- TAUT(Al) - the set of all tautologies definition let Al be QC-alphabet ; func TAUT Al -> Subset of (CQC-WFF Al) equals :: CQC_THE1:def 7 Cn ({} (CQC-WFF Al)); correctness coherence Cn ({} (CQC-WFF Al)) is Subset of (CQC-WFF Al); ; end; :: deftheorem defines TAUT CQC_THE1:def_7_:_ for Al being QC-alphabet holds TAUT Al = Cn ({} (CQC-WFF Al)); theorem Th38: :: CQC_THE1:38 for Al being QC-alphabet for T being Subset of (CQC-WFF Al) st T is being_a_theory holds TAUT Al c= T proofend; theorem :: CQC_THE1:39 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds TAUT Al c= Cn X by Th15, Th38; theorem :: CQC_THE1:40 for Al being QC-alphabet holds TAUT Al is being_a_theory by Th15; theorem Th41: :: CQC_THE1:41 for Al being QC-alphabet holds VERUM Al in TAUT Al proofend; theorem :: CQC_THE1:42 for Al being QC-alphabet for p being Element of CQC-WFF Al holds (('not' p) => p) => p in TAUT Al proofend; theorem :: CQC_THE1:43 for Al being QC-alphabet for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in TAUT Al proofend; theorem :: CQC_THE1:44 for Al being QC-alphabet for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al proofend; theorem :: CQC_THE1:45 for Al being QC-alphabet for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in TAUT Al proofend; theorem :: CQC_THE1:46 for Al being QC-alphabet for p, q being Element of CQC-WFF Al st p in TAUT Al & p => q in TAUT Al holds q in TAUT Al proofend; theorem :: CQC_THE1:47 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al holds (All (x,p)) => p in TAUT Al by Th12; theorem :: CQC_THE1:48 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al st p => q in TAUT Al & not x in still_not-bound_in p holds p => (All (x,q)) in TAUT Al by Th13; theorem :: CQC_THE1:49 for Al being QC-alphabet for s being QC-formula of Al for x, y being bound_QC-variable of Al st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in TAUT Al holds s . y in TAUT Al by Th14; :: --------- Relation of consequence of a set of formulas definition let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); let s be QC-formula of Al; predX |- s means :Def8: :: CQC_THE1:def 8 s in Cn X; end; :: deftheorem Def8 defines |- CQC_THE1:def_8_:_ for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for s being QC-formula of Al holds ( X |- s iff s in Cn X ); theorem :: CQC_THE1:50 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds X |- VERUM Al proofend; theorem :: CQC_THE1:51 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds X |- (('not' p) => p) => p proofend; theorem :: CQC_THE1:52 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al holds X |- p => (('not' p) => q) proofend; theorem :: CQC_THE1:53 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q, r being Element of CQC-WFF Al holds X |- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) proofend; theorem :: CQC_THE1:54 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al holds X |- (p '&' q) => (q '&' p) proofend; theorem :: CQC_THE1:55 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al st X |- p & X |- p => q holds X |- q proofend; theorem :: CQC_THE1:56 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al for x being bound_QC-variable of Al holds X |- (All (x,p)) => p proofend; theorem :: CQC_THE1:57 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al st X |- p => q & not x in still_not-bound_in p holds X |- p => (All (x,q)) proofend; theorem :: CQC_THE1:58 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for s being QC-formula of Al for y, x being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x holds X |- s . y proofend; definition let Al be QC-alphabet ; let s be QC-formula of Al; attrs is valid means :Def9: :: CQC_THE1:def 9 {} (CQC-WFF Al) |- s; end; :: deftheorem Def9 defines valid CQC_THE1:def_9_:_ for Al being QC-alphabet for s being QC-formula of Al holds ( s is valid iff {} (CQC-WFF Al) |- s ); Lm13: for Al being QC-alphabet for s being QC-formula of Al holds ( s is valid iff s in TAUT Al ) proofend; definition let Al be QC-alphabet ; let s be QC-formula of Al; redefine attr s is valid means :: CQC_THE1:def 10 s in TAUT Al; compatibility ( s is valid iff s in TAUT Al ) by Lm13; end; :: deftheorem defines valid CQC_THE1:def_10_:_ for Al being QC-alphabet for s being QC-formula of Al holds ( s is valid iff s in TAUT Al ); theorem :: CQC_THE1:59 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al st p is valid holds X |- p proofend; theorem :: CQC_THE1:60 for Al being QC-alphabet holds VERUM Al is valid proofend; theorem :: CQC_THE1:61 for Al being QC-alphabet for p being Element of CQC-WFF Al holds (('not' p) => p) => p is valid proofend; theorem :: CQC_THE1:62 for Al being QC-alphabet for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) is valid proofend; theorem :: CQC_THE1:63 for Al being QC-alphabet for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) is valid proofend; theorem :: CQC_THE1:64 for Al being QC-alphabet for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) is valid proofend; theorem :: CQC_THE1:65 for Al being QC-alphabet for p, q being Element of CQC-WFF Al st p is valid & p => q is valid holds q is valid proofend; theorem :: CQC_THE1:66 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al holds (All (x,p)) => p is valid proofend; theorem :: CQC_THE1:67 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al st p => q is valid & not x in still_not-bound_in p holds p => (All (x,q)) is valid proofend; theorem :: CQC_THE1:68 for Al being QC-alphabet for s being QC-formula of Al for y, x being bound_QC-variable of Al st s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid holds s . y is valid proofend;