:: CQC_THE1 semantic presentation 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)} proof let n be Element of NAT ; ::_thesis: { k where k is Element of NAT : k <= n + 1 } = { i where i is Element of NAT : i <= n } \/ {(n + 1)} thus { k where k is Element of NAT : k <= n + 1 } c= { i where i is Element of NAT : i <= n } \/ {(n + 1)} :: according to XBOOLE_0:def_10 ::_thesis: { i where i is Element of NAT : i <= n } \/ {(n + 1)} c= { k where k is Element of NAT : k <= n + 1 } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { k where k is Element of NAT : k <= n + 1 } or a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} ) assume a in { k where k is Element of NAT : k <= n + 1 } ; ::_thesis: a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} then consider k being Element of NAT such that A1: k = a and A2: k <= n + 1 ; ( k <= n or k = n + 1 ) by A2, NAT_1:8; then ( a in { i where i is Element of NAT : i <= n } or a in {(n + 1)} ) by A1, TARSKI:def_1; hence a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} by XBOOLE_0:def_3; ::_thesis: verum end; thus { i where i is Element of NAT : i <= n } \/ {(n + 1)} c= { k where k is Element of NAT : k <= n + 1 } ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} or a in { k where k is Element of NAT : k <= n + 1 } ) assume a in { i where i is Element of NAT : i <= n } \/ {(n + 1)} ; ::_thesis: a in { k where k is Element of NAT : k <= n + 1 } then ( a in { i where i is Element of NAT : i <= n } or a in {(n + 1)} ) by XBOOLE_0:def_3; then A3: ( ex i being Element of NAT st ( a = i & i <= n ) or a = n + 1 ) by TARSKI:def_1; now__::_thesis:_(_ex_i_being_Element_of_NAT_st_ (_a_=_i_&_i_<=_n_)_implies_a_in__{__k_where_k_is_Element_of_NAT_:_k_<=_n_+_1__}__) given i being Element of NAT such that A4: a = i and A5: i <= n ; ::_thesis: a in { k where k is Element of NAT : k <= n + 1 } n <= n + 1 by NAT_1:11; then i <= n + 1 by A5, XXREAL_0:2; hence a in { k where k is Element of NAT : k <= n + 1 } by A4; ::_thesis: verum end; hence a in { k where k is Element of NAT : k <= n + 1 } by A3; ::_thesis: verum end; end; theorem Th2: :: CQC_THE1:2 for n being Element of NAT holds { k where k is Element of NAT : k <= n } is finite proof defpred S1[ Element of NAT ] means { k where k is Element of NAT : k <= \$1 } is finite ; { k where k is Element of NAT : k <= 0 } = {0} proof thus { k where k is Element of NAT : k <= 0 } c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= { k where k is Element of NAT : k <= 0 } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { k where k is Element of NAT : k <= 0 } or a in {0} ) assume a in { k where k is Element of NAT : k <= 0 } ; ::_thesis: a in {0} then consider k being Element of NAT such that A1: k = a and A2: k <= 0 ; k = 0 by A2, NAT_1:3; hence a in {0} by A1, TARSKI:def_1; ::_thesis: verum end; thus {0} c= { k where k is Element of NAT : k <= 0 } ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {0} or a in { k where k is Element of NAT : k <= 0 } ) assume a in {0} ; ::_thesis: a in { k where k is Element of NAT : k <= 0 } then a = 0 by TARSKI:def_1; hence a in { k where k is Element of NAT : k <= 0 } ; ::_thesis: verum end; end; then A3: S1[ 0 ] ; A4: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A5: S1[n] ; ::_thesis: S1[n + 1] { l where l is Element of NAT : l <= n + 1 } = { k where k is Element of NAT : k <= n } \/ {(n + 1)} by Th1; hence S1[n + 1] by A5; ::_thesis: verum end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A4); ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let T, S be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory & S is being_a_theory implies T /\ S is being_a_theory ) assume that A1: T is being_a_theory and A2: S is being_a_theory ; ::_thesis: T /\ S is being_a_theory ( VERUM Al in T & VERUM Al in S ) by A1, A2, Def1; hence VERUM Al in T /\ S by XBOOLE_0:def_4; :: according to CQC_THE1:def_1 ::_thesis: 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 /\ S & p => (('not' p) => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) let p, q, r be Element of CQC-WFF Al; ::_thesis: for s being QC-formula of Al for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in T /\ S & p => (('not' p) => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) let s be QC-formula of Al; ::_thesis: for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in T /\ S & p => (('not' p) => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) let x, y be bound_QC-variable of Al; ::_thesis: ( (('not' p) => p) => p in T /\ S & p => (('not' p) => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) ( (('not' p) => p) => p in T & (('not' p) => p) => p in S ) by A1, A2, Def1; hence (('not' p) => p) => p in T /\ S by XBOOLE_0:def_4; ::_thesis: ( p => (('not' p) => q) in T /\ S & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) ( p => (('not' p) => q) in T & p => (('not' p) => q) in S ) by A1, A2, Def1; hence p => (('not' p) => q) in T /\ S by XBOOLE_0:def_4; ::_thesis: ( (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S & (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) ( (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in S ) by A1, A2, Def1; hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T /\ S by XBOOLE_0:def_4; ::_thesis: ( (p '&' q) => (q '&' p) in T /\ S & ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) ( (p '&' q) => (q '&' p) in T & (p '&' q) => (q '&' p) in S ) by A1, A2, Def1; hence (p '&' q) => (q '&' p) in T /\ S by XBOOLE_0:def_4; ::_thesis: ( ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) & (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) A3: ( p in T & p => q in T implies q in T ) by A1, Def1; ( p in S & p => q in S implies q in S ) by A2, Def1; hence ( p in T /\ S & p => q in T /\ S implies q in T /\ S ) by A3, XBOOLE_0:def_4; ::_thesis: ( (All (x,p)) => p in T /\ S & ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) ( (All (x,p)) => p in T & (All (x,p)) => p in S ) by A1, A2, Def1; hence (All (x,p)) => p in T /\ S by XBOOLE_0:def_4; ::_thesis: ( ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) ) A4: ( p => q in T & not x in still_not-bound_in p implies p => (All (x,q)) in T ) by A1, Def1; ( p => q in S & not x in still_not-bound_in p implies p => (All (x,q)) in S ) by A2, Def1; hence ( p => q in T /\ S & not x in still_not-bound_in p implies p => (All (x,q)) in T /\ S ) by A4, XBOOLE_0:def_4; ::_thesis: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) A5: ( 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 ) by A1, Def1; ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in S implies s . y in S ) by A2, Def1; hence ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in T /\ S implies s . y in T /\ S ) by A5, XBOOLE_0:def_4; ::_thesis: verum end; 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 ) proof defpred S1[ set ] means for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds \$1 in T; consider Y being set such that A1: for a being set holds ( a in Y iff ( a in CQC-WFF Al & S1[a] ) ) from XBOOLE_0:sch_1(); Y c= CQC-WFF Al proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in CQC-WFF Al ) assume a in Y ; ::_thesis: a in CQC-WFF Al hence a in CQC-WFF Al by A1; ::_thesis: verum end; then reconsider Z = Y as Subset of (CQC-WFF Al) ; take Z ; ::_thesis: for t being Element of CQC-WFF Al holds ( t in Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) thus for t being Element of CQC-WFF Al holds ( t in Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) by A1; ::_thesis: verum end; 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 proof let Y, Z be Subset of (CQC-WFF Al); ::_thesis: ( ( for t being Element of CQC-WFF Al holds ( t in Y 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 Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) ) implies Y = Z ) assume that A2: for t being Element of CQC-WFF Al holds ( t in Y iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) and A3: for t being Element of CQC-WFF Al holds ( t in Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T ) ; ::_thesis: Y = Z for a being set holds ( a in Y iff a in Z ) proof let a be set ; ::_thesis: ( a in Y iff a in Z ) thus ( a in Y implies a in Z ) ::_thesis: ( a in Z implies a in Y ) proof assume A4: a in Y ; ::_thesis: a in Z then reconsider t = a as Element of CQC-WFF Al ; for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T by A2, A4; hence a in Z by A3; ::_thesis: verum end; thus ( a in Z implies a in Y ) ::_thesis: verum proof assume A5: a in Z ; ::_thesis: a in Y then reconsider t = a as Element of CQC-WFF Al ; for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T by A3, A5; hence a in Y by A2; ::_thesis: verum end; end; hence Y = Z by TARSKI:1; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds VERUM Al in Cn X let X be Subset of (CQC-WFF Al); ::_thesis: VERUM Al in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds VERUM Al in T by Def1; hence VERUM Al in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds (('not' p) => p) => p in Cn X let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al holds (('not' p) => p) => p in Cn X let p be Element of CQC-WFF Al; ::_thesis: (('not' p) => p) => p in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds (('not' p) => p) => p in T by Def1; hence (('not' p) => p) => p in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in Cn X let p, q be Element of CQC-WFF Al; ::_thesis: p => (('not' p) => q) in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds p => (('not' p) => q) in T by Def1; hence p => (('not' p) => q) in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X let p, q, r be Element of CQC-WFF Al; ::_thesis: (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in T by Def1; hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in Cn X let p, q be Element of CQC-WFF Al; ::_thesis: (p '&' q) => (q '&' p) in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds (p '&' q) => (q '&' p) in T by Def1; hence (p '&' q) => (q '&' p) in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al st p in Cn X & p => q in Cn X holds q in Cn X let p, q be Element of CQC-WFF Al; ::_thesis: ( p in Cn X & p => q in Cn X implies q in Cn X ) assume A1: ( p in Cn X & p => q in Cn X ) ; ::_thesis: q in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds q in T proof let T be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory & X c= T implies q in T ) assume that A2: T is being_a_theory and A3: X c= T ; ::_thesis: q in T ( p in T & p => q in T ) by A1, A2, A3, Def2; hence q in T by A2, Def1; ::_thesis: verum end; hence q in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al holds (All (x,p)) => p in Cn X let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al holds (All (x,p)) => p in Cn X let x be bound_QC-variable of Al; ::_thesis: (All (x,p)) => p in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds (All (x,p)) => p in T by Def1; hence (All (x,p)) => p in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: 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 let p, q be Element of CQC-WFF Al; ::_thesis: 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 let x be bound_QC-variable of Al; ::_thesis: ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) assume that A1: p => q in Cn X and A2: not x in still_not-bound_in p ; ::_thesis: p => (All (x,q)) in Cn X for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds p => (All (x,q)) in T proof let T be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory & X c= T implies p => (All (x,q)) in T ) assume that A3: T is being_a_theory and A4: X c= T ; ::_thesis: p => (All (x,q)) in T p => q in T by A1, A3, A4, Def2; hence p => (All (x,q)) in T by A2, A3, Def1; ::_thesis: verum end; hence p => (All (x,q)) in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: 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 let s be QC-formula of Al; ::_thesis: 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 let x, y be bound_QC-variable of Al; ::_thesis: ( 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 implies s . y in Cn X ) assume that A1: s . x in CQC-WFF Al and A2: s . y in CQC-WFF Al and A3: not x in still_not-bound_in s and A4: s . x in Cn X ; ::_thesis: s . y in Cn X reconsider s1 = s . x as Element of CQC-WFF Al by A1; reconsider q = s . y as Element of CQC-WFF Al by A2; for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds q in T proof let T be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory & X c= T implies q in T ) assume that A5: T is being_a_theory and A6: X c= T ; ::_thesis: q in T s1 in T by A4, A5, A6, Def2; hence q in T by A3, A5, Def1; ::_thesis: verum end; hence s . y in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds Cn X is being_a_theory let X be Subset of (CQC-WFF Al); ::_thesis: Cn X is being_a_theory thus VERUM Al in Cn X by Th6; :: according to CQC_THE1:def_1 ::_thesis: 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 Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( 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 implies s . y in Cn X ) ) let p, q, r be Element of CQC-WFF Al; ::_thesis: for s being QC-formula of Al for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( 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 implies s . y in Cn X ) ) let s be QC-formula of Al; ::_thesis: for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( 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 implies s . y in Cn X ) ) let x, y be bound_QC-variable of Al; ::_thesis: ( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) & (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( 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 implies s . y in Cn X ) ) thus ( (('not' p) => p) => p in Cn X & p => (('not' p) => q) in Cn X & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X & (p '&' q) => (q '&' p) in Cn X & ( p in Cn X & p => q in Cn X implies q in Cn X ) ) by Th7, Th8, Th9, Th10, Th11; ::_thesis: ( (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( 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 implies s . y in Cn X ) ) thus ( (All (x,p)) => p in Cn X & ( p => q in Cn X & not x in still_not-bound_in p implies p => (All (x,q)) in Cn X ) & ( 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 implies s . y in Cn X ) ) by Th12, Th13, Th14; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for T, X being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds Cn X c= T let T, X be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory & X c= T implies Cn X c= T ) assume A1: ( T is being_a_theory & X c= T ) ; ::_thesis: Cn X c= T thus Cn X c= T ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cn X or a in T ) assume a in Cn X ; ::_thesis: a in T hence a in T by A1, Def2; ::_thesis: verum end; end; theorem Th17: :: CQC_THE1:17 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds X c= Cn X proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds X c= Cn X let X be Subset of (CQC-WFF Al); ::_thesis: X c= Cn X let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in Cn X ) assume A1: a in X ; ::_thesis: a in Cn X then reconsider t = a as Element of CQC-WFF Al ; for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T by A1; hence a in Cn X by Def2; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for X, Y being Subset of (CQC-WFF Al) st X c= Y holds Cn X c= Cn Y let X, Y be Subset of (CQC-WFF Al); ::_thesis: ( X c= Y implies Cn X c= Cn Y ) assume A1: X c= Y ; ::_thesis: Cn X c= Cn Y thus Cn X c= Cn Y ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cn X or a in Cn Y ) assume A2: a in Cn X ; ::_thesis: a in Cn Y then reconsider t = a as Element of CQC-WFF Al ; for T being Subset of (CQC-WFF Al) st T is being_a_theory & Y c= T holds t in T proof let T be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory & Y c= T implies t in T ) assume that A3: T is being_a_theory and A4: Y c= T ; ::_thesis: t in T X c= T by A1, A4, XBOOLE_1:1; hence t in T by A2, A3, Def2; ::_thesis: verum end; hence a in Cn Y by Def2; ::_thesis: verum end; end; Lm1: for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds Cn (Cn X) c= Cn X proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds Cn (Cn X) c= Cn X let X be Subset of (CQC-WFF Al); ::_thesis: Cn (Cn X) c= Cn X let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cn (Cn X) or a in Cn X ) assume A1: a in Cn (Cn X) ; ::_thesis: a in Cn X then reconsider t = a as Element of CQC-WFF Al ; for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds t in T proof let T be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory & X c= T implies t in T ) assume that A2: T is being_a_theory and A3: X c= T ; ::_thesis: t in T Cn X c= T by A2, A3, Th16; hence t in T by A1, A2, Def2; ::_thesis: verum end; hence a in Cn X by Def2; ::_thesis: verum end; theorem :: CQC_THE1:19 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds Cn (Cn X) = Cn X proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds Cn (Cn X) = Cn X let X be Subset of (CQC-WFF Al); ::_thesis: Cn (Cn X) = Cn X ( Cn (Cn X) c= Cn X & Cn X c= Cn (Cn X) ) by Lm1, Th17; hence Cn (Cn X) = Cn X by XBOOLE_0:def_10; ::_thesis: verum end; 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 ) proof let Al be QC-alphabet ; ::_thesis: for T being Subset of (CQC-WFF Al) holds ( T is being_a_theory iff Cn T = T ) let T be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory iff Cn T = T ) thus ( T is being_a_theory implies Cn T = T ) ::_thesis: ( Cn T = T implies T is being_a_theory ) proof assume A1: T is being_a_theory ; ::_thesis: Cn T = T A2: T c= Cn T by Th17; Cn T c= T proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cn T or a in T ) assume a in Cn T ; ::_thesis: a in T hence a in T by A1, Def2; ::_thesis: verum end; hence Cn T = T by A2, XBOOLE_0:def_10; ::_thesis: verum end; thus ( Cn T = T implies T is being_a_theory ) by Th15; ::_thesis: verum end; 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 proof 9 in { k where k is Element of NAT : k <= 9 } ; hence not Proof_Step_Kinds is empty ; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: 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 let n be Nat; ::_thesis: ( 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 implies (f . n) `2 = 9 ) assume A1: ( 1 <= n & n <= len f ) ; ::_thesis: ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) dom f = Seg (len f) by FINSEQ_1:def_3; then n in dom f by A1, FINSEQ_1:1; then ( rng f c= [:(CQC-WFF Al),Proof_Step_Kinds:] & f . n in rng f ) by FINSEQ_1:def_4, FUNCT_1:def_3; then (f . n) `2 in Proof_Step_Kinds by MCART_1:10; then ex k being Element of NAT st ( k = (f . n) `2 & k <= 9 ) ; hence ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by NAT_1:33; ::_thesis: verum end; 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 <> {} proof let Al be QC-alphabet ; ::_thesis: 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 <> {} let X be Subset of (CQC-WFF Al); ::_thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds rng f <> {} let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( f is_a_proof_wrt X implies rng f <> {} ) assume f is_a_proof_wrt X ; ::_thesis: rng f <> {} then f <> {} by Def5; hence rng f <> {} by RELAT_1:41; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds 1 <= len f let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( f is_a_proof_wrt X implies 1 <= len f ) assume f is_a_proof_wrt X ; ::_thesis: 1 <= len f then A1: f <> {} by Def5; 0 <= len f by NAT_1:2; then 0 + 1 <= len f by A1, NAT_1:13; hence 1 <= len f ; ::_thesis: verum end; 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 ) proof let Al be QC-alphabet ; ::_thesis: 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 ) let X be Subset of (CQC-WFF Al); ::_thesis: 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 ) let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( 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 ) assume A1: f is_a_proof_wrt X ; ::_thesis: ( (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 ) then A2: 1 <= len f by Th25; then A3: f,1 is_a_correct_step_wrt X by A1, Def5; assume A4: ( not (f . 1) `2 = 0 & not (f . 1) `2 = 1 & not (f . 1) `2 = 2 & not (f . 1) `2 = 3 & not (f . 1) `2 = 4 & not (f . 1) `2 = 5 & not (f . 1) `2 = 6 ) ; ::_thesis: contradiction percases ( (f . 1) `2 = 7 or (f . 1) `2 = 8 or (f . 1) `2 = 9 ) by A2, A4, Th23; suppose (f . 1) `2 = 7 ; ::_thesis: contradiction then ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < 1 & 1 <= j & j < i & p = (f . j) `1 & q = (f . 1) `1 & (f . i) `1 = p => q ) by A3, Def4; hence contradiction ; ::_thesis: verum end; suppose (f . 1) `2 = 8 ; ::_thesis: contradiction then 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 < 1 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . 1) `1 = p => (All (x,q)) ) by A3, Def4; hence contradiction ; ::_thesis: verum end; suppose (f . 1) `2 = 9 ; ::_thesis: contradiction then 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 < 1 & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . 1) `1 = s . y ) by A3, Def4; hence contradiction ; ::_thesis: verum end; end; end; 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 ) proof let Al be QC-alphabet ; ::_thesis: 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 ) let n be Element of NAT ; ::_thesis: 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 ) let X be Subset of (CQC-WFF Al); ::_thesis: 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 ) let f, g be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( 1 <= n & n <= len f implies ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X ) ) assume that A1: 1 <= n and A2: n <= len f ; ::_thesis: ( f,n is_a_correct_step_wrt X iff f ^ g,n is_a_correct_step_wrt X ) n in Seg (len f) by A1, A2, FINSEQ_1:1; then n in dom f by FINSEQ_1:def_3; then A3: (f ^ g) . n = f . n by FINSEQ_1:def_7; len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; then len f <= len (f ^ g) by NAT_1:11; then A4: n <= len (f ^ g) by A2, XXREAL_0:2; thus ( f,n is_a_correct_step_wrt X implies f ^ g,n is_a_correct_step_wrt X ) ::_thesis: ( f ^ g,n is_a_correct_step_wrt X implies f,n is_a_correct_step_wrt X ) proof assume A5: f,n is_a_correct_step_wrt X ; ::_thesis: f ^ g,n is_a_correct_step_wrt X percases ( ((f ^ g) . n) `2 = 0 or ((f ^ g) . n) `2 = 1 or ((f ^ g) . n) `2 = 2 or ((f ^ g) . n) `2 = 3 or ((f ^ g) . n) `2 = 4 or ((f ^ g) . n) `2 = 5 or ((f ^ g) . n) `2 = 6 or ((f ^ g) . n) `2 = 7 or ((f ^ g) . n) `2 = 8 or ((f ^ g) . n) `2 = 9 ) by A1, A4, Th23; :: according to CQC_THE1:def_4 case ((f ^ g) . n) `2 = 0 ; ::_thesis: ((f ^ g) . n) `1 in X hence ((f ^ g) . n) `1 in X by A3, A5, Def4; ::_thesis: verum end; case ((f ^ g) . n) `2 = 1 ; ::_thesis: ((f ^ g) . n) `1 = VERUM Al hence ((f ^ g) . n) `1 = VERUM Al by A3, A5, Def4; ::_thesis: verum end; case ((f ^ g) . n) `2 = 2 ; ::_thesis: ex p being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (('not' p) => p) => p hence ex p being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (('not' p) => p) => p by A3, A5, Def4; ::_thesis: verum end; case ((f ^ g) . n) `2 = 3 ; ::_thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = p => (('not' p) => q) hence ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = p => (('not' p) => q) by A3, A5, Def4; ::_thesis: verum end; case ((f ^ g) . n) `2 = 4 ; ::_thesis: ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) hence ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A3, A5, Def4; ::_thesis: verum end; case ((f ^ g) . n) `2 = 5 ; ::_thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p '&' q) => (q '&' p) hence ex p, q being Element of CQC-WFF Al st ((f ^ g) . n) `1 = (p '&' q) => (q '&' p) by A3, A5, Def4; ::_thesis: verum end; case ((f ^ g) . n) `2 = 6 ; ::_thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . n) `1 = (All (x,p)) => p hence ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . n) `1 = (All (x,p)) => p by A3, A5, Def4; ::_thesis: verum end; case ((f ^ g) . n) `2 = 7 ; ::_thesis: 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 = ((f ^ g) . j) `1 & q = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = p => q ) then consider i, j being Element of NAT , r, t being Element of CQC-WFF Al such that A6: 1 <= i and A7: i < n and A8: 1 <= j and A9: j < i and A10: ( r = (f . j) `1 & t = (f . n) `1 & (f . i) `1 = r => t ) by A3, A5, Def4; A11: i <= len f by A2, A7, XXREAL_0:2; then A12: j <= len f by A9, XXREAL_0:2; A13: i in Seg (len f) by A6, A11, FINSEQ_1:1; A14: j in Seg (len f) by A8, A12, FINSEQ_1:1; A15: i in dom f by A13, FINSEQ_1:def_3; A16: j in dom f by A14, FINSEQ_1:def_3; A17: f . i = (f ^ g) . i by A15, FINSEQ_1:def_7; f . j = (f ^ g) . j by A16, FINSEQ_1:def_7; hence 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 = ((f ^ g) . j) `1 & q = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = p => q ) by A3, A6, A7, A8, A9, A10, A17; ::_thesis: verum end; case ((f ^ g) . n) `2 = 8 ; ::_thesis: 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 & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All (x,q)) ) then consider i being Element of NAT , r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that A18: 1 <= i and A19: i < n and A20: ( (f . i) `1 = r => t & not x in still_not-bound_in r & (f . n) `1 = r => (All (x,t)) ) by A3, A5, Def4; i <= len f by A2, A19, XXREAL_0:2; then i in Seg (len f) by A18, FINSEQ_1:1; then i in dom f by FINSEQ_1:def_3; then f . i = (f ^ g) . i by FINSEQ_1:def_7; hence 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 & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . n) `1 = p => (All (x,q)) ) by A3, A18, A19, A20; ::_thesis: verum end; case ((f ^ g) . n) `2 = 9 ; ::_thesis: 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 = ((f ^ g) . i) `1 & s . y = ((f ^ g) . n) `1 ) then consider i being Element of NAT , x, y being bound_QC-variable of Al, s being QC-formula of Al such that A21: 1 <= i and A22: i < n and A23: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . n) `1 = s . y ) by A3, A5, Def4; i <= len f by A2, A22, XXREAL_0:2; then i in Seg (len f) by A21, FINSEQ_1:1; then i in dom f by FINSEQ_1:def_3; then f . i = (f ^ g) . i by FINSEQ_1:def_7; hence 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 = ((f ^ g) . i) `1 & s . y = ((f ^ g) . n) `1 ) by A3, A21, A22, A23; ::_thesis: verum end; end; end; assume A24: f ^ g,n is_a_correct_step_wrt X ; ::_thesis: f,n is_a_correct_step_wrt X percases ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A1, A2, Th23; :: according to CQC_THE1:def_4 case (f . n) `2 = 0 ; ::_thesis: (f . n) `1 in X hence (f . n) `1 in X by A3, A24, Def4; ::_thesis: verum end; case (f . n) `2 = 1 ; ::_thesis: (f . n) `1 = VERUM Al hence (f . n) `1 = VERUM Al by A3, A24, Def4; ::_thesis: verum end; case (f . n) `2 = 2 ; ::_thesis: ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p hence ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p by A3, A24, Def4; ::_thesis: verum end; case (f . n) `2 = 3 ; ::_thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q) hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q) by A3, A24, Def4; ::_thesis: verum end; case (f . n) `2 = 4 ; ::_thesis: ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) hence ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A3, A24, Def4; ::_thesis: verum end; case (f . n) `2 = 5 ; ::_thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) by A3, A24, Def4; ::_thesis: verum end; case (f . n) `2 = 6 ; ::_thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p hence ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p by A3, A24, Def4; ::_thesis: verum end; case (f . n) `2 = 7 ; ::_thesis: 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 = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) then consider i, j being Element of NAT , r, t being Element of CQC-WFF Al such that A25: 1 <= i and A26: i < n and A27: 1 <= j and A28: j < i and A29: ( r = ((f ^ g) . j) `1 & t = ((f ^ g) . n) `1 & ((f ^ g) . i) `1 = r => t ) by A3, A24, Def4; A30: i <= len f by A2, A26, XXREAL_0:2; then A31: j <= len f by A28, XXREAL_0:2; A32: i in Seg (len f) by A25, A30, FINSEQ_1:1; A33: j in Seg (len f) by A27, A31, FINSEQ_1:1; A34: i in dom f by A32, FINSEQ_1:def_3; A35: j in dom f by A33, FINSEQ_1:def_3; A36: f . i = (f ^ g) . i by A34, FINSEQ_1:def_7; f . j = (f ^ g) . j by A35, FINSEQ_1:def_7; hence 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 = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A3, A25, A26, A27, A28, A29, A36; ::_thesis: verum end; case (f . n) `2 = 8 ; ::_thesis: 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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) then consider i being Element of NAT , r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that A37: 1 <= i and A38: i < n and A39: ( ((f ^ g) . i) `1 = r => t & not x in still_not-bound_in r & ((f ^ g) . n) `1 = r => (All (x,t)) ) by A3, A24, Def4; i <= len f by A2, A38, XXREAL_0:2; then i in Seg (len f) by A37, FINSEQ_1:1; then i in dom f by FINSEQ_1:def_3; then f . i = (f ^ g) . i by FINSEQ_1:def_7; hence 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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A3, A37, A38, A39; ::_thesis: verum end; case (f . n) `2 = 9 ; ::_thesis: 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 = (f . i) `1 & s . y = (f . n) `1 ) then consider i being Element of NAT , x, y being bound_QC-variable of Al, s being QC-formula of Al such that A40: 1 <= i and A41: i < n and A42: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & ((f ^ g) . n) `1 = s . y ) by A3, A24, Def4; i <= len f by A2, A41, XXREAL_0:2; then i in Seg (len f) by A40, FINSEQ_1:1; then i in dom f by FINSEQ_1:def_3; then f . i = (f ^ g) . i by FINSEQ_1:def_7; hence 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 = (f . i) `1 & s . y = (f . n) `1 ) by A3, A40, A41, A42; ::_thesis: verum end; end; end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let n be Element of NAT ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: 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 let g, f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( 1 <= n & n <= len g & g,n is_a_correct_step_wrt X implies f ^ g,n + (len f) is_a_correct_step_wrt X ) assume that A1: 1 <= n and A2: n <= len g and A3: g,n is_a_correct_step_wrt X ; ::_thesis: f ^ g,n + (len f) is_a_correct_step_wrt X n in Seg (len g) by A1, A2, FINSEQ_1:1; then n in dom g by FINSEQ_1:def_3; then A4: g . n = (f ^ g) . (n + (len f)) by FINSEQ_1:def_7; n + (len f) <= (len f) + (len g) by A2, XREAL_1:6; then A5: n + (len f) <= len (f ^ g) by FINSEQ_1:22; percases ( ((f ^ g) . (n + (len f))) `2 = 0 or ((f ^ g) . (n + (len f))) `2 = 1 or ((f ^ g) . (n + (len f))) `2 = 2 or ((f ^ g) . (n + (len f))) `2 = 3 or ((f ^ g) . (n + (len f))) `2 = 4 or ((f ^ g) . (n + (len f))) `2 = 5 or ((f ^ g) . (n + (len f))) `2 = 6 or ((f ^ g) . (n + (len f))) `2 = 7 or ((f ^ g) . (n + (len f))) `2 = 8 or ((f ^ g) . (n + (len f))) `2 = 9 ) by A1, A5, Th23, NAT_1:12; :: according to CQC_THE1:def_4 case ((f ^ g) . (n + (len f))) `2 = 0 ; ::_thesis: ((f ^ g) . (n + (len f))) `1 in X hence ((f ^ g) . (n + (len f))) `1 in X by A3, A4, Def4; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 1 ; ::_thesis: ((f ^ g) . (n + (len f))) `1 = VERUM Al hence ((f ^ g) . (n + (len f))) `1 = VERUM Al by A3, A4, Def4; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 2 ; ::_thesis: ex p being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (('not' p) => p) => p hence ex p being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (('not' p) => p) => p by A3, A4, Def4; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 3 ; ::_thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = p => (('not' p) => q) hence ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = p => (('not' p) => q) by A3, A4, Def4; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 4 ; ::_thesis: ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) hence ex p, q, r being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A3, A4, Def4; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 5 ; ::_thesis: ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => (q '&' p) hence ex p, q being Element of CQC-WFF Al st ((f ^ g) . (n + (len f))) `1 = (p '&' q) => (q '&' p) by A3, A4, Def4; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 6 ; ::_thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . (n + (len f))) `1 = (All (x,p)) => p hence ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st ((f ^ g) . (n + (len f))) `1 = (All (x,p)) => p by A3, A4, Def4; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 7 ; ::_thesis: ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q ) then consider i, j being Element of NAT , r, t being Element of CQC-WFF Al such that A6: 1 <= i and A7: i < n and A8: 1 <= j and A9: j < i and A10: ( r = (g . j) `1 & t = (g . n) `1 & (g . i) `1 = r => t ) by A3, A4, Def4; A11: ( 1 <= i + (len f) & i + (len f) < n + (len f) ) by A6, A7, NAT_1:12, XREAL_1:6; A12: ( 1 <= j + (len f) & j + (len f) < i + (len f) ) by A8, A9, NAT_1:12, XREAL_1:6; A13: i <= len g by A2, A7, XXREAL_0:2; then A14: j <= len g by A9, XXREAL_0:2; A15: i in Seg (len g) by A6, A13, FINSEQ_1:1; A16: j in Seg (len g) by A8, A14, FINSEQ_1:1; A17: i in dom g by A15, FINSEQ_1:def_3; A18: j in dom g by A16, FINSEQ_1:def_3; A19: g . i = (f ^ g) . (i + (len f)) by A17, FINSEQ_1:def_7; g . j = (f ^ g) . (j + (len f)) by A18, FINSEQ_1:def_7; hence ex i, j being Element of NAT ex p, q being Element of CQC-WFF Al st ( 1 <= i & i < n + (len f) & 1 <= j & j < i & p = ((f ^ g) . j) `1 & q = ((f ^ g) . (n + (len f))) `1 & ((f ^ g) . i) `1 = p => q ) by A4, A10, A11, A12, A19; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 8 ; ::_thesis: 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 + (len f) & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) ) then consider i being Element of NAT , r, t being Element of CQC-WFF Al, x being bound_QC-variable of Al such that A20: 1 <= i and A21: i < n and A22: ( (g . i) `1 = r => t & not x in still_not-bound_in r & (g . n) `1 = r => (All (x,t)) ) by A3, A4, Def4; A23: ( 1 <= (len f) + i & (len f) + i < n + (len f) ) by A20, A21, NAT_1:12, XREAL_1:6; i <= len g by A2, A21, XXREAL_0:2; then i in Seg (len g) by A20, FINSEQ_1:1; then i in dom g by FINSEQ_1:def_3; then g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def_7; hence 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 + (len f) & ((f ^ g) . i) `1 = p => q & not x in still_not-bound_in p & ((f ^ g) . (n + (len f))) `1 = p => (All (x,q)) ) by A4, A22, A23; ::_thesis: verum end; case ((f ^ g) . (n + (len f))) `2 = 9 ; ::_thesis: 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 + (len f) & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 ) then consider i being Element of NAT , x, y being bound_QC-variable of Al, s being QC-formula of Al such that A24: 1 <= i and A25: i < n and A26: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (g . i) `1 & (g . n) `1 = s . y ) by A3, A4, Def4; A27: ( 1 <= (len f) + i & (len f) + i < n + (len f) ) by A24, A25, NAT_1:12, XREAL_1:6; i <= len g by A2, A25, XXREAL_0:2; then i in Seg (len g) by A24, FINSEQ_1:1; then i in dom g by FINSEQ_1:def_3; then g . i = (f ^ g) . ((len f) + i) by FINSEQ_1:def_7; hence 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 + (len f) & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = ((f ^ g) . i) `1 & s . y = ((f ^ g) . (n + (len f))) `1 ) by A4, A26, A27; ::_thesis: verum end; end; end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: 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 let f, g be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( f is_a_proof_wrt X & g is_a_proof_wrt X implies f ^ g is_a_proof_wrt X ) assume that A1: f is_a_proof_wrt X and A2: g is_a_proof_wrt X ; ::_thesis: f ^ g is_a_proof_wrt X f <> {} by A1, Def5; hence f ^ g <> {} ; :: according to CQC_THE1:def_5 ::_thesis: for n being Element of NAT st 1 <= n & n <= len (f ^ g) holds f ^ g,n is_a_correct_step_wrt X let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (f ^ g) implies f ^ g,n is_a_correct_step_wrt X ) assume that A3: 1 <= n and A4: n <= len (f ^ g) ; ::_thesis: f ^ g,n is_a_correct_step_wrt X now__::_thesis:_f_^_g,n_is_a_correct_step_wrt_X percases ( n <= len f or len f < n ) ; supposeA5: n <= len f ; ::_thesis: f ^ g,n is_a_correct_step_wrt X then f,n is_a_correct_step_wrt X by A1, A3, Def5; hence f ^ g,n is_a_correct_step_wrt X by A3, A5, Th27; ::_thesis: verum end; supposeA6: len f < n ; ::_thesis: f ^ g,n is_a_correct_step_wrt X then reconsider k = n - (len f) as Element of NAT by NAT_1:21; A7: k + (len f) <= (len g) + (len f) by A4, FINSEQ_1:22; (len f) + 1 <= k + (len f) by A6, NAT_1:13; then A8: 1 <= k by XREAL_1:6; A9: k <= len g by A7, XREAL_1:6; then ( k + (len f) = n & g,k is_a_correct_step_wrt X ) by A2, A8, Def5; hence f ^ g,n is_a_correct_step_wrt X by A8, A9, Th28; ::_thesis: verum end; end; end; hence f ^ g,n is_a_correct_step_wrt X ; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X, Y be Subset of (CQC-WFF Al); ::_thesis: 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 let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( f is_a_proof_wrt X & X c= Y implies f is_a_proof_wrt Y ) assume that A1: f is_a_proof_wrt X and A2: X c= Y ; ::_thesis: f is_a_proof_wrt Y thus f <> {} by A1, Def5; :: according to CQC_THE1:def_5 ::_thesis: for n being Element of NAT st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt Y let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len f implies f,n is_a_correct_step_wrt Y ) assume A3: ( 1 <= n & n <= len f ) ; ::_thesis: f,n is_a_correct_step_wrt Y then A4: f,n is_a_correct_step_wrt X by A1, Def5; percases ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A3, Th23; :: according to CQC_THE1:def_4 case (f . n) `2 = 0 ; ::_thesis: (f . n) `1 in Y then (f . n) `1 in X by A4, Def4; hence (f . n) `1 in Y by A2; ::_thesis: verum end; case (f . n) `2 = 1 ; ::_thesis: (f . n) `1 = VERUM Al hence (f . n) `1 = VERUM Al by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 2 ; ::_thesis: ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p hence ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 3 ; ::_thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q) hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q) by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 4 ; ::_thesis: ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) hence ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 5 ; ::_thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 6 ; ::_thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p hence ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 7 ; ::_thesis: 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 = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) hence 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 = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 8 ; ::_thesis: 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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) hence 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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A4, Def4; ::_thesis: verum end; case (f . n) `2 = 9 ; ::_thesis: 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 = (f . i) `1 & s . y = (f . n) `1 ) hence 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 = (f . i) `1 & s . y = (f . n) `1 ) by A4, Def4; ::_thesis: verum end; end; end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let l be Element of NAT ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: 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 let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( f is_a_proof_wrt X & 1 <= l & l <= len f implies (f . l) `1 in Cn X ) assume that A1: f is_a_proof_wrt X and A2: ( 1 <= l & l <= len f ) ; ::_thesis: (f . l) `1 in Cn X for n being Element of NAT st 1 <= n & n <= len f holds (f . n) `1 in Cn X proof defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len f implies (f . \$1) `1 in Cn X ); A3: for n being Nat st ( for k being Nat st k < n holds S1[k] ) holds S1[n] proof let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds S1[k] ) implies S1[n] ) assume A4: for k being Nat st k < n holds S1[k] ; ::_thesis: S1[n] A5: n in NAT by ORDINAL1:def_12; assume that A6: 1 <= n and A7: n <= len f ; ::_thesis: (f . n) `1 in Cn X A8: f,n is_a_correct_step_wrt X by A1, A5, A6, A7, Def5; now__::_thesis:_(f_._n)_`1_in_Cn_X percases ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A6, A7, Th23; suppose (f . n) `2 = 0 ; ::_thesis: (f . n) `1 in Cn X then A9: (f . n) `1 in X by A8, Def4; X c= Cn X by Th17; hence (f . n) `1 in Cn X by A9; ::_thesis: verum end; suppose (f . n) `2 = 1 ; ::_thesis: (f . n) `1 in Cn X then (f . n) `1 = VERUM Al by A8, Def4; hence (f . n) `1 in Cn X by Th6; ::_thesis: verum end; suppose (f . n) `2 = 2 ; ::_thesis: (f . n) `1 in Cn X then ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p by A8, Def4; hence (f . n) `1 in Cn X by Th7; ::_thesis: verum end; suppose (f . n) `2 = 3 ; ::_thesis: (f . n) `1 in Cn X then ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q) by A8, Def4; hence (f . n) `1 in Cn X by Th8; ::_thesis: verum end; suppose (f . n) `2 = 4 ; ::_thesis: (f . n) `1 in Cn X then ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A8, Def4; hence (f . n) `1 in Cn X by Th9; ::_thesis: verum end; suppose (f . n) `2 = 5 ; ::_thesis: (f . n) `1 in Cn X then ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) by A8, Def4; hence (f . n) `1 in Cn X by Th10; ::_thesis: verum end; suppose (f . n) `2 = 6 ; ::_thesis: (f . n) `1 in Cn X then ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p by A8, Def4; hence (f . n) `1 in Cn X by Th12; ::_thesis: verum end; suppose (f . n) `2 = 7 ; ::_thesis: (f . n) `1 in Cn X then consider i, j being Element of NAT , p, q being Element of CQC-WFF Al such that A10: 1 <= i and A11: i < n and A12: 1 <= j and A13: j < i and A14: ( p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A8, Def4; A15: j < n by A11, A13, XXREAL_0:2; A16: i <= len f by A7, A11, XXREAL_0:2; then j <= len f by A13, XXREAL_0:2; then A17: (f . j) `1 in Cn X by A4, A12, A15; (f . i) `1 in Cn X by A4, A10, A11, A16; hence (f . n) `1 in Cn X by A14, A17, Th11; ::_thesis: verum end; suppose (f . n) `2 = 8 ; ::_thesis: (f . n) `1 in Cn X then consider i being Element of NAT , p, q being Element of CQC-WFF Al, x being bound_QC-variable of Al such that A18: 1 <= i and A19: i < n and A20: ( (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A8, Def4; i <= len f by A7, A19, XXREAL_0:2; hence (f . n) `1 in Cn X by A4, A18, A19, A20, Th13; ::_thesis: verum end; suppose (f . n) `2 = 9 ; ::_thesis: (f . n) `1 in Cn X then consider i being Element of NAT , x, y being bound_QC-variable of Al, s being QC-formula of Al such that A21: 1 <= i and A22: i < n and A23: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . n) `1 = s . y ) by A8, Def4; i <= len f by A7, A22, XXREAL_0:2; hence (f . n) `1 in Cn X by A4, A21, A22, A23, Th14; ::_thesis: verum end; end; end; hence (f . n) `1 in Cn X ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_4(A3); hence for n being Element of NAT st 1 <= n & n <= len f holds (f . n) `1 in Cn X ; ::_thesis: verum end; hence (f . l) `1 in Cn X by A2; ::_thesis: verum end; 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 proof 0 <= len f by NAT_1:2; then 0 + 1 <= len f by A1, NAT_1:13; then A2: len f in Seg (len f) by FINSEQ_1:1; Seg (len f) = dom f by FINSEQ_1:def_3; then A3: f . (len f) in rng f by A2, FUNCT_1:def_3; rng f c= [:(CQC-WFF Al),Proof_Step_Kinds:] by FINSEQ_1:def_4; hence (f . (len f)) `1 is Element of CQC-WFF Al by A3, MCART_1:10; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds Effect f in Cn X let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; ::_thesis: ( f is_a_proof_wrt X implies Effect f in Cn X ) assume A1: f is_a_proof_wrt X ; ::_thesis: Effect f in Cn X then A2: 1 <= len f by Th25; then A3: (f . (len f)) `1 in Cn X by A1, Th31; f <> {} by A2; hence Effect f in Cn X by A3, Def6; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: { 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 defpred S1[ set ] means ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = \$1 ); thus { p where p is Element of CQC-WFF Al : S1[p] } c= CQC-WFF Al from FRAENKEL:sch_10(); ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: 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 ) } let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a 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 ) } ) assume A1: a in X ; ::_thesis: a 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 ) } then reconsider p = a as Element of CQC-WFF Al ; reconsider pp = [p,0] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set f = <*pp*>; A2: len <*pp*> = 1 by FINSEQ_1:40; A3: <*pp*> . 1 = pp by FINSEQ_1:40; then (<*pp*> . (len <*pp*>)) `1 = p by A2, MCART_1:7; then A4: Effect <*pp*> = p by Def6; for n being Element of NAT st 1 <= n & n <= len <*pp*> holds <*pp*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X ) assume ( 1 <= n & n <= len <*pp*> ) ; ::_thesis: <*pp*>,n is_a_correct_step_wrt X then A5: n = 1 by A2, XXREAL_0:1; A6: (<*pp*> . 1) `2 = 0 by A3, MCART_1:7; (<*pp*> . n) `1 in X by A1, A3, A5, MCART_1:7; hence <*pp*>,n is_a_correct_step_wrt X by A5, A6, Def4; ::_thesis: verum end; then <*pp*> is_a_proof_wrt X by Def5; hence a 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 ) } by A4; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: 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 ) } reconsider pp = [(VERUM Al),1] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set f = <*pp*>; A1: len <*pp*> = 1 by FINSEQ_1:40; A2: <*pp*> . 1 = pp by FINSEQ_1:40; then (<*pp*> . (len <*pp*>)) `1 = VERUM Al by A1, MCART_1:7; then A3: Effect <*pp*> = VERUM Al by Def6; for n being Element of NAT st 1 <= n & n <= len <*pp*> holds <*pp*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X ) assume ( 1 <= n & n <= len <*pp*> ) ; ::_thesis: <*pp*>,n is_a_correct_step_wrt X then A4: n = 1 by A1, XXREAL_0:1; A5: (<*pp*> . 1) `2 = 1 by A2, MCART_1:7; (<*pp*> . n) `1 = VERUM Al by A2, A4, MCART_1:7; hence <*pp*>,n is_a_correct_step_wrt X by A4, A5, Def4; ::_thesis: verum end; then <*pp*> is_a_proof_wrt X by Def5; hence 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 ) } by A3; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let p be Element of CQC-WFF Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: (('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 ) } reconsider pp = [((('not' p) => p) => p),2] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set f = <*pp*>; A1: len <*pp*> = 1 by FINSEQ_1:40; A2: <*pp*> . 1 = pp by FINSEQ_1:40; then (<*pp*> . (len <*pp*>)) `1 = (('not' p) => p) => p by A1, MCART_1:7; then A3: Effect <*pp*> = (('not' p) => p) => p by Def6; for n being Element of NAT st 1 <= n & n <= len <*pp*> holds <*pp*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X ) assume ( 1 <= n & n <= len <*pp*> ) ; ::_thesis: <*pp*>,n is_a_correct_step_wrt X then A4: n = 1 by A1, XXREAL_0:1; A5: (<*pp*> . 1) `2 = 2 by A2, MCART_1:7; (<*pp*> . n) `1 = (('not' p) => p) => p by A2, A4, MCART_1:7; hence <*pp*>,n is_a_correct_step_wrt X by A4, A5, Def4; ::_thesis: verum end; then <*pp*> is_a_proof_wrt X by Def5; hence (('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 ) } by A3; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let p, q be Element of CQC-WFF Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: 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 ) } reconsider pp = [(p => (('not' p) => q)),3] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set f = <*pp*>; A1: len <*pp*> = 1 by FINSEQ_1:40; A2: <*pp*> . 1 = pp by FINSEQ_1:40; then (<*pp*> . (len <*pp*>)) `1 = p => (('not' p) => q) by A1, MCART_1:7; then A3: Effect <*pp*> = p => (('not' p) => q) by Def6; for n being Element of NAT st 1 <= n & n <= len <*pp*> holds <*pp*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X ) assume ( 1 <= n & n <= len <*pp*> ) ; ::_thesis: <*pp*>,n is_a_correct_step_wrt X then A4: n = 1 by A1, XXREAL_0:1; A5: (<*pp*> . 1) `2 = 3 by A2, MCART_1:7; (<*pp*> . n) `1 = p => (('not' p) => q) by A2, A4, MCART_1:7; hence <*pp*>,n is_a_correct_step_wrt X by A4, A5, Def4; ::_thesis: verum end; then <*pp*> is_a_proof_wrt X by Def5; hence 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 ) } by A3; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let p, q, r be Element of CQC-WFF Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: (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 ) } reconsider pp = [((p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))),4] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set f = <*pp*>; A1: len <*pp*> = 1 by FINSEQ_1:40; A2: <*pp*> . 1 = pp by FINSEQ_1:40; then (<*pp*> . (len <*pp*>)) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A1, MCART_1:7; then A3: Effect <*pp*> = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by Def6; for n being Element of NAT st 1 <= n & n <= len <*pp*> holds <*pp*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X ) assume ( 1 <= n & n <= len <*pp*> ) ; ::_thesis: <*pp*>,n is_a_correct_step_wrt X then A4: n = 1 by A1, XXREAL_0:1; A5: (<*pp*> . 1) `2 = 4 by A2, MCART_1:7; (<*pp*> . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A2, A4, MCART_1:7; hence <*pp*>,n is_a_correct_step_wrt X by A4, A5, Def4; ::_thesis: verum end; then <*pp*> is_a_proof_wrt X by Def5; hence (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 ) } by A3; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let p, q be Element of CQC-WFF Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: (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 ) } reconsider pp = [((p '&' q) => (q '&' p)),5] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set f = <*pp*>; A1: len <*pp*> = 1 by FINSEQ_1:40; A2: <*pp*> . 1 = pp by FINSEQ_1:40; then (<*pp*> . (len <*pp*>)) `1 = (p '&' q) => (q '&' p) by A1, MCART_1:7; then A3: Effect <*pp*> = (p '&' q) => (q '&' p) by Def6; for n being Element of NAT st 1 <= n & n <= len <*pp*> holds <*pp*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X ) assume ( 1 <= n & n <= len <*pp*> ) ; ::_thesis: <*pp*>,n is_a_correct_step_wrt X then A4: n = 1 by A1, XXREAL_0:1; A5: (<*pp*> . 1) `2 = 5 by A2, MCART_1:7; (<*pp*> . n) `1 = (p '&' q) => (q '&' p) by A2, A4, MCART_1:7; hence <*pp*>,n is_a_correct_step_wrt X by A4, A5, Def4; ::_thesis: verum end; then <*pp*> is_a_proof_wrt X by Def5; hence (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 ) } by A3; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let p, q be Element of CQC-WFF Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: ( 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 ) } implies 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 ) } ) assume that A1: 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 ) } and A2: 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 ) } ; ::_thesis: 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 ) } ex t being Element of CQC-WFF Al st ( t = p & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = t ) ) by A1; then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that A3: f is_a_proof_wrt X and A4: Effect f = p ; ex r being Element of CQC-WFF Al st ( r = p => q & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = r ) ) by A2; then consider g being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that A5: g is_a_proof_wrt X and A6: Effect g = p => q ; A7: f <> {} by A3, Def5; A8: g <> {} by A5, Def5; reconsider qq = [q,7] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set h = (f ^ g) ^ <*qq*>; A9: len ((f ^ g) ^ <*qq*>) = (len (f ^ g)) + (len <*qq*>) by FINSEQ_1:22 .= (len (f ^ g)) + 1 by FINSEQ_1:40 ; then A10: len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1 by FINSEQ_1:22; ((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq by A9, FINSEQ_1:42; then (((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q by MCART_1:7; then A11: Effect ((f ^ g) ^ <*qq*>) = q by Def6; for n being Element of NAT st 1 <= n & n <= len ((f ^ g) ^ <*qq*>) holds (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len ((f ^ g) ^ <*qq*>) implies (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X ) assume that A12: 1 <= n and A13: n <= len ((f ^ g) ^ <*qq*>) ; ::_thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X now__::_thesis:_(f_^_g)_^_<*qq*>,n_is_a_correct_step_wrt_X percases ( n <= (len f) + (len g) or n = len ((f ^ g) ^ <*qq*>) ) by A10, A13, NAT_1:8; suppose n <= (len f) + (len g) ; ::_thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X then A14: n <= len (f ^ g) by FINSEQ_1:22; f ^ g is_a_proof_wrt X by A3, A5, Th29; then f ^ g,n is_a_correct_step_wrt X by A12, A14, Def5; hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A12, A14, Th27; ::_thesis: verum end; supposeA15: n = len ((f ^ g) ^ <*qq*>) ; ::_thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X then ((f ^ g) ^ <*qq*>) . n = qq by A9, FINSEQ_1:42; then A16: ( (((f ^ g) ^ <*qq*>) . n) `2 = 7 & (((f ^ g) ^ <*qq*>) . n) `1 = q ) by MCART_1:7; len f <> 0 by A3, Th25; then len f in Seg (len f) by FINSEQ_1:3; then A17: len f in dom f by FINSEQ_1:def_3; (f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>) by FINSEQ_1:32; then A18: (((f ^ g) ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by A17, FINSEQ_1:def_7 .= p by A4, A7, Def6 ; ( dom g = Seg (len g) & len g <> 0 ) by A5, Th25, FINSEQ_1:def_3; then A19: len g in dom g by FINSEQ_1:3; ( 1 <= len f & len f <= (len f) + (len g) ) by A3, Th25, NAT_1:11; then (len f) + (len g) in Seg ((len f) + (len g)) by FINSEQ_1:3; then (len f) + (len g) in Seg (len (f ^ g)) by FINSEQ_1:22; then (len f) + (len g) in dom (f ^ g) by FINSEQ_1:def_3; then A20: (((f ^ g) ^ <*qq*>) . ((len f) + (len g))) `1 = ((f ^ g) . ((len f) + (len g))) `1 by FINSEQ_1:def_7 .= (g . (len g)) `1 by A19, FINSEQ_1:def_7 .= p => q by A6, A8, Def6 ; 1 <= len g by A5, Th25; then (len f) + 1 <= (len f) + (len g) by XREAL_1:7; then A21: len f < (len f) + (len g) by NAT_1:13; A22: ( 1 <= len f & 1 <= (len f) + (len g) ) by A3, Th25, NAT_1:12; (len f) + (len g) < n by A10, A15, NAT_1:13; hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A16, A18, A20, A21, A22, Def4; ::_thesis: verum end; end; end; hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X ; ::_thesis: verum end; then (f ^ g) ^ <*qq*> is_a_proof_wrt X by Def5; hence 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 ) } by A11; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let p be Element of CQC-WFF Al; ::_thesis: 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 ) } let x be bound_QC-variable of Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: (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 ) } reconsider pp = [((All (x,p)) => p),6] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set f = <*pp*>; A1: len <*pp*> = 1 by FINSEQ_1:40; A2: <*pp*> . 1 = pp by FINSEQ_1:40; then (<*pp*> . (len <*pp*>)) `1 = (All (x,p)) => p by A1, MCART_1:7; then A3: Effect <*pp*> = (All (x,p)) => p by Def6; for n being Element of NAT st 1 <= n & n <= len <*pp*> holds <*pp*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X ) assume ( 1 <= n & n <= len <*pp*> ) ; ::_thesis: <*pp*>,n is_a_correct_step_wrt X then A4: n = 1 by A1, XXREAL_0:1; A5: (<*pp*> . 1) `2 = 6 by A2, MCART_1:7; (<*pp*> . n) `1 = (All (x,p)) => p by A2, A4, MCART_1:7; hence <*pp*>,n is_a_correct_step_wrt X by A4, A5, Def4; ::_thesis: verum end; then <*pp*> is_a_proof_wrt X by Def5; hence (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 ) } by A3; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let p, q be Element of CQC-WFF Al; ::_thesis: 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 ) } let x be bound_QC-variable of Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: ( 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 implies 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 ) } ) assume that A1: 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 ) } and A2: not x in still_not-bound_in p ; ::_thesis: 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 ) } ex t being Element of CQC-WFF Al st ( t = p => q & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = t ) ) by A1; then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that A3: f is_a_proof_wrt X and A4: Effect f = p => q ; A5: f <> {} by A3, Def5; reconsider qq = [(p => (All (x,q))),8] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th21, ZFMISC_1:87; set h = f ^ <*qq*>; A6: len (f ^ <*qq*>) = (len f) + (len <*qq*>) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; for n being Element of NAT st 1 <= n & n <= len (f ^ <*qq*>) holds f ^ <*qq*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (f ^ <*qq*>) implies f ^ <*qq*>,n is_a_correct_step_wrt X ) assume that A7: 1 <= n and A8: n <= len (f ^ <*qq*>) ; ::_thesis: f ^ <*qq*>,n is_a_correct_step_wrt X now__::_thesis:_f_^_<*qq*>,n_is_a_correct_step_wrt_X percases ( n <= len f or n = len (f ^ <*qq*>) ) by A6, A8, NAT_1:8; supposeA9: n <= len f ; ::_thesis: f ^ <*qq*>,n is_a_correct_step_wrt X then f,n is_a_correct_step_wrt X by A3, A7, Def5; hence f ^ <*qq*>,n is_a_correct_step_wrt X by A7, A9, Th27; ::_thesis: verum end; supposeA10: n = len (f ^ <*qq*>) ; ::_thesis: f ^ <*qq*>,n is_a_correct_step_wrt X then (f ^ <*qq*>) . n = qq by A6, FINSEQ_1:42; then A11: ( ((f ^ <*qq*>) . n) `2 = 8 & ((f ^ <*qq*>) . n) `1 = p => (All (x,q)) ) by MCART_1:7; len f <> 0 by A3, Th25; then len f in Seg (len f) by FINSEQ_1:3; then len f in dom f by FINSEQ_1:def_3; then A12: ((f ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by FINSEQ_1:def_7 .= p => q by A4, A5, Def6 ; A13: 1 <= len f by A3, Th25; len f < n by A6, A10, NAT_1:13; hence f ^ <*qq*>,n is_a_correct_step_wrt X by A2, A11, A12, A13, Def4; ::_thesis: verum end; end; end; hence f ^ <*qq*>,n is_a_correct_step_wrt X ; ::_thesis: verum end; then A14: f ^ <*qq*> is_a_proof_wrt X by Def5; Effect (f ^ <*qq*>) = ((f ^ <*qq*>) . ((len f) + 1)) `1 by A6, Def6 .= qq `1 by FINSEQ_1:42 .= p => (All (x,q)) by MCART_1:7 ; hence 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 ) } by A14; ::_thesis: verum end; 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 ) } proof let Al be QC-alphabet ; ::_thesis: 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 ) } let s be QC-formula of Al; ::_thesis: 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 ) } let x, y be bound_QC-variable of Al; ::_thesis: 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 ) } let X be Subset of (CQC-WFF Al); ::_thesis: ( 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 ) } implies 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 ) } ) assume that A1: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al ) and A2: not x in still_not-bound_in s and A3: 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 ) } ; ::_thesis: 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 ) } ex t being Element of CQC-WFF Al st ( t = s . x & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = t ) ) by A3; then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that A4: f is_a_proof_wrt X and A5: Effect f = s . x ; A6: f <> {} by A4, Def5; reconsider qq = [(s . y),9] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by A1, Th21, ZFMISC_1:87; set h = f ^ <*qq*>; A7: len (f ^ <*qq*>) = (len f) + (len <*qq*>) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; for n being Element of NAT st 1 <= n & n <= len (f ^ <*qq*>) holds f ^ <*qq*>,n is_a_correct_step_wrt X proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (f ^ <*qq*>) implies f ^ <*qq*>,n is_a_correct_step_wrt X ) assume that A8: 1 <= n and A9: n <= len (f ^ <*qq*>) ; ::_thesis: f ^ <*qq*>,n is_a_correct_step_wrt X now__::_thesis:_f_^_<*qq*>,n_is_a_correct_step_wrt_X percases ( n <= len f or n = len (f ^ <*qq*>) ) by A7, A9, NAT_1:8; supposeA10: n <= len f ; ::_thesis: f ^ <*qq*>,n is_a_correct_step_wrt X then f,n is_a_correct_step_wrt X by A4, A8, Def5; hence f ^ <*qq*>,n is_a_correct_step_wrt X by A8, A10, Th27; ::_thesis: verum end; supposeA11: n = len (f ^ <*qq*>) ; ::_thesis: f ^ <*qq*>,n is_a_correct_step_wrt X then (f ^ <*qq*>) . n = qq by A7, FINSEQ_1:42; then A12: ( ((f ^ <*qq*>) . n) `2 = 9 & ((f ^ <*qq*>) . n) `1 = s . y ) by MCART_1:7; len f <> 0 by A4, Th25; then len f in Seg (len f) by FINSEQ_1:3; then len f in dom f by FINSEQ_1:def_3; then A13: ((f ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by FINSEQ_1:def_7 .= s . x by A5, A6, Def6 ; A14: 1 <= len f by A4, Th25; len f < n by A7, A11, NAT_1:13; hence f ^ <*qq*>,n is_a_correct_step_wrt X by A1, A2, A12, A13, A14, Def4; ::_thesis: verum end; end; end; hence f ^ <*qq*>,n is_a_correct_step_wrt X ; ::_thesis: verum end; then A15: f ^ <*qq*> is_a_proof_wrt X by Def5; Effect (f ^ <*qq*>) = ((f ^ <*qq*>) . ((len f) + 1)) `1 by A7, Def6 .= qq `1 by FINSEQ_1:42 .= s . y by MCART_1:7 ; hence 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 ) } by A15; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let Y, X be Subset of (CQC-WFF Al); ::_thesis: ( 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 ) } implies Y is being_a_theory ) assume A1: 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 ) } ; ::_thesis: Y is being_a_theory hence VERUM Al in Y by Lm3; :: according to CQC_THE1:def_1 ::_thesis: 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 Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) let p, q, r be Element of CQC-WFF Al; ::_thesis: for s being QC-formula of Al for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) let s be QC-formula of Al; ::_thesis: for x, y being bound_QC-variable of Al holds ( (('not' p) => p) => p in Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) let x, y be bound_QC-variable of Al; ::_thesis: ( (('not' p) => p) => p in Y & p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) thus (('not' p) => p) => p in Y by A1, Lm4; ::_thesis: ( p => (('not' p) => q) in Y & (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) thus p => (('not' p) => q) in Y by A1, Lm5; ::_thesis: ( (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y & (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) thus (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Y by A1, Lm6; ::_thesis: ( (p '&' q) => (q '&' p) in Y & ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) thus (p '&' q) => (q '&' p) in Y by A1, Lm7; ::_thesis: ( ( p in Y & p => q in Y implies q in Y ) & (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) thus ( p in Y & p => q in Y implies q in Y ) by A1, Lm8; ::_thesis: ( (All (x,p)) => p in Y & ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) thus (All (x,p)) => p in Y by A1, Lm9; ::_thesis: ( ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) & ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) ) thus ( p => q in Y & not x in still_not-bound_in p implies p => (All (x,q)) in Y ) by A1, Lm10; ::_thesis: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) thus ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in Y implies s . y in Y ) by A1, Lm11; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: { 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 let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { 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 ) } or a in Cn X ) assume a in { 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 ) } ; ::_thesis: a in Cn X then ex q being Element of CQC-WFF Al st ( q = a & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = q ) ) ; hence a in Cn X by Th32; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: { 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 set PX = { 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 ) } ; A1: { 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 by Lm12; reconsider PX = { 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 ) } as Subset of (CQC-WFF Al) by Lm2; X c= PX by Th33; then Cn X c= { 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 ) } by Th16, Th34; hence { 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 by A1, XBOOLE_0:def_10; ::_thesis: verum end; 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 ) ) proof let Al be QC-alphabet ; ::_thesis: 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 ) ) let X be Subset of (CQC-WFF Al); ::_thesis: 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 ) ) let p be Element of CQC-WFF Al; ::_thesis: ( 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 ) ) thus ( p in Cn X implies ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) ) ::_thesis: ( ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X ) proof assume p in Cn X ; ::_thesis: ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) then 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 ) } by Th35; then ex F being Element of CQC-WFF Al st ( F = p & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = F ) ) ; hence ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) ; ::_thesis: verum end; thus ( ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt X & Effect f = p ) implies p in Cn X ) ::_thesis: verum proof given f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that A1: ( f is_a_proof_wrt X & Effect f = p ) ; ::_thesis: p in Cn X 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 ) } by A1; hence p in Cn X by Th35; ::_thesis: verum end; end; 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 ) proof let Al be QC-alphabet ; ::_thesis: 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 ) let X be Subset of (CQC-WFF Al); ::_thesis: 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 ) let p be Element of CQC-WFF Al; ::_thesis: ( p in Cn X implies ex Y being Subset of (CQC-WFF Al) st ( Y c= X & Y is finite & p in Cn Y ) ) assume p in Cn X ; ::_thesis: ex Y being Subset of (CQC-WFF Al) st ( Y c= X & Y is finite & p in Cn Y ) then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that A1: f is_a_proof_wrt X and A2: Effect f = p by Th36; A3: f <> {} by A1, Def5; rng f c= [:(CQC-WFF Al),Proof_Step_Kinds:] by FINSEQ_1:def_4; then consider A being set such that A4: A is finite and A5: A c= CQC-WFF Al and A6: rng f c= [:A,Proof_Step_Kinds:] by FINSET_1:14; reconsider Z = A as Subset of (CQC-WFF Al) by A5; take Y = Z /\ X; ::_thesis: ( Y c= X & Y is finite & p in Cn Y ) thus Y c= X by XBOOLE_1:17; ::_thesis: ( Y is finite & p in Cn Y ) thus Y is finite by A4; ::_thesis: p in Cn Y for n being Element of NAT st 1 <= n & n <= len f holds f,n is_a_correct_step_wrt Y proof let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len f implies f,n is_a_correct_step_wrt Y ) assume A7: ( 1 <= n & n <= len f ) ; ::_thesis: f,n is_a_correct_step_wrt Y then A8: f,n is_a_correct_step_wrt X by A1, Def5; percases ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A7, Th23; :: according to CQC_THE1:def_4 case (f . n) `2 = 0 ; ::_thesis: (f . n) `1 in Y then A9: (f . n) `1 in X by A8, Def4; n in Seg (len f) by A7, FINSEQ_1:1; then n in dom f by FINSEQ_1:def_3; then f . n in rng f by FUNCT_1:def_3; then (f . n) `1 in A by A6, MCART_1:10; hence (f . n) `1 in Y by A9, XBOOLE_0:def_4; ::_thesis: verum end; case (f . n) `2 = 1 ; ::_thesis: (f . n) `1 = VERUM Al hence (f . n) `1 = VERUM Al by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 2 ; ::_thesis: ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p hence ex p being Element of CQC-WFF Al st (f . n) `1 = (('not' p) => p) => p by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 3 ; ::_thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q) hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = p => (('not' p) => q) by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 4 ; ::_thesis: ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) hence ex p, q, r being Element of CQC-WFF Al st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 5 ; ::_thesis: ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) hence ex p, q being Element of CQC-WFF Al st (f . n) `1 = (p '&' q) => (q '&' p) by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 6 ; ::_thesis: ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p hence ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st (f . n) `1 = (All (x,p)) => p by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 7 ; ::_thesis: 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 = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) hence 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 = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 8 ; ::_thesis: 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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) hence 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 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All (x,q)) ) by A8, Def4; ::_thesis: verum end; case (f . n) `2 = 9 ; ::_thesis: 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 = (f . i) `1 & s . y = (f . n) `1 ) hence 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 = (f . i) `1 & s . y = (f . n) `1 ) by A8, Def4; ::_thesis: verum end; end; end; then f is_a_proof_wrt Y by A3, Def5; then p in { q where q is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st ( f is_a_proof_wrt Y & Effect f = q ) } by A2; hence p in Cn Y by Th35; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for T being Subset of (CQC-WFF Al) st T is being_a_theory holds TAUT Al c= T let T be Subset of (CQC-WFF Al); ::_thesis: ( T is being_a_theory implies TAUT Al c= T ) assume A1: T is being_a_theory ; ::_thesis: TAUT Al c= T Cn ({} (CQC-WFF Al)) c= Cn T by Th18, XBOOLE_1:2; hence TAUT Al c= T by A1, Th20; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: VERUM Al in TAUT Al TAUT Al is being_a_theory by Th15; hence VERUM Al in TAUT Al by Def1; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al holds (('not' p) => p) => p in TAUT Al let p be Element of CQC-WFF Al; ::_thesis: (('not' p) => p) => p in TAUT Al TAUT Al is being_a_theory by Th15; hence (('not' p) => p) => p in TAUT Al by Def1; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in TAUT Al let p, q be Element of CQC-WFF Al; ::_thesis: p => (('not' p) => q) in TAUT Al TAUT Al is being_a_theory by Th15; hence p => (('not' p) => q) in TAUT Al by Def1; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al let p, q, r be Element of CQC-WFF Al; ::_thesis: (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al TAUT Al is being_a_theory by Th15; hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al by Def1; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) in TAUT Al let p, q be Element of CQC-WFF Al; ::_thesis: (p '&' q) => (q '&' p) in TAUT Al TAUT Al is being_a_theory by Th15; hence (p '&' q) => (q '&' p) in TAUT Al by Def1; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al st p in TAUT Al & p => q in TAUT Al holds q in TAUT Al let p, q be Element of CQC-WFF Al; ::_thesis: ( p in TAUT Al & p => q in TAUT Al implies q in TAUT Al ) TAUT Al is being_a_theory by Th15; hence ( p in TAUT Al & p => q in TAUT Al implies q in TAUT Al ) by Def1; ::_thesis: verum end; 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; 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 proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds X |- VERUM Al let X be Subset of (CQC-WFF Al); ::_thesis: X |- VERUM Al VERUM Al in Cn X by Th6; hence X |- VERUM Al by Def8; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds X |- (('not' p) => p) => p let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al holds X |- (('not' p) => p) => p let p be Element of CQC-WFF Al; ::_thesis: X |- (('not' p) => p) => p (('not' p) => p) => p in Cn X by Th7; hence X |- (('not' p) => p) => p by Def8; ::_thesis: verum end; 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) proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al holds X |- p => (('not' p) => q) let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al holds X |- p => (('not' p) => q) let p, q be Element of CQC-WFF Al; ::_thesis: X |- p => (('not' p) => q) p => (('not' p) => q) in Cn X by Th8; hence X |- p => (('not' p) => q) by Def8; ::_thesis: verum end; 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))) proof let Al be QC-alphabet ; ::_thesis: 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))) let X be Subset of (CQC-WFF Al); ::_thesis: for p, q, r being Element of CQC-WFF Al holds X |- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) let p, q, r be Element of CQC-WFF Al; ::_thesis: X |- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in Cn X by Th9; hence X |- (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by Def8; ::_thesis: verum end; 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) proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al holds X |- (p '&' q) => (q '&' p) let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al holds X |- (p '&' q) => (q '&' p) let p, q be Element of CQC-WFF Al; ::_thesis: X |- (p '&' q) => (q '&' p) (p '&' q) => (q '&' p) in Cn X by Th10; hence X |- (p '&' q) => (q '&' p) by Def8; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al st X |- p & X |- p => q holds X |- q let p, q be Element of CQC-WFF Al; ::_thesis: ( X |- p & X |- p => q implies X |- q ) assume ( X |- p & X |- p => q ) ; ::_thesis: X |- q then ( p in Cn X & p => q in Cn X ) by Def8; then q in Cn X by Th11; hence X |- q by Def8; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al holds X |- (All (x,p)) => p let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al holds X |- (All (x,p)) => p let x be bound_QC-variable of Al; ::_thesis: X |- (All (x,p)) => p (All (x,p)) => p in Cn X by Th12; hence X |- (All (x,p)) => p by Def8; ::_thesis: verum end; 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)) proof let Al be QC-alphabet ; ::_thesis: 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)) let X be Subset of (CQC-WFF Al); ::_thesis: 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)) let p, q be Element of CQC-WFF Al; ::_thesis: 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)) let x be bound_QC-variable of Al; ::_thesis: ( X |- p => q & not x in still_not-bound_in p implies X |- p => (All (x,q)) ) assume that A1: X |- p => q and A2: not x in still_not-bound_in p ; ::_thesis: X |- p => (All (x,q)) p => q in Cn X by A1, Def8; then p => (All (x,q)) in Cn X by A2, Th13; hence X |- p => (All (x,q)) by Def8; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let X be Subset of (CQC-WFF Al); ::_thesis: 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 let s be QC-formula of Al; ::_thesis: 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 let y, x be bound_QC-variable of Al; ::_thesis: ( s . y in CQC-WFF Al & not x in still_not-bound_in s & X |- s . x implies X |- s . y ) assume that A1: ( s . y in CQC-WFF Al & not x in still_not-bound_in s ) and A2: X |- s . x ; ::_thesis: X |- s . y s . x in Cn X by A2, Def8; then s . y in Cn X by A1, Th14; hence X |- s . y by Def8; ::_thesis: verum end; 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 ) proof let Al be QC-alphabet ; ::_thesis: for s being QC-formula of Al holds ( s is valid iff s in TAUT Al ) let s be QC-formula of Al; ::_thesis: ( s is valid iff s in TAUT Al ) ( s is valid iff {} (CQC-WFF Al) |- s ) by Def9; hence ( s is valid iff s in TAUT Al ) by Def8; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al st p is valid holds X |- p let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al st p is valid holds X |- p let p be Element of CQC-WFF Al; ::_thesis: ( p is valid implies X |- p ) assume p is valid ; ::_thesis: X |- p then A1: p in TAUT Al by Lm13; TAUT Al c= Cn X by Th15, Th38; hence X |- p by A1, Def8; ::_thesis: verum end; theorem :: CQC_THE1:60 for Al being QC-alphabet holds VERUM Al is valid proof let Al be QC-alphabet ; ::_thesis: VERUM Al is valid VERUM Al in TAUT Al by Th41; hence VERUM Al is valid by Lm13; ::_thesis: verum end; theorem :: CQC_THE1:61 for Al being QC-alphabet for p being Element of CQC-WFF Al holds (('not' p) => p) => p is valid proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al holds (('not' p) => p) => p is valid let p be Element of CQC-WFF Al; ::_thesis: (('not' p) => p) => p is valid (('not' p) => p) => p in TAUT Al proof TAUT Al is being_a_theory by Th15; hence (('not' p) => p) => p in TAUT Al by Def1; ::_thesis: verum end; hence (('not' p) => p) => p is valid by Lm13; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) is valid let p, q be Element of CQC-WFF Al; ::_thesis: p => (('not' p) => q) is valid p => (('not' p) => q) in TAUT Al proof TAUT Al is being_a_theory by Th15; hence p => (('not' p) => q) in TAUT Al by Def1; ::_thesis: verum end; hence p => (('not' p) => q) is valid by Lm13; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q, r being Element of CQC-WFF Al holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) is valid let p, q, r be Element of CQC-WFF Al; ::_thesis: (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) is valid (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al proof TAUT Al is being_a_theory by Th15; hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in TAUT Al by Def1; ::_thesis: verum end; hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) is valid by Lm13; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al holds (p '&' q) => (q '&' p) is valid let p, q be Element of CQC-WFF Al; ::_thesis: (p '&' q) => (q '&' p) is valid (p '&' q) => (q '&' p) in TAUT Al proof TAUT Al is being_a_theory by Th15; hence (p '&' q) => (q '&' p) in TAUT Al by Def1; ::_thesis: verum end; hence (p '&' q) => (q '&' p) is valid by Lm13; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al st p is valid & p => q is valid holds q is valid let p, q be Element of CQC-WFF Al; ::_thesis: ( p is valid & p => q is valid implies q is valid ) A1: TAUT Al is being_a_theory by Th15; assume ( p is valid & p => q is valid ) ; ::_thesis: q is valid then ( p in TAUT Al & p => q in TAUT Al ) by Lm13; then q in TAUT Al by Def1, A1; hence q is valid by Lm13; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al holds (All (x,p)) => p is valid let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al holds (All (x,p)) => p is valid let x be bound_QC-variable of Al; ::_thesis: (All (x,p)) => p is valid (All (x,p)) => p in TAUT Al by Th12; hence (All (x,p)) => p is valid by Lm13; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let p, q be Element of CQC-WFF Al; ::_thesis: 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 let x be bound_QC-variable of Al; ::_thesis: ( p => q is valid & not x in still_not-bound_in p implies p => (All (x,q)) is valid ) assume that A1: p => q is valid and A2: not x in still_not-bound_in p ; ::_thesis: p => (All (x,q)) is valid p => q in TAUT Al by A1, Lm13; then p => (All (x,q)) in TAUT Al by A2, Th13; hence p => (All (x,q)) is valid by Lm13; ::_thesis: verum end; 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 proof let Al be QC-alphabet ; ::_thesis: 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 let s be QC-formula of Al; ::_thesis: 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 let y, x be bound_QC-variable of Al; ::_thesis: ( s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x is valid implies s . y is valid ) assume that A1: ( s . y in CQC-WFF Al & not x in still_not-bound_in s ) and A2: s . x is valid ; ::_thesis: s . y is valid s . x in TAUT Al by A2, Lm13; then s . y in TAUT Al by A1, Th14; hence s . y is valid by Lm13; ::_thesis: verum end;