:: A Sequent Calculus for First-Order Logic :: by Patrick Braselmann and Peter Koepke :: :: Received September 25, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin definition let D be non empty set ; let f be FinSequence of D; func Ant f -> FinSequence of D means :Def1: :: CALCUL_1:def 1 for i being Element of NAT st len f = i + 1 holds it = f | (Seg i) if len f > 0 otherwise it = {} ; existence ( ( len f > 0 implies ex b1 being FinSequence of D st for i being Element of NAT st len f = i + 1 holds b1 = f | (Seg i) ) & ( not len f > 0 implies ex b1 being FinSequence of D st b1 = {} ) ) proofend; uniqueness for b1, b2 being FinSequence of D holds ( ( len f > 0 & ( for i being Element of NAT st len f = i + 1 holds b1 = f | (Seg i) ) & ( for i being Element of NAT st len f = i + 1 holds b2 = f | (Seg i) ) implies b1 = b2 ) & ( not len f > 0 & b1 = {} & b2 = {} implies b1 = b2 ) ) proofend; consistency for b1 being FinSequence of D holds verum ; end; :: deftheorem Def1 defines Ant CALCUL_1:def_1_:_ for D being non empty set for f, b3 being FinSequence of D holds ( ( len f > 0 implies ( b3 = Ant f iff for i being Element of NAT st len f = i + 1 holds b3 = f | (Seg i) ) ) & ( not len f > 0 implies ( b3 = Ant f iff b3 = {} ) ) ); definition let Al be QC-alphabet ; let f be FinSequence of CQC-WFF Al; func Suc f -> Element of CQC-WFF Al equals :Def2: :: CALCUL_1:def 2 f . (len f) if len f > 0 otherwise VERUM Al; coherence ( ( len f > 0 implies f . (len f) is Element of CQC-WFF Al ) & ( not len f > 0 implies VERUM Al is Element of CQC-WFF Al ) ) proofend; consistency for b1 being Element of CQC-WFF Al holds verum ; end; :: deftheorem Def2 defines Suc CALCUL_1:def_2_:_ for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds ( ( len f > 0 implies Suc f = f . (len f) ) & ( not len f > 0 implies Suc f = VERUM Al ) ); definition let f be Relation; let p be set ; predp is_tail_of f means :Def3: :: CALCUL_1:def 3 p in rng f; end; :: deftheorem Def3 defines is_tail_of CALCUL_1:def_3_:_ for f being Relation for p being set holds ( p is_tail_of f iff p in rng f ); Lm1: now__::_thesis:_for_f_being_FinSequence for_p_being_set_st_p_is_tail_of_f_holds_ ex_i_being_Element_of_NAT_st_ (_i_in_dom_f_&_f_._i_=_p_) let f be FinSequence; ::_thesis: for p being set st p is_tail_of f holds ex i being Element of NAT st ( i in dom f & f . i = p ) let p be set ; ::_thesis: ( p is_tail_of f implies ex i being Element of NAT st ( i in dom f & f . i = p ) ) assume p is_tail_of f ; ::_thesis: ex i being Element of NAT st ( i in dom f & f . i = p ) then p in rng f by Def3; then consider i being set such that A1: i in dom f and A2: f . i = p by FUNCT_1:def_3; reconsider i = i as Element of NAT by A1; take i = i; ::_thesis: ( i in dom f & f . i = p ) thus ( i in dom f & f . i = p ) by A1, A2; ::_thesis: verum end; Lm2: now__::_thesis:_for_f_being_FinSequence for_p_being_set_st_ex_i_being_Element_of_NAT_st_ (_i_in_dom_f_&_f_._i_=_p_)_holds_ p_is_tail_of_f let f be FinSequence; ::_thesis: for p being set st ex i being Element of NAT st ( i in dom f & f . i = p ) holds p is_tail_of f let p be set ; ::_thesis: ( ex i being Element of NAT st ( i in dom f & f . i = p ) implies p is_tail_of f ) assume ex i being Element of NAT st ( i in dom f & f . i = p ) ; ::_thesis: p is_tail_of f then p in rng f by FUNCT_1:def_3; hence p is_tail_of f by Def3; ::_thesis: verum end; definition let Al be QC-alphabet ; let f, g be FinSequence of CQC-WFF Al; predf is_Subsequence_of g means :Def4: :: CALCUL_1:def 4 ex N being Subset of NAT st f c= Seq (g | N); end; :: deftheorem Def4 defines is_Subsequence_of CALCUL_1:def_4_:_ for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al holds ( f is_Subsequence_of g iff ex N being Subset of NAT st f c= Seq (g | N) ); theorem Th1: :: CALCUL_1:1 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st f is_Subsequence_of g holds ( rng f c= rng g & ex N being Subset of NAT st rng f c= rng (g | N) ) proofend; theorem Th2: :: CALCUL_1:2 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al st len f > 0 holds ( (len (Ant f)) + 1 = len f & len (Ant f) < len f ) proofend; theorem Th3: :: CALCUL_1:3 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al st len f > 0 holds ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) proofend; theorem Th4: :: CALCUL_1:4 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al st len f > 1 holds len (Ant f) > 0 proofend; theorem Th5: :: CALCUL_1:5 for Al being QC-alphabet for p being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al holds ( Suc (f ^ <*p*>) = p & Ant (f ^ <*p*>) = f ) proofend; theorem Th6: :: CALCUL_1:6 for fin, fin1 being FinSequence holds ( len fin <= len (fin ^ fin1) & len fin1 <= len (fin ^ fin1) & ( fin <> {} implies ( 1 <= len fin & len fin1 < len (fin1 ^ fin) ) ) ) proofend; theorem Th7: :: CALCUL_1:7 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al holds Seq ((f ^ g) | (dom f)) = (f ^ g) | (dom f) proofend; theorem Th8: :: CALCUL_1:8 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of f ^ g proofend; theorem Th9: :: CALCUL_1:9 for b, c being set for fin being FinSequence holds 1 < len ((fin ^ <*b*>) ^ <*c*>) proofend; theorem Th10: :: CALCUL_1:10 for b being set for fin being FinSequence holds ( 1 <= len (fin ^ <*b*>) & len (fin ^ <*b*>) in dom (fin ^ <*b*>) ) proofend; theorem Th11: :: CALCUL_1:11 for m, n being Element of NAT st 0 < m holds len (Sgm ((Seg n) \/ {(n + m)})) = n + 1 proofend; theorem Th12: :: CALCUL_1:12 for m, n being Element of NAT st 0 < m holds dom (Sgm ((Seg n) \/ {(n + m)})) = Seg (n + 1) proofend; theorem Th13: :: CALCUL_1:13 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st 0 < len f holds f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*> proofend; theorem Th14: :: CALCUL_1:14 for Al being QC-alphabet for c, d being set for f being FinSequence of CQC-WFF Al holds ( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d ) proofend; begin definition let Al be QC-alphabet ; let f be FinSequence of CQC-WFF Al; func still_not-bound_in f -> Subset of (bound_QC-variables Al) means :Def5: :: CALCUL_1:def 5 for a being set holds ( a in it iff ex i being Element of NAT ex p being Element of CQC-WFF Al st ( i in dom f & p = f . i & a in still_not-bound_in p ) ); existence ex b1 being Subset of (bound_QC-variables Al) st for a being set holds ( a in b1 iff ex i being Element of NAT ex p being Element of CQC-WFF Al st ( i in dom f & p = f . i & a in still_not-bound_in p ) ) proofend; uniqueness for b1, b2 being Subset of (bound_QC-variables Al) st ( for a being set holds ( a in b1 iff ex i being Element of NAT ex p being Element of CQC-WFF Al st ( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being set holds ( a in b2 iff ex i being Element of NAT ex p being Element of CQC-WFF Al st ( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines still_not-bound_in CALCUL_1:def_5_:_ for Al being QC-alphabet for f being FinSequence of CQC-WFF Al for b3 being Subset of (bound_QC-variables Al) holds ( b3 = still_not-bound_in f iff for a being set holds ( a in b3 iff ex i being Element of NAT ex p being Element of CQC-WFF Al st ( i in dom f & p = f . i & a in still_not-bound_in p ) ) ); definition let Al be QC-alphabet ; func set_of_CQC-WFF-seq Al -> set means :Def6: :: CALCUL_1:def 6 for a being set holds ( a in it iff a is FinSequence of CQC-WFF Al ); existence ex b1 being set st for a being set holds ( a in b1 iff a is FinSequence of CQC-WFF Al ) proofend; uniqueness for b1, b2 being set st ( for a being set holds ( a in b1 iff a is FinSequence of CQC-WFF Al ) ) & ( for a being set holds ( a in b2 iff a is FinSequence of CQC-WFF Al ) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines set_of_CQC-WFF-seq CALCUL_1:def_6_:_ for Al being QC-alphabet for b2 being set holds ( b2 = set_of_CQC-WFF-seq Al iff for a being set holds ( a in b2 iff a is FinSequence of CQC-WFF Al ) ); definition let Al be QC-alphabet ; let PR be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; let n be Nat; predPR,n is_a_correct_step means :Def7: :: CALCUL_1:def 7 ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) if (PR . n) `2 = 0 ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> if (PR . n) `2 = 1 ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) if (PR . n) `2 = 2 ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) if (PR . n) `2 = 3 ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) if (PR . n) `2 = 4 ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) if (PR . n) `2 = 5 ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) if (PR . n) `2 = 6 ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) if (PR . n) `2 = 7 ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) if (PR . n) `2 = 8 ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) if (PR . n) `2 = 9 ; consistency ( ( (PR . n) `2 = 0 & (PR . n) `2 = 1 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 3 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 4 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 5 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 6 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 7 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 8 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 0 & (PR . n) `2 = 9 implies ( ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 2 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 3 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 4 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 5 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 6 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 7 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 8 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 1 & (PR . n) `2 = 9 implies ( ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 3 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 4 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 5 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 6 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 7 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 8 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 2 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 4 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 5 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 6 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 7 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 3 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 5 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 6 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 7 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 6 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 7 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 8 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 & (PR . n) `2 = 9 implies ( ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 7 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 8 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 8 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 & (PR . n) `2 = 9 implies ( ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) ) ; end; :: deftheorem Def7 defines is_a_correct_step CALCUL_1:def_7_:_ for Al being QC-alphabet for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] for n being Nat holds ( ( (PR . n) `2 = 0 implies ( PR,n is_a_correct_step iff ex f being FinSequence of CQC-WFF Al st ( Suc f is_tail_of Ant f & (PR . n) `1 = f ) ) ) & ( (PR . n) `2 = 1 implies ( PR,n is_a_correct_step iff ex f being FinSequence of CQC-WFF Al st (PR . n) `1 = f ^ <*(VERUM Al)*> ) ) & ( (PR . n) `2 = 2 implies ( PR,n is_a_correct_step iff ex i being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & Ant f is_Subsequence_of Ant g & Suc f = Suc g & (PR . i) `1 = f & (PR . n) `1 = g ) ) ) & ( (PR . n) `2 = 3 implies ( PR,n is_a_correct_step iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*(Suc f)*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 4 implies ( PR,n is_a_correct_step iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant (Ant f)) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 5 implies ( PR,n is_a_correct_step iff ex i, j being Element of NAT ex f, g being FinSequence of CQC-WFF Al st ( 1 <= i & i < n & 1 <= j & j < i & Ant f = Ant g & f = (PR . j) `1 & g = (PR . i) `1 & (Ant f) ^ <*((Suc f) '&' (Suc g))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 6 implies ( PR,n is_a_correct_step iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*p*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 7 implies ( PR,n is_a_correct_step iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n & p '&' q = Suc f & f = (PR . i) `1 & (Ant f) ^ <*q*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 8 implies ( PR,n is_a_correct_step iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = All (x,p) & f = (PR . i) `1 & (Ant f) ^ <*(p . (x,y))*> = (PR . n) `1 ) ) ) & ( (PR . n) `2 = 9 implies ( PR,n is_a_correct_step iff ex i being Element of NAT ex f being FinSequence of CQC-WFF Al ex p being Element of CQC-WFF Al ex x, y being bound_QC-variable of Al st ( 1 <= i & i < n & Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 & (Ant f) ^ <*(All (x,p))*> = (PR . n) `1 ) ) ) ); definition let Al be QC-alphabet ; let PR be FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]; attrPR is a_proof means :Def8: :: CALCUL_1:def 8 ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds PR,n is_a_correct_step ) ); end; :: deftheorem Def8 defines a_proof CALCUL_1:def_8_:_ for Al being QC-alphabet for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] holds ( PR is a_proof iff ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds PR,n is_a_correct_step ) ) ); definition let Al be QC-alphabet ; let f be FinSequence of CQC-WFF Al; pred |- f means :Def9: :: CALCUL_1:def 9 ex PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st ( PR is a_proof & f = (PR . (len PR)) `1 ); end; :: deftheorem Def9 defines |- CALCUL_1:def_9_:_ for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds ( |- f iff ex PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st ( PR is a_proof & f = (PR . (len PR)) `1 ) ); definition let Al be QC-alphabet ; let p be Element of CQC-WFF Al; let X be Subset of (CQC-WFF Al); predp is_formal_provable_from X means :Def10: :: CALCUL_1:def 10 ex f being FinSequence of CQC-WFF Al st ( rng (Ant f) c= X & Suc f = p & |- f ); end; :: deftheorem Def10 defines is_formal_provable_from CALCUL_1:def_10_:_ for Al being QC-alphabet for p being Element of CQC-WFF Al for X being Subset of (CQC-WFF Al) holds ( p is_formal_provable_from X iff ex f being FinSequence of CQC-WFF Al st ( rng (Ant f) c= X & Suc f = p & |- f ) ); definition let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); let A be non empty set ; let J be interpretation of Al,A; let v be Element of Valuations_in (Al,A); predJ,v |= X means :Def11: :: CALCUL_1:def 11 for p being Element of CQC-WFF Al st p in X holds J,v |= p; end; :: deftheorem Def11 defines |= CALCUL_1:def_11_:_ for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds ( J,v |= X iff for p being Element of CQC-WFF Al st p in X holds J,v |= p ); definition let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); let p be Element of CQC-WFF Al; predX |= p means :: CALCUL_1:def 12 for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) st J,v |= X holds J,v |= p; end; :: deftheorem defines |= CALCUL_1:def_12_:_ for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds ( X |= p iff for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) st J,v |= X holds J,v |= p ); definition let Al be QC-alphabet ; let p be Element of CQC-WFF Al; pred |= p means :: CALCUL_1:def 13 {} (CQC-WFF Al) |= p; end; :: deftheorem defines |= CALCUL_1:def_13_:_ for Al being QC-alphabet for p being Element of CQC-WFF Al holds ( |= p iff {} (CQC-WFF Al) |= p ); definition let Al be QC-alphabet ; let f be FinSequence of CQC-WFF Al; let A be non empty set ; let J be interpretation of Al,A; let v be Element of Valuations_in (Al,A); predJ,v |= f means :Def14: :: CALCUL_1:def 14 J,v |= rng f; end; :: deftheorem Def14 defines |= CALCUL_1:def_14_:_ for Al being QC-alphabet for f being FinSequence of CQC-WFF Al for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds ( J,v |= f iff J,v |= rng f ); definition let Al be QC-alphabet ; let f be FinSequence of CQC-WFF Al; let p be Element of CQC-WFF Al; predf |= p means :Def15: :: CALCUL_1:def 15 for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) st J,v |= f holds J,v |= p; end; :: deftheorem Def15 defines |= CALCUL_1:def_15_:_ for Al being QC-alphabet for f being FinSequence of CQC-WFF Al for p being Element of CQC-WFF Al holds ( f |= p iff for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) st J,v |= f holds J,v |= p ); theorem Th15: :: CALCUL_1:15 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al st Suc f is_tail_of Ant f holds Ant f |= Suc f proofend; theorem Th16: :: CALCUL_1:16 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st Ant f is_Subsequence_of Ant g & Suc f = Suc g & Ant f |= Suc f holds Ant g |= Suc g proofend; theorem Th17: :: CALCUL_1:17 for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) for f being FinSequence of CQC-WFF Al st len f > 0 holds ( ( J,v |= Ant f & J,v |= Suc f ) iff J,v |= f ) proofend; theorem Th18: :: CALCUL_1:18 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st len f > 1 & len g > 1 & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & Ant f |= Suc f & Ant g |= Suc g holds Ant (Ant f) |= Suc f proofend; theorem Th19: :: CALCUL_1:19 for Al being QC-alphabet for p being Element of CQC-WFF Al for f, g being FinSequence of CQC-WFF Al st len f > 1 & Ant f = Ant g & 'not' p = Suc (Ant f) & 'not' (Suc f) = Suc g & Ant f |= Suc f & Ant g |= Suc g holds Ant (Ant f) |= p proofend; theorem Th20: :: CALCUL_1:20 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st Ant f = Ant g & Ant f |= Suc f & Ant g |= Suc g holds Ant f |= (Suc f) '&' (Suc g) proofend; theorem Th21: :: CALCUL_1:21 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st Ant f |= p '&' q holds Ant f |= p proofend; theorem Th22: :: CALCUL_1:22 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st Ant f |= p '&' q holds Ant f |= q proofend; theorem Th23: :: CALCUL_1:23 for Al being QC-alphabet for p being Element of CQC-WFF Al for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) for Sub being CQC_Substitution of Al holds ( J,v |= [p,Sub] iff J,v |= p ) proofend; theorem Th24: :: CALCUL_1:24 for Al being QC-alphabet for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al for A being non empty set for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds ( J,v |= p . (x,y) iff ex a being Element of A st ( v . y = a & J,v . (x | a) |= p ) ) proofend; theorem Th25: :: CALCUL_1:25 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & Ant f |= Suc f holds for y being bound_QC-variable of Al holds Ant f |= p . (x,y) proofend; theorem Th26: :: CALCUL_1:26 for Al being QC-alphabet for x being bound_QC-variable of Al for A being non empty set for v being Element of Valuations_in (Al,A) for a being Element of A for X being set st X c= bound_QC-variables Al & not x in X holds (v . (x | a)) | X = v | X proofend; theorem Th27: :: CALCUL_1:27 for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A for f being FinSequence of CQC-WFF Al for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in f) = w | (still_not-bound_in f) & J,v |= f holds J,w |= f proofend; theorem Th28: :: CALCUL_1:28 for Al being QC-alphabet for p being Element of CQC-WFF Al for y, x being bound_QC-variable of Al for A being non empty set for v being Element of Valuations_in (Al,A) for a being Element of A st not y in still_not-bound_in (All (x,p)) holds ((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p) proofend; theorem Th29: :: CALCUL_1:29 for Al being QC-alphabet for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st Suc f = p . (x,y) & Ant f |= Suc f & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) holds Ant f |= All (x,p) proofend; theorem Th30: :: CALCUL_1:30 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds Ant (f ^ <*(VERUM Al)*>) |= Suc (f ^ <*(VERUM Al)*>) proofend; theorem Th31: :: CALCUL_1:31 for Al being QC-alphabet for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] for n being Nat st 1 <= n & n <= len PR & not (PR . n) `2 = 0 & not (PR . n) `2 = 1 & not (PR . n) `2 = 2 & not (PR . n) `2 = 3 & not (PR . n) `2 = 4 & not (PR . n) `2 = 5 & not (PR . n) `2 = 6 & not (PR . n) `2 = 7 & not (PR . n) `2 = 8 holds (PR . n) `2 = 9 proofend; Lm3: for Al being QC-alphabet for n being Element of NAT for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st 1 <= n & n <= len PR holds (PR . n) `1 is FinSequence of CQC-WFF Al proofend; :: Theorem on the Correctness (Ebb et al, Chapter IV, Theorem 6.2) theorem :: CALCUL_1:32 for Al being QC-alphabet for p being Element of CQC-WFF Al for X being Subset of (CQC-WFF Al) st p is_formal_provable_from X holds X |= p proofend; begin theorem Th33: :: CALCUL_1:33 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al st Suc f is_tail_of Ant f holds |- f proofend; theorem Th34: :: CALCUL_1:34 for Al being QC-alphabet for PR, PR1 being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] for n being Nat st 1 <= n & n <= len PR holds ( PR,n is_a_correct_step iff PR ^ PR1,n is_a_correct_step ) proofend; theorem Th35: :: CALCUL_1:35 for Al being QC-alphabet for n being Element of NAT for PR1, PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st 1 <= n & n <= len PR1 & PR1,n is_a_correct_step holds PR ^ PR1,n + (len PR) is_a_correct_step proofend; theorem Th36: :: CALCUL_1:36 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st Ant f is_Subsequence_of Ant g & Suc f = Suc g & |- f holds |- g proofend; theorem Th37: :: CALCUL_1:37 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g holds |- (Ant (Ant f)) ^ <*(Suc f)*> proofend; theorem Th38: :: CALCUL_1:38 for Al being QC-alphabet for p being Element of CQC-WFF Al for f, g being FinSequence of CQC-WFF Al st len f > 1 & Ant f = Ant g & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc g & |- f & |- g holds |- (Ant (Ant f)) ^ <*p*> proofend; theorem Th39: :: CALCUL_1:39 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al st Ant f = Ant g & |- f & |- g holds |- (Ant f) ^ <*((Suc f) '&' (Suc g))*> proofend; theorem Th40: :: CALCUL_1:40 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds |- (Ant f) ^ <*p*> proofend; theorem Th41: :: CALCUL_1:41 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st p '&' q = Suc f & |- f holds |- (Ant f) ^ <*q*> proofend; theorem Th42: :: CALCUL_1:42 for Al being QC-alphabet for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st Suc f = All (x,p) & |- f holds |- (Ant f) ^ <*(p . (x,y))*> proofend; theorem Th43: :: CALCUL_1:43 for Al being QC-alphabet for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & |- f holds |- (Ant f) ^ <*(All (x,p))*> proofend; theorem Th44: :: CALCUL_1:44 for Al being QC-alphabet for p being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- f & |- (Ant f) ^ <*('not' (Suc f))*> holds |- (Ant f) ^ <*p*> proofend; theorem Th45: :: CALCUL_1:45 for Al being QC-alphabet for p being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st 1 <= len f & |- f & |- f ^ <*p*> holds |- (Ant f) ^ <*p*> proofend; theorem Th46: :: CALCUL_1:46 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds |- (f ^ <*('not' q)*>) ^ <*('not' p)*> proofend; theorem :: CALCUL_1:47 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- (f ^ <*('not' p)*>) ^ <*('not' q)*> holds |- (f ^ <*q*>) ^ <*p*> proofend; theorem Th48: :: CALCUL_1:48 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- (f ^ <*('not' p)*>) ^ <*q*> holds |- (f ^ <*('not' q)*>) ^ <*p*> proofend; theorem Th49: :: CALCUL_1:49 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*('not' q)*> holds |- (f ^ <*q*>) ^ <*('not' p)*> proofend; theorem :: CALCUL_1:50 for Al being QC-alphabet for p, r, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> holds |- (f ^ <*(p 'or' q)*>) ^ <*r*> proofend; theorem :: CALCUL_1:51 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds |- f ^ <*(p 'or' q)*> proofend; theorem :: CALCUL_1:52 for Al being QC-alphabet for q, p being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- f ^ <*q*> holds |- f ^ <*(p 'or' q)*> proofend; theorem Th53: :: CALCUL_1:53 for Al being QC-alphabet for p, r, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> holds |- (f ^ <*(p 'or' q)*>) ^ <*r*> proofend; theorem Th54: :: CALCUL_1:54 for Al being QC-alphabet for p being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds |- f ^ <*('not' ('not' p))*> proofend; theorem Th55: :: CALCUL_1:55 for Al being QC-alphabet for p being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- f ^ <*('not' ('not' p))*> holds |- f ^ <*p*> proofend; theorem :: CALCUL_1:56 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for f being FinSequence of CQC-WFF Al st |- f ^ <*(p => q)*> & |- f ^ <*p*> holds |- f ^ <*q*> proofend; theorem Th57: :: CALCUL_1:57 for Al being QC-alphabet for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al holds ('not' p) . (x,y) = 'not' (p . (x,y)) proofend; theorem :: CALCUL_1:58 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st ex y being bound_QC-variable of Al st |- f ^ <*(p . (x,y))*> holds |- f ^ <*(Ex (x,p))*> proofend; theorem Th59: :: CALCUL_1:59 for Al being QC-alphabet for f, g being FinSequence of CQC-WFF Al holds still_not-bound_in (f ^ g) = (still_not-bound_in f) \/ (still_not-bound_in g) proofend; theorem Th60: :: CALCUL_1:60 for Al being QC-alphabet for p being Element of CQC-WFF Al holds still_not-bound_in <*p*> = still_not-bound_in p proofend; theorem :: CALCUL_1:61 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for x, y being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st |- (f ^ <*(p . (x,y))*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex (x,p))*>) ^ <*q*>) holds |- (f ^ <*(Ex (x,p))*>) ^ <*q*> proofend; theorem Th62: :: CALCUL_1:62 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds still_not-bound_in f = union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being Element of NAT st ( i in dom f & p = f . i ) } proofend; theorem Th63: :: CALCUL_1:63 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds still_not-bound_in f is finite proofend; theorem Th64: :: CALCUL_1:64 for Al being QC-alphabet holds ( card (bound_QC-variables Al) = card (QC-symbols Al) & not bound_QC-variables Al is finite ) proofend; theorem Th65: :: CALCUL_1:65 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds not for x being bound_QC-variable of Al holds x in still_not-bound_in f proofend; theorem Th66: :: CALCUL_1:66 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,p))*> holds |- f ^ <*(All (x,('not' ('not' p))))*> proofend; theorem Th67: :: CALCUL_1:67 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al st |- f ^ <*(All (x,('not' ('not' p))))*> holds |- f ^ <*(All (x,p))*> proofend; theorem :: CALCUL_1:68 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for f being FinSequence of CQC-WFF Al holds ( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> ) proofend; definition let f be FinSequence; let p be set ; redefine pred p is_tail_of f means :: CALCUL_1:def 16 ex i being Element of NAT st ( i in dom f & f . i = p ); compatibility ( p is_tail_of f iff ex i being Element of NAT st ( i in dom f & f . i = p ) ) by Lm1, Lm2; end; :: deftheorem defines is_tail_of CALCUL_1:def_16_:_ for f being FinSequence for p being set holds ( p is_tail_of f iff ex i being Element of NAT st ( i in dom f & f . i = p ) );