let F, G, H be Element of QC-WFF ; for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H holds
s in G -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); for s being FinSequence st t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H holds
s in G -entry_points_in_subformula_tree_of H
let s be FinSequence; ( t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H implies s in G -entry_points_in_subformula_tree_of H )
defpred S1[ Element of NAT ] means for F, G, H being Element of QC-WFF
for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = $1 holds
s in G -entry_points_in_subformula_tree_of H;
A1:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
thus
S1[
k + 1]
verumproof
let F,
G,
H be
Element of
QC-WFF ;
for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 holds
s in G -entry_points_in_subformula_tree_of Hlet t be
Element of
dom (tree_of_subformulae F);
for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 holds
s in G -entry_points_in_subformula_tree_of Hlet s be
FinSequence;
( G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 implies s in G -entry_points_in_subformula_tree_of H )
assume that A3:
G = (tree_of_subformulae F) . t
and A4:
t ^ s in F -entry_points_in_subformula_tree_of H
and A5:
len s = k + 1
;
s in G -entry_points_in_subformula_tree_of H
consider v being
FinSequence,
x being
set such that A6:
s = v ^ <*x*>
and A7:
len v = k
by A5, TREES_2:4;
F -entry_points_in_subformula_tree_of H = { t1 where t1 is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t1 = H }
by Th49;
then consider t'' being
Element of
dom (tree_of_subformulae F) such that A8:
t'' = t ^ s
and A9:
(tree_of_subformulae F) . t'' = H
by A4;
reconsider s1 =
s as
FinSequence of
NAT by A8, FINSEQ_1:50;
A10:
s1 = v ^ <*x*>
by A6;
then reconsider u =
<*x*> as
FinSequence of
NAT by FINSEQ_1:50;
reconsider v =
v as
FinSequence of
NAT by A10, FINSEQ_1:50;
A11:
rng u c= NAT
by FINSEQ_1:def 4;
A12:
1
in {1}
by TARSKI:def 1;
(
dom u = Seg 1 &
u . 1
= x )
by FINSEQ_1:def 8;
then
x in rng u
by A12, FINSEQ_1:4, FUNCT_1:def 5;
then reconsider m =
x as
Element of
NAT by A11;
consider t' being
FinSequence of
NAT such that A13:
t' = t ^ v
;
A14:
t'' = t' ^ <*m*>
by A6, A8, A13, FINSEQ_1:45;
then
t' is_a_prefix_of t''
by TREES_1:8;
then reconsider t' =
t' as
Element of
dom (tree_of_subformulae F) by TREES_1:45;
consider H' being
Element of
QC-WFF such that A15:
H' = (tree_of_subformulae F) . t'
;
t ^ v in F -entry_points_in_subformula_tree_of H'
by A13, A15, Def3;
then A16:
v in G -entry_points_in_subformula_tree_of H'
by A2, A3, A7;
G -entry_points_in_subformula_tree_of H' = { v1 where v1 is Element of dom (tree_of_subformulae G) : (tree_of_subformulae G) . v1 = H' }
by Th49;
then A17:
ex
v1 being
Element of
dom (tree_of_subformulae G) st
(
v = v1 &
(tree_of_subformulae G) . v1 = H' )
by A16;
then reconsider v =
v as
Element of
dom (tree_of_subformulae G) ;
A18:
H is_immediate_constituent_of H'
by A9, A14, A15, Th36;
(
H = (tree_of_subformulae G) . (v ^ <*m*>) &
v ^ <*m*> in dom (tree_of_subformulae G) )
hence
s in G -entry_points_in_subformula_tree_of H
by A6, Def3;
verum
end;
end;
A23:
S1[ 0 ]
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A23, A1);
then A29:
( G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = len s implies s in G -entry_points_in_subformula_tree_of H )
;
assume
( t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H )
; s in G -entry_points_in_subformula_tree_of H
hence
s in G -entry_points_in_subformula_tree_of H
by A29, Def3; verum