modal_1.miz
begin
reserve x,y,x1,x2,z for
set,
n,m,k for
Nat,
t1 for
DecoratedTree of
[:
NAT ,
NAT :],
w,s,t,u for
FinSequence of
NAT ,
D for non
empty
set;
Lm1:
{}
is_a_proper_prefix_of
<*m*> by
XBOOLE_1: 2;
definition
let Z be
Tree;
::
MODAL_1:def1
func
Root Z ->
Element of Z equals
{} ;
coherence by
TREES_1: 22;
end
definition
let D;
let T be
DecoratedTree of D;
::
MODAL_1:def2
func
Root T ->
Element of D equals (T
. (
Root (
dom T)));
coherence ;
end
theorem ::
MODAL_1:1
Th1: n
<> m implies not (
<*n*>,(
<*m*>
^ s))
are_c=-comparable
proof
assume
A1: n
<> m;
assume
A2: (
<*n*>,(
<*m*>
^ s))
are_c=-comparable ;
per cases by
A2;
suppose
<*n*>
is_a_prefix_of (
<*m*>
^ s);
then
A3: ex a be
FinSequence st (
<*m*>
^ s)
= (
<*n*>
^ a) by
TREES_1: 1;
m
= ((
<*m*>
^ s)
. 1) by
FINSEQ_1: 41
.= n by
A3,
FINSEQ_1: 41;
hence contradiction by
A1;
end;
suppose (
<*m*>
^ s)
is_a_prefix_of
<*n*>;
then
consider a be
FinSequence such that
A4:
<*n*>
= ((
<*m*>
^ s)
^ a) by
TREES_1: 1;
n
= (((
<*m*>
^ s)
^ a)
. 1) by
A4,
FINSEQ_1: 40
.= ((
<*m*>
^ (s
^ a))
. 1) by
FINSEQ_1: 32
.= m by
FINSEQ_1: 41;
hence contradiction by
A1;
end;
end;
::$Canceled
theorem ::
MODAL_1:3
Th2: n
<> m implies not
<*n*>
is_a_proper_prefix_of (
<*m*>
^ s)
proof
assume
A1: n
<> m;
assume
<*n*>
is_a_proper_prefix_of (
<*m*>
^ s);
then
<*n*>
is_a_prefix_of (
<*m*>
^ s);
then
A2: ex a be
FinSequence st (
<*m*>
^ s)
= (
<*n*>
^ a) by
TREES_1: 1;
m
= ((
<*m*>
^ s)
. 1) by
FINSEQ_1: 41
.= n by
A2,
FINSEQ_1: 41;
hence contradiction by
A1;
end;
::$Canceled
theorem ::
MODAL_1:8
Th3: for Z be
Tree, n, m st n
<= m &
<*m*>
in Z holds
<*n*>
in Z
proof
reconsider s =
{} as
FinSequence of
NAT by
TREES_1: 22;
let Z be
Tree, n, m;
assume that
A1: n
<= m and
A2:
<*m*>
in Z;
(
{}
^
<*m*>)
in Z by
A2,
FINSEQ_1: 34;
then (s
^
<*n*>)
in Z by
A1,
TREES_1:def 3;
hence thesis by
FINSEQ_1: 34;
end;
theorem ::
MODAL_1:9
(w
^ t)
is_a_proper_prefix_of (w
^ s) implies t
is_a_proper_prefix_of s by
TREES_1: 49;
theorem ::
MODAL_1:10
Th5: t1
in (
PFuncs ((
NAT
* ),
[:
NAT ,
NAT :]))
proof
(
rng t1)
c=
[:
NAT ,
NAT :] & (
dom t1)
c= (
NAT
* ) by
TREES_1:def 3;
hence thesis by
PARTFUN1:def 3;
end;
theorem ::
MODAL_1:11
Th6: for Z,Z1,Z2 be
Tree, z be
Element of Z st (Z
with-replacement (z,Z1))
= (Z
with-replacement (z,Z2)) holds Z1
= Z2
proof
let Z,Z1,Z2 be
Tree, z be
Element of Z;
assume
A1: (Z
with-replacement (z,Z1))
= (Z
with-replacement (z,Z2));
now
let s;
thus s
in Z1 implies s
in Z2
proof
assume
A2: s
in Z1;
per cases ;
suppose s
=
{} ;
hence thesis by
TREES_1: 22;
end;
suppose s
<>
{} ;
then
A3: z
is_a_proper_prefix_of (z
^ s) by
TREES_1: 10;
(z
^ s)
in (Z
with-replacement (z,Z2)) by
A1,
A2,
TREES_1:def 9;
then ex w st w
in Z2 & (z
^ s)
= (z
^ w) by
A3,
TREES_1:def 9;
hence thesis by
FINSEQ_1: 33;
end;
end;
assume
A4: s
in Z2;
per cases ;
suppose s
=
{} ;
hence s
in Z1 by
TREES_1: 22;
end;
suppose s
<>
{} ;
then
A5: z
is_a_proper_prefix_of (z
^ s) by
TREES_1: 10;
(z
^ s)
in (Z
with-replacement (z,Z1)) by
A1,
A4,
TREES_1:def 9;
then ex w st w
in Z1 & (z
^ s)
= (z
^ w) by
A5,
TREES_1:def 9;
hence s
in Z1 by
FINSEQ_1: 33;
end;
end;
hence thesis by
TREES_2:def 1;
end;
theorem ::
MODAL_1:12
Th7: for Z,Z1,Z2 be
DecoratedTree of D, z be
Element of (
dom Z) st (Z
with-replacement (z,Z1))
= (Z
with-replacement (z,Z2)) holds Z1
= Z2
proof
let Z,Z1,Z2 be
DecoratedTree of D, z be
Element of (
dom Z);
assume
A1: (Z
with-replacement (z,Z1))
= (Z
with-replacement (z,Z2));
set T2 = (Z
with-replacement (z,Z2));
set T1 = (Z
with-replacement (z,Z1));
A2: (
dom T1)
= ((
dom Z)
with-replacement (z,(
dom Z1))) by
TREES_2:def 11;
then
A3: ((
dom Z)
with-replacement (z,(
dom Z1)))
= ((
dom Z)
with-replacement (z,(
dom Z2))) by
A1,
TREES_2:def 11;
A4: for s st s
in (
dom Z1) holds (Z1
. s)
= (Z2
. s)
proof
let s;
A5: z
is_a_prefix_of (z
^ s) by
TREES_1: 1;
assume
A6: s
in (
dom Z1);
then (z
^ s)
in ((
dom Z)
with-replacement (z,(
dom Z1))) by
TREES_1:def 9;
then
A7: ex u st u
in (
dom Z1) & (z
^ s)
= (z
^ u) & (T1
. (z
^ s))
= (Z1
. u) by
A5,
TREES_2:def 11;
(z
^ s)
in ((
dom Z)
with-replacement (z,(
dom Z2))) by
A3,
A6,
TREES_1:def 9;
then
consider w such that w
in (
dom Z2) and
A8: (z
^ s)
= (z
^ w) and
A9: (T2
. (z
^ s))
= (Z2
. w) by
A5,
TREES_2:def 11;
s
= w by
A8,
FINSEQ_1: 33;
hence thesis by
A1,
A9,
A7,
FINSEQ_1: 33;
end;
(
dom T2)
= ((
dom Z)
with-replacement (z,(
dom Z2))) by
TREES_2:def 11;
hence thesis by
A1,
A2,
A4,
Th6,
TREES_2: 31;
end;
theorem ::
MODAL_1:13
Th8: for Z1,Z2 be
Tree, p be
FinSequence of
NAT st p
in Z1 holds for v be
Element of (Z1
with-replacement (p,Z2)), w be
Element of Z1 st v
= w & w
is_a_proper_prefix_of p holds (
succ v)
= (
succ w)
proof
let Z1,Z2 be
Tree, p be
FinSequence of
NAT ;
assume
A1: p
in Z1;
set Z = (Z1
with-replacement (p,Z2));
let v be
Element of Z, w be
Element of Z1;
assume that
A2: v
= w and
A3: w
is_a_proper_prefix_of p;
w
is_a_prefix_of p by
A3;
then
consider r be
FinSequence such that
A4: p
= (w
^ r) by
TREES_1: 1;
now
let n be
Nat;
assume
A5: n
in (
dom r);
then ((
len w)
+ n)
in (
dom p) by
A4,
FINSEQ_1: 28;
then
A6: (p
. ((
len w)
+ n))
in (
rng p) by
FUNCT_1:def 3;
(p
. ((
len w)
+ n))
= (r
. n) by
A4,
A5,
FINSEQ_1:def 7;
hence (r
. n)
in
NAT by
A6;
end;
then
reconsider r as
FinSequence of
NAT by
FINSEQ_2: 12;
A7: r
<>
{} by
A3,
A4,
FINSEQ_1: 34;
now
let x be
object;
thus x
in (
succ v) implies x
in (
succ w)
proof
assume x
in (
succ v);
then x
in { (v
^
<*n*>) : (v
^
<*n*>)
in Z } by
TREES_2:def 5;
then
consider n such that
A8: x
= (v
^
<*n*>) and
A9: (v
^
<*n*>)
in Z;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
x
= (v
^
<*n*>) by
A8;
then
reconsider x9 = x as
FinSequence of
NAT ;
now
per cases by
A1,
A8,
A9,
TREES_1:def 9;
suppose x9
in Z1 & not p
is_a_proper_prefix_of x9;
then x
in { (w
^
<*m*>) : (w
^
<*m*>)
in Z1 } by
A2,
A8;
hence thesis by
TREES_2:def 5;
end;
suppose ex r be
FinSequence of
NAT st r
in Z2 & x9
= (p
^ r);
then
consider s such that s
in Z2 and
A10: (v
^
<*n*>)
= (p
^ s) by
A8;
(w
^
<*n*>)
= (w
^ (r
^ s)) by
A2,
A4,
A10,
FINSEQ_1: 32;
then
A11:
<*n*>
= (r
^ s) by
FINSEQ_1: 33;
s
=
{}
proof
assume not thesis;
then (
len s)
>
0 by
NAT_1: 3;
then
A12: (
0
+ 1)
<= (
len s) by
NAT_1: 13;
(
len r)
>
0 by
A7,
NAT_1: 3;
then (
0
+ 1)
<= (
len r) by
NAT_1: 13;
then (1
+ 1)
<= ((
len r)
+ (
len s)) by
A12,
XREAL_1: 7;
then 2
<= (
len
<*n*>) by
A11,
FINSEQ_1: 22;
then 2
<= 1 by
FINSEQ_1: 39;
hence contradiction;
end;
then
<*n*>
= r by
A11,
FINSEQ_1: 34;
then x
in { (w
^
<*m*>) : (w
^
<*m*>)
in Z1 } by
A1,
A2,
A4,
A8;
hence thesis by
TREES_2:def 5;
end;
end;
hence thesis;
end;
assume x
in (
succ w);
then x
in { (w
^
<*n*>) : (w
^
<*n*>)
in Z1 } by
TREES_2:def 5;
then
consider n such that
A13: x
= (w
^
<*n*>) and
A14: (w
^
<*n*>)
in Z1;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
now
assume
A15: not (v
^
<*n*>)
in Z;
now
per cases by
A1,
A15,
TREES_1:def 9;
suppose not (v
^
<*n*>)
in Z1;
hence contradiction by
A2,
A14;
end;
suppose p
is_a_proper_prefix_of (v
^
<*n*>);
then r
is_a_proper_prefix_of
<*n*> by
A2,
A4,
TREES_1: 49;
then r
in (
ProperPrefixes
<*n*>) by
TREES_1: 12;
then r
in
{
{} } by
TREES_1: 16;
hence contradiction by
A7,
TARSKI:def 1;
end;
end;
hence contradiction;
end;
then x
in { (v
^
<*m*>) : (v
^
<*m*>)
in Z } by
A2,
A13;
hence x
in (
succ v) by
TREES_2:def 5;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
MODAL_1:14
Th9: for Z1,Z2 be
Tree, p be
FinSequence of
NAT st p
in Z1 holds for v be
Element of (Z1
with-replacement (p,Z2)), w be
Element of Z1 st v
= w & not (p,w)
are_c=-comparable holds (
succ v)
= (
succ w)
proof
let Z1,Z2 be
Tree, p be
FinSequence of
NAT ;
assume
A1: p
in Z1;
set Z = (Z1
with-replacement (p,Z2));
let v be
Element of Z, w be
Element of Z1;
assume that
A2: v
= w and
A3: not (p,w)
are_c=-comparable ;
A4: not p
is_a_prefix_of w by
A3;
now
let x be
object;
thus x
in (
succ v) implies x
in (
succ w)
proof
assume x
in (
succ v);
then x
in { (v
^
<*n*>) : (v
^
<*n*>)
in Z } by
TREES_2:def 5;
then
consider n such that
A5: x
= (v
^
<*n*>) and
A6: (v
^
<*n*>)
in Z;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
x
= (v
^
<*n*>) by
A5;
then
reconsider x9 = x as
FinSequence of
NAT ;
(v
^
<*n*>)
in Z1
proof
assume
A7: not (v
^
<*n*>)
in Z1;
then ex t st t
in Z2 & x9
= (p
^ t) by
A1,
A5,
A6,
TREES_1:def 9;
then
A8: p
is_a_prefix_of (v
^
<*n*>) by
A5,
TREES_1: 1;
per cases by
A8;
suppose p
is_a_proper_prefix_of (v
^
<*n*>);
hence contradiction by
A2,
A4,
TREES_1: 9;
end;
suppose p
= (v
^
<*n*>);
hence contradiction by
A1,
A7;
end;
end;
then x
in { (w
^
<*m*>) : (w
^
<*m*>)
in Z1 } by
A2,
A5;
hence thesis by
TREES_2:def 5;
end;
assume x
in (
succ w);
then x
in { (w
^
<*n*>) : (w
^
<*n*>)
in Z1 } by
TREES_2:def 5;
then
consider n such that
A9: x
= (w
^
<*n*>) and
A10: (w
^
<*n*>)
in Z1;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
not p
is_a_proper_prefix_of (w
^
<*n*>) by
A4,
TREES_1: 9;
then (v
^
<*n*>)
in Z by
A1,
A2,
A10,
TREES_1:def 9;
then x
in { (v
^
<*m*>) : (v
^
<*m*>)
in Z } by
A2,
A9;
hence x
in (
succ v) by
TREES_2:def 5;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
MODAL_1:15
for Z1,Z2 be
Tree, p be
FinSequence of
NAT st p
in Z1 holds for v be
Element of (Z1
with-replacement (p,Z2)), w be
Element of Z2 st v
= (p
^ w) holds ((
succ v),(
succ w))
are_equipotent by
TREES_2: 37;
theorem ::
MODAL_1:16
Th11: for Z1 be
Tree, p be
FinSequence of
NAT st p
in Z1 holds for v be
Element of Z1, w be
Element of (Z1
| p) st v
= (p
^ w) holds ((
succ v),(
succ w))
are_equipotent
proof
let Z1 be
Tree, p be
FinSequence of
NAT such that
A1: p
in Z1;
set T = (Z1
| p);
let t be
Element of Z1, t2 be
Element of (Z1
| p) such that
A2: t
= (p
^ t2);
A3: for n holds (t
^
<*n*>)
in Z1 iff (t2
^
<*n*>)
in T
proof
let n;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
A4: (t
^
<*nn*>)
= (p
^ (t2
^
<*nn*>)) by
A2,
FINSEQ_1: 32;
hence (t
^
<*n*>)
in Z1 implies (t2
^
<*n*>)
in T by
A1,
TREES_1:def 6;
assume (t2
^
<*n*>)
in T;
hence thesis by
A1,
A4,
TREES_1:def 6;
end;
defpred
P[
object,
object] means for n st $1
= (t
^
<*n*>) holds $2
= (t2
^
<*n*>);
A5: for x be
object st x
in (
succ t) holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in (
succ t);
then x
in { (t
^
<*n*>) : (t
^
<*n*>)
in Z1 } by
TREES_2:def 5;
then
consider n such that
A6: x
= (t
^
<*n*>) and (t
^
<*n*>)
in Z1;
take (t2
^
<*n*>);
let m;
assume x
= (t
^
<*m*>);
hence thesis by
A6,
FINSEQ_1: 33;
end;
consider f be
Function such that
A7: (
dom f)
= (
succ t) & for x be
object st x
in (
succ t) holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A5);
now
let x be
object;
thus x
in (
rng f) implies x
in (
succ t2)
proof
assume x
in (
rng f);
then
consider y be
object such that
A8: y
in (
dom f) and
A9: x
= (f
. y) by
FUNCT_1:def 3;
y
in { (t
^
<*n*>) : (t
^
<*n*>)
in Z1 } by
A7,
A8,
TREES_2:def 5;
then
consider n such that
A10: y
= (t
^
<*n*>) and
A11: (t
^
<*n*>)
in Z1;
A12: (t2
^
<*n*>)
in T by
A3,
A11;
x
= (t2
^
<*n*>) by
A7,
A8,
A9,
A10;
then x
in { (t2
^
<*m*>) : (t2
^
<*m*>)
in T } by
A12;
hence thesis by
TREES_2:def 5;
end;
assume x
in (
succ t2);
then x
in { (t2
^
<*n*>) : (t2
^
<*n*>)
in T } by
TREES_2:def 5;
then
consider n such that
A13: x
= (t2
^
<*n*>) and
A14: (t2
^
<*n*>)
in T;
(t
^
<*n*>)
in Z1 by
A3,
A14;
then (t
^
<*n*>)
in { (t
^
<*m*>) : (t
^
<*m*>)
in Z1 };
then
A15: (t
^
<*n*>)
in (
dom f) by
A7,
TREES_2:def 5;
then (f
. (t
^
<*n*>))
= x by
A7,
A13;
hence x
in (
rng f) by
A15,
FUNCT_1:def 3;
end;
then
A16: (
rng f)
= (
succ t2) by
TARSKI: 2;
now
let x1,x2 be
object;
assume that
A17: x1
in (
dom f) and
A18: x2
in (
dom f) and
A19: (f
. x1)
= (f
. x2);
x2
in { (t
^
<*n*>) : (t
^
<*n*>)
in Z1 } by
A7,
A18,
TREES_2:def 5;
then
consider k such that
A20: x2
= (t
^
<*k*>) and (t
^
<*k*>)
in Z1;
x1
in { (t
^
<*n*>) : (t
^
<*n*>)
in Z1 } by
A7,
A17,
TREES_2:def 5;
then
consider m such that
A21: x1
= (t
^
<*m*>) and (t
^
<*m*>)
in Z1;
(t2
^
<*m*>)
= (f
. x1) by
A7,
A17,
A21
.= (t2
^
<*k*>) by
A7,
A18,
A19,
A20;
hence x1
= x2 by
A21,
A20,
FINSEQ_1: 33;
end;
then f is
one-to-one by
FUNCT_1:def 4;
hence thesis by
A7,
A16,
WELLORD2:def 4;
end;
theorem ::
MODAL_1:17
Th12: for Z be
finite
Tree st (
branchdeg (
Root Z))
=
0 holds (
card Z)
= 1 & Z
=
{
{} }
proof
let Z be
finite
Tree;
assume (
branchdeg (
Root Z))
=
0 ;
then
0
= (
card (
succ (
Root Z))) by
TREES_2:def 12;
then
A1: (
succ (
Root Z))
=
{} ;
now
let x be
object;
thus x
in Z implies x
in
{(
Root Z)}
proof
assume x
in Z;
then
reconsider z = x as
Element of Z;
assume not thesis;
then z
<> (
Root Z) by
TARSKI:def 1;
then
consider w be
FinSequence of
NAT , n be
Element of
NAT such that
A2: z
= (
<*n*>
^ w) by
FINSEQ_2: 130;
<*n*>
is_a_prefix_of z by
A2,
TREES_1: 1;
then
<*n*>
in Z by
TREES_1: 20;
then (
{}
^
<*n*>)
in Z by
FINSEQ_1: 34;
hence contradiction by
A1,
TREES_2: 12;
end;
assume x
in
{(
Root Z)};
then
reconsider x9 = x as
Element of Z;
x9
in Z;
hence x
in Z;
end;
then Z
=
{(
Root Z)} by
TARSKI: 2;
hence thesis by
CARD_2: 42;
end;
theorem ::
MODAL_1:18
Th13: for Z be
finite
Tree st (
branchdeg (
Root Z))
= 1 holds (
succ (
Root Z))
=
{
<*
0 *>}
proof
let Z be
finite
Tree;
assume (
branchdeg (
Root Z))
= 1;
then (
card (
succ (
Root Z)))
= 1 by
TREES_2:def 12;
then
consider x be
object such that
A1: (
succ (
Root Z))
=
{x} by
CARD_2: 42;
A2: x
in (
succ (
Root Z)) by
A1,
TARSKI:def 1;
then
reconsider x9 = x as
Element of Z;
x9
in { ((
Root Z)
^
<*n*>) : ((
Root Z)
^
<*n*>)
in Z } by
A2,
TREES_2:def 5;
then
consider m such that
A3: x9
= ((
Root Z)
^
<*m*>) and
A4: ((
Root Z)
^
<*m*>)
in Z;
A5: x9
=
<*m*> by
A3,
FINSEQ_1: 34;
now
A6:
<*
0 *>
= ((
Root Z)
^
<*
0 *>) by
FINSEQ_1: 34;
<*m*>
in Z by
A4,
FINSEQ_1: 34;
then
<*
0 *>
in Z by
Th3,
NAT_1: 2;
then ((
Root Z)
^
<*
0 *>)
in (
succ (
Root Z)) by
A6,
TREES_2: 12;
then
A7:
<*
0 *>
= x by
A1,
A6,
TARSKI:def 1;
assume m
<>
0 ;
hence contradiction by
A5,
A7,
TREES_1: 3;
end;
hence thesis by
A1,
A3,
FINSEQ_1: 34;
end;
theorem ::
MODAL_1:19
Th14: for Z be
finite
Tree st (
branchdeg (
Root Z))
= 2 holds (
succ (
Root Z))
=
{
<*
0 *>,
<*1*>}
proof
let Z be
finite
Tree;
assume (
branchdeg (
Root Z))
= 2;
then (
card (
succ (
Root Z)))
= 2 by
TREES_2:def 12;
then
consider x,y be
object such that
A1: x
<> y and
A2: (
succ (
Root Z))
=
{x, y} by
CARD_2: 60;
A3: x
in (
succ (
Root Z)) by
A2,
TARSKI:def 2;
then
reconsider x9 = x as
Element of Z;
x9
in { ((
Root Z)
^
<*n*>) : ((
Root Z)
^
<*n*>)
in Z } by
A3,
TREES_2:def 5;
then
consider m such that
A4: x9
= ((
Root Z)
^
<*m*>) and ((
Root Z)
^
<*m*>)
in Z;
A5: x9
=
<*m*> by
A4,
FINSEQ_1: 34;
A6: y
in (
succ (
Root Z)) by
A2,
TARSKI:def 2;
then
reconsider y9 = y as
Element of Z;
y9
in { ((
Root Z)
^
<*n*>) : ((
Root Z)
^
<*n*>)
in Z } by
A6,
TREES_2:def 5;
then
consider k such that
A7: y9
= ((
Root Z)
^
<*k*>) and ((
Root Z)
^
<*k*>)
in Z;
A8: y9
=
<*k*> by
A7,
FINSEQ_1: 34;
per cases ;
suppose
A9: m
=
0 ;
now
A10:
<*1*>
= ((
Root Z)
^
<*1*>) by
FINSEQ_1: 34;
assume
A11: k
<> 1;
then k
<>
0 & ... & k
<> 1 by
A1,
A5,
A8,
A9;
then 1
< k by
NAT_1: 25;
then (1
+ 1)
<= k by
NAT_1: 13;
then
<*1*>
in Z by
A8,
Th3,
XXREAL_0: 2;
then
<*1*>
in (
succ (
Root Z)) by
A10,
TREES_2: 12;
then
<*1*>
=
<*
0 *> or
<*1*>
=
<*k*> by
A2,
A5,
A8,
A9,
TARSKI:def 2;
hence contradiction by
A11,
TREES_1: 3;
end;
hence thesis by
A2,
A4,
A8,
A9,
FINSEQ_1: 34;
end;
suppose
A12: m
<>
0 ;
<*
0 *>
in Z &
<*
0 *>
= ((
Root Z)
^
<*
0 *>) by
A5,
Th3,
FINSEQ_1: 34,
NAT_1: 2;
then
<*
0 *>
in (
succ (
Root Z)) by
TREES_2: 12;
then
A13:
<*
0 *>
=
<*m*> or
<*
0 *>
=
<*k*> by
A2,
A5,
A8,
TARSKI:def 2;
now
A14:
<*1*>
= ((
Root Z)
^
<*1*>) by
FINSEQ_1: 34;
assume
A15: m
<> 1;
then 1
< m by
A12,
NAT_1: 25;
then (1
+ 1)
<= m by
NAT_1: 13;
then
<*1*>
in Z by
A5,
Th3,
XXREAL_0: 2;
then
<*1*>
in (
succ (
Root Z)) by
A14,
TREES_2: 12;
then
<*1*>
=
<*
0 *> or
<*1*>
=
<*m*> by
A2,
A5,
A8,
A12,
A13,
TARSKI:def 2,
TREES_1: 3;
hence contradiction by
A15,
TREES_1: 3;
end;
hence thesis by
A2,
A4,
A8,
A13,
FINSEQ_1: 34,
TREES_1: 3;
end;
end;
reserve s9,w9,v9 for
Element of (
NAT
* );
theorem ::
MODAL_1:20
Th15: for Z be
Tree, o be
Element of Z st o
<> (
Root Z) holds ((Z
| o),{ (o
^ s9) : (o
^ s9)
in Z })
are_equipotent & not (
Root Z)
in { (o
^ w9) : (o
^ w9)
in Z }
proof
let Z be
Tree, o be
Element of Z such that
A1: o
<> (
Root Z);
set A = { (o
^ s9) : (o
^ s9)
in Z };
thus ((Z
| o),A)
are_equipotent
proof
defpred
P[
object,
object] means for s st $1
= s holds $2
= (o
^ s);
A2: for x be
object st x
in (Z
| o) holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in (Z
| o);
then
reconsider s = x as
FinSequence of
NAT by
TREES_1: 19;
take (o
^ s);
let w;
assume x
= w;
hence thesis;
end;
ex f be
Function st (
dom f)
= (Z
| o) & for x be
object st x
in (Z
| o) holds
P[x, (f
. x)] from
CLASSES1:sch 1(
A2);
then
consider f be
Function such that
A3: (
dom f)
= (Z
| o) and
A4: for x be
object st x
in (Z
| o) holds for s st x
= s holds (f
. x)
= (o
^ s);
now
let x be
object;
thus x
in (
rng f) implies x
in A
proof
assume x
in (
rng f);
then
consider x1 be
object such that
A5: x1
in (
dom f) and
A6: x
= (f
. x1) by
FUNCT_1:def 3;
reconsider x1 as
FinSequence of
NAT by
A3,
A5,
TREES_1: 19;
reconsider x1 as
Element of (
NAT
* ) by
FINSEQ_1:def 11;
(o
^ x1)
in Z & x
= (o
^ x1) by
A3,
A4,
A5,
A6,
TREES_1:def 6;
hence thesis;
end;
assume x
in A;
then
consider v9 such that
A7: x
= (o
^ v9) and
A8: (o
^ v9)
in Z;
v9
in (Z
| o) by
A8,
TREES_1:def 6;
then
A9: x
= (f
. v9) by
A4,
A7;
v9
in (
dom f) by
A3,
A8,
TREES_1:def 6;
hence x
in (
rng f) by
A9,
FUNCT_1:def 3;
end;
then
A10: (
rng f)
= A by
TARSKI: 2;
now
let x1,x2 be
object;
assume that
A11: x1
in (
dom f) and
A12: x2
in (
dom f) and
A13: (f
. x1)
= (f
. x2);
reconsider s1 = x1, s2 = x2 as
FinSequence of
NAT by
A3,
A11,
A12,
TREES_1: 19;
(o
^ s1)
= (f
. x2) by
A3,
A4,
A11,
A13
.= (o
^ s2) by
A3,
A4,
A12;
hence x1
= x2 by
FINSEQ_1: 33;
end;
then f is
one-to-one by
FUNCT_1:def 4;
hence thesis by
A3,
A10,
WELLORD2:def 4;
end;
assume not thesis;
then ex v9 st (
Root Z)
= (o
^ v9) & (o
^ v9)
in Z;
hence contradiction by
A1;
end;
theorem ::
MODAL_1:21
Th16: for Z be
finite
Tree, o be
Element of Z st o
<> (
Root Z) holds (
card (Z
| o))
< (
card Z)
proof
let Z be
finite
Tree, o be
Element of Z such that
A1: o
<> (
Root Z);
set A = { (o
^ s9) : (o
^ s9)
in Z };
A2: ((Z
| o),A)
are_equipotent by
A1,
Th15;
then
reconsider A as
finite
set by
CARD_1: 38;
reconsider B = (A
\/
{(
Root Z)}) as
finite
set;
now
let x be
object such that
A3: x
in B;
now
per cases by
A3,
XBOOLE_0:def 3;
suppose x
in { (o
^ s9) : (o
^ s9)
in Z };
then ex v9 st x
= (o
^ v9) & (o
^ v9)
in Z;
hence x
in Z;
end;
suppose x
in
{(
Root Z)};
hence x
in Z;
end;
end;
hence x
in Z;
end;
then
A4: B
c= Z;
(
card B)
= ((
card A)
+ 1) by
A1,
Th15,
CARD_2: 41
.= ((
card (Z
| o))
+ 1) by
A2,
CARD_1: 5;
then ((
card (Z
| o))
+ 1)
<= (
card Z) by
A4,
NAT_1: 43;
hence thesis by
NAT_1: 13;
end;
theorem ::
MODAL_1:22
Th17: for Z be
finite
Tree, z be
Element of Z st (
succ (
Root Z))
=
{z} holds Z
= ((
elementary_tree 1)
with-replacement (
<*
0 *>,(Z
| z)))
proof
let Z be
finite
Tree, z be
Element of Z;
set e = (
elementary_tree 1);
A1:
<*
0 *>
in e by
TARSKI:def 2,
TREES_1: 51;
A2:
{}
in Z by
TREES_1: 22;
assume
A3: (
succ (
Root Z))
=
{z};
then (
card (
succ (
Root Z)))
= 1 by
CARD_1: 30;
then (
branchdeg (
Root Z))
= 1 by
TREES_2:def 12;
then
{z}
=
{
<*
0 *>} by
A3,
Th13;
then z
in
{
<*
0 *>} by
TARSKI:def 1;
then
A4: z
=
<*
0 *> by
TARSKI:def 1;
then
A5:
<*
0 *>
in Z;
now
let x be
object;
thus x
in Z implies x
in (e
with-replacement (
<*
0 *>,(Z
| z)))
proof
assume x
in Z;
then
reconsider x9 = x as
Element of Z;
per cases ;
suppose x9
=
{} ;
hence thesis by
TREES_1: 22;
end;
suppose x9
<>
{} ;
then
consider w be
FinSequence of
NAT , n be
Element of
NAT such that
A6: x9
= (
<*n*>
^ w) by
FINSEQ_2: 130;
<*n*>
is_a_prefix_of x9 by
A6,
TREES_1: 1;
then
A7:
<*n*>
in Z by
TREES_1: 20;
<*n*>
= ((
Root Z)
^
<*n*>) by
FINSEQ_1: 34;
then
A8:
<*n*>
in (
succ (
Root Z)) by
A7,
TREES_2: 12;
then
<*n*>
= z by
A3,
TARSKI:def 1;
then
A9: w
in (Z
| z) by
A6,
TREES_1:def 6;
<*n*>
=
<*
0 *> by
A3,
A4,
A8,
TARSKI:def 1;
hence thesis by
A1,
A6,
A9,
TREES_1:def 9;
end;
end;
assume x
in (e
with-replacement (
<*
0 *>,(Z
| z)));
then
reconsider x9 = x as
Element of (e
with-replacement (
<*
0 *>,(Z
| z)));
per cases by
A1,
TREES_1:def 9;
suppose x9
in e & not
<*
0 *>
is_a_proper_prefix_of x9;
hence x
in Z by
A5,
A2,
TARSKI:def 2,
TREES_1: 51;
end;
suppose ex s st s
in (Z
| z) & x9
= (
<*
0 *>
^ s);
hence x
in Z by
A4,
TREES_1:def 6;
end;
end;
hence thesis by
TARSKI: 2;
end;
Lm2: for f be
Function st (
dom f) is
finite holds f is
finite
proof
let f be
Function;
assume
A1: (
dom f) is
finite;
then (
rng f) is
finite by
FINSET_1: 8;
then
[:(
dom f), (
rng f):] is
finite by
A1;
hence thesis by
FINSET_1: 1,
RELAT_1: 7;
end;
theorem ::
MODAL_1:23
Th18: for Z be
finite
DecoratedTree of D, z be
Element of (
dom Z) st (
succ (
Root (
dom Z)))
=
{z} holds Z
= (((
elementary_tree 1)
--> (
Root Z))
with-replacement (
<*
0 *>,(Z
| z)))
proof
set e = (
elementary_tree 1);
let Z be
finite
DecoratedTree of D, z be
Element of (
dom Z);
set E = ((
elementary_tree 1)
--> (
Root Z));
A1: (
dom E)
= e by
FUNCOP_1: 13;
A2: (
dom (Z
| z))
= ((
dom Z)
| z) by
TREES_2:def 10;
A3:
<*
0 *>
in e by
TARSKI:def 2,
TREES_1: 51;
then
A4:
<*
0 *>
in (
dom E) by
FUNCOP_1: 13;
assume
A5: (
succ (
Root (
dom Z)))
=
{z};
then (
card (
succ (
Root (
dom Z))))
= 1 by
CARD_1: 30;
then (
branchdeg (
Root (
dom Z)))
= 1 by
TREES_2:def 12;
then
{z}
=
{
<*
0 *>} by
A5,
Th13;
then z
in
{
<*
0 *>} by
TARSKI:def 1;
then
A6: z
=
<*
0 *> by
TARSKI:def 1;
A7: for s st s
in (
dom (E
with-replacement (
<*
0 *>,(Z
| z)))) holds ((E
with-replacement (
<*
0 *>,(Z
| z)))
. s)
= (Z
. s)
proof
let s;
assume
A8: s
in (
dom (E
with-replacement (
<*
0 *>,(Z
| z))));
A9: (
dom (E
with-replacement (
<*
0 *>,(Z
| z))))
= ((
dom E)
with-replacement (
<*
0 *>,(
dom (Z
| z)))) by
A4,
TREES_2:def 11;
then
A10: not
<*
0 *>
is_a_prefix_of s & ((E
with-replacement (
<*
0 *>,(Z
| z)))
. s)
= (E
. s) or ex w st w
in (
dom (Z
| z)) & s
= (
<*
0 *>
^ w) & ((E
with-replacement (
<*
0 *>,(Z
| z)))
. s)
= ((Z
| z)
. w) by
A4,
A8,
TREES_2:def 11;
now
per cases by
A4,
A9,
A8,
TREES_1:def 9;
suppose
A11: s
in (
dom E) & not
<*
0 *>
is_a_proper_prefix_of s;
now
per cases by
A11,
TARSKI:def 2,
TREES_1: 51;
suppose
A12: s
=
{} ;
then s
in e by
TREES_1: 22;
then
A13: (E
. s)
= (Z
. s) by
A12,
FUNCOP_1: 7;
not ex w st w
in (
dom (Z
| z)) & s
= (
<*
0 *>
^ w) & ((E
with-replacement (
<*
0 *>,(Z
| z)))
. s)
= ((Z
| z)
. w) by
A12;
hence thesis by
A4,
A9,
A8,
A13,
TREES_2:def 11;
end;
suppose s
=
<*
0 *>;
hence thesis by
A6,
A2,
A10,
TREES_2:def 10;
end;
end;
hence thesis;
end;
suppose ex w st w
in (
dom (Z
| z)) & s
= (
<*
0 *>
^ w);
hence thesis by
A6,
A2,
A10,
TREES_1: 1,
TREES_2:def 10;
end;
end;
hence thesis;
end;
(
dom (E
with-replacement (
<*
0 *>,(Z
| z))))
= (e
with-replacement (
<*
0 *>,((
dom Z)
| z))) by
A3,
A1,
A2,
TREES_2:def 11;
then (
dom (E
with-replacement (
<*
0 *>,(Z
| z))))
= (
dom Z) by
A5,
Th17;
hence thesis by
A7,
TREES_2: 31;
end;
theorem ::
MODAL_1:24
Th19: for Z be
Tree, x1,x2 be
Element of Z st x1
=
<*
0 *> & x2
=
<*1*> & (
succ (
Root Z))
=
{x1, x2} holds Z
= (((
elementary_tree 2)
with-replacement (
<*
0 *>,(Z
| x1)))
with-replacement (
<*1*>,(Z
| x2)))
proof
set e = (
elementary_tree 2);
let Z be
Tree, x1,x2 be
Element of Z such that
A1: x1
=
<*
0 *> and
A2: x2
=
<*1*> and
A3: (
succ (
Root Z))
=
{x1, x2};
set T1 = ((
elementary_tree 2)
with-replacement (
<*
0 *>,(Z
| x1)));
A4:
<*
0 *>
in e by
ENUMSET1:def 1,
TREES_1: 53;
A5:
now
let s;
thus s
in Z implies s
in T1 & not
<*1*>
is_a_proper_prefix_of s or ex w st w
in (Z
| x2) & s
= (
<*1*>
^ w)
proof
assume
A6: s
in Z;
per cases ;
suppose s
=
{} ;
hence thesis by
TREES_1: 22;
end;
suppose s
<>
{} ;
then
consider w be
FinSequence of
NAT , n be
Element of
NAT such that
A7: s
= (
<*n*>
^ w) by
FINSEQ_2: 130;
<*n*>
is_a_prefix_of s by
A7,
TREES_1: 1;
then
A8:
<*n*>
in Z by
A6,
TREES_1: 20;
<*n*>
= ((
Root Z)
^
<*n*>) by
FINSEQ_1: 34;
then
A9:
<*n*>
in (
succ (
Root Z)) by
A8,
TREES_2: 12;
now
per cases by
A1,
A2,
A3,
A9,
TARSKI:def 2;
suppose
A10:
<*n*>
=
<*
0 *>;
then w
in (Z
| x1) by
A1,
A6,
A7,
TREES_1:def 6;
hence thesis by
A4,
A7,
A10,
Th2,
TREES_1:def 9;
end;
suppose
A11:
<*n*>
=
<*1*>;
then w
in (Z
| x2) by
A2,
A6,
A7,
TREES_1:def 6;
hence thesis by
A7,
A11;
end;
end;
hence thesis;
end;
end;
assume
A12: s
in T1 & not
<*1*>
is_a_proper_prefix_of s or ex w st w
in (Z
| x2) & s
= (
<*1*>
^ w);
now
per cases by
A12;
suppose
A13: s
in T1 & not
<*1*>
is_a_proper_prefix_of s;
now
per cases by
A4,
A13,
TREES_1:def 9;
suppose s
in e & not
<*
0 *>
is_a_proper_prefix_of s;
then s
=
{} or s
=
<*
0 *> or s
=
<*1*> by
ENUMSET1:def 1,
TREES_1: 53;
hence s
in Z by
A1,
A2,
A3;
end;
suppose ex w st w
in (Z
| x1) & s
= (
<*
0 *>
^ w);
hence s
in Z by
A1,
TREES_1:def 6;
end;
end;
hence s
in Z;
end;
suppose ex w st w
in (Z
| x2) & s
= (
<*1*>
^ w);
hence s
in Z by
A2,
TREES_1:def 6;
end;
end;
hence s
in Z;
end;
A14: not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 3;
<*1*>
in e by
ENUMSET1:def 1,
TREES_1: 53;
then
<*1*>
in T1 by
A4,
A14,
TREES_1:def 9;
hence thesis by
A5,
TREES_1:def 9;
end;
theorem ::
MODAL_1:25
Th20: for Z be
DecoratedTree of D, x1,x2 be
Element of (
dom Z) st x1
=
<*
0 *> & x2
=
<*1*> & (
succ (
Root (
dom Z)))
=
{x1, x2} holds Z
= ((((
elementary_tree 2)
--> (
Root Z))
with-replacement (
<*
0 *>,(Z
| x1)))
with-replacement (
<*1*>,(Z
| x2)))
proof
A1: not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 52;
set e = (
elementary_tree 2);
let Z be
DecoratedTree of D, x1,x2 be
Element of (
dom Z) such that
A2: x1
=
<*
0 *> and
A3: x2
=
<*1*> and
A4: (
succ (
Root (
dom Z)))
=
{x1, x2};
A5: (
dom (Z
| x2))
= ((
dom Z)
| x2) by
TREES_2:def 10;
set T1 = (((
elementary_tree 2)
--> (
Root Z))
with-replacement (
<*
0 *>,(Z
| x1)));
set E = ((
elementary_tree 2)
--> (
Root Z));
A6: (
dom (Z
| x1))
= ((
dom Z)
| x1) by
TREES_2:def 10;
set T = (T1
with-replacement (
<*1*>,(Z
| x2)));
A7:
<*
0 *>
in e by
ENUMSET1:def 1,
TREES_1: 53;
then
A8:
<*
0 *>
in (
dom E) by
FUNCOP_1: 13;
then
A9: (
dom T1)
= ((
dom E)
with-replacement (
<*
0 *>,(
dom (Z
| x1)))) by
TREES_2:def 11;
<*1*>
in e by
ENUMSET1:def 1,
TREES_1: 53;
then
<*1*>
in (
dom E) by
FUNCOP_1: 13;
then
A10:
<*1*>
in (
dom T1) by
A8,
A9,
A1,
TREES_1:def 9;
then
A11: (
dom T)
= ((
dom T1)
with-replacement (
<*1*>,(
dom (Z
| x2)))) by
TREES_2:def 11;
A12: (
dom E)
= e by
FUNCOP_1: 13;
then
A13: (
dom T1)
= (e
with-replacement (
<*
0 *>,((
dom Z)
| x1))) by
A7,
A6,
TREES_2:def 11;
A14: for s st s
in (
dom T) holds (T
. s)
= (Z
. s)
proof
let s;
assume
A15: s
in (
dom T);
then
A16: not
<*1*>
is_a_prefix_of s & (T
. s)
= (T1
. s) or ex u st u
in (
dom (Z
| x2)) & s
= (
<*1*>
^ u) & (T
. s)
= ((Z
| x2)
. u) by
A10,
A11,
TREES_2:def 11;
now
per cases by
A10,
A11,
A15,
TREES_1:def 9;
suppose
A17: s
in (
dom T1) & not
<*1*>
is_a_proper_prefix_of s;
then
A18: not
<*
0 *>
is_a_prefix_of s & (T1
. s)
= (E
. s) or ex u st u
in (
dom (Z
| x1)) & s
= (
<*
0 *>
^ u) & (T1
. s)
= ((Z
| x1)
. u) by
A8,
A9,
TREES_2:def 11;
now
per cases by
A7,
A13,
A17,
TREES_1:def 9;
suppose
A19: s
in e & not
<*
0 *>
is_a_proper_prefix_of s;
now
per cases by
A19,
ENUMSET1:def 1,
TREES_1: 53;
suppose
A20: s
=
{} ;
then ( not ex u st u
in (
dom (Z
| x2)) & s
= (
<*1*>
^ u) & (T
. s)
= ((Z
| x2)
. u)) & (E
. s)
= (Z
. s) by
A19,
FUNCOP_1: 7;
hence thesis by
A10,
A11,
A15,
A18,
A20,
TREES_2:def 11;
end;
suppose s
=
<*
0 *>;
hence thesis by
A2,
A3,
A6,
A5,
A16,
A18,
TREES_2:def 10;
end;
suppose s
=
<*1*>;
hence thesis by
A3,
A5,
A16,
TREES_2:def 10;
end;
end;
hence thesis;
end;
suppose ex w st w
in ((
dom Z)
| x1) & s
= (
<*
0 *>
^ w);
hence thesis by
A2,
A3,
A6,
A5,
A16,
A18,
TREES_1: 1,
TREES_2:def 10;
end;
end;
hence thesis;
end;
suppose ex w st w
in (
dom (Z
| x2)) & s
= (
<*1*>
^ w);
hence thesis by
A3,
A5,
A16,
TREES_1: 1,
TREES_2:def 10;
end;
end;
hence thesis;
end;
(
dom Z)
= (
dom T) by
A2,
A3,
A4,
A12,
A6,
A5,
A9,
A11,
Th19;
hence thesis by
A14,
TREES_2: 31;
end;
definition
::
MODAL_1:def3
func
MP-variables ->
set equals
[:
{3},
NAT :];
coherence ;
end
registration
cluster
MP-variables -> non
empty;
coherence ;
end
definition
mode
MP-variable is
Element of
MP-variables ;
end
definition
::
MODAL_1:def4
func
MP-conectives ->
set equals
[:
{
0 , 1, 2},
NAT :];
coherence ;
end
registration
cluster
MP-conectives -> non
empty;
coherence ;
end
definition
mode
MP-conective is
Element of
MP-conectives ;
end
theorem ::
MODAL_1:26
Th21:
MP-conectives
misses
MP-variables
proof
assume not thesis;
then
consider x be
object such that
A1: x
in
[:
{
0 , 1, 2},
NAT :] and
A2: x
in
[:
{3},
NAT :] by
XBOOLE_0: 3;
consider x1,x2 be
object such that
A3: x1
in
{
0 , 1, 2} and x2
in
NAT and
A4: x
=
[x1, x2] by
A1,
ZFMISC_1:def 2;
x1
= 3 by
A2,
A4,
ZFMISC_1: 105;
hence contradiction by
A3,
ENUMSET1:def 1;
end;
reserve p,q for
MP-variable;
definition
let T be
finite
Tree, v be
Element of T;
:: original:
branchdeg
redefine
func
branchdeg v ->
Nat ;
coherence
proof
(
branchdeg v)
= (
card (
succ v)) by
TREES_2:def 12;
hence thesis;
end;
end
definition
::
MODAL_1:def5
func
MP-WFF ->
DTree-set of
[:
NAT ,
NAT :] means
:
Def5: (for x be
DecoratedTree of
[:
NAT ,
NAT :] st x
in it holds x is
finite) & for x be
finite
DecoratedTree of
[:
NAT ,
NAT :] holds x
in it iff for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ]);
existence
proof
deffunc
F(
set) =
[
0 ,
0 ];
set t = (
elementary_tree
0 );
set A =
[:
NAT ,
NAT :];
defpred
P[
object] means $1 is
finite
DecoratedTree of A & (for y be
finite
DecoratedTree of A st y
= $1 holds (
dom y) is
finite & for v be
Element of (
dom y) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (y
. v)
=
[
0 ,
0 ] or ex k st (y
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (y
. v)
=
[1,
0 ] or (y
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (y
. v)
=
[2,
0 ]));
consider Y be
set such that
A1: for x be
object holds x
in Y iff x
in (
PFuncs ((
NAT
* ),A)) &
P[x] from
XBOOLE_0:sch 1;
A2: for x be
finite
DecoratedTree of A holds x
in Y iff (
dom x) is
finite & for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ])
proof
let x be
finite
DecoratedTree of A;
thus x
in Y implies (
dom x) is
finite & for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ]) by
A1;
assume that (
dom x) is
finite and
A3: for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ]);
A4: x
in (
PFuncs ((
NAT
* ),A)) by
Th5;
for y be
finite
DecoratedTree of A st y
= x holds (
dom y) is
finite & for v be
Element of (
dom y) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (y
. v)
=
[
0 ,
0 ] or ex k st (y
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (y
. v)
=
[1,
0 ] or (y
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (y
. v)
=
[2,
0 ]) by
A3;
hence thesis by
A1,
A4;
end;
consider T be
DecoratedTree such that
A5: (
dom T)
= t & for p be
FinSequence of
NAT st p
in t holds (T
. p)
=
F(p) from
TREES_2:sch 7;
(
rng T)
c= A
proof
let x be
object;
assume x
in (
rng T);
then
consider z be
object such that
A6: z
in (
dom T) and
A7: x
= (T
. z) by
FUNCT_1:def 3;
z
= (
<*>
NAT ) by
A5,
A6,
TARSKI:def 1,
TREES_1: 29;
then
reconsider z as
FinSequence of
NAT ;
(T
. z)
=
[
0 ,
0 ] by
A5,
A6;
hence thesis by
A7;
end;
then
reconsider T as
finite
DecoratedTree of A by
A5,
Lm2,
RELAT_1:def 19;
A8: for y be
finite
DecoratedTree of A st y
= T holds (
dom y) is
finite & for v be
Element of (
dom y) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (y
. v)
=
[
0 ,
0 ] or ex k st (y
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (y
. v)
=
[1,
0 ] or (y
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (y
. v)
=
[2,
0 ])
proof
let y be
finite
DecoratedTree of A;
assume
A9: y
= T;
thus (
dom y) is
finite;
let v be
Element of (
dom y);
A10: (
succ v)
=
{}
proof
set x = the
Element of (
succ v);
assume not thesis;
then
A11: x
in (
succ v);
(
succ v)
= { (v
^
<*n*>) : (v
^
<*n*>)
in (
dom y) } by
TREES_2:def 5;
then ex n st x
= (v
^
<*n*>) & (v
^
<*n*>)
in (
dom y) by
A11;
hence contradiction by
A5,
A9,
TARSKI:def 1,
TREES_1: 29;
end;
hence (
branchdeg v)
<= 2 by
CARD_1: 27,
TREES_2:def 12;
thus thesis by
A5,
A9,
A10,
CARD_1: 27,
TREES_2:def 12;
end;
T
in (
PFuncs ((
NAT
* ),A)) by
Th5;
then
reconsider Y as non
empty
set by
A1,
A8;
for x be
object st x
in Y holds x is
DecoratedTree of A by
A1;
then
reconsider Y as
DTree-set of A by
TREES_3:def 6;
take Y;
thus thesis by
A1,
A2;
end;
uniqueness
proof
let D1,D2 be
DTree-set of
[:
NAT ,
NAT :] such that
A12: for x be
DecoratedTree of
[:
NAT ,
NAT :] st x
in D1 holds x is
finite and
A13: for x be
finite
DecoratedTree of
[:
NAT ,
NAT :] holds x
in D1 iff for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ]) and
A14: for x be
DecoratedTree of
[:
NAT ,
NAT :] st x
in D2 holds x is
finite and
A15: for x be
finite
DecoratedTree of
[:
NAT ,
NAT :] holds x
in D2 iff for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ]);
thus D1
c= D2
proof
let x be
object;
assume
A16: x
in D1;
reconsider y = x as
finite
DecoratedTree of
[:
NAT ,
NAT :] by
A12,
A16;
for v be
Element of (
dom y) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (y
. v)
=
[
0 ,
0 ] or ex k st (y
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (y
. v)
=
[1,
0 ] or (y
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (y
. v)
=
[2,
0 ]) by
A13,
A16;
hence thesis by
A15;
end;
let x be
object;
assume
A17: x
in D2;
reconsider y = x as
finite
DecoratedTree of
[:
NAT ,
NAT :] by
A14,
A17;
for v be
Element of (
dom y) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (y
. v)
=
[
0 ,
0 ] or ex k st (y
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (y
. v)
=
[1,
0 ] or (y
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (y
. v)
=
[2,
0 ]) by
A15,
A17;
hence thesis by
A13;
end;
end
definition
mode
MP-wff is
Element of
MP-WFF ;
end
registration
cluster ->
finite for
MP-wff;
coherence by
Def5;
end
reserve A,A1,B,B1,C,C1 for
MP-wff;
definition
let A;
let a be
Element of (
dom A);
:: original:
|
redefine
func A
| a ->
MP-wff ;
coherence
proof
set x = (A
| a);
A1: (
dom x)
= ((
dom A)
| a) by
TREES_2:def 10;
then
reconsider db = (
dom x) as
finite
Tree;
reconsider x as
finite
DecoratedTree of
[:
NAT ,
NAT :] by
A1,
Lm2;
now
thus db is
finite;
let v be
Element of db;
set da = (
dom A);
reconsider v9 = v as
Element of (da
| a) by
TREES_2:def 10;
v
in db;
then
A2: v
in (da
| a) by
TREES_2:def 10;
then
reconsider w = (a
^ v) as
Element of da by
TREES_1:def 6;
((
succ v9),(
succ w))
are_equipotent & (
succ v9)
= (
succ v) by
Th11,
TREES_2:def 10;
then (
card (
succ v))
= (
card (
succ w)) by
CARD_1: 5;
then (
branchdeg v)
= (
card (
succ w)) by
TREES_2:def 12;
then
A3: (
branchdeg v)
= (
branchdeg w) by
TREES_2:def 12;
hence (
branchdeg v)
<= 2 by
Def5;
thus (
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]
proof
assume
A4: (
branchdeg v)
=
0 ;
per cases by
A3,
A4,
Def5;
suppose (A
. w)
=
[
0 ,
0 ];
hence thesis by
A2,
TREES_2:def 10;
end;
suppose ex k st (A
. w)
=
[3, k];
then
consider k such that
A5: (A
. w)
=
[3, k];
(x
. v)
=
[3, k] by
A2,
A5,
TREES_2:def 10;
hence thesis;
end;
end;
thus (
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]
proof
assume
A6: (
branchdeg v)
= 1;
per cases by
A3,
A6,
Def5;
suppose (A
. w)
=
[1,
0 ];
hence thesis by
A2,
TREES_2:def 10;
end;
suppose (A
. w)
=
[1, 1];
hence thesis by
A2,
TREES_2:def 10;
end;
end;
thus (
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ]
proof
assume (
branchdeg v)
= 2;
then (A
. w)
=
[2,
0 ] by
A3,
Def5;
hence thesis by
A2,
TREES_2:def 10;
end;
end;
hence thesis by
Def5;
end;
end
definition
let a be
Element of
MP-conectives ;
::
MODAL_1:def6
func
the_arity_of a ->
Nat equals (a
`1 );
coherence
proof
reconsider X =
{
0 , 1, 2} as non
empty
set;
consider a1 be
Element of X, k be
Element of
NAT such that
A1: a
=
[a1, k] by
DOMAIN_1: 1;
a1
=
0 or a1
= 1 or a1
= 2 by
ENUMSET1:def 1;
hence thesis by
A1;
end;
end
definition
let D be non
empty
set, T,T1 be
DecoratedTree of D, p be
FinSequence of
NAT ;
assume
A1: p
in (
dom T);
::
MODAL_1:def7
func
@ (T,p,T1) ->
DecoratedTree of D equals
:
Def7: (T
with-replacement (p,T1));
coherence
proof
set X = (T
with-replacement (p,T1));
(
rng X)
c= D
proof
let x be
object;
assume x
in (
rng X);
then
consider z be
object such that
A2: z
in (
dom X) and
A3: x
= (X
. z) by
FUNCT_1:def 3;
reconsider z as
FinSequence of
NAT by
A2,
TREES_1: 19;
A4: (
dom X)
= ((
dom T)
with-replacement (p,(
dom T1))) by
A1,
TREES_2:def 11;
now
per cases by
A1,
A2,
A4,
TREES_2:def 11;
suppose
A5: not p
is_a_prefix_of z & (X
. z)
= (T
. z);
then not ex s be
FinSequence of
NAT st s
in (
dom T1) & z
= (p
^ s) by
TREES_1: 1;
then
reconsider z as
Element of (
dom T) by
A1,
A2,
A4,
TREES_1:def 9;
(T
. z) is
Element of D;
hence thesis by
A3,
A5;
end;
suppose ex s st s
in (
dom T1) & z
= (p
^ s) & (X
. z)
= (T1
. s);
then
consider s such that
A6: s
in (
dom T1) and z
= (p
^ s) and
A7: (X
. z)
= (T1
. s);
reconsider s as
Element of (
dom T1) by
A6;
(T1
. s) is
Element of D;
hence thesis by
A3,
A7;
end;
end;
hence thesis;
end;
hence thesis by
RELAT_1:def 19;
end;
end
theorem ::
MODAL_1:27
Th22: (((
elementary_tree 1)
-->
[1,
0 ])
with-replacement (
<*
0 *>,A)) is
MP-wff
proof
reconsider d =
<*
0 *> as
Element of (
elementary_tree 1) by
TREES_1: 28;
set x = (((
elementary_tree 1)
-->
[1,
0 ])
with-replacement (
<*
0 *>,A));
<*
0 *>
in (
elementary_tree 1) by
TREES_1: 28;
then
A1:
<*
0 *>
in (
dom ((
elementary_tree 1)
-->
[1,
0 ])) by
FUNCOP_1: 13;
then
A2: (
@ (((
elementary_tree 1)
-->
[1,
0 ]),
<*
0 *>,A))
= x by
Def7;
(
dom x)
= ((
dom ((
elementary_tree 1)
-->
[1,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
A1,
TREES_2:def 11;
then (
dom x)
= ((
elementary_tree 1)
with-replacement (d,(
dom A))) by
FUNCOP_1: 13;
then
reconsider x as
finite
DecoratedTree of
[:
NAT ,
NAT :] by
A2,
Lm2;
A3: (
dom x)
= ((
dom ((
elementary_tree 1)
-->
[1,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
A1,
TREES_2:def 11;
for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ])
proof
set e = ((
elementary_tree 1)
-->
[1,
0 ]);
let v be
Element of (
dom x);
now
per cases by
A1,
A3,
TREES_2:def 11;
suppose
A4: not
<*
0 *>
is_a_prefix_of v & (x
. v)
= (e
. v);
A5: (
dom e)
=
{
{} ,
<*
0 *>} by
FUNCOP_1: 13,
TREES_1: 51;
A6: not ex s st s
in (
dom A) & v
= (
<*
0 *>
^ s) by
A4,
TREES_1: 1;
then
A7: v
in (
dom e) by
A1,
A3,
TREES_1:def 9;
then
A8: v
=
{} by
A4,
A5,
TARSKI:def 2;
reconsider v9 = v as
Element of (
dom e) by
A1,
A3,
A6,
TREES_1:def 9;
now
let x be
object;
thus x
in (
succ v9) implies x
in
{
<*
0 *>}
proof
assume x
in (
succ v9);
then x
in { (v9
^
<*n*>) : (v9
^
<*n*>)
in (
dom e) } by
TREES_2:def 5;
then
consider n such that
A9: x
= (v9
^
<*n*>) and
A10: (v9
^
<*n*>)
in (
dom e);
<*n*>
in (
dom e) by
A8,
A10,
FINSEQ_1: 34;
then
A11:
<*n*>
=
{} or
<*n*>
=
<*
0 *> by
A5,
TARSKI:def 2;
x
=
<*n*> by
A8,
A9,
FINSEQ_1: 34;
hence thesis by
A11,
TARSKI:def 1;
end;
assume x
in
{
<*
0 *>};
then
A12: x
=
<*
0 *> by
TARSKI:def 1;
then
A13: x
= (v9
^
<*
0 *>) by
A8,
FINSEQ_1: 34;
then (v9
^
<*
0 *>)
in (
dom e) by
A5,
A12,
TARSKI:def 2;
then x
in { (v9
^
<*n*>) : (v9
^
<*n*>)
in (
dom e) } by
A13;
hence x
in (
succ v9) by
TREES_2:def 5;
end;
then
A14: (
succ v9)
=
{
<*
0 *>} by
TARSKI: 2;
(
succ v)
= (
succ v9) by
A1,
A3,
A8,
Lm1,
Th8;
then 1
= (
card (
succ v)) by
A14,
CARD_1: 30;
then
A15: (
branchdeg v)
= 1 by
TREES_2:def 12;
hence (
branchdeg v)
<= 2;
v
in (
elementary_tree 1) by
A7;
hence thesis by
A4,
A15,
FUNCOP_1: 7;
end;
suppose ex s st s
in (
dom A) & v
= (
<*
0 *>
^ s) & (x
. v)
= (A
. s);
then
consider s such that
A16: s
in (
dom A) and
A17: v
= (
<*
0 *>
^ s) and
A18: (x
. v)
= (A
. s);
reconsider s as
Element of (
dom A) by
A16;
((
succ v),(
succ s))
are_equipotent by
A1,
A3,
A17,
TREES_2: 37;
then (
card (
succ v))
= (
card (
succ s)) by
CARD_1: 5;
then
A19: (
branchdeg v)
= (
card (
succ s)) by
TREES_2:def 12;
A20: (
branchdeg s)
<= 2 by
Def5;
hence (
branchdeg v)
<= 2 by
A19,
TREES_2:def 12;
A21: (
branchdeg s)
= 1 implies (A
. s)
=
[1,
0 ] or (A
. s)
=
[1, 1] by
Def5;
A22: (
branchdeg s)
= 2 implies (A
. s)
=
[2,
0 ] by
Def5;
(
branchdeg s)
=
0 implies (A
. s)
=
[
0 ,
0 ] or ex m st (A
. s)
=
[3, m] by
Def5;
hence thesis by
A18,
A20,
A21,
A22,
A19,
TREES_2:def 12;
end;
end;
hence thesis;
end;
hence thesis by
Def5;
end;
theorem ::
MODAL_1:28
Th23: (((
elementary_tree 1)
-->
[1, 1])
with-replacement (
<*
0 *>,A)) is
MP-wff
proof
reconsider d =
<*
0 *> as
Element of (
elementary_tree 1) by
TREES_1: 28;
set x = (((
elementary_tree 1)
-->
[1, 1])
with-replacement (
<*
0 *>,A));
<*
0 *>
in (
elementary_tree 1) by
TREES_1: 28;
then
A1:
<*
0 *>
in (
dom ((
elementary_tree 1)
-->
[1, 1])) by
FUNCOP_1: 13;
then (
dom x)
= ((
dom ((
elementary_tree 1)
-->
[1, 1]))
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
then
A2: (
dom x)
= ((
elementary_tree 1)
with-replacement (d,(
dom A))) by
FUNCOP_1: 13;
(
@ (((
elementary_tree 1)
-->
[1, 1]),
<*
0 *>,A))
= (((
elementary_tree 1)
-->
[1, 1])
with-replacement (
<*
0 *>,A)) by
A1,
Def7;
then
reconsider x = (((
elementary_tree 1)
-->
[1, 1])
with-replacement (
<*
0 *>,A)) as
finite
DecoratedTree of
[:
NAT ,
NAT :] by
A2,
Lm2;
A3: (
dom x)
= ((
dom ((
elementary_tree 1)
-->
[1, 1]))
with-replacement (
<*
0 *>,(
dom A))) by
A1,
TREES_2:def 11;
for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ])
proof
set e = ((
elementary_tree 1)
-->
[1, 1]);
let v be
Element of (
dom x);
now
per cases by
A1,
A3,
TREES_2:def 11;
suppose
A4: not
<*
0 *>
is_a_prefix_of v & (x
. v)
= (e
. v);
A5: (
dom e)
=
{
{} ,
<*
0 *>} by
FUNCOP_1: 13,
TREES_1: 51;
A6: not ex s st s
in (
dom A) & v
= (
<*
0 *>
^ s) by
A4,
TREES_1: 1;
then
A7: v
in (
dom e) by
A1,
A3,
TREES_1:def 9;
then
A8: v
=
{} by
A4,
A5,
TARSKI:def 2;
reconsider v9 = v as
Element of (
dom e) by
A1,
A3,
A6,
TREES_1:def 9;
now
let x be
object;
thus x
in (
succ v9) implies x
in
{
<*
0 *>}
proof
assume x
in (
succ v9);
then x
in { (v9
^
<*n*>) : (v9
^
<*n*>)
in (
dom e) } by
TREES_2:def 5;
then
consider n such that
A9: x
= (v9
^
<*n*>) and
A10: (v9
^
<*n*>)
in (
dom e);
<*n*>
in (
dom e) by
A8,
A10,
FINSEQ_1: 34;
then
A11:
<*n*>
=
{} or
<*n*>
=
<*
0 *> by
A5,
TARSKI:def 2;
x
=
<*n*> by
A8,
A9,
FINSEQ_1: 34;
hence thesis by
A11,
TARSKI:def 1;
end;
assume x
in
{
<*
0 *>};
then
A12: x
=
<*
0 *> by
TARSKI:def 1;
then
A13: x
= (v9
^
<*
0 *>) by
A8,
FINSEQ_1: 34;
then (v9
^
<*
0 *>)
in (
dom e) by
A5,
A12,
TARSKI:def 2;
then x
in { (v9
^
<*n*>) : (v9
^
<*n*>)
in (
dom e) } by
A13;
hence x
in (
succ v9) by
TREES_2:def 5;
end;
then
A14: (
succ v9)
=
{
<*
0 *>} by
TARSKI: 2;
(
succ v)
= (
succ v9) by
A1,
A3,
A8,
Lm1,
Th8;
then 1
= (
card (
succ v)) by
A14,
CARD_1: 30;
then
A15: (
branchdeg v)
= 1 by
TREES_2:def 12;
hence (
branchdeg v)
<= 2;
v
in (
elementary_tree 1) by
A7;
hence thesis by
A4,
A15,
FUNCOP_1: 7;
end;
suppose ex s st s
in (
dom A) & v
= (
<*
0 *>
^ s) & (x
. v)
= (A
. s);
then
consider s such that
A16: s
in (
dom A) and
A17: v
= (
<*
0 *>
^ s) and
A18: (x
. v)
= (A
. s);
reconsider s as
Element of (
dom A) by
A16;
((
succ v),(
succ s))
are_equipotent by
A1,
A3,
A17,
TREES_2: 37;
then (
card (
succ v))
= (
card (
succ s)) by
CARD_1: 5;
then
A19: (
branchdeg v)
= (
card (
succ s)) by
TREES_2:def 12;
A20: (
branchdeg s)
<= 2 by
Def5;
hence (
branchdeg v)
<= 2 by
A19,
TREES_2:def 12;
A21: (
branchdeg s)
= 1 implies (A
. s)
=
[1,
0 ] or (A
. s)
=
[1, 1] by
Def5;
A22: (
branchdeg s)
= 2 implies (A
. s)
=
[2,
0 ] by
Def5;
(
branchdeg s)
=
0 implies (A
. s)
=
[
0 ,
0 ] or ex m st (A
. s)
=
[3, m] by
Def5;
hence thesis by
A18,
A20,
A21,
A22,
A19,
TREES_2:def 12;
end;
end;
hence thesis;
end;
hence thesis by
Def5;
end;
theorem ::
MODAL_1:29
Th24: ((((
elementary_tree 2)
-->
[2,
0 ])
with-replacement (
<*
0 *>,A))
with-replacement (
<*1*>,B)) is
MP-wff
proof
reconsider d =
<*
0 *> as
Element of (
elementary_tree 2) by
TREES_1: 28;
set y = (((
elementary_tree 2)
-->
[2,
0 ])
with-replacement (
<*
0 *>,A));
set x = (y
with-replacement (
<*1*>,B));
A1: not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 3;
reconsider db = (
dom B) as
finite
Tree;
reconsider da = (
dom A) as
finite
Tree;
<*
0 *>
in (
elementary_tree 2) by
TREES_1: 28;
then
A2:
<*
0 *>
in (
dom ((
elementary_tree 2)
-->
[2,
0 ])) by
FUNCOP_1: 13;
then (
@ (((
elementary_tree 2)
-->
[2,
0 ]),
<*
0 *>,A))
= y by
Def7;
then
reconsider y as
DecoratedTree of
[:
NAT ,
NAT :];
A3: (
dom y)
= ((
dom ((
elementary_tree 2)
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
A2,
TREES_2:def 11;
(
dom ((
elementary_tree 2)
-->
[2,
0 ]))
= (
elementary_tree 2) by
FUNCOP_1: 13;
then (
dom y)
= ((
elementary_tree 2)
with-replacement (d,da)) by
TREES_2:def 11;
then
reconsider dy = (
dom y) as
finite
Tree;
<*1*>
in (
elementary_tree 2) by
TREES_1: 28;
then
A4:
<*1*>
in (
dom ((
elementary_tree 2)
-->
[2,
0 ])) by
FUNCOP_1: 13;
then
A5:
<*1*>
in (
dom y) by
A2,
A3,
A1,
TREES_1:def 9;
reconsider d1 =
<*1*> as
Element of dy by
A2,
A3,
A4,
A1,
TREES_1:def 9;
(
dom x)
= (dy
with-replacement (d1,db)) & (
@ (y,
<*1*>,B))
= x by
A5,
Def7,
TREES_2:def 11;
then
reconsider x as
finite
DecoratedTree of
[:
NAT ,
NAT :] by
Lm2;
A6: (
dom x)
= ((
dom y)
with-replacement (
<*1*>,(
dom B))) by
A5,
TREES_2:def 11;
for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ])
proof
set e = ((
elementary_tree 2)
-->
[2,
0 ]);
let v be
Element of (
dom x);
now
per cases by
A5,
A6,
TREES_2:def 11;
suppose
A7: not
<*1*>
is_a_prefix_of v & (x
. v)
= (y
. v);
then
A8: not ex s st s
in (
dom B) & v
= (
<*1*>
^ s) by
TREES_1: 1;
then
A9: v
in ((
dom e)
with-replacement (
<*
0 *>,(
dom A))) by
A3,
A5,
A6,
TREES_1:def 9;
now
per cases by
A2,
A9,
TREES_2:def 11;
suppose
A10: not
<*
0 *>
is_a_prefix_of v & (y
. v)
= (e
. v);
A11: (
dom e)
=
{
{} ,
<*
0 *>,
<*1*>} by
FUNCOP_1: 13,
TREES_1: 53;
A12: not ex s st s
in (
dom A) & v
= (
<*
0 *>
^ s) by
A10,
TREES_1: 1;
then
A13: v
in (
dom e) by
A2,
A9,
TREES_1:def 9;
then
A14: v
=
{} by
A7,
A10,
A11,
ENUMSET1:def 1;
reconsider v9 = v as
Element of (
dom e) by
A2,
A9,
A12,
TREES_1:def 9;
A15: (
succ v)
= (
succ v9)
proof
reconsider v99 = v as
Element of (
dom y) by
A5,
A6,
A8,
TREES_1:def 9;
(
succ v99)
= (
succ v9) by
A2,
A3,
A14,
Lm1,
Th8;
hence thesis by
A5,
A6,
A14,
Lm1,
Th8;
end;
now
let x be
object;
thus x
in (
succ v9) implies x
in
{
<*
0 *>,
<*1*>}
proof
assume x
in (
succ v9);
then x
in { (v9
^
<*n*>) : (v9
^
<*n*>)
in (
dom e) } by
TREES_2:def 5;
then
consider n such that
A16: x
= (v9
^
<*n*>) and
A17: (v9
^
<*n*>)
in (
dom e);
<*n*>
in (
dom e) by
A14,
A17,
FINSEQ_1: 34;
then
A18:
<*n*>
=
{} or
<*n*>
=
<*
0 *> or
<*n*>
=
<*1*> by
A11,
ENUMSET1:def 1;
x
=
<*n*> by
A14,
A16,
FINSEQ_1: 34;
hence thesis by
A18,
TARSKI:def 2;
end;
assume x
in
{
<*
0 *>,
<*1*>};
then
A19: x
=
<*
0 *> or x
=
<*1*> by
TARSKI:def 2;
now
per cases by
A14,
A19,
FINSEQ_1: 34;
suppose
A20: x
= (v9
^
<*
0 *>);
then (v9
^
<*
0 *>)
in (
dom e) by
A11,
A19,
ENUMSET1:def 1;
then x
in { (v9
^
<*n*>) : (v9
^
<*n*>)
in (
dom e) } by
A20;
hence x
in (
succ v9) by
TREES_2:def 5;
end;
suppose
A21: x
= (v9
^
<*1*>);
then (v9
^
<*1*>)
in (
dom e) by
A11,
A19,
ENUMSET1:def 1;
then x
in { (v9
^
<*n*>) : (v9
^
<*n*>)
in (
dom e) } by
A21;
hence x
in (
succ v9) by
TREES_2:def 5;
end;
end;
hence x
in (
succ v9);
end;
then
A22: (
succ v9)
=
{
<*
0 *>,
<*1*>} by
TARSKI: 2;
<*
0 *>
<>
<*1*> by
TREES_1: 3;
then
A23: 2
= (
card (
succ v)) by
A22,
A15,
CARD_2: 57;
hence (
branchdeg v)
<= 2 by
TREES_2:def 12;
v
in (
elementary_tree 2) by
A13;
hence thesis by
A7,
A10,
A23,
FUNCOP_1: 7,
TREES_2:def 12;
end;
suppose ex s st s
in (
dom A) & v
= (
<*
0 *>
^ s) & (y
. v)
= (A
. s);
then
consider s such that
A24: s
in (
dom A) and
A25: v
= (
<*
0 *>
^ s) and
A26: (y
. v)
= (A
. s);
reconsider s as
Element of (
dom A) by
A24;
((
succ v),(
succ s))
are_equipotent
proof
reconsider v9 = v as
Element of (
dom y) by
A5,
A6,
A8,
TREES_1:def 9;
((
succ v9),(
succ s))
are_equipotent by
A2,
A3,
A25,
TREES_2: 37;
hence thesis by
A5,
A6,
A25,
Th1,
Th9;
end;
then (
card (
succ v))
= (
card (
succ s)) by
CARD_1: 5;
then
A27: (
branchdeg v)
= (
card (
succ s)) by
TREES_2:def 12;
A28: (
branchdeg s)
<= 2 by
Def5;
hence (
branchdeg v)
<= 2 by
A27,
TREES_2:def 12;
A29: (
branchdeg s)
= 1 implies (A
. s)
=
[1,
0 ] or (A
. s)
=
[1, 1] by
Def5;
A30: (
branchdeg s)
= 2 implies (A
. s)
=
[2,
0 ] by
Def5;
(
branchdeg s)
=
0 implies (A
. s)
=
[
0 ,
0 ] or ex m st (A
. s)
=
[3, m] by
Def5;
hence thesis by
A7,
A26,
A28,
A29,
A30,
A27,
TREES_2:def 12;
end;
end;
hence thesis;
end;
suppose ex s st s
in (
dom B) & v
= (
<*1*>
^ s) & (x
. v)
= (B
. s);
then
consider s such that
A31: s
in (
dom B) and
A32: v
= (
<*1*>
^ s) and
A33: (x
. v)
= (B
. s);
reconsider s as
Element of (
dom B) by
A31;
((
succ v),(
succ s))
are_equipotent by
A5,
A6,
A32,
TREES_2: 37;
then (
card (
succ v))
= (
card (
succ s)) by
CARD_1: 5;
then
A34: (
branchdeg v)
= (
card (
succ s)) by
TREES_2:def 12;
A35: (
branchdeg s)
= 2 implies (B
. s)
=
[2,
0 ] by
Def5;
A36: (
branchdeg s)
= 1 implies (B
. s)
=
[1,
0 ] or (B
. s)
=
[1, 1] by
Def5;
A37: (
branchdeg s)
=
0 implies (B
. s)
=
[
0 ,
0 ] or ex m st (B
. s)
=
[3, m] by
Def5;
(
branchdeg s)
<= 2 by
Def5;
hence thesis by
A33,
A37,
A36,
A35,
A34,
TREES_2:def 12;
end;
end;
hence thesis;
end;
hence thesis by
Def5;
end;
definition
let A;
::
MODAL_1:def8
func
'not' A ->
MP-wff equals (((
elementary_tree 1)
-->
[1,
0 ])
with-replacement (
<*
0 *>,A));
coherence by
Th22;
::
MODAL_1:def9
func
(#) A ->
MP-wff equals (((
elementary_tree 1)
-->
[1, 1])
with-replacement (
<*
0 *>,A));
coherence by
Th23;
let B;
::
MODAL_1:def10
func A
'&' B ->
MP-wff equals ((((
elementary_tree 2)
-->
[2,
0 ])
with-replacement (
<*
0 *>,A))
with-replacement (
<*1*>,B));
coherence by
Th24;
end
definition
let A;
::
MODAL_1:def11
func
? A ->
MP-wff equals (
'not' (
(#) (
'not' A)));
correctness ;
let B;
::
MODAL_1:def12
func A
'or' B ->
MP-wff equals (
'not' ((
'not' A)
'&' (
'not' B)));
correctness ;
::
MODAL_1:def13
func A
=> B ->
MP-wff equals (
'not' (A
'&' (
'not' B)));
correctness ;
end
theorem ::
MODAL_1:30
Th25: ((
elementary_tree
0 )
-->
[3, n]) is
MP-wff
proof
3
in
NAT & n
in
NAT by
ORDINAL1:def 12;
then
reconsider 3n =
[3, n] as
Element of
[:
NAT ,
NAT :] by
ZFMISC_1: 87;
set x = ((
elementary_tree
0 )
--> 3n);
A1: (
dom x)
=
{
{} } by
FUNCOP_1: 13,
TREES_1: 29;
reconsider x as
finite
DecoratedTree of
[:
NAT ,
NAT :];
A2: (
dom x)
= (
elementary_tree
0 ) by
FUNCOP_1: 13;
for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ])
proof
let v be
Element of (
dom x);
A3: (
succ v)
=
{}
proof
set y = the
Element of (
succ v);
assume not thesis;
then y
in (
succ v);
then y
in { (v
^
<*m*>) : (v
^
<*m*>)
in (
dom x) } by
TREES_2:def 5;
then ex m st y
= (v
^
<*m*>) & (v
^
<*m*>)
in (
dom x);
hence contradiction by
A1,
TARSKI:def 1;
end;
hence (
branchdeg v)
<= 2 by
CARD_1: 27,
TREES_2:def 12;
thus (
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex m st (x
. v)
=
[3, m] by
A2,
FUNCOP_1: 7;
thus thesis by
A3,
CARD_1: 27,
TREES_2:def 12;
end;
hence thesis by
Def5;
end;
theorem ::
MODAL_1:31
Th26: ((
elementary_tree
0 )
-->
[
0 ,
0 ]) is
MP-wff
proof
set x = ((
elementary_tree
0 )
-->
[
0 ,
0 ]);
reconsider x as
finite
DecoratedTree of
[:
NAT ,
NAT :];
A1: (
dom x)
=
{
{} } by
FUNCOP_1: 13,
TREES_1: 29;
A2: (
dom x)
= (
elementary_tree
0 ) by
FUNCOP_1: 13;
for v be
Element of (
dom x) holds (
branchdeg v)
<= 2 & ((
branchdeg v)
=
0 implies (x
. v)
=
[
0 ,
0 ] or ex k st (x
. v)
=
[3, k]) & ((
branchdeg v)
= 1 implies (x
. v)
=
[1,
0 ] or (x
. v)
=
[1, 1]) & ((
branchdeg v)
= 2 implies (x
. v)
=
[2,
0 ])
proof
let v be
Element of (
dom x);
A3: (
succ v)
=
{}
proof
set y = the
Element of (
succ v);
assume not thesis;
then y
in (
succ v);
then y
in { (v
^
<*m*>) : (v
^
<*m*>)
in (
dom x) } by
TREES_2:def 5;
then ex m st y
= (v
^
<*m*>) & (v
^
<*m*>)
in (
dom x);
hence contradiction by
A1,
TARSKI:def 1;
end;
hence (
branchdeg v)
<= 2 by
CARD_1: 27,
TREES_2:def 12;
thus thesis by
A2,
A3,
CARD_1: 27,
FUNCOP_1: 7,
TREES_2:def 12;
end;
hence thesis by
Def5;
end;
definition
let p;
::
MODAL_1:def14
func
@ p ->
MP-wff equals ((
elementary_tree
0 )
--> p);
coherence
proof
consider x1,x2 be
object such that
A1: x1
in
{3} and
A2: x2
in
NAT & p
=
[x1, x2] by
ZFMISC_1:def 2;
x1
= 3 by
A1,
TARSKI:def 1;
hence thesis by
A2,
Th25;
end;
end
theorem ::
MODAL_1:32
Th27: (
@ p)
= (
@ q) implies p
= q
proof
assume
A1: (
@ p)
= (
@ q);
A2:
{}
in (
elementary_tree
0 ) by
TREES_1: 22;
then p
= ((
@ p)
.
{} ) by
FUNCOP_1: 7
.= q by
A2,
A1,
FUNCOP_1: 7;
hence thesis;
end;
Lm3:
<*
0 *>
in (
dom ((
elementary_tree 1)
-->
[n, m]))
proof
<*
0 *>
in (
elementary_tree 1) by
TARSKI:def 2,
TREES_1: 51;
hence thesis by
FUNCOP_1: 13;
end;
theorem ::
MODAL_1:33
Th28: (
'not' A)
= (
'not' B) implies A
= B
proof
assume
A1: (
'not' A)
= (
'not' B);
<*
0 *>
in (
dom ((
elementary_tree 1)
-->
[1,
0 ])) by
Lm3;
hence thesis by
A1,
Th7;
end;
theorem ::
MODAL_1:34
Th29: (
(#) A)
= (
(#) B) implies A
= B
proof
set AA = ((
elementary_tree 1)
-->
[1, 1]);
assume
A1: (
(#) A)
= (
(#) B);
<*
0 *>
in (
dom AA) by
Lm3;
hence thesis by
A1,
Th7;
end;
theorem ::
MODAL_1:35
Th30: (A
'&' B)
= (A1
'&' B1) implies A
= A1 & B
= B1
proof
set e = (
elementary_tree 2);
set y = ((e
-->
[2,
0 ])
with-replacement (
<*
0 *>,A));
set y1 = ((e
-->
[2,
0 ])
with-replacement (
<*
0 *>,A1));
assume
A1: (A
'&' B)
= (A1
'&' B1);
A2:
<*1*>
in e by
TREES_1: 28;
A3:
<*
0 *>
in e & (
dom (e
-->
[2,
0 ]))
= e by
FUNCOP_1: 13,
TREES_1: 28;
then
A4: (
dom y1)
= ((
dom (e
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom A1))) by
TREES_2:def 11;
not
<*1*>
is_a_proper_prefix_of
<*
0 *> by
TREES_1: 52;
then
A5:
<*
0 *>
in ((
dom (e
-->
[2,
0 ]))
with-replacement (
<*1*>,(
dom B))) by
A2,
A3,
TREES_1:def 9;
A6: not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 52;
then
A7:
<*1*>
in (
dom y1) by
A2,
A3,
A4,
TREES_1:def 9;
A8: (
dom y)
= ((
dom (e
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
A3,
TREES_2:def 11;
then
A9:
<*1*>
in (
dom y) by
A2,
A3,
A6,
TREES_1:def 9;
then
A10: (
dom (A
'&' B))
= ((
dom y)
with-replacement (
<*1*>,(
dom B))) by
TREES_2:def 11;
A11: (
dom (A1
'&' B1))
= ((
dom y1)
with-replacement (
<*1*>,(
dom B1))) by
A7,
TREES_2:def 11;
now
let s;
thus s
in (
dom B) implies s
in (
dom B1)
proof
assume s
in (
dom B);
then
A12: (
<*1*>
^ s)
in (
dom (A1
'&' B1)) by
A1,
A9,
A10,
TREES_1:def 9;
now
per cases ;
suppose s
=
{} ;
hence thesis by
TREES_1: 22;
end;
suppose s
<>
{} ;
then
<*1*>
is_a_proper_prefix_of (
<*1*>
^ s) by
TREES_1: 10;
then ex w st w
in (
dom B1) & (
<*1*>
^ s)
= (
<*1*>
^ w) by
A7,
A11,
A12,
TREES_1:def 9;
hence thesis by
FINSEQ_1: 33;
end;
end;
hence thesis;
end;
assume s
in (
dom B1);
then
A13: (
<*1*>
^ s)
in (
dom (A
'&' B)) by
A1,
A7,
A11,
TREES_1:def 9;
now
per cases ;
suppose s
=
{} ;
hence s
in (
dom B) by
TREES_1: 22;
end;
suppose s
<>
{} ;
then
<*1*>
is_a_proper_prefix_of (
<*1*>
^ s) by
TREES_1: 10;
then ex w st w
in (
dom B) & (
<*1*>
^ s)
= (
<*1*>
^ w) by
A9,
A10,
A13,
TREES_1:def 9;
hence s
in (
dom B) by
FINSEQ_1: 33;
end;
end;
hence s
in (
dom B);
end;
then
A14: (
dom B)
= (
dom B1) by
TREES_2:def 1;
A15: for s st s
in (
dom B) holds (B
. s)
= (B1
. s)
proof
let s;
assume s
in (
dom B);
then
A16: (
<*1*>
^ s)
in (
dom (A1
'&' B1)) by
A1,
A9,
A10,
TREES_1:def 9;
A17:
<*1*>
is_a_prefix_of (
<*1*>
^ s) by
TREES_1: 1;
then
consider w such that w
in (
dom B1) and
A18: (
<*1*>
^ s)
= (
<*1*>
^ w) and
A19: ((A1
'&' B1)
. (
<*1*>
^ s))
= (B1
. w) by
A7,
A11,
A16,
TREES_2:def 11;
A20: ex u st u
in (
dom B) & (
<*1*>
^ s)
= (
<*1*>
^ u) & ((A
'&' B)
. (
<*1*>
^ s))
= (B
. u) by
A1,
A9,
A10,
A16,
A17,
TREES_2:def 11;
s
= w by
A18,
FINSEQ_1: 33;
hence thesis by
A1,
A19,
A20,
FINSEQ_1: 33;
end;
then
A21: B
= B1 by
A14,
TREES_2: 31;
A22: not (
<*
0 *>,
<*1*>)
are_c=-comparable by
TREES_1: 5;
then
A23: (
dom (A
'&' B))
= (((
dom (e
-->
[2,
0 ]))
with-replacement (
<*1*>,(
dom B)))
with-replacement (
<*
0 *>,(
dom A))) by
A2,
A3,
A8,
A10,
TREES_2: 8;
A24: (
dom (A1
'&' B1))
= (((
dom (e
-->
[2,
0 ]))
with-replacement (
<*1*>,(
dom B)))
with-replacement (
<*
0 *>,(
dom A1))) by
A22,
A2,
A3,
A4,
A11,
A14,
TREES_2: 8;
then
A25: (
dom A)
= (
dom A1) by
A1,
A5,
A23,
Th6;
for s st s
in (
dom A) holds (A
. s)
= (A1
. s)
proof
let s;
assume
A26: s
in (
dom A);
then
A27: (
<*
0 *>
^ s)
in (
dom y) by
A3,
A8,
TREES_1:def 9;
A28:
<*
0 *>
is_a_prefix_of (
<*
0 *>
^ s) by
TREES_1: 1;
then
A29: ex w st w
in (
dom A) & (
<*
0 *>
^ s)
= (
<*
0 *>
^ w) & (y
. (
<*
0 *>
^ s))
= (A
. w) by
A3,
A8,
A27,
TREES_2:def 11;
(
<*
0 *>
^ s)
in (
dom y1) by
A3,
A4,
A25,
A26,
TREES_1:def 9;
then
A30: ex u st u
in (
dom A1) & (
<*
0 *>
^ s)
= (
<*
0 *>
^ u) & (y1
. (
<*
0 *>
^ s))
= (A1
. u) by
A3,
A4,
A28,
TREES_2:def 11;
not
<*1*>
is_a_proper_prefix_of (
<*
0 *>
^ s) by
Th2;
then
A31: (
<*
0 *>
^ s)
in (
dom (A
'&' B)) by
A9,
A10,
A27,
TREES_1:def 9;
not ex w st w
in (
dom B) & (
<*
0 *>
^ s)
= (
<*1*>
^ w) & ((A
'&' B)
. (
<*
0 *>
^ s))
= (B
. w) by
TREES_1: 1,
TREES_1: 50;
then ((A
'&' B)
. (
<*
0 *>
^ s))
= (y
. (
<*
0 *>
^ s)) by
A9,
A10,
A31,
TREES_2:def 11;
then
A32: (A
. s)
= ((A1
'&' B)
. (
<*
0 *>
^ s)) by
A1,
A21,
A29,
FINSEQ_1: 33;
not ex w st w
in (
dom B1) & (
<*
0 *>
^ s)
= (
<*1*>
^ w) & ((A1
'&' B1)
. (
<*
0 *>
^ s))
= (B1
. w) by
TREES_1: 1,
TREES_1: 50;
then ((A1
'&' B1)
. (
<*
0 *>
^ s))
= (y1
. (
<*
0 *>
^ s)) by
A1,
A7,
A11,
A31,
TREES_2:def 11;
hence thesis by
A21,
A32,
A30,
FINSEQ_1: 33;
end;
hence thesis by
A1,
A5,
A14,
A23,
A24,
A15,
Th6,
TREES_2: 31;
end;
definition
::
MODAL_1:def15
func
VERUM ->
MP-wff equals ((
elementary_tree
0 )
-->
[
0 ,
0 ]);
coherence by
Th26;
end
theorem ::
MODAL_1:36
Th31: (
card (
dom A))
= 1 implies A
=
VERUM or ex p st A
= (
@ p)
proof
assume (
card (
dom A))
= 1;
then
consider x be
object such that
A1: (
dom A)
=
{x} by
CARD_2: 42;
reconsider x as
Element of (
dom A) by
A1,
TARSKI:def 1;
A2:
{}
in (
dom A) by
TREES_1: 22;
then
A3: (
dom A)
= (
elementary_tree
0 ) by
A1,
TARSKI:def 1,
TREES_1: 29;
A4: (
dom A)
=
{
{} } by
A2,
A1,
TARSKI:def 1;
(
succ x)
=
{}
proof
set y = the
Element of (
succ x);
assume not thesis;
then
A5: y
in (
succ x);
(
succ x)
= { (x
^
<*n*>) : (x
^
<*n*>)
in (
dom A) } by
TREES_2:def 5;
then ex n st y
= (x
^
<*n*>) & (x
^
<*n*>)
in (
dom A) by
A5;
hence contradiction by
A4,
TARSKI:def 1;
end;
then
A6: (
branchdeg x)
=
0 by
CARD_1: 27,
TREES_2:def 12;
now
per cases by
A6,
Def5;
suppose (A
. x)
=
[
0 ,
0 ];
then for z be
object holds z
in (
dom A) implies (A
. z)
=
[
0 ,
0 ] by
A1,
TARSKI:def 1;
hence thesis by
A3,
FUNCOP_1: 11;
end;
suppose ex n st (A
. x)
=
[3, n];
then
consider n such that
A7: (A
. x)
=
[3, n];
3
in
NAT & n
in
NAT by
ORDINAL1:def 12;
then
reconsider p =
[3, n] as
MP-variable by
ZFMISC_1: 105;
for z be
object holds z
in (
dom A) implies (A
. z)
=
[3, n] by
A1,
A7,
TARSKI:def 1;
then A
= (
@ p) by
A3,
FUNCOP_1: 11;
hence thesis;
end;
end;
hence thesis;
end;
theorem ::
MODAL_1:37
Th32: (
card (
dom A))
>= 2 implies (ex B st A
= (
'not' B) or A
= (
(#) B)) or ex B, C st A
= (B
'&' C)
proof
set b = (
branchdeg (
Root (
dom A)));
set a = (
Root (
dom A));
assume
A1: (
card (
dom A))
>= 2;
A2:
now
assume b
=
0 ;
then (
card (
dom A))
= 1 by
Th12;
hence contradiction by
A1;
end;
A3: b
<= 2 by
Def5;
now
b
=
0 or ... or b
= 2 by
A3,
NAT_1: 60;
per cases by
A2;
case
A4: b
= 1;
then (
card (
succ a))
= 1 by
TREES_2:def 12;
then
consider x be
object such that
A5: (
succ a)
=
{x} by
CARD_2: 42;
x
in (
succ a) by
A5,
TARSKI:def 1;
then
reconsider x9 = x as
Element of (
dom A);
take B = (A
| x9);
now
per cases by
A4,
Def5;
suppose (A
. a)
=
[1,
0 ];
then (
Root A)
=
[1,
0 ];
hence A
= (
'not' B) or A
= (
(#) B) by
A5,
Th18;
end;
suppose (A
. a)
=
[1, 1];
then (
Root A)
=
[1, 1];
hence A
= (
'not' B) or A
= (
(#) B) by
A5,
Th18;
end;
end;
hence thesis;
end;
case
A6: b
= 2;
then
A7: (
succ a)
=
{
<*
0 *>,
<*1*>} by
Th14;
then
<*
0 *>
in (
succ a) &
<*1*>
in (
succ a) by
TARSKI:def 2;
then
reconsider x =
<*
0 *>, y =
<*1*> as
Element of (
dom A);
take B = (A
| x);
take C = (A
| y);
(
Root A)
=
[2,
0 ] by
A6,
Def5;
then A
= (B
'&' C) by
A7,
Th20;
hence thesis;
end;
end;
hence thesis;
end;
theorem ::
MODAL_1:38
Th33: (
card (
dom A))
< (
card (
dom (
'not' A)))
proof
set e = (
elementary_tree 1);
<*
0 *>
in e by
TARSKI:def 2,
TREES_1: 51;
then
A1:
<*
0 *>
in (
dom (e
-->
[1,
0 ])) by
FUNCOP_1: 13;
then
A2: (
dom (
'not' A))
= ((
dom (e
-->
[1,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
then
reconsider o =
<*
0 *> as
Element of (
dom (
'not' A)) by
A1,
TREES_1:def 9;
now
let s;
thus s
in (
dom A) implies (o
^ s)
in (
dom (
'not' A)) by
A1,
A2,
TREES_1:def 9;
assume
A3: (o
^ s)
in (
dom (
'not' A));
now
per cases ;
suppose s
=
{} ;
hence s
in (
dom A) by
TREES_1: 22;
end;
suppose s
<>
{} ;
then o
is_a_proper_prefix_of (o
^ s) by
TREES_1: 10;
then ex w st w
in (
dom A) & (o
^ s)
= (o
^ w) by
A1,
A2,
A3,
TREES_1:def 9;
hence s
in (
dom A) by
FINSEQ_1: 33;
end;
end;
hence s
in (
dom A);
end;
then
A4: (
dom A)
= ((
dom (
'not' A))
| o) by
TREES_1:def 6;
o
<> (
Root (
dom (
'not' A)));
hence thesis by
A4,
Th16;
end;
theorem ::
MODAL_1:39
Th34: (
card (
dom A))
< (
card (
dom (
(#) A)))
proof
set e = (
elementary_tree 1);
<*
0 *>
in e by
TARSKI:def 2,
TREES_1: 51;
then
A1:
<*
0 *>
in (
dom (e
-->
[1, 1])) by
FUNCOP_1: 13;
then
A2: (
dom (
(#) A))
= ((
dom (e
-->
[1, 1]))
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
then
reconsider o =
<*
0 *> as
Element of (
dom (
(#) A)) by
A1,
TREES_1:def 9;
now
let s;
thus s
in (
dom A) implies (o
^ s)
in (
dom (
(#) A)) by
A1,
A2,
TREES_1:def 9;
assume
A3: (o
^ s)
in (
dom (
(#) A));
now
per cases ;
suppose s
=
{} ;
hence s
in (
dom A) by
TREES_1: 22;
end;
suppose s
<>
{} ;
then o
is_a_proper_prefix_of (o
^ s) by
TREES_1: 10;
then ex w st w
in (
dom A) & (o
^ s)
= (o
^ w) by
A1,
A2,
A3,
TREES_1:def 9;
hence s
in (
dom A) by
FINSEQ_1: 33;
end;
end;
hence s
in (
dom A);
end;
then
A4: (
dom A)
= ((
dom (
(#) A))
| o) by
TREES_1:def 6;
o
<> (
Root (
dom (
(#) A)));
hence thesis by
A4,
Th16;
end;
theorem ::
MODAL_1:40
Th35: (
card (
dom A))
< (
card (
dom (A
'&' B))) & (
card (
dom B))
< (
card (
dom (A
'&' B)))
proof
set e = (
elementary_tree 2);
set y = ((e
-->
[2,
0 ])
with-replacement (
<*
0 *>,A));
A1: not
<*1*>
is_a_proper_prefix_of
<*
0 *> by
TREES_1: 52;
A2:
<*
0 *>
in e & (
dom (e
-->
[2,
0 ]))
= e by
FUNCOP_1: 13,
TREES_1: 28;
then
A3: (
dom y)
= ((
dom (e
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
<*1*>
in e & not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 28,
TREES_1: 52;
then
A4:
<*1*>
in (
dom y) by
A2,
A3,
TREES_1:def 9;
then
A5: (
dom (A
'&' B))
= ((
dom y)
with-replacement (
<*1*>,(
dom B))) by
TREES_2:def 11;
then
reconsider u =
<*1*> as
Element of (
dom (A
'&' B)) by
A4,
TREES_1:def 9;
<*
0 *>
in (
dom y) by
A2,
A3,
TREES_1:def 9;
then
reconsider o =
<*
0 *> as
Element of (
dom (A
'&' B)) by
A4,
A5,
A1,
TREES_1:def 9;
now
let s;
thus s
in (
dom A) implies (o
^ s)
in (
dom (A
'&' B))
proof
assume s
in (
dom A);
then
A6: (o
^ s)
in (
dom y) by
A2,
A3,
TREES_1:def 9;
not
<*1*>
is_a_proper_prefix_of (o
^ s) by
Th2;
hence thesis by
A4,
A5,
A6,
TREES_1:def 9;
end;
assume
A7: (o
^ s)
in (
dom (A
'&' B));
now
per cases ;
suppose s
=
{} ;
hence s
in (
dom A) by
TREES_1: 22;
end;
suppose
A8: s
<>
{} ;
not ex w st w
in (
dom B) & (o
^ s)
= (
<*1*>
^ w) by
TREES_1: 1,
TREES_1: 50;
then
A9: (o
^ s)
in (
dom y) by
A4,
A5,
A7,
TREES_1:def 9;
o
is_a_proper_prefix_of (o
^ s) by
A8,
TREES_1: 10;
then ex w st w
in (
dom A) & (o
^ s)
= (o
^ w) by
A2,
A3,
A9,
TREES_1:def 9;
hence s
in (
dom A) by
FINSEQ_1: 33;
end;
end;
hence s
in (
dom A);
end;
then
A10: (
dom A)
= ((
dom (A
'&' B))
| o) by
TREES_1:def 6;
now
let s;
thus s
in (
dom B) implies (u
^ s)
in (
dom (A
'&' B)) by
A4,
A5,
TREES_1:def 9;
assume
A11: (u
^ s)
in (
dom (A
'&' B));
now
per cases ;
suppose s
=
{} ;
hence s
in (
dom B) by
TREES_1: 22;
end;
suppose s
<>
{} ;
then
<*1*>
is_a_proper_prefix_of (u
^ s) by
TREES_1: 10;
then ex w st w
in (
dom B) & (u
^ s)
= (
<*1*>
^ w) by
A4,
A5,
A11,
TREES_1:def 9;
hence s
in (
dom B) by
FINSEQ_1: 33;
end;
end;
hence s
in (
dom B);
end;
then
A12: (
dom B)
= ((
dom (A
'&' B))
| u) by
TREES_1:def 6;
o
<> (
Root (
dom (A
'&' B)));
hence (
card (
dom A))
< (
card (
dom (A
'&' B))) by
A10,
Th16;
u
<> (
Root (
dom (A
'&' B)));
hence thesis by
A12,
Th16;
end;
definition
let IT be
MP-wff;
::
MODAL_1:def16
attr IT is
atomic means
:
Def16: ex p st IT
= (
@ p);
::
MODAL_1:def17
attr IT is
negative means
:
Def17: ex A st IT
= (
'not' A);
::
MODAL_1:def18
attr IT is
necessitive means
:
Def18: ex A st IT
= (
(#) A);
::
MODAL_1:def19
attr IT is
conjunctive means
:
Def19: ex A, B st IT
= (A
'&' B);
end
registration
cluster
atomic for
MP-wff;
existence
proof
reconsider p =
[3,
0 ] as
MP-variable by
ZFMISC_1: 105;
take (
@ p);
take p;
thus thesis;
end;
cluster
negative for
MP-wff;
existence
proof
set A =
VERUM ;
take (
'not' A);
take A;
thus thesis;
end;
cluster
necessitive for
MP-wff;
existence
proof
set A =
VERUM ;
take (
(#) A);
take A;
thus thesis;
end;
cluster
conjunctive for
MP-wff;
existence
proof
set B =
VERUM ;
set A =
VERUM ;
take (A
'&' B);
take B;
take A;
thus thesis;
end;
end
scheme ::
MODAL_1:sch1
MPInd { Prop[
Element of
MP-WFF ] } :
for A be
Element of
MP-WFF holds Prop[A]
provided
A1: Prop[
VERUM ]
and
A2: for p be
MP-variable holds Prop[(
@ p)]
and
A3: for A be
Element of
MP-WFF st Prop[A] holds Prop[(
'not' A)]
and
A4: for A be
Element of
MP-WFF st Prop[A] holds Prop[(
(#) A)]
and
A5: for A,B be
Element of
MP-WFF st Prop[A] & Prop[B] holds Prop[(A
'&' B)];
defpred
P[
Nat] means for A st (
card (
dom A))
<= $1 holds Prop[A];
A6: for k st
P[k] holds
P[(k
+ 1)]
proof
let k such that
A7: for A st (
card (
dom A))
<= k holds Prop[A];
let A such that
A8: (
card (
dom A))
<= (k
+ 1);
set a = (
Root (
dom A));
set b = (
branchdeg a);
A9: b
<= 2 by
Def5;
now
b
=
0 or ... or b
= 2 by
A9,
NAT_1: 60;
per cases ;
suppose b
=
0 ;
then
A10: (
card (
dom A))
= 1 by
Th12;
now
per cases by
A10,
Th31;
suppose A
=
VERUM ;
hence thesis by
A1;
end;
suppose ex p st A
= (
@ p);
hence thesis by
A2;
end;
end;
hence thesis;
end;
suppose
A11: b
= 1;
then
A12: (
succ a)
=
{
<*
0 *>} by
Th13;
then
<*
0 *>
in (
succ a) by
TARSKI:def 1;
then
reconsider o =
<*
0 *> as
Element of (
dom A);
A13: A
= (((
elementary_tree 1)
--> (
Root A))
with-replacement (
<*
0 *>,(A
| o))) by
A12,
Th18;
now
per cases by
A11,
Def5;
suppose
A14: (A
. a)
=
[1,
0 ];
(
dom (A
| o))
= ((
dom A)
| o) & o
<> (
Root (
dom A)) by
TREES_2:def 10;
then (
card (
dom (A
| o)))
< (k
+ 1) by
A8,
Th16,
XXREAL_0: 2;
then
A15: (
card (
dom (A
| o)))
<= k by
NAT_1: 13;
A
= (
'not' (A
| o)) by
A13,
A14;
hence thesis by
A3,
A7,
A15;
end;
suppose
A16: (A
. a)
=
[1, 1];
(
dom (A
| o))
= ((
dom A)
| o) & o
<> (
Root (
dom A)) by
TREES_2:def 10;
then (
card (
dom (A
| o)))
< (k
+ 1) by
A8,
Th16,
XXREAL_0: 2;
then
A17: (
card (
dom (A
| o)))
<= k by
NAT_1: 13;
A
= (
(#) (A
| o)) by
A13,
A16;
hence thesis by
A4,
A7,
A17;
end;
end;
hence thesis;
end;
suppose
A18: b
= 2;
then
A19: (
succ a)
=
{
<*
0 *>,
<*1*>} by
Th14;
then
<*
0 *>
in (
succ a) &
<*1*>
in (
succ a) by
TARSKI:def 2;
then
reconsider o1 =
<*
0 *>, o2 =
<*1*> as
Element of (
dom A);
(
dom (A
| o1))
= ((
dom A)
| o1) & o1
<> (
Root (
dom A)) by
TREES_2:def 10;
then (
card (
dom (A
| o1)))
< (k
+ 1) by
A8,
Th16,
XXREAL_0: 2;
then (
card (
dom (A
| o1)))
<= k by
NAT_1: 13;
then
A20: Prop[(A
| o1)] by
A7;
(
dom (A
| o2))
= ((
dom A)
| o2) & o2
<> (
Root (
dom A)) by
TREES_2:def 10;
then (
card (
dom (A
| o2)))
< (k
+ 1) by
A8,
Th16,
XXREAL_0: 2;
then (
card (
dom (A
| o2)))
<= k by
NAT_1: 13;
then
A21: Prop[(A
| o2)] by
A7;
A
= ((((
elementary_tree 2)
--> (
Root A))
with-replacement (
<*
0 *>,(A
| o1)))
with-replacement (
<*1*>,(A
| o2))) by
A19,
Th20;
then A
= ((A
| o1)
'&' (A
| o2)) by
A18,
Def5;
hence thesis by
A5,
A20,
A21;
end;
end;
hence thesis;
end;
let A;
A22: (
card (
dom A))
<= (
card (
dom A));
A23:
P[
0 ] by
NAT_1: 2;
for n holds
P[n] from
NAT_1:sch 2(
A23,
A6);
hence thesis by
A22;
end;
theorem ::
MODAL_1:41
for A be
Element of
MP-WFF holds A
=
VERUM or A is
atomic
MP-wff or A is
negative
MP-wff or A is
necessitive
MP-wff or A is
conjunctive
MP-wff
proof
defpred
Prop[
Element of
MP-WFF ] means $1
=
VERUM or $1 is
atomic
MP-wff or $1 is
negative
MP-wff or $1 is
necessitive
MP-wff or $1 is
conjunctive
MP-wff;
A1:
Prop[
VERUM ];
A2: for A be
Element of
MP-WFF st
Prop[A] holds
Prop[(
'not' A)] by
Def17;
A3: for A,B be
Element of
MP-WFF st
Prop[A] &
Prop[B] holds
Prop[(A
'&' B)] by
Def19;
A4: for A be
Element of
MP-WFF st
Prop[A] holds
Prop[(
(#) A)] by
Def18;
A5: for p be
MP-variable holds
Prop[(
@ p)] by
Def16;
thus for A be
Element of
MP-WFF holds
Prop[A] from
MPInd(
A1,
A5,
A2,
A4,
A3);
end;
theorem ::
MODAL_1:42
Th37: A
=
VERUM or (ex p st A
= (
@ p)) or (ex B st A
= (
'not' B)) or (ex B st A
= (
(#) B)) or ex B, C st A
= (B
'&' C)
proof
now
per cases by
NAT_1: 25;
suppose (
card (
dom A))
= 1;
hence thesis by
Th31;
end;
suppose (
card (
dom A))
> 1;
then (
card (
dom A))
>= (1
+ 1) by
NAT_1: 13;
hence thesis by
Th32;
end;
end;
hence thesis;
end;
theorem ::
MODAL_1:43
Th38: (
@ p)
<> (
'not' A) & (
@ p)
<> (
(#) A) & (
@ p)
<> (A
'&' B)
proof
set e2 = (
elementary_tree 2);
set e1 = (
elementary_tree 1);
set e0 = (
elementary_tree
0 );
A1: (
dom (
@ p))
= e0 by
FUNCOP_1: 13;
A2:
<*
0 *>
in e1 by
TARSKI:def 2,
TREES_1: 51;
(
dom (e1
-->
[1,
0 ]))
= e1 by
FUNCOP_1: 13;
then (
dom (
'not' A))
= (e1
with-replacement (
<*
0 *>,(
dom A))) by
A2,
TREES_2:def 11;
then
<*
0 *>
in (
dom (
'not' A)) by
A2,
TREES_1:def 9;
hence (
@ p)
<> (
'not' A) by
A1,
TARSKI:def 1,
TREES_1: 29;
(
dom (e1
-->
[1, 1]))
= e1 by
FUNCOP_1: 13;
then (
dom (
(#) A))
= (e1
with-replacement (
<*
0 *>,(
dom A))) by
A2,
TREES_2:def 11;
then
<*
0 *>
in (
dom (
(#) A)) by
A2,
TREES_1:def 9;
hence (
@ p)
<> (
(#) A) by
A1,
TARSKI:def 1,
TREES_1: 29;
set y = ((e2
-->
[2,
0 ])
with-replacement (
<*
0 *>,A));
A3:
<*1*>
in e2 & not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 28,
TREES_1: 52;
A4:
<*
0 *>
in e2 & (
dom (e2
-->
[2,
0 ]))
= e2 by
FUNCOP_1: 13,
TREES_1: 28;
then (
dom y)
= ((
dom (e2
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
then
A5:
<*1*>
in (
dom y) by
A4,
A3,
TREES_1:def 9;
then (
dom (A
'&' B))
= ((
dom y)
with-replacement (
<*1*>,(
dom B))) by
TREES_2:def 11;
then
<*1*>
in (
dom (A
'&' B)) by
A5,
TREES_1:def 9;
hence thesis by
A1,
TARSKI:def 1,
TREES_1: 29;
end;
theorem ::
MODAL_1:44
Th39: (
'not' A)
<> (
(#) B) & (
'not' A)
<> (B
'&' C)
proof
set e2 = (
elementary_tree 2);
set e1 = (
elementary_tree 1);
set E = (e1
-->
[1,
0 ]);
set F = (e1
-->
[1, 1]);
reconsider e =
{} as
Element of (
dom (
'not' A)) by
TREES_1: 22;
A1:
{}
in (
dom (
(#) B)) & not ex u st u
in (
dom B) & e
= (
<*
0 *>
^ u) & ((
(#) B)
. e)
= (B
. u) by
TREES_1: 22;
A2:
<*
0 *>
in e1 by
TARSKI:def 2,
TREES_1: 51;
then
A3:
<*
0 *>
in (
dom E) by
FUNCOP_1: 13;
then
A4: (
dom (
'not' A))
= ((
dom E)
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
A5:
<*
0 *>
in (
dom F) by
A2,
FUNCOP_1: 13;
then (
dom (
(#) B))
= ((
dom F)
with-replacement (
<*
0 *>,(
dom B))) by
TREES_2:def 11;
then
A6: ((
(#) B)
. e)
= (F
. e) by
A5,
A1,
TREES_2:def 11;
e
in e1 by
TREES_1: 22;
then
A7: (E
. e)
=
[1,
0 ] & (F
. e)
=
[1, 1] by
FUNCOP_1: 7;
( not ex u st u
in (
dom A) & e
= (
<*
0 *>
^ u) & ((
'not' A)
. e)
= (A
. u)) &
[1,
0 ]
<>
[1, 1] by
XTUPLE_0: 1;
hence (
'not' A)
<> (
(#) B) by
A3,
A4,
A6,
A7,
TREES_2:def 11;
set y = ((e2
-->
[2,
0 ])
with-replacement (
<*
0 *>,B));
A8:
<*1*>
in e2 & not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 28,
TREES_1: 52;
A9:
<*
0 *>
in e2 & (
dom (e2
-->
[2,
0 ]))
= e2 by
FUNCOP_1: 13,
TREES_1: 28;
then (
dom y)
= ((
dom (e2
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom B))) by
TREES_2:def 11;
then
A10:
<*1*>
in (
dom y) by
A9,
A8,
TREES_1:def 9;
then (
dom (B
'&' C))
= ((
dom y)
with-replacement (
<*1*>,(
dom C))) by
TREES_2:def 11;
then
A11:
<*1*>
in (
dom (B
'&' C)) by
A10,
TREES_1:def 9;
A12:
now
assume
<*1*>
in (
dom E);
then
<*1*>
=
{} or
<*1*>
=
<*
0 *> by
TARSKI:def 2,
TREES_1: 51;
hence contradiction by
TREES_1: 3;
end;
assume not thesis;
then ex s st s
in (
dom A) &
<*1*>
= (
<*
0 *>
^ s) by
A3,
A4,
A11,
A12,
TREES_1:def 9;
then
<*
0 *>
is_a_prefix_of
<*1*> by
TREES_1: 1;
hence contradiction by
TREES_1: 3;
end;
theorem ::
MODAL_1:45
Th40: (
(#) A)
<> (B
'&' C)
proof
set e2 = (
elementary_tree 2);
set e1 = (
elementary_tree 1);
set F = (e1
-->
[1, 1]);
set y = ((e2
-->
[2,
0 ])
with-replacement (
<*
0 *>,B));
A1:
<*1*>
in e2 & not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 28,
TREES_1: 52;
A2:
<*
0 *>
in e2 & (
dom (e2
-->
[2,
0 ]))
= e2 by
FUNCOP_1: 13,
TREES_1: 28;
then (
dom y)
= ((
dom (e2
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom B))) by
TREES_2:def 11;
then
A3:
<*1*>
in (
dom y) by
A2,
A1,
TREES_1:def 9;
then (
dom (B
'&' C))
= ((
dom y)
with-replacement (
<*1*>,(
dom C))) by
TREES_2:def 11;
then
A4:
<*1*>
in (
dom (B
'&' C)) by
A3,
TREES_1:def 9;
assume
A5: not thesis;
A6:
now
assume
<*1*>
in (
dom F);
then
<*1*>
=
{} or
<*1*>
=
<*
0 *> by
TARSKI:def 2,
TREES_1: 51;
hence contradiction by
TREES_1: 3;
end;
<*
0 *>
in e1 by
TARSKI:def 2,
TREES_1: 51;
then
A7:
<*
0 *>
in (
dom F) by
FUNCOP_1: 13;
then (
dom (
(#) A))
= ((
dom F)
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
then ex s st s
in (
dom A) &
<*1*>
= (
<*
0 *>
^ s) by
A7,
A4,
A6,
A5,
TREES_1:def 9;
then
<*
0 *>
is_a_prefix_of
<*1*> by
TREES_1: 1;
hence contradiction by
TREES_1: 3;
end;
Lm4:
VERUM
<> (
'not' A) &
VERUM
<> (
(#) A) &
VERUM
<> (A
'&' B)
proof
set e2 = (
elementary_tree 2);
set e1 = (
elementary_tree 1);
A1: (
dom
VERUM )
= (
elementary_tree
0 ) by
FUNCOP_1: 13;
set F = (e1
-->
[1, 1]);
set E = (e1
-->
[1,
0 ]);
A2:
<*
0 *>
in e1 by
TARSKI:def 2,
TREES_1: 51;
then
<*
0 *>
in (
dom E) by
FUNCOP_1: 13;
then (
dom E)
= e1 & (
dom (
'not' A))
= ((
dom E)
with-replacement (
<*
0 *>,(
dom A))) by
FUNCOP_1: 13,
TREES_2:def 11;
then
<*
0 *>
in (
dom (
'not' A)) by
A2,
TREES_1:def 9;
hence
VERUM
<> (
'not' A) by
A1,
TARSKI:def 1,
TREES_1: 29;
<*
0 *>
in (
dom F) by
A2,
FUNCOP_1: 13;
then (
dom F)
= e1 & (
dom (
(#) A))
= ((
dom F)
with-replacement (
<*
0 *>,(
dom A))) by
FUNCOP_1: 13,
TREES_2:def 11;
then
<*
0 *>
in (
dom (
(#) A)) by
A2,
TREES_1:def 9;
hence
VERUM
<> (
(#) A) by
A1,
TARSKI:def 1,
TREES_1: 29;
set y = ((e2
-->
[2,
0 ])
with-replacement (
<*
0 *>,A));
A3:
<*1*>
in e2 & not
<*
0 *>
is_a_proper_prefix_of
<*1*> by
TREES_1: 28,
TREES_1: 52;
A4:
<*
0 *>
in e2 & (
dom (e2
-->
[2,
0 ]))
= e2 by
FUNCOP_1: 13,
TREES_1: 28;
then (
dom y)
= ((
dom (e2
-->
[2,
0 ]))
with-replacement (
<*
0 *>,(
dom A))) by
TREES_2:def 11;
then
A5:
<*1*>
in (
dom y) by
A4,
A3,
TREES_1:def 9;
then (
dom (A
'&' B))
= ((
dom y)
with-replacement (
<*1*>,(
dom B))) by
TREES_2:def 11;
then
A6:
<*1*>
in (
dom (A
'&' B)) by
A5,
TREES_1:def 9;
assume not thesis;
hence contradiction by
A1,
A6,
TARSKI:def 1,
TREES_1: 29;
end;
Lm5:
[
0 ,
0 ] is
MP-conective
proof
0
in
{
0 , 1, 2} by
ENUMSET1:def 1;
hence thesis by
ZFMISC_1: 87;
end;
Lm6:
VERUM
<> (
@ p)
proof
assume
A1: not thesis;
(
rng (
@ p))
=
{p} & (
rng
VERUM )
=
{
[
0 ,
0 ]} by
FUNCOP_1: 8;
then
[
0 ,
0 ]
in
{p} by
A1,
TARSKI:def 1;
hence contradiction by
Lm5,
Th21,
XBOOLE_0: 3;
end;
theorem ::
MODAL_1:46
VERUM
<> (
@ p) &
VERUM
<> (
'not' A) &
VERUM
<> (
(#) A) &
VERUM
<> (A
'&' B) by
Lm4,
Lm6;
scheme ::
MODAL_1:sch2
MPFuncEx { D() -> non
empty
set , d() ->
Element of D() , F(
Element of
MP-variables ) ->
Element of D() , N,H(
Element of D()) ->
Element of D() , C(
Element of D(),
Element of D()) ->
Element of D() } :
ex f be
Function of
MP-WFF , D() st (f
.
VERUM )
= d() & (for p be
MP-variable holds (f
. (
@ p))
= F(p)) & (for A be
Element of
MP-WFF holds (f
. (
'not' A))
= N(.)) & (for A be
Element of
MP-WFF holds (f
. (
(#) A))
= H(.)) & for A,B be
Element of
MP-WFF holds (f
. (A
'&' B))
= C(.,.);
defpred
Pfn[
Function of
MP-WFF , D(),
Nat] means for A st (
card (
dom A))
<= $2 holds (A
=
VERUM implies ($1
. A)
= d()) & (for p st A
= (
@ p) holds ($1
. A)
= F(p)) & (for B st A
= (
'not' B) holds ($1
. A)
= N(.)) & (for B st A
= (
(#) B) holds ($1
. A)
= H(.)) & (for B, C st A
= (B
'&' C) holds ($1
. A)
= C(.,.));
defpred
Pfgp[
Element of D(),
Function of
MP-WFF , D(),
Element of
MP-WFF ] means ($3
=
VERUM implies $1
= d()) & (for p st $3
= (
@ p) holds $1
= F(p)) & (for A st $3
= (
'not' A) holds $1
= N(.)) & (for A st $3
= (
(#) A) holds $1
= H(.)) & (for A, B st $3
= (A
'&' B) holds $1
= C(.,.));
defpred
P[
Nat] means ex F be
Function of
MP-WFF , D() st
Pfn[F, $1];
defpred
Qfn[
object,
object] means ex A be
Element of
MP-WFF st A
= $1 & for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom A))] holds $2
= (g
. A);
A1: for k st
P[k] holds
P[(k
+ 1)]
proof
let k;
given F be
Function of
MP-WFF , D() such that
A2:
Pfn[F, k];
defpred
Q[
Element of
MP-WFF ,
Element of D()] means ((
card (
dom $1))
<> (k
+ 1) implies $2
= (F
. $1)) & ((
card (
dom $1))
= (k
+ 1) implies
Pfgp[$2, F, $1]);
A3: for x be
Element of
MP-WFF holds ex y be
Element of D() st
Q[x, y]
proof
let A be
Element of
MP-WFF ;
now
per cases by
Th37;
case (
card (
dom A))
<> (k
+ 1);
take y = (F
. A);
end;
case
A4: (
card (
dom A))
= (k
+ 1) & A
=
VERUM ;
take y = d();
thus
Pfgp[y, F, A] by
A4,
Lm4,
Lm6;
end;
case (
card (
dom A))
= (k
+ 1) & ex p st A
= (
@ p);
then
consider p such that
A5: A
= (
@ p);
take y = F(p);
thus
Pfgp[y, F, A] by
A5,
Lm6,
Th27,
Th38;
end;
case (
card (
dom A))
= (k
+ 1) & ex B st A
= (
'not' B);
then
consider B such that
A6: A
= (
'not' B);
take y = N(.);
thus
Pfgp[y, F, A] by
A6,
Lm4,
Th28,
Th38,
Th39;
end;
case (
card (
dom A))
= (k
+ 1) & ex B st A
= (
(#) B);
then
consider B such that
A7: A
= (
(#) B);
take y = H(.);
thus
Pfgp[y, F, A] by
A7,
Lm4,
Th29,
Th38,
Th39,
Th40;
end;
case (
card (
dom A))
= (k
+ 1) & ex B, C st A
= (B
'&' C);
then
consider B, C such that
A8: A
= (B
'&' C);
take y = C(.,.);
now
let B1, C1;
assume
A9: A
= (B1
'&' C1);
then B
= B1 by
A8,
Th30;
hence y
= C(.,.) by
A8,
A9,
Th30;
end;
hence
Pfgp[y, F, A] by
A8,
Lm4,
Th38,
Th39,
Th40;
end;
end;
hence thesis;
end;
consider G be
Function of
MP-WFF , D() such that
A10: for p be
Element of
MP-WFF holds
Q[p, (G
. p)] from
FUNCT_2:sch 3(
A3);
take H = G;
thus
Pfn[H, (k
+ 1)]
proof
let A be
Element of
MP-WFF ;
set p = (
card (
dom A));
assume
A11: p
<= (k
+ 1);
thus A
=
VERUM implies (H
. A)
= d()
proof
per cases ;
suppose p
<> (k
+ 1);
then p
<= k & (H
. A)
= (F
. A) by
A10,
A11,
NAT_1: 8;
hence thesis by
A2;
end;
suppose p
= (k
+ 1);
hence thesis by
A10;
end;
end;
thus for p st A
= (
@ p) holds (H
. A)
= F(p)
proof
let q such that
A12: A
= (
@ q);
per cases ;
suppose p
<> (k
+ 1);
then p
<= k & (H
. A)
= (F
. A) by
A10,
A11,
NAT_1: 8;
hence thesis by
A2,
A12;
end;
suppose p
= (k
+ 1);
hence thesis by
A10,
A12;
end;
end;
thus for B st A
= (
'not' B) holds (H
. A)
= N(.)
proof
let B;
assume
A13: A
= (
'not' B);
then (
card (
dom B))
<> (k
+ 1) by
A11,
Th33;
then
A14: (H
. B)
= (F
. B) by
A10;
per cases ;
suppose p
<> (k
+ 1);
then p
<= k & (H
. A)
= (F
. A) by
A10,
A11,
NAT_1: 8;
hence thesis by
A2,
A13,
A14;
end;
suppose p
= (k
+ 1);
hence thesis by
A10,
A13,
A14;
end;
end;
thus for B st A
= (
(#) B) holds (H
. A)
= H(.)
proof
let B;
assume
A15: A
= (
(#) B);
then (
card (
dom B))
<> (k
+ 1) by
A11,
Th34;
then
A16: (H
. B)
= (F
. B) by
A10;
per cases ;
suppose p
<> (k
+ 1);
then p
<= k & (H
. A)
= (F
. A) by
A10,
A11,
NAT_1: 8;
hence thesis by
A2,
A15,
A16;
end;
suppose p
= (k
+ 1);
hence thesis by
A10,
A15,
A16;
end;
end;
thus for B, C st A
= (B
'&' C) holds (H
. A)
= C(.,.)
proof
let B, C;
assume
A17: A
= (B
'&' C);
then (
card (
dom B))
<> (k
+ 1) by
A11,
Th35;
then
A18: (H
. B)
= (F
. B) by
A10;
(
card (
dom C))
<> (k
+ 1) by
A11,
A17,
Th35;
then
A19: (H
. C)
= (F
. C) by
A10;
per cases ;
suppose p
<> (k
+ 1);
then p
<= k & (H
. A)
= (F
. A) by
A10,
A11,
NAT_1: 8;
hence thesis by
A2,
A17,
A18,
A19;
end;
suppose p
= (k
+ 1);
hence thesis by
A10,
A17,
A18,
A19;
end;
end;
end;
end;
A20:
P[
0 ]
proof
set F = the
Function of
MP-WFF , D();
take F;
let A;
assume (
card (
dom A))
<=
0 ;
hence thesis by
NAT_1: 2;
end;
A21: for n holds
P[n] from
NAT_1:sch 2(
A20,
A1);
A22: for x be
object st x
in
MP-WFF holds ex y be
object st
Qfn[x, y]
proof
let x be
object;
assume x
in
MP-WFF ;
then
reconsider x9 = x as
Element of
MP-WFF ;
consider F be
Function of
MP-WFF , D() such that
A23:
Pfn[F, (
card (
dom x9))] by
A21;
take (F
. x), x9;
thus x
= x9;
let G be
Function of
MP-WFF , D();
defpred
Prop[
Element of
MP-WFF ] means (
card (
dom $1))
<= (
card (
dom x9)) implies (F
. $1)
= (G
. $1);
assume
A24:
Pfn[G, (
card (
dom x9))];
A25: for p holds
Prop[(
@ p)]
proof
let p;
assume
A26: (
card (
dom (
@ p)))
<= (
card (
dom x9));
hence (F
. (
@ p))
= F(p) by
A23
.= (G
. (
@ p)) by
A24,
A26;
end;
A27: for A,B be
Element of
MP-WFF st
Prop[A] &
Prop[B] holds
Prop[(A
'&' B)]
proof
let A, B;
assume that
A28:
Prop[A] &
Prop[B] and
A29: (
card (
dom (A
'&' B)))
<= (
card (
dom x9));
(
card (
dom A))
< (
card (
dom (A
'&' B))) & (
card (
dom B))
< (
card (
dom (A
'&' B))) by
Th35;
hence (F
. (A
'&' B))
= C(.,.) by
A23,
A28,
A29,
XXREAL_0: 2
.= (G
. (A
'&' B)) by
A24,
A29;
end;
A30: for A be
Element of
MP-WFF st
Prop[A] holds
Prop[(
(#) A)]
proof
let A such that
A31:
Prop[A];
assume
A32: (
card (
dom (
(#) A)))
<= (
card (
dom x9));
(
card (
dom A))
< (
card (
dom (
(#) A))) by
Th34;
hence (F
. (
(#) A))
= H(.) by
A23,
A31,
A32,
XXREAL_0: 2
.= (G
. (
(#) A)) by
A24,
A32;
end;
A33: for A be
Element of
MP-WFF st
Prop[A] holds
Prop[(
'not' A)]
proof
let A such that
A34:
Prop[A];
assume
A35: (
card (
dom (
'not' A)))
<= (
card (
dom x9));
(
card (
dom A))
< (
card (
dom (
'not' A))) by
Th33;
hence (F
. (
'not' A))
= N(.) by
A23,
A34,
A35,
XXREAL_0: 2
.= (G
. (
'not' A)) by
A24,
A35;
end;
A36:
Prop[
VERUM ]
proof
assume
A37: (
card (
dom
VERUM ))
<= (
card (
dom x9));
hence (F
.
VERUM )
= d() by
A23
.= (G
.
VERUM ) by
A24,
A37;
end;
for p be
Element of
MP-WFF holds
Prop[p] from
MPInd(
A36,
A25,
A33,
A30,
A27);
hence thesis;
end;
consider F be
Function such that
A38: (
dom F)
=
MP-WFF and
A39: for x be
object st x
in
MP-WFF holds
Qfn[x, (F
. x)] from
CLASSES1:sch 1(
A22);
(
rng F)
c= D()
proof
let y be
object;
assume y
in (
rng F);
then
consider x be
object such that
A40: x
in
MP-WFF & y
= (F
. x) by
A38,
FUNCT_1:def 3;
consider p be
Element of
MP-WFF such that p
= x and
A41: for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom p))] holds y
= (g
. p) by
A39,
A40;
consider G be
Function of
MP-WFF , D() such that
A42:
Pfn[G, (
card (
dom p))] by
A21;
y
= (G
. p) by
A41,
A42;
hence thesis;
end;
then
reconsider F as
Function of
MP-WFF , D() by
A38,
FUNCT_2:def 1,
RELSET_1: 4;
consider A such that
A43: A
=
VERUM and
A44: for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom A))] holds (F
.
VERUM )
= (g
. A) by
A39;
take F;
consider G be
Function of
MP-WFF , D() such that
A45:
Pfn[G, (
card (
dom A))] by
A21;
(F
.
VERUM )
= (G
.
VERUM ) by
A43,
A44,
A45;
hence (F
.
VERUM )
= d() by
A43,
A45;
thus for p be
MP-variable holds (F
. (
@ p))
= F(p)
proof
let p be
MP-variable;
consider A such that
A46: A
= (
@ p) and
A47: for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom A))] holds (F
. (
@ p))
= (g
. A) by
A39;
consider G be
Function of
MP-WFF , D() such that
A48:
Pfn[G, (
card (
dom A))] by
A21;
(F
. (
@ p))
= (G
. (
@ p)) by
A46,
A47,
A48;
hence thesis by
A46,
A48;
end;
thus for A be
Element of
MP-WFF holds (F
. (
'not' A))
= N(.)
proof
let A be
Element of
MP-WFF ;
consider A1 such that
A49: A1
= (
'not' A) and
A50: for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom A1))] holds (F
. (
'not' A))
= (g
. A1) by
A39;
consider G be
Function of
MP-WFF , D() such that
A51:
Pfn[G, (
card (
dom A1))] by
A21;
A52: for k st k
< (
card (
dom (
'not' A))) holds
Pfn[G, k]
proof
let k;
assume
A53: k
< (
card (
dom (
'not' A)));
let a be
Element of
MP-WFF ;
assume (
card (
dom a))
<= k;
then (
card (
dom a))
<= (
card (
dom (
'not' A))) by
A53,
XXREAL_0: 2;
hence thesis by
A49,
A51;
end;
A54: ex B st B
= A & for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom B))] holds (F
. A)
= (g
. B) by
A39;
set k = (
card (
dom A));
k
< (
card (
dom (
'not' A))) by
Th33;
then
Pfn[G, k] by
A52;
then
A55: (F
. A)
= (G
. A) by
A54;
(F
. (
'not' A))
= (G
. (
'not' A)) by
A49,
A50,
A51;
hence thesis by
A49,
A51,
A55;
end;
thus for A be
Element of
MP-WFF holds (F
. (
(#) A))
= H(.)
proof
let A be
Element of
MP-WFF ;
consider A1 such that
A56: A1
= (
(#) A) and
A57: for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom A1))] holds (F
. (
(#) A))
= (g
. A1) by
A39;
consider G be
Function of
MP-WFF , D() such that
A58:
Pfn[G, (
card (
dom A1))] by
A21;
A59: for k st k
< (
card (
dom (
(#) A))) holds
Pfn[G, k]
proof
let k;
assume
A60: k
< (
card (
dom (
(#) A)));
let a be
Element of
MP-WFF ;
assume (
card (
dom a))
<= k;
then (
card (
dom a))
<= (
card (
dom (
(#) A))) by
A60,
XXREAL_0: 2;
hence thesis by
A56,
A58;
end;
A61: ex B st B
= A & for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom B))] holds (F
. A)
= (g
. B) by
A39;
set k = (
card (
dom A));
k
< (
card (
dom (
(#) A))) by
Th34;
then
Pfn[G, k] by
A59;
then
A62: (F
. A)
= (G
. A) by
A61;
(F
. (
(#) A))
= (G
. (
(#) A)) by
A56,
A57,
A58;
hence thesis by
A56,
A58,
A62;
end;
thus for A,B be
Element of
MP-WFF holds (F
. (A
'&' B))
= C(.,.)
proof
let A,B be
Element of
MP-WFF ;
set k1 = (
card (
dom A));
set k2 = (
card (
dom B));
consider A1 such that
A63: A1
= (A
'&' B) and
A64: for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom A1))] holds (F
. (A
'&' B))
= (g
. A1) by
A39;
consider G be
Function of
MP-WFF , D() such that
A65:
Pfn[G, (
card (
dom A1))] by
A21;
A66: for k st k
< (
card (
dom (A
'&' B))) holds
Pfn[G, k]
proof
let k;
assume
A67: k
< (
card (
dom (A
'&' B)));
let a be
Element of
MP-WFF ;
assume (
card (
dom a))
<= k;
then (
card (
dom a))
<= (
card (
dom (A
'&' B))) by
A67,
XXREAL_0: 2;
hence thesis by
A63,
A65;
end;
A68: ex B1 st B1
= A & for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom B1))] holds (F
. A)
= (g
. B1) by
A39;
k1
< (
card (
dom (A
'&' B))) by
Th35;
then
Pfn[G, k1] by
A66;
then
A69: (F
. A)
= (G
. A) by
A68;
A70: ex C st C
= B & for g be
Function of
MP-WFF , D() st
Pfn[g, (
card (
dom C))] holds (F
. B)
= (g
. C) by
A39;
k2
< (
card (
dom (A
'&' B))) by
Th35;
then
Pfn[G, k2] by
A66;
then
A71: (F
. B)
= (G
. B) by
A70;
(F
. (A
'&' B))
= (G
. (A
'&' B)) by
A63,
A64,
A65;
hence thesis by
A63,
A65,
A69,
A71;
end;
end;