cqc_the1.miz
begin
reserve Al for
QC-alphabet;
reserve i,j,n,k,l for
Nat;
reserve a for
set;
reserve T,S,X,Y for
Subset of (
CQC-WFF Al);
reserve p,q,r,t,F,H,G for
Element of (
CQC-WFF Al);
reserve s for
QC-formula of Al;
reserve x,y for
bound_QC-variable of Al;
definition
let Al, T;
::
CQC_THE1:def1
attr T is
being_a_theory means (
VERUM Al)
in T & for p, q, r, s, x, y 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
::$Canceled
theorem ::
CQC_THE1:5
T is
being_a_theory & S is
being_a_theory implies (T
/\ S) is
being_a_theory
proof
assume that
A1: T is
being_a_theory and
A2: S is
being_a_theory;
(
VERUM Al)
in T & (
VERUM Al)
in S by
A1,
A2;
hence (
VERUM Al)
in (T
/\ S) by
XBOOLE_0:def 4;
let p, q, r, s, x, y;
(((
'not' p)
=> p)
=> p)
in T & (((
'not' p)
=> p)
=> p)
in S by
A1,
A2;
hence (((
'not' p)
=> p)
=> p)
in (T
/\ S) by
XBOOLE_0:def 4;
(p
=> ((
'not' p)
=> q))
in T & (p
=> ((
'not' p)
=> q))
in S by
A1,
A2;
hence (p
=> ((
'not' p)
=> q))
in (T
/\ S) by
XBOOLE_0:def 4;
((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in T & ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in S by
A1,
A2;
hence ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in (T
/\ S) by
XBOOLE_0:def 4;
((p
'&' q)
=> (q
'&' p))
in T & ((p
'&' q)
=> (q
'&' p))
in S by
A1,
A2;
hence ((p
'&' q)
=> (q
'&' p))
in (T
/\ S) by
XBOOLE_0:def 4;
A3: p
in T & (p
=> q)
in T implies q
in T by
A1;
p
in S & (p
=> q)
in S implies q
in S by
A2;
hence p
in (T
/\ S) & (p
=> q)
in (T
/\ S) implies q
in (T
/\ S) by
A3,
XBOOLE_0:def 4;
((
All (x,p))
=> p)
in T & ((
All (x,p))
=> p)
in S by
A1,
A2;
hence ((
All (x,p))
=> p)
in (T
/\ S) by
XBOOLE_0:def 4;
A4: (p
=> q)
in T & not x
in (
still_not-bound_in p) implies (p
=> (
All (x,q)))
in T by
A1;
(p
=> q)
in S & not x
in (
still_not-bound_in p) implies (p
=> (
All (x,q)))
in S by
A2;
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;
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;
(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;
hence thesis by
A5,
XBOOLE_0:def 4;
end;
definition
let Al, X;
::
CQC_THE1:def2
func
Cn (X) ->
Subset of (
CQC-WFF Al) means
:
Def2: t
in it iff for T st T is
being_a_theory & X
c= T holds t
in T;
existence
proof
defpred
P[
object] means for T st T is
being_a_theory & X
c= T holds $1
in T;
consider Y be
set such that
A1: for a be
object holds a
in Y iff a
in (
CQC-WFF Al) &
P[a] from
XBOOLE_0:sch 1;
Y
c= (
CQC-WFF Al) by
A1;
then
reconsider Z = Y as
Subset of (
CQC-WFF Al);
take Z;
thus thesis by
A1;
end;
uniqueness
proof
let Y,Z be
Subset of (
CQC-WFF Al) such that
A2: t
in Y iff for T st T is
being_a_theory & X
c= T holds t
in T and
A3: t
in Z iff for T st T is
being_a_theory & X
c= T holds t
in T;
for a be
object holds a
in Y iff a
in Z
proof
let a be
object;
thus a
in Y implies a
in Z
proof
assume
A4: a
in Y;
then
reconsider t = a as
Element of (
CQC-WFF Al);
for T st T is
being_a_theory & X
c= T holds t
in T by
A2,
A4;
hence thesis by
A3;
end;
thus a
in Z implies a
in Y
proof
assume
A5: a
in Z;
then
reconsider t = a as
Element of (
CQC-WFF Al);
for T st T is
being_a_theory & X
c= T holds t
in T by
A3,
A5;
hence thesis by
A2;
end;
end;
hence thesis by
TARSKI: 2;
end;
end
theorem ::
CQC_THE1:6
Th2: (
VERUM Al)
in (
Cn X)
proof
T is
being_a_theory & X
c= T implies (
VERUM Al)
in T;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:7
Th3: (((
'not' p)
=> p)
=> p)
in (
Cn X)
proof
T is
being_a_theory & X
c= T implies (((
'not' p)
=> p)
=> p)
in T;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:8
Th4: (p
=> ((
'not' p)
=> q))
in (
Cn X)
proof
T is
being_a_theory & X
c= T implies (p
=> ((
'not' p)
=> q))
in T;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:9
Th5: ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in (
Cn X)
proof
T is
being_a_theory & X
c= T implies ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in T;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:10
Th6: ((p
'&' q)
=> (q
'&' p))
in (
Cn X)
proof
T is
being_a_theory & X
c= T implies ((p
'&' q)
=> (q
'&' p))
in T;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:11
Th7: p
in (
Cn X) & (p
=> q)
in (
Cn X) implies q
in (
Cn X)
proof
assume
A1: p
in (
Cn X) & (p
=> q)
in (
Cn X);
T is
being_a_theory & X
c= T implies q
in T
proof
assume that
A2: T is
being_a_theory and
A3: X
c= T;
p
in T & (p
=> q)
in T by
A1,
A2,
A3,
Def2;
hence thesis by
A2;
end;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:12
Th8: ((
All (x,p))
=> p)
in (
Cn X)
proof
T is
being_a_theory & X
c= T implies ((
All (x,p))
=> p)
in T;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:13
Th9: (p
=> q)
in (
Cn X) & not x
in (
still_not-bound_in p) implies (p
=> (
All (x,q)))
in (
Cn X)
proof
assume that
A1: (p
=> q)
in (
Cn X) and
A2: not x
in (
still_not-bound_in p);
T is
being_a_theory & X
c= T implies (p
=> (
All (x,q)))
in T
proof
assume that
A3: T is
being_a_theory and
A4: X
c= T;
(p
=> q)
in T by
A1,
A3,
A4,
Def2;
hence thesis by
A2,
A3;
end;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:14
Th10: (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)
proof
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);
reconsider s1 = (s
. x) as
Element of (
CQC-WFF Al) by
A1;
reconsider q = (s
. y) as
Element of (
CQC-WFF Al) by
A2;
T is
being_a_theory & X
c= T implies q
in T
proof
assume that
A5: T is
being_a_theory and
A6: X
c= T;
s1
in T by
A4,
A5,
A6,
Def2;
hence thesis by
A3,
A5;
end;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:15
Th11: (
Cn X) is
being_a_theory by
Th2,
Th3,
Th4,
Th5,
Th6,
Th7,
Th8,
Th9,
Th10;
theorem ::
CQC_THE1:16
Th12: T is
being_a_theory & X
c= T implies (
Cn X)
c= T by
Def2;
theorem ::
CQC_THE1:17
Th13: X
c= (
Cn X)
proof
let a be
object;
assume
A1: a
in X;
then
reconsider t = a as
Element of (
CQC-WFF Al);
for T st T is
being_a_theory & X
c= T holds t
in T by
A1;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:18
Th14: X
c= Y implies (
Cn X)
c= (
Cn Y)
proof
assume
A1: X
c= Y;
thus (
Cn X)
c= (
Cn Y)
proof
let a be
object;
assume
A2: a
in (
Cn X);
then
reconsider t = a as
Element of (
CQC-WFF Al);
for T st T is
being_a_theory & Y
c= T holds t
in T
proof
let T such that
A3: T is
being_a_theory and
A4: Y
c= T;
X
c= T by
A1,
A4;
hence thesis by
A2,
A3,
Def2;
end;
hence thesis by
Def2;
end;
end;
Lm1: (
Cn (
Cn X))
c= (
Cn X)
proof
let a be
object;
assume
A1: a
in (
Cn (
Cn X));
then
reconsider t = a as
Element of (
CQC-WFF Al);
for T st T is
being_a_theory & X
c= T holds t
in T
proof
let T;
assume that
A2: T is
being_a_theory and
A3: X
c= T;
(
Cn X)
c= T by
A2,
A3,
Th12;
hence thesis by
A1,
A2,
Def2;
end;
hence thesis by
Def2;
end;
theorem ::
CQC_THE1:19
(
Cn (
Cn X))
= (
Cn X) by
Lm1,
Th13;
theorem ::
CQC_THE1:20
Th16: T is
being_a_theory iff (
Cn T)
= T
proof
thus T is
being_a_theory implies (
Cn T)
= T
proof
assume
A1: T is
being_a_theory;
A2: T
c= (
Cn T) by
Th13;
(
Cn T)
c= T by
A1,
Def2;
hence thesis by
A2;
end;
thus thesis by
Th11;
end;
definition
::
CQC_THE1:def3
func
Proof_Step_Kinds ->
set equals { k : k
<= 9 };
coherence ;
end
theorem ::
CQC_THE1:21
Th17:
0
in
Proof_Step_Kinds & ... & 9
in
Proof_Step_Kinds ;
registration
cluster
Proof_Step_Kinds -> non
empty;
coherence by
Th17;
end
theorem ::
CQC_THE1:22
Proof_Step_Kinds is
finite
proof
Proof_Step_Kinds
= (
succ (
Segm 9)) by
NAT_1: 54;
hence thesis;
end;
reserve f,g for
FinSequence of
[:(
CQC-WFF Al),
Proof_Step_Kinds :];
theorem ::
CQC_THE1:23
Th19: for n be
Nat holds 1
<= n & n
<= (
len f) implies ((f
. n)
`2 )
=
0 or ... or ((f
. n)
`2 )
= 9
proof
let n be
Nat;
assume
A1: 1
<= n & n
<= (
len f);
(
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 st k
= ((f
. n)
`2 ) & k
<= 9;
hence thesis;
end;
definition
let Al;
let PR be
FinSequence of
[:(
CQC-WFF Al),
Proof_Step_Kinds :], n be
Nat, X;
::
CQC_THE1:def4
pred PR,n
is_a_correct_step_wrt X means
:
Def4: ((PR
. n)
`1 )
in X if ((PR
. n)
`2 )
=
0 ,
((PR
. n)
`1 )
= (
VERUM Al) if ((PR
. n)
`2 )
= 1,
ex p st ((PR
. n)
`1 )
= (((
'not' p)
=> p)
=> p) if ((PR
. n)
`2 )
= 2,
ex p, q st ((PR
. n)
`1 )
= (p
=> ((
'not' p)
=> q)) if ((PR
. n)
`2 )
= 3,
ex p, q, r st ((PR
. n)
`1 )
= ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))) if ((PR
. n)
`2 )
= 4,
ex p, q st ((PR
. n)
`1 )
= ((p
'&' q)
=> (q
'&' p)) if ((PR
. n)
`2 )
= 5,
ex p, x st ((PR
. n)
`1 )
= ((
All (x,p))
=> p) if ((PR
. n)
`2 )
= 6,
ex i, j, p, q 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, p, q, x 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, x, y, s 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 ;
end
definition
let Al, X, f;
::
CQC_THE1:def5
pred f
is_a_proof_wrt X means f
<>
{} & for n st 1
<= n & n
<= (
len f) holds (f,n)
is_a_correct_step_wrt X;
end
theorem ::
CQC_THE1:24
f
is_a_proof_wrt X implies (
rng f)
<>
{} by
RELAT_1: 41;
theorem ::
CQC_THE1:25
Th21: f
is_a_proof_wrt X implies 1
<= (
len f)
proof
assume f
is_a_proof_wrt X;
then
A1: f
<>
{} ;
(
0
+ 1)
<= (
len f) by
A1,
NAT_1: 13;
hence thesis;
end;
theorem ::
CQC_THE1:26
f
is_a_proof_wrt X implies ((f
. 1)
`2 )
=
0 or ... or ((f
. 1)
`2 )
= 6
proof
assume
A1: f
is_a_proof_wrt X;
then
A2: 1
<= (
len f) by
Th21;
then
A3: (f,1)
is_a_correct_step_wrt X by
A1;
assume
A4: ((f
. 1)
`2 )
<>
0 & ... & ((f
. 1)
`2 )
<> 6;
((f
. 1)
`2 )
=
0 or ... or ((f
. 1)
`2 )
= 9 by
A2,
Th19;
per cases by
A4;
suppose ((f
. 1)
`2 )
= 7;
then ex i, j, p, q 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;
end;
suppose ((f
. 1)
`2 )
= 8;
then ex i, p, q, x 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;
end;
suppose ((f
. 1)
`2 )
= 9;
then ex i, x, y, s 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;
end;
end;
theorem ::
CQC_THE1:27
Th23: 1
<= n & n
<= (
len f) implies ((f,n)
is_a_correct_step_wrt X iff ((f
^ g),n)
is_a_correct_step_wrt X)
proof
assume that
A1: 1
<= n and
A2: n
<= (
len f);
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
proof
assume
A5: (f,n)
is_a_correct_step_wrt X;
(((f
^ g)
. n)
`2 )
=
0 or ... or (((f
^ g)
. n)
`2 )
= 9 by
A1,
A4,
Th19;
per cases ;
case (((f
^ g)
. n)
`2 )
=
0 ;
hence thesis by
A3,
A5,
Def4;
end;
case (((f
^ g)
. n)
`2 )
= 1;
hence thesis by
A3,
A5,
Def4;
end;
case (((f
^ g)
. n)
`2 )
= 2;
hence thesis by
A3,
A5,
Def4;
end;
case (((f
^ g)
. n)
`2 )
= 3;
hence thesis by
A3,
A5,
Def4;
end;
case (((f
^ g)
. n)
`2 )
= 4;
hence thesis by
A3,
A5,
Def4;
end;
case (((f
^ g)
. n)
`2 )
= 5;
hence thesis by
A3,
A5,
Def4;
end;
case (((f
^ g)
. n)
`2 )
= 6;
hence thesis by
A3,
A5,
Def4;
end;
case (((f
^ g)
. n)
`2 )
= 7;
then
consider i, j, r, t 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 thesis by
A3,
A6,
A7,
A8,
A9,
A10,
A17;
end;
case (((f
^ g)
. n)
`2 )
= 8;
then
consider i, r, t, x 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 thesis by
A3,
A18,
A19,
A20;
end;
case (((f
^ g)
. n)
`2 )
= 9;
then
consider i, x, y, s 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 thesis by
A3,
A21,
A22,
A23;
end;
end;
assume
A24: ((f
^ g),n)
is_a_correct_step_wrt X;
((f
. n)
`2 )
=
0 or ... or ((f
. n)
`2 )
= 9 by
A1,
A2,
Th19;
per cases ;
case ((f
. n)
`2 )
=
0 ;
hence thesis by
A3,
A24,
Def4;
end;
case ((f
. n)
`2 )
= 1;
hence thesis by
A3,
A24,
Def4;
end;
case ((f
. n)
`2 )
= 2;
hence thesis by
A3,
A24,
Def4;
end;
case ((f
. n)
`2 )
= 3;
hence thesis by
A3,
A24,
Def4;
end;
case ((f
. n)
`2 )
= 4;
hence thesis by
A3,
A24,
Def4;
end;
case ((f
. n)
`2 )
= 5;
hence thesis by
A3,
A24,
Def4;
end;
case ((f
. n)
`2 )
= 6;
hence thesis by
A3,
A24,
Def4;
end;
case ((f
. n)
`2 )
= 7;
then
consider i, j, r, t 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 thesis by
A3,
A25,
A26,
A27,
A28,
A29,
A36;
end;
case ((f
. n)
`2 )
= 8;
then
consider i, r, t, x 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 thesis by
A3,
A37,
A38,
A39;
end;
case ((f
. n)
`2 )
= 9;
then
consider i, x, y, s 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 thesis by
A3,
A40,
A41,
A42;
end;
end;
theorem ::
CQC_THE1:28
Th24: 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
proof
assume that
A1: 1
<= n and
A2: n
<= (
len g) and
A3: (g,n)
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 (n
+ (
len f))
<= (
len (f
^ g)) by
FINSEQ_1: 22;
then (((f
^ g)
. (n
+ (
len f)))
`2 )
=
0 or ... or (((f
^ g)
. (n
+ (
len f)))
`2 )
= 9 by
A1,
Th19,
NAT_1: 12;
per cases ;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
=
0 ;
hence thesis by
A3,
A4,
Def4;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 1;
hence thesis by
A3,
A4,
Def4;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 2;
hence thesis by
A3,
A4,
Def4;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 3;
hence thesis by
A3,
A4,
Def4;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 4;
hence thesis by
A3,
A4,
Def4;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 5;
hence thesis by
A3,
A4,
Def4;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 6;
hence thesis by
A3,
A4,
Def4;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 7;
then
consider i, j, r, t such that
A5: 1
<= i and
A6: i
< n and
A7: 1
<= j and
A8: j
< i and
A9: r
= ((g
. j)
`1 ) & t
= ((g
. n)
`1 ) & ((g
. i)
`1 )
= (r
=> t) by
A3,
A4,
Def4;
A10: 1
<= (i
+ (
len f)) & (i
+ (
len f))
< (n
+ (
len f)) by
A5,
A6,
NAT_1: 12,
XREAL_1: 6;
A11: 1
<= (j
+ (
len f)) & (j
+ (
len f))
< (i
+ (
len f)) by
A7,
A8,
NAT_1: 12,
XREAL_1: 6;
A12: i
<= (
len g) by
A2,
A6,
XXREAL_0: 2;
then
A13: j
<= (
len g) by
A8,
XXREAL_0: 2;
A14: i
in (
Seg (
len g)) by
A5,
A12,
FINSEQ_1: 1;
A15: j
in (
Seg (
len g)) by
A7,
A13,
FINSEQ_1: 1;
A16: i
in (
dom g) by
A14,
FINSEQ_1:def 3;
A17: j
in (
dom g) by
A15,
FINSEQ_1:def 3;
A18: (g
. i)
= ((f
^ g)
. (i
+ (
len f))) by
A16,
FINSEQ_1:def 7;
(g
. j)
= ((f
^ g)
. (j
+ (
len f))) by
A17,
FINSEQ_1:def 7;
hence thesis by
A4,
A9,
A10,
A11,
A18;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 8;
then
consider i, r, t, x such that
A19: 1
<= i and
A20: i
< n and
A21: ((g
. i)
`1 )
= (r
=> t) & not x
in (
still_not-bound_in r) & ((g
. n)
`1 )
= (r
=> (
All (x,t))) by
A3,
A4,
Def4;
A22: 1
<= ((
len f)
+ i) & ((
len f)
+ i)
< (n
+ (
len f)) by
A19,
A20,
NAT_1: 12,
XREAL_1: 6;
i
<= (
len g) by
A2,
A20,
XXREAL_0: 2;
then i
in (
Seg (
len g)) by
A19,
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 thesis by
A4,
A21,
A22;
end;
case (((f
^ g)
. (n
+ (
len f)))
`2 )
= 9;
then
consider i, x, y, s such that
A23: 1
<= i and
A24: i
< n and
A25: (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;
A26: 1
<= ((
len f)
+ i) & ((
len f)
+ i)
< (n
+ (
len f)) by
A23,
A24,
NAT_1: 12,
XREAL_1: 6;
i
<= (
len g) by
A2,
A24,
XXREAL_0: 2;
then i
in (
Seg (
len g)) by
A23,
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 thesis by
A4,
A25,
A26;
end;
end;
theorem ::
CQC_THE1:29
Th25: f
is_a_proof_wrt X & g
is_a_proof_wrt X implies (f
^ g)
is_a_proof_wrt X
proof
assume that
A1: f
is_a_proof_wrt X and
A2: g
is_a_proof_wrt X;
f
<>
{} by
A1;
hence (f
^ g)
<>
{} ;
let n such that
A3: 1
<= n and
A4: n
<= (
len (f
^ g));
now
per cases ;
suppose
A5: n
<= (
len f);
then (f,n)
is_a_correct_step_wrt X by
A1,
A3;
hence thesis by
A3,
A5,
Th23;
end;
suppose
A6: (
len f)
< n;
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;
hence thesis by
A8,
A9,
Th24;
end;
end;
hence thesis;
end;
theorem ::
CQC_THE1:30
f
is_a_proof_wrt X & X
c= Y implies f
is_a_proof_wrt Y
proof
assume that
A1: f
is_a_proof_wrt X and
A2: X
c= Y;
thus f
<>
{} by
A1;
let n;
assume
A3: 1
<= n & n
<= (
len f);
then
A4: (f,n)
is_a_correct_step_wrt X by
A1;
((f
. n)
`2 )
=
0 or ... or ((f
. n)
`2 )
= 9 by
A3,
Th19;
per cases ;
case ((f
. n)
`2 )
=
0 ;
then ((f
. n)
`1 )
in X by
A4,
Def4;
hence thesis by
A2;
end;
case ((f
. n)
`2 )
= 1;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 2;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 3;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 4;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 5;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 6;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 7;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 8;
hence thesis by
A4,
Def4;
end;
case ((f
. n)
`2 )
= 9;
hence thesis by
A4,
Def4;
end;
end;
theorem ::
CQC_THE1:31
Th27: f
is_a_proof_wrt X & 1
<= l & l
<= (
len f) implies ((f
. l)
`1 )
in (
Cn X)
proof
assume that
A1: f
is_a_proof_wrt X and
A2: 1
<= l & l
<= (
len f);
for n holds 1
<= n & n
<= (
len f) implies ((f
. n)
`1 )
in (
Cn X)
proof
defpred
P[
Nat] means 1
<= $1 & $1
<= (
len f) implies ((f
. $1)
`1 )
in (
Cn X);
A3: for n be
Nat st for k be
Nat st k
< n holds
P[k] holds
P[n]
proof
let n be
Nat;
assume
A4: for k be
Nat st k
< n holds
P[k];
assume that
A5: 1
<= n and
A6: n
<= (
len f);
A7: (f,n)
is_a_correct_step_wrt X by
A1,
A5,
A6;
now
((f
. n)
`2 )
=
0 or ... or ((f
. n)
`2 )
= 9 by
A5,
A6,
Th19;
per cases ;
suppose ((f
. n)
`2 )
=
0 ;
then
A8: ((f
. n)
`1 )
in X by
A7,
Def4;
X
c= (
Cn X) by
Th13;
hence thesis by
A8;
end;
suppose ((f
. n)
`2 )
= 1;
then ((f
. n)
`1 )
= (
VERUM Al) by
A7,
Def4;
hence thesis by
Th2;
end;
suppose ((f
. n)
`2 )
= 2;
then ex p st ((f
. n)
`1 )
= (((
'not' p)
=> p)
=> p) by
A7,
Def4;
hence thesis by
Th3;
end;
suppose ((f
. n)
`2 )
= 3;
then ex p, q st ((f
. n)
`1 )
= (p
=> ((
'not' p)
=> q)) by
A7,
Def4;
hence thesis by
Th4;
end;
suppose ((f
. n)
`2 )
= 4;
then ex p, q, r st ((f
. n)
`1 )
= ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))) by
A7,
Def4;
hence thesis by
Th5;
end;
suppose ((f
. n)
`2 )
= 5;
then ex p, q st ((f
. n)
`1 )
= ((p
'&' q)
=> (q
'&' p)) by
A7,
Def4;
hence thesis by
Th6;
end;
suppose ((f
. n)
`2 )
= 6;
then ex p, x st ((f
. n)
`1 )
= ((
All (x,p))
=> p) by
A7,
Def4;
hence thesis by
Th8;
end;
suppose ((f
. n)
`2 )
= 7;
then
consider i, j, p, q such that
A9: 1
<= i and
A10: i
< n and
A11: 1
<= j and
A12: j
< i and
A13: p
= ((f
. j)
`1 ) & q
= ((f
. n)
`1 ) & ((f
. i)
`1 )
= (p
=> q) by
A7,
Def4;
A14: j
< n by
A10,
A12,
XXREAL_0: 2;
A15: i
<= (
len f) by
A6,
A10,
XXREAL_0: 2;
then j
<= (
len f) by
A12,
XXREAL_0: 2;
then
A16: ((f
. j)
`1 )
in (
Cn X) by
A4,
A11,
A14;
((f
. i)
`1 )
in (
Cn X) by
A4,
A9,
A10,
A15;
hence thesis by
A13,
A16,
Th7;
end;
suppose ((f
. n)
`2 )
= 8;
then
consider i, p, q, x such that
A17: 1
<= i and
A18: i
< n and
A19: ((f
. i)
`1 )
= (p
=> q) & not x
in (
still_not-bound_in p) & ((f
. n)
`1 )
= (p
=> (
All (x,q))) by
A7,
Def4;
i
<= (
len f) by
A6,
A18,
XXREAL_0: 2;
hence thesis by
A4,
A17,
A18,
A19,
Th9;
end;
suppose ((f
. n)
`2 )
= 9;
then
consider i, x, y, s such that
A20: 1
<= i and
A21: i
< n and
A22: (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
A7,
Def4;
i
<= (
len f) by
A6,
A21,
XXREAL_0: 2;
hence thesis by
A4,
A20,
A21,
A22,
Th10;
end;
end;
hence thesis;
end;
for n be
Nat holds
P[n] from
NAT_1:sch 4(
A3);
hence thesis;
end;
hence thesis by
A2;
end;
definition
let Al, f;
assume
A1: f
<>
{} ;
::
CQC_THE1:def6
func
Effect (f) ->
Element of (
CQC-WFF Al) equals
:
Def6: ((f
. (
len f))
`1 );
coherence
proof
(
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 thesis by
A3,
MCART_1: 10;
end;
end
theorem ::
CQC_THE1:32
Th28: f
is_a_proof_wrt X implies (
Effect f)
in (
Cn X)
proof
assume
A1: f
is_a_proof_wrt X;
then
A2: 1
<= (
len f) by
Th21;
then
A3: ((f
. (
len f))
`1 )
in (
Cn X) by
A1,
Th27;
f
<>
{} by
A2;
hence thesis by
A3,
Def6;
end;
Lm2: for X holds { p : ex f st f
is_a_proof_wrt X & (
Effect f)
= p }
c= (
CQC-WFF Al)
proof
let X;
defpred
P[
set] means ex f st f
is_a_proof_wrt X & (
Effect f)
= $1;
thus { p :
P[p] }
c= (
CQC-WFF Al) from
FRAENKEL:sch 10;
end;
theorem ::
CQC_THE1:33
Th29: X
c= { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F }
proof
let a be
object;
assume
A1: a
in X;
then
reconsider p = a as
Element of (
CQC-WFF Al);
reconsider pp =
[p,
0 ] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set f =
<*pp*>;
A2: (
len f)
= 1 by
FINSEQ_1: 40;
A3: (f
. 1)
= pp by
FINSEQ_1: 40;
then ((f
. (
len f))
`1 )
= p by
A2;
then
A4: (
Effect f)
= p by
Def6;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt X
proof
assume 1
<= n & n
<= (
len f);
then
A5: n
= 1 by
A2,
XXREAL_0: 1;
A6: ((f
. 1)
`2 )
=
0 by
A3;
((f
. n)
`1 )
in X by
A1,
A3,
A5;
hence thesis by
A5,
A6,
Def4;
end;
then f
is_a_proof_wrt X;
hence thesis by
A4;
end;
Lm3: for X holds (
VERUM Al)
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F }
proof
let X;
reconsider pp =
[(
VERUM Al), 1] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set f =
<*pp*>;
A1: (
len f)
= 1 by
FINSEQ_1: 40;
A2: (f
. 1)
= pp by
FINSEQ_1: 40;
then ((f
. (
len f))
`1 )
= (
VERUM Al) by
A1;
then
A3: (
Effect f)
= (
VERUM Al) by
Def6;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt X
proof
assume 1
<= n & n
<= (
len f);
then
A4: n
= 1 by
A1,
XXREAL_0: 1;
A5: ((f
. 1)
`2 )
= 1 by
A2;
((f
. n)
`1 )
= (
VERUM Al) by
A2,
A4;
hence thesis by
A4,
A5,
Def4;
end;
then f
is_a_proof_wrt X;
hence thesis by
A3;
end;
Lm4: for X holds (((
'not' p)
=> p)
=> p)
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F }
proof
let X;
reconsider pp =
[(((
'not' p)
=> p)
=> p), 2] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set f =
<*pp*>;
A1: (
len f)
= 1 by
FINSEQ_1: 40;
A2: (f
. 1)
= pp by
FINSEQ_1: 40;
then ((f
. (
len f))
`1 )
= (((
'not' p)
=> p)
=> p) by
A1;
then
A3: (
Effect f)
= (((
'not' p)
=> p)
=> p) by
Def6;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt X
proof
assume 1
<= n & n
<= (
len f);
then
A4: n
= 1 by
A1,
XXREAL_0: 1;
A5: ((f
. 1)
`2 )
= 2 by
A2;
((f
. n)
`1 )
= (((
'not' p)
=> p)
=> p) by
A2,
A4;
hence thesis by
A4,
A5,
Def4;
end;
then f
is_a_proof_wrt X;
hence thesis by
A3;
end;
Lm5: for X holds (p
=> ((
'not' p)
=> q))
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F }
proof
let X;
reconsider pp =
[(p
=> ((
'not' p)
=> q)), 3] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set f =
<*pp*>;
A1: (
len f)
= 1 by
FINSEQ_1: 40;
A2: (f
. 1)
= pp by
FINSEQ_1: 40;
then ((f
. (
len f))
`1 )
= (p
=> ((
'not' p)
=> q)) by
A1;
then
A3: (
Effect f)
= (p
=> ((
'not' p)
=> q)) by
Def6;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt X
proof
assume 1
<= n & n
<= (
len f);
then
A4: n
= 1 by
A1,
XXREAL_0: 1;
A5: ((f
. 1)
`2 )
= 3 by
A2;
((f
. n)
`1 )
= (p
=> ((
'not' p)
=> q)) by
A2,
A4;
hence thesis by
A4,
A5,
Def4;
end;
then f
is_a_proof_wrt X;
hence thesis by
A3;
end;
Lm6: for X holds ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F }
proof
let X;
reconsider pp =
[((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))), 4] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set f =
<*pp*>;
A1: (
len f)
= 1 by
FINSEQ_1: 40;
A2: (f
. 1)
= pp by
FINSEQ_1: 40;
then ((f
. (
len f))
`1 )
= ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))) by
A1;
then
A3: (
Effect f)
= ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))) by
Def6;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt X
proof
assume 1
<= n & n
<= (
len f);
then
A4: n
= 1 by
A1,
XXREAL_0: 1;
A5: ((f
. 1)
`2 )
= 4 by
A2;
((f
. n)
`1 )
= ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))) by
A2,
A4;
hence thesis by
A4,
A5,
Def4;
end;
then f
is_a_proof_wrt X;
hence thesis by
A3;
end;
Lm7: for X holds ((p
'&' q)
=> (q
'&' p))
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F }
proof
let X;
reconsider pp =
[((p
'&' q)
=> (q
'&' p)), 5] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set f =
<*pp*>;
A1: (
len f)
= 1 by
FINSEQ_1: 40;
A2: (f
. 1)
= pp by
FINSEQ_1: 40;
then ((f
. (
len f))
`1 )
= ((p
'&' q)
=> (q
'&' p)) by
A1;
then
A3: (
Effect f)
= ((p
'&' q)
=> (q
'&' p)) by
Def6;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt X
proof
assume 1
<= n & n
<= (
len f);
then
A4: n
= 1 by
A1,
XXREAL_0: 1;
A5: ((f
. 1)
`2 )
= 5 by
A2;
((f
. n)
`1 )
= ((p
'&' q)
=> (q
'&' p)) by
A2,
A4;
hence thesis by
A4,
A5,
Def4;
end;
then f
is_a_proof_wrt X;
hence thesis by
A3;
end;
Lm8: for X holds p
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F } & (p
=> q)
in { G : ex f st f
is_a_proof_wrt X & (
Effect f)
= G } implies q
in { H : ex f st f
is_a_proof_wrt X & (
Effect f)
= H }
proof
let X;
assume that
A1: p
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F } and
A2: (p
=> q)
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F };
ex t st t
= p & ex f st f
is_a_proof_wrt X & (
Effect f)
= t by
A1;
then
consider f such that
A3: f
is_a_proof_wrt X and
A4: (
Effect f)
= p;
ex r st r
= (p
=> q) & ex f st f
is_a_proof_wrt X & (
Effect f)
= r by
A2;
then
consider g such that
A5: g
is_a_proof_wrt X and
A6: (
Effect g)
= (p
=> q);
reconsider qq =
[q, 7] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set h = ((f
^ g)
^
<*qq*>);
A7: (
len h)
= ((
len (f
^ g))
+ (
len
<*qq*>)) by
FINSEQ_1: 22
.= ((
len (f
^ g))
+ 1) by
FINSEQ_1: 40;
then
A8: (
len h)
= (((
len f)
+ (
len g))
+ 1) by
FINSEQ_1: 22;
(h
. (
len h))
= qq by
A7,
FINSEQ_1: 42;
then ((h
. (
len h))
`1 )
= q;
then
A9: (
Effect h)
= q by
Def6;
1
<= n & n
<= (
len h) implies (h,n)
is_a_correct_step_wrt X
proof
assume that
A10: 1
<= n and
A11: n
<= (
len h);
now
per cases by
A8,
A11,
NAT_1: 8;
suppose n
<= ((
len f)
+ (
len g));
then
A12: n
<= (
len (f
^ g)) by
FINSEQ_1: 22;
(f
^ g)
is_a_proof_wrt X by
A3,
A5,
Th25;
then ((f
^ g),n)
is_a_correct_step_wrt X by
A10,
A12;
hence thesis by
A10,
A12,
Th23;
end;
suppose
A13: n
= (
len h);
then (h
. n)
= qq by
A7,
FINSEQ_1: 42;
then
A14: ((h
. n)
`2 )
= 7 & ((h
. n)
`1 )
= q;
(
len f)
<>
0 by
A3;
then (
len f)
in (
Seg (
len f)) by
FINSEQ_1: 3;
then
A15: (
len f)
in (
dom f) by
FINSEQ_1:def 3;
h
= (f
^ (g
^
<*qq*>)) by
FINSEQ_1: 32;
then
A16: ((h
. (
len f))
`1 )
= ((f
. (
len f))
`1 ) by
A15,
FINSEQ_1:def 7
.= p by
A4,
A3,
Def6;
(
dom g)
= (
Seg (
len g)) & (
len g)
<>
0 by
A5,
FINSEQ_1:def 3;
then
A17: (
len g)
in (
dom g) by
FINSEQ_1: 3;
1
<= (
len f) & (
len f)
<= ((
len f)
+ (
len g)) by
A3,
Th21,
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
A18: ((h
. ((
len f)
+ (
len g)))
`1 )
= (((f
^ g)
. ((
len f)
+ (
len g)))
`1 ) by
FINSEQ_1:def 7
.= ((g
. (
len g))
`1 ) by
A17,
FINSEQ_1:def 7
.= (p
=> q) by
A6,
A5,
Def6;
1
<= (
len g) by
A5,
Th21;
then ((
len f)
+ 1)
<= ((
len f)
+ (
len g)) by
XREAL_1: 7;
then
A19: (
len f)
< ((
len f)
+ (
len g)) by
NAT_1: 13;
A20: 1
<= (
len f) & 1
<= ((
len f)
+ (
len g)) by
A3,
Th21,
NAT_1: 12;
((
len f)
+ (
len g))
< n by
A8,
A13,
NAT_1: 13;
hence thesis by
A14,
A16,
A18,
A19,
A20,
Def4;
end;
end;
hence thesis;
end;
then h
is_a_proof_wrt X;
hence thesis by
A9;
end;
Lm9: for X holds ((
All (x,p))
=> p)
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F }
proof
let X;
reconsider pp =
[((
All (x,p))
=> p), 6] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set f =
<*pp*>;
A1: (
len f)
= 1 by
FINSEQ_1: 40;
A2: (f
. 1)
= pp by
FINSEQ_1: 40;
then ((f
. (
len f))
`1 )
= ((
All (x,p))
=> p) by
A1;
then
A3: (
Effect f)
= ((
All (x,p))
=> p) by
Def6;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt X
proof
assume 1
<= n & n
<= (
len f);
then
A4: n
= 1 by
A1,
XXREAL_0: 1;
A5: ((f
. 1)
`2 )
= 6 by
A2;
((f
. n)
`1 )
= ((
All (x,p))
=> p) by
A2,
A4;
hence thesis by
A4,
A5,
Def4;
end;
then f
is_a_proof_wrt X;
hence thesis by
A3;
end;
Lm10: for X holds (p
=> q)
in { F : ex f 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 : ex f st f
is_a_proof_wrt X & (
Effect f)
= G }
proof
let X;
assume that
A1: (p
=> q)
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F } and
A2: not x
in (
still_not-bound_in p);
ex t st t
= (p
=> q) & ex f st f
is_a_proof_wrt X & (
Effect f)
= t by
A1;
then
consider f such that
A3: f
is_a_proof_wrt X and
A4: (
Effect f)
= (p
=> q);
reconsider qq =
[(p
=> (
All (x,q))), 8] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
Th17,
ZFMISC_1: 87;
set h = (f
^
<*qq*>);
A5: (
len h)
= ((
len f)
+ (
len
<*qq*>)) by
FINSEQ_1: 22
.= ((
len f)
+ 1) by
FINSEQ_1: 39;
1
<= n & n
<= (
len h) implies (h,n)
is_a_correct_step_wrt X
proof
assume that
A6: 1
<= n and
A7: n
<= (
len h);
now
per cases by
A5,
A7,
NAT_1: 8;
suppose
A8: n
<= (
len f);
then (f,n)
is_a_correct_step_wrt X by
A3,
A6;
hence thesis by
A6,
A8,
Th23;
end;
suppose
A9: n
= (
len h);
then (h
. n)
= qq by
A5,
FINSEQ_1: 42;
then
A10: ((h
. n)
`2 )
= 8 & ((h
. n)
`1 )
= (p
=> (
All (x,q)));
(
len f)
<>
0 by
A3;
then (
len f)
in (
Seg (
len f)) by
FINSEQ_1: 3;
then (
len f)
in (
dom f) by
FINSEQ_1:def 3;
then
A11: ((h
. (
len f))
`1 )
= ((f
. (
len f))
`1 ) by
FINSEQ_1:def 7
.= (p
=> q) by
A4,
A3,
Def6;
A12: 1
<= (
len f) by
A3,
Th21;
(
len f)
< n by
A5,
A9,
NAT_1: 13;
hence thesis by
A2,
A10,
A11,
A12,
Def4;
end;
end;
hence thesis;
end;
then
A13: h
is_a_proof_wrt X;
(
Effect h)
= ((h
. ((
len f)
+ 1))
`1 ) by
A5,
Def6
.= (qq
`1 ) by
FINSEQ_1: 42
.= (p
=> (
All (x,q)));
hence thesis by
A13;
end;
Lm11: for X holds (s
. x)
in (
CQC-WFF Al) & (s
. y)
in (
CQC-WFF Al) & not x
in (
still_not-bound_in s) & (s
. x)
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F } implies (s
. y)
in { G : ex f st f
is_a_proof_wrt X & (
Effect f)
= G }
proof
let X;
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 : ex f st f
is_a_proof_wrt X & (
Effect f)
= F };
ex t st t
= (s
. x) & ex f st f
is_a_proof_wrt X & (
Effect f)
= t by
A3;
then
consider f such that
A4: f
is_a_proof_wrt X and
A5: (
Effect f)
= (s
. x);
reconsider qq =
[(s
. y), 9] as
Element of
[:(
CQC-WFF Al),
Proof_Step_Kinds :] by
A1,
Th17,
ZFMISC_1: 87;
set h = (f
^
<*qq*>);
A6: (
len h)
= ((
len f)
+ (
len
<*qq*>)) by
FINSEQ_1: 22
.= ((
len f)
+ 1) by
FINSEQ_1: 39;
1
<= n & n
<= (
len h) implies (h,n)
is_a_correct_step_wrt X
proof
assume that
A7: 1
<= n and
A8: n
<= (
len h);
now
per cases by
A6,
A8,
NAT_1: 8;
suppose
A9: n
<= (
len f);
then (f,n)
is_a_correct_step_wrt X by
A4,
A7;
hence thesis by
A7,
A9,
Th23;
end;
suppose
A10: n
= (
len h);
then (h
. n)
= qq by
A6,
FINSEQ_1: 42;
then
A11: ((h
. n)
`2 )
= 9 & ((h
. n)
`1 )
= (s
. y);
(
len f)
<>
0 by
A4;
then (
len f)
in (
Seg (
len f)) by
FINSEQ_1: 3;
then (
len f)
in (
dom f) by
FINSEQ_1:def 3;
then
A12: ((h
. (
len f))
`1 )
= ((f
. (
len f))
`1 ) by
FINSEQ_1:def 7
.= (s
. x) by
A5,
A4,
Def6;
A13: 1
<= (
len f) by
A4,
Th21;
(
len f)
< n by
A6,
A10,
NAT_1: 13;
hence thesis by
A1,
A2,
A11,
A12,
A13,
Def4;
end;
end;
hence thesis;
end;
then
A14: h
is_a_proof_wrt X;
(
Effect h)
= ((h
. ((
len f)
+ 1))
`1 ) by
A6,
Def6
.= (qq
`1 ) by
FINSEQ_1: 42
.= (s
. y);
hence thesis by
A14;
end;
theorem ::
CQC_THE1:34
Th30: for X holds Y
= { p : ex f st f
is_a_proof_wrt X & (
Effect f)
= p } implies Y is
being_a_theory by
Lm3,
Lm4,
Lm5,
Lm6,
Lm7,
Lm8,
Lm9,
Lm10,
Lm11;
Lm12: for X holds { p : ex f st f
is_a_proof_wrt X & (
Effect f)
= p }
c= (
Cn X)
proof
let X;
let a be
object;
assume a
in { p : ex f st f
is_a_proof_wrt X & (
Effect f)
= p };
then ex q st q
= a & ex f st f
is_a_proof_wrt X & (
Effect f)
= q;
hence thesis by
Th28;
end;
theorem ::
CQC_THE1:35
Th31: for X holds { p : ex f st f
is_a_proof_wrt X & (
Effect f)
= p }
= (
Cn X)
proof
let X;
set PX = { p : ex f st f
is_a_proof_wrt X & (
Effect f)
= p };
A1: PX
c= (
Cn X) by
Lm12;
reconsider PX as
Subset of (
CQC-WFF Al) by
Lm2;
X
c= PX by
Th29;
then (
Cn X)
c= { p : ex f st f
is_a_proof_wrt X & (
Effect f)
= p } by
Th12,
Th30;
hence thesis by
A1;
end;
theorem ::
CQC_THE1:36
Th32: p
in (
Cn X) iff ex f st f
is_a_proof_wrt X & (
Effect f)
= p
proof
thus p
in (
Cn X) implies ex f st f
is_a_proof_wrt X & (
Effect f)
= p
proof
assume p
in (
Cn X);
then p
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F } by
Th31;
then ex F st F
= p & ex f st f
is_a_proof_wrt X & (
Effect f)
= F;
hence thesis;
end;
thus (ex f st f
is_a_proof_wrt X & (
Effect f)
= p) implies p
in (
Cn X)
proof
given f such that
A1: f
is_a_proof_wrt X & (
Effect f)
= p;
p
in { F : ex f st f
is_a_proof_wrt X & (
Effect f)
= F } by
A1;
hence thesis by
Th31;
end;
end;
theorem ::
CQC_THE1:37
p
in (
Cn X) implies ex Y st Y
c= X & Y is
finite & p
in (
Cn Y)
proof
assume p
in (
Cn X);
then
consider f such that
A1: f
is_a_proof_wrt X and
A2: (
Effect f)
= p by
Th32;
A3: f
<>
{} by
A1;
consider A be
set such that
A4: A is
finite and
A5: A
c= (
CQC-WFF Al) and
A6: (
rng f)
c=
[:A,
Proof_Step_Kinds :] by
FINSEQ_1:def 4,
FINSET_1: 14;
reconsider Z = A as
Subset of (
CQC-WFF Al) by
A5;
take Y = (Z
/\ X);
thus Y
c= X by
XBOOLE_1: 17;
thus Y is
finite by
A4;
1
<= n & n
<= (
len f) implies (f,n)
is_a_correct_step_wrt Y
proof
assume
A7: 1
<= n & n
<= (
len f);
then
A8: (f,n)
is_a_correct_step_wrt X by
A1;
((f
. n)
`2 )
=
0 or ... or ((f
. n)
`2 )
= 9 by
A7,
Th19;
per cases ;
case ((f
. n)
`2 )
=
0 ;
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 thesis by
A9,
XBOOLE_0:def 4;
end;
case ((f
. n)
`2 )
= 1;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 2;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 3;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 4;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 5;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 6;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 7;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 8;
hence thesis by
A8,
Def4;
end;
case ((f
. n)
`2 )
= 9;
hence thesis by
A8,
Def4;
end;
end;
then f
is_a_proof_wrt Y by
A3;
then p
in { q : ex f st f
is_a_proof_wrt Y & (
Effect f)
= q } by
A2;
hence thesis by
Th31;
end;
definition
let Al;
::
CQC_THE1:def7
func
TAUT (Al) ->
Subset of (
CQC-WFF Al) equals (
Cn (
{} (
CQC-WFF Al)));
correctness ;
end
theorem ::
CQC_THE1:38
Th34: T is
being_a_theory implies (
TAUT Al)
c= T
proof
assume
A1: T is
being_a_theory;
(
Cn (
{} (
CQC-WFF Al)))
c= (
Cn T) by
Th14,
XBOOLE_1: 2;
hence thesis by
A1,
Th16;
end;
theorem ::
CQC_THE1:39
(
TAUT Al)
c= (
Cn X) by
Th11,
Th34;
theorem ::
CQC_THE1:40
(
TAUT Al) is
being_a_theory by
Th11;
theorem ::
CQC_THE1:41
Th37: (
VERUM Al)
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
theorem ::
CQC_THE1:42
(((
'not' p)
=> p)
=> p)
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
theorem ::
CQC_THE1:43
(p
=> ((
'not' p)
=> q))
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
theorem ::
CQC_THE1:44
((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
theorem ::
CQC_THE1:45
((p
'&' q)
=> (q
'&' p))
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
theorem ::
CQC_THE1:46
p
in (
TAUT Al) & (p
=> q)
in (
TAUT Al) implies q
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
theorem ::
CQC_THE1:47
((
All (x,p))
=> p)
in (
TAUT Al) by
Th8;
theorem ::
CQC_THE1:48
(p
=> q)
in (
TAUT Al) & not x
in (
still_not-bound_in p) implies (p
=> (
All (x,q)))
in (
TAUT Al) by
Th9;
theorem ::
CQC_THE1:49
(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) implies (s
. y)
in (
TAUT Al) by
Th10;
definition
let Al, X, s;
::
CQC_THE1:def8
pred X
|- s means
:
Def8: s
in (
Cn X);
end
theorem ::
CQC_THE1:50
X
|- (
VERUM Al) by
Th2;
theorem ::
CQC_THE1:51
X
|- (((
'not' p)
=> p)
=> p) by
Th3;
theorem ::
CQC_THE1:52
X
|- (p
=> ((
'not' p)
=> q)) by
Th4;
theorem ::
CQC_THE1:53
X
|- ((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))) by
Th5;
theorem ::
CQC_THE1:54
X
|- ((p
'&' q)
=> (q
'&' p)) by
Th6;
theorem ::
CQC_THE1:55
X
|- p & X
|- (p
=> q) implies X
|- q by
Th7;
theorem ::
CQC_THE1:56
X
|- ((
All (x,p))
=> p) by
Th8;
theorem ::
CQC_THE1:57
X
|- (p
=> q) & not x
in (
still_not-bound_in p) implies X
|- (p
=> (
All (x,q))) by
Th9;
theorem ::
CQC_THE1:58
(s
. y)
in (
CQC-WFF Al) & not x
in (
still_not-bound_in s) & X
|- (s
. x) implies X
|- (s
. y) by
Th10;
definition
let Al, s;
::
CQC_THE1:def9
attr s is
valid means (
{} (
CQC-WFF Al))
|- s;
end
definition
let Al, s;
:: original:
valid
redefine
::
CQC_THE1:def10
attr s is
valid means s
in (
TAUT Al);
compatibility by
Def8;
end
theorem ::
CQC_THE1:59
p is
valid implies X
|- p
proof
assume p is
valid;
then
A1: p
in (
TAUT Al);
(
TAUT Al)
c= (
Cn X) by
Th11,
Th34;
hence thesis by
A1;
end;
theorem ::
CQC_THE1:60
(
VERUM Al) is
valid by
Th37;
theorem ::
CQC_THE1:61
(((
'not' p)
=> p)
=> p) is
valid
proof
(((
'not' p)
=> p)
=> p)
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
hence thesis;
end;
theorem ::
CQC_THE1:62
(p
=> ((
'not' p)
=> q)) is
valid
proof
(p
=> ((
'not' p)
=> q))
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
hence thesis;
end;
theorem ::
CQC_THE1:63
((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r)))) is
valid
proof
((p
=> q)
=> ((
'not' (q
'&' r))
=> (
'not' (p
'&' r))))
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
hence thesis;
end;
theorem ::
CQC_THE1:64
((p
'&' q)
=> (q
'&' p)) is
valid
proof
((p
'&' q)
=> (q
'&' p))
in (
TAUT Al)
proof
(
TAUT Al) is
being_a_theory by
Th11;
hence thesis;
end;
hence thesis;
end;
theorem ::
CQC_THE1:65
p is
valid & (p
=> q) is
valid implies q is
valid
proof
A1: (
TAUT Al) is
being_a_theory by
Th11;
assume p is
valid & (p
=> q) is
valid;
then p
in (
TAUT Al) & (p
=> q)
in (
TAUT Al);
then q
in (
TAUT Al) by
A1;
hence thesis;
end;
theorem ::
CQC_THE1:66
((
All (x,p))
=> p) is
valid by
Th8;
theorem ::
CQC_THE1:67
(p
=> q) is
valid & not x
in (
still_not-bound_in p) implies (p
=> (
All (x,q))) is
valid by
Th9;
theorem ::
CQC_THE1:68
(s
. y)
in (
CQC-WFF Al) & not x
in (
still_not-bound_in s) & (s
. x) is
valid implies (s
. y) is
valid by
Th10;