let A be QC-alphabet ; for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H
let F, G, H be Element of QC-WFF A; for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H
let s be Element of dom (tree_of_subformulae G); ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H implies t ^ s in F -entry_points_in_subformula_tree_of H )
defpred S1[ Nat] means for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = $1 holds
t ^ s in F -entry_points_in_subformula_tree_of H;
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
thus
S1[
k + 1]
verumproof
A3:
1
in {1}
by TARSKI:def 1;
let F,
G,
H be
Element of
QC-WFF A;
for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 holds
t ^ s in F -entry_points_in_subformula_tree_of Hlet t be
Element of
dom (tree_of_subformulae F);
for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 holds
t ^ s in F -entry_points_in_subformula_tree_of Hlet s be
Element of
dom (tree_of_subformulae G);
( G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 implies t ^ s in F -entry_points_in_subformula_tree_of H )
assume that A4:
G = (tree_of_subformulae F) . t
and A5:
H = (tree_of_subformulae G) . s
and A6:
len s = k + 1
;
t ^ s in F -entry_points_in_subformula_tree_of H
consider v being
FinSequence,
x being
set such that A7:
s = v ^ <*x*>
and A8:
len v = k
by A6, TREES_2:3;
reconsider u =
<*x*> as
FinSequence of
NAT by A7, FINSEQ_1:36;
A9:
rng u c= NAT
by FINSEQ_1:def 4;
(
dom u = Seg 1 &
u . 1
= x )
by FINSEQ_1:def 8;
then
x in rng u
by A3, FINSEQ_1:2, FUNCT_1:def 3;
then reconsider m =
x as
Element of
NAT by A9;
reconsider v =
v as
FinSequence of
NAT by A7, FINSEQ_1:36;
reconsider s9 =
v as
Element of
dom (tree_of_subformulae G) by A7, TREES_1:21;
consider H9 being
Element of
QC-WFF A such that A10:
H9 = (tree_of_subformulae G) . s9
;
A11:
t ^ s9 in F -entry_points_in_subformula_tree_of H9
by A2, A4, A8, A10;
F -entry_points_in_subformula_tree_of H9 c= dom (tree_of_subformulae F)
by TREES_1:def 11;
then consider t9 being
Element of
dom (tree_of_subformulae F) such that A12:
t9 = t ^ s9
by A11;
A13:
H9 = (tree_of_subformulae F) . t9
by A11, A12, Def3;
A14:
s = s9 ^ <*m*>
by A7;
then A15:
H is_immediate_constituent_of H9
by A5, A10, Th7;
A16:
(
H = (tree_of_subformulae F) . (t9 ^ <*m*>) &
t9 ^ <*m*> in dom (tree_of_subformulae F) )
t ^ s = t9 ^ <*m*>
by A7, A12, FINSEQ_1:32;
hence
t ^ s in F -entry_points_in_subformula_tree_of H
by A16, Def3;
verum
end;
end;
A21:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A21, A1);
then A27:
( G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = len s implies t ^ s in F -entry_points_in_subformula_tree_of H )
;
assume
( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H )
; t ^ s in F -entry_points_in_subformula_tree_of H
hence
t ^ s in F -entry_points_in_subformula_tree_of H
by A27, Def3; verum