:: 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;