:: MODAL_1 semantic presentation begin Lm1: for m being Element of NAT holds {} is_a_proper_prefix_of <*m*> proof let m be Element of NAT ; ::_thesis: {} is_a_proper_prefix_of <*m*> {} is_a_prefix_of <*m*> by XBOOLE_1:2; hence {} is_a_proper_prefix_of <*m*> by XBOOLE_0:def_8; ::_thesis: verum end; definition let Z be Tree; func Root Z -> Element of Z equals :: MODAL_1:def 1 {} ; coherence {} is Element of Z by TREES_1:22; end; :: deftheorem defines Root MODAL_1:def_1_:_ for Z being Tree holds Root Z = {} ; definition let D be non empty set ; let T be DecoratedTree of D; func Root T -> Element of D equals :: MODAL_1:def 2 T . (Root (dom T)); coherence T . (Root (dom T)) is Element of D ; end; :: deftheorem defines Root MODAL_1:def_2_:_ for D being non empty set for T being DecoratedTree of D holds Root T = T . (Root (dom T)); theorem Th1: :: MODAL_1:1 for n, m being Element of NAT for s being FinSequence of NAT st n <> m holds not <*n*>,<*m*> ^ s are_c=-comparable proof let n, m be Element of NAT ; ::_thesis: for s being FinSequence of NAT st n <> m holds not <*n*>,<*m*> ^ s are_c=-comparable let s be FinSequence of NAT ; ::_thesis: ( n <> m implies not <*n*>,<*m*> ^ s are_c=-comparable ) assume A1: n <> m ; ::_thesis: not <*n*>,<*m*> ^ s are_c=-comparable assume A2: <*n*>,<*m*> ^ s are_c=-comparable ; ::_thesis: contradiction percases ( <*n*> is_a_prefix_of <*m*> ^ s or <*m*> ^ s is_a_prefix_of <*n*> ) by A2, XBOOLE_0:def_9; suppose <*n*> is_a_prefix_of <*m*> ^ s ; ::_thesis: contradiction then A3: ex a being 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; ::_thesis: verum end; suppose <*m*> ^ s is_a_prefix_of <*n*> ; ::_thesis: contradiction then consider a being 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; ::_thesis: verum end; end; end; theorem :: MODAL_1:2 for s being FinSequence of NAT st s <> {} holds ex w being FinSequence of NAT ex n being Element of NAT st s = <*n*> ^ w by FINSEQ_2:130; theorem Th3: :: MODAL_1:3 for n, m being Element of NAT for s being FinSequence of NAT st n <> m holds not <*n*> is_a_proper_prefix_of <*m*> ^ s proof let n, m be Element of NAT ; ::_thesis: for s being FinSequence of NAT st n <> m holds not <*n*> is_a_proper_prefix_of <*m*> ^ s let s be FinSequence of NAT ; ::_thesis: ( n <> m implies not <*n*> is_a_proper_prefix_of <*m*> ^ s ) assume A1: n <> m ; ::_thesis: not <*n*> is_a_proper_prefix_of <*m*> ^ s assume <*n*> is_a_proper_prefix_of <*m*> ^ s ; ::_thesis: contradiction then <*n*> is_a_prefix_of <*m*> ^ s by XBOOLE_0:def_8; then A2: ex a being 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; ::_thesis: verum end; theorem :: MODAL_1:4 for n, m being Element of NAT for s being FinSequence of NAT st n <> m holds not <*n*> is_a_prefix_of <*m*> ^ s by TREES_1:50; theorem :: MODAL_1:5 for n, m being Element of NAT holds not <*n*> is_a_proper_prefix_of <*m*> by TREES_1:52; theorem :: MODAL_1:6 elementary_tree 1 = {{},<*0*>} by TREES_1:51; theorem :: MODAL_1:7 elementary_tree 2 = {{},<*0*>,<*1*>} by TREES_1:53; theorem Th8: :: MODAL_1:8 for Z being Tree for n, m being Element of NAT 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; ::_thesis: for n, m being Element of NAT st n <= m & <*m*> in Z holds <*n*> in Z let n, m be Element of NAT ; ::_thesis: ( n <= m & <*m*> in Z implies <*n*> in Z ) assume that A1: n <= m and A2: <*m*> in Z ; ::_thesis: <*n*> in Z {} ^ <*m*> in Z by A2, FINSEQ_1:34; then s ^ <*n*> in Z by A1, TREES_1:def_3; hence <*n*> in Z by FINSEQ_1:34; ::_thesis: verum end; theorem :: MODAL_1:9 for w, t, s being FinSequence of NAT st w ^ t is_a_proper_prefix_of w ^ s holds t is_a_proper_prefix_of s by TREES_1:49; theorem Th10: :: MODAL_1:10 for t1 being DecoratedTree of [:NAT,NAT:] holds t1 in PFuncs ((NAT *),[:NAT,NAT:]) proof let t1 be DecoratedTree of [:NAT,NAT:]; ::_thesis: t1 in PFuncs ((NAT *),[:NAT,NAT:]) ( rng t1 c= [:NAT,NAT:] & dom t1 c= NAT * ) by TREES_1:def_3; hence t1 in PFuncs ((NAT *),[:NAT,NAT:]) by PARTFUN1:def_3; ::_thesis: verum end; theorem Th11: :: MODAL_1:11 for Z, Z1, Z2 being Tree for z being Element of Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2 proof let Z, Z1, Z2 be Tree; ::_thesis: for z being Element of Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2 let z be Element of Z; ::_thesis: ( Z with-replacement (z,Z1) = Z with-replacement (z,Z2) implies Z1 = Z2 ) assume A1: Z with-replacement (z,Z1) = Z with-replacement (z,Z2) ; ::_thesis: Z1 = Z2 now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_s_in_Z1_implies_s_in_Z2_)_&_(_s_in_Z2_implies_s_in_Z1_)_) let s be FinSequence of NAT ; ::_thesis: ( ( s in Z1 implies s in Z2 ) & ( s in Z2 implies b1 in Z1 ) ) thus ( s in Z1 implies s in Z2 ) ::_thesis: ( s in Z2 implies b1 in Z1 ) proof assume A2: s in Z1 ; ::_thesis: s in Z2 percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: s in Z2 hence s in Z2 by TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: s in Z2 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 being FinSequence of NAT st ( w in Z2 & z ^ s = z ^ w ) by A3, TREES_1:def_9; hence s in Z2 by FINSEQ_1:33; ::_thesis: verum end; end; end; assume A4: s in Z2 ; ::_thesis: b1 in Z1 percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: b1 in Z1 hence s in Z1 by TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: b1 in Z1 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 being FinSequence of NAT st ( w in Z1 & z ^ s = z ^ w ) by A5, TREES_1:def_9; hence s in Z1 by FINSEQ_1:33; ::_thesis: verum end; end; end; hence Z1 = Z2 by TREES_2:def_1; ::_thesis: verum end; theorem Th12: :: MODAL_1:12 for D being non empty set for Z, Z1, Z2 being DecoratedTree of D for z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2 proof let D be non empty set ; ::_thesis: for Z, Z1, Z2 being DecoratedTree of D for z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2 let Z, Z1, Z2 be DecoratedTree of D; ::_thesis: for z being Element of dom Z st Z with-replacement (z,Z1) = Z with-replacement (z,Z2) holds Z1 = Z2 let z be Element of dom Z; ::_thesis: ( Z with-replacement (z,Z1) = Z with-replacement (z,Z2) implies Z1 = Z2 ) assume A1: Z with-replacement (z,Z1) = Z with-replacement (z,Z2) ; ::_thesis: Z1 = Z2 set T2 = Z with-replacement (z,Z2); set T1 = Z with-replacement (z,Z1); A2: dom (Z with-replacement (z,Z1)) = (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 being FinSequence of NAT st s in dom Z1 holds Z1 . s = Z2 . s proof let s be FinSequence of NAT ; ::_thesis: ( s in dom Z1 implies Z1 . s = Z2 . s ) A5: z is_a_prefix_of z ^ s by TREES_1:1; assume A6: s in dom Z1 ; ::_thesis: Z1 . s = Z2 . s then z ^ s in (dom Z) with-replacement (z,(dom Z1)) by TREES_1:def_9; then A7: ex u being FinSequence of NAT st ( u in dom Z1 & z ^ s = z ^ u & (Z with-replacement (z,Z1)) . (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 being FinSequence of NAT such that w in dom Z2 and A8: z ^ s = z ^ w and A9: (Z with-replacement (z,Z2)) . (z ^ s) = Z2 . w by A5, TREES_2:def_11; s = w by A8, FINSEQ_1:33; hence Z1 . s = Z2 . s by A1, A9, A7, FINSEQ_1:33; ::_thesis: verum end; dom (Z with-replacement (z,Z2)) = (dom Z) with-replacement (z,(dom Z2)) by TREES_2:def_11; hence Z1 = Z2 by A1, A2, A4, Th11, TREES_2:31; ::_thesis: verum end; theorem Th13: :: MODAL_1:13 for Z1, Z2 being Tree for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds succ v = succ w proof let Z1, Z2 be Tree; ::_thesis: for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds succ v = succ w let p be FinSequence of NAT ; ::_thesis: ( p in Z1 implies for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds succ v = succ w ) assume A1: p in Z1 ; ::_thesis: for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds succ v = succ w set Z = Z1 with-replacement (p,Z2); let v be Element of Z1 with-replacement (p,Z2); ::_thesis: for w being Element of Z1 st v = w & w is_a_proper_prefix_of p holds succ v = succ w let w be Element of Z1; ::_thesis: ( v = w & w is_a_proper_prefix_of p implies succ v = succ w ) assume that A2: v = w and A3: w is_a_proper_prefix_of p ; ::_thesis: succ v = succ w w is_a_prefix_of p by A3, XBOOLE_0:def_8; then consider r being FinSequence such that A4: p = w ^ r by TREES_1:1; now__::_thesis:_for_n_being_Nat_st_n_in_dom_r_holds_ r_._n_in_NAT let n be Nat; ::_thesis: ( n in dom r implies r . n in NAT ) assume A5: n in dom r ; ::_thesis: r . n in NAT 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; ::_thesis: verum end; then reconsider r = r as FinSequence of NAT by FINSEQ_2:12; A7: r <> {} by A3, A4, FINSEQ_1:34; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_v_implies_x_in_succ_w_)_&_(_x_in_succ_w_implies_x_in_succ_v_)_) let x be set ; ::_thesis: ( ( x in succ v implies x in succ w ) & ( x in succ w implies x in succ v ) ) thus ( x in succ v implies x in succ w ) ::_thesis: ( x in succ w implies x in succ v ) proof assume x in succ v ; ::_thesis: x in succ w then x in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in Z1 with-replacement (p,Z2) } by TREES_2:def_5; then consider n being Element of NAT such that A8: x = v ^ <*n*> and A9: v ^ <*n*> in Z1 with-replacement (p,Z2) ; reconsider x9 = x as FinSequence of NAT by A8; now__::_thesis:_x_in_succ_w percases ( ( x9 in Z1 & not p is_a_proper_prefix_of x9 ) or ex r being FinSequence of NAT st ( r in Z2 & x9 = p ^ r ) ) by A1, A8, A9, TREES_1:def_9; suppose ( x9 in Z1 & not p is_a_proper_prefix_of x9 ) ; ::_thesis: x in succ w then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A2, A8; hence x in succ w by TREES_2:def_5; ::_thesis: verum end; suppose ex r being FinSequence of NAT st ( r in Z2 & x9 = p ^ r ) ; ::_thesis: x in succ w then consider s being FinSequence of NAT 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 s = {} ; ::_thesis: contradiction 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 ; ::_thesis: verum end; then <*n*> = r by A11, FINSEQ_1:34; then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A1, A2, A4, A8; hence x in succ w by TREES_2:def_5; ::_thesis: verum end; end; end; hence x in succ w ; ::_thesis: verum end; assume x in succ w ; ::_thesis: x in succ v then x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in Z1 } by TREES_2:def_5; then consider n being Element of NAT such that A13: x = w ^ <*n*> and A14: w ^ <*n*> in Z1 ; now__::_thesis:_v_^_<*n*>_in_Z1_with-replacement_(p,Z2) assume A15: not v ^ <*n*> in Z1 with-replacement (p,Z2) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( not v ^ <*n*> in Z1 or p is_a_proper_prefix_of v ^ <*n*> ) by A1, A15, TREES_1:def_9; suppose not v ^ <*n*> in Z1 ; ::_thesis: contradiction hence contradiction by A2, A14; ::_thesis: verum end; suppose p is_a_proper_prefix_of v ^ <*n*> ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; then x in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in Z1 with-replacement (p,Z2) } by A2, A13; hence x in succ v by TREES_2:def_5; ::_thesis: verum end; hence succ v = succ w by TARSKI:1; ::_thesis: verum end; theorem Th14: :: MODAL_1:14 for Z1, Z2 being Tree for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & not p,w are_c=-comparable holds succ v = succ w proof let Z1, Z2 be Tree; ::_thesis: for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & not p,w are_c=-comparable holds succ v = succ w let p be FinSequence of NAT ; ::_thesis: ( p in Z1 implies for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & not p,w are_c=-comparable holds succ v = succ w ) assume A1: p in Z1 ; ::_thesis: for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z1 st v = w & not p,w are_c=-comparable holds succ v = succ w set Z = Z1 with-replacement (p,Z2); let v be Element of Z1 with-replacement (p,Z2); ::_thesis: for w being Element of Z1 st v = w & not p,w are_c=-comparable holds succ v = succ w let w be Element of Z1; ::_thesis: ( v = w & not p,w are_c=-comparable implies succ v = succ w ) assume that A2: v = w and A3: not p,w are_c=-comparable ; ::_thesis: succ v = succ w A4: not p is_a_prefix_of w by A3, XBOOLE_0:def_9; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_v_implies_x_in_succ_w_)_&_(_x_in_succ_w_implies_x_in_succ_v_)_) let x be set ; ::_thesis: ( ( x in succ v implies x in succ w ) & ( x in succ w implies x in succ v ) ) thus ( x in succ v implies x in succ w ) ::_thesis: ( x in succ w implies x in succ v ) proof assume x in succ v ; ::_thesis: x in succ w then x in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in Z1 with-replacement (p,Z2) } by TREES_2:def_5; then consider n being Element of NAT such that A5: x = v ^ <*n*> and A6: v ^ <*n*> in Z1 with-replacement (p,Z2) ; reconsider x9 = x as FinSequence of NAT by A5; v ^ <*n*> in Z1 proof assume A7: not v ^ <*n*> in Z1 ; ::_thesis: contradiction then ex t being FinSequence of NAT 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; percases ( p is_a_proper_prefix_of v ^ <*n*> or p = v ^ <*n*> ) by A8, XBOOLE_0:def_8; suppose p is_a_proper_prefix_of v ^ <*n*> ; ::_thesis: contradiction hence contradiction by A2, A4, TREES_1:9; ::_thesis: verum end; suppose p = v ^ <*n*> ; ::_thesis: contradiction hence contradiction by A1, A7; ::_thesis: verum end; end; end; then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A2, A5; hence x in succ w by TREES_2:def_5; ::_thesis: verum end; assume x in succ w ; ::_thesis: x in succ v then x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in Z1 } by TREES_2:def_5; then consider n being Element of NAT such that A9: x = w ^ <*n*> and A10: w ^ <*n*> in Z1 ; not p is_a_proper_prefix_of w ^ <*n*> by A4, TREES_1:9; then v ^ <*n*> in Z1 with-replacement (p,Z2) by A1, A2, A10, TREES_1:def_9; then x in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in Z1 with-replacement (p,Z2) } by A2, A9; hence x in succ v by TREES_2:def_5; ::_thesis: verum end; hence succ v = succ w by TARSKI:1; ::_thesis: verum end; theorem :: MODAL_1:15 for Z1, Z2 being Tree for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 with-replacement (p,Z2) for w being Element of Z2 st v = p ^ w holds succ v, succ w are_equipotent by TREES_2:37; theorem Th16: :: MODAL_1:16 for Z1 being Tree for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 for w being Element of Z1 | p st v = p ^ w holds succ v, succ w are_equipotent proof let Z1 be Tree; ::_thesis: for p being FinSequence of NAT st p in Z1 holds for v being Element of Z1 for w being Element of Z1 | p st v = p ^ w holds succ v, succ w are_equipotent let p be FinSequence of NAT ; ::_thesis: ( p in Z1 implies for v being Element of Z1 for w being Element of Z1 | p st v = p ^ w holds succ v, succ w are_equipotent ) assume A1: p in Z1 ; ::_thesis: for v being Element of Z1 for w being Element of Z1 | p st v = p ^ w holds succ v, succ w are_equipotent set T = Z1 | p; let t be Element of Z1; ::_thesis: for w being Element of Z1 | p st t = p ^ w holds succ t, succ w are_equipotent let t2 be Element of Z1 | p; ::_thesis: ( t = p ^ t2 implies succ t, succ t2 are_equipotent ) assume A2: t = p ^ t2 ; ::_thesis: succ t, succ t2 are_equipotent A3: for n being Element of NAT holds ( t ^ <*n*> in Z1 iff t2 ^ <*n*> in Z1 | p ) proof let n be Element of NAT ; ::_thesis: ( t ^ <*n*> in Z1 iff t2 ^ <*n*> in Z1 | p ) A4: t ^ <*n*> = p ^ (t2 ^ <*n*>) by A2, FINSEQ_1:32; hence ( t ^ <*n*> in Z1 implies t2 ^ <*n*> in Z1 | p ) by A1, TREES_1:def_6; ::_thesis: ( t2 ^ <*n*> in Z1 | p implies t ^ <*n*> in Z1 ) assume t2 ^ <*n*> in Z1 | p ; ::_thesis: t ^ <*n*> in Z1 hence t ^ <*n*> in Z1 by A1, A4, TREES_1:def_6; ::_thesis: verum end; defpred S1[ set , set ] means for n being Element of NAT st $1 = t ^ <*n*> holds $2 = t2 ^ <*n*>; A5: for x being set st x in succ t holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in succ t implies ex y being set st S1[x,y] ) assume x in succ t ; ::_thesis: ex y being set st S1[x,y] then x in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by TREES_2:def_5; then consider n being Element of NAT such that A6: x = t ^ <*n*> and t ^ <*n*> in Z1 ; take t2 ^ <*n*> ; ::_thesis: S1[x,t2 ^ <*n*>] let m be Element of NAT ; ::_thesis: ( x = t ^ <*m*> implies t2 ^ <*n*> = t2 ^ <*m*> ) assume x = t ^ <*m*> ; ::_thesis: t2 ^ <*n*> = t2 ^ <*m*> hence t2 ^ <*n*> = t2 ^ <*m*> by A6, FINSEQ_1:33; ::_thesis: verum end; consider f being Function such that A7: ( dom f = succ t & ( for x being set st x in succ t holds S1[x,f . x] ) ) from CLASSES1:sch_1(A5); now__::_thesis:_for_x_being_set_holds_ (_(_x_in_rng_f_implies_x_in_succ_t2_)_&_(_x_in_succ_t2_implies_x_in_rng_f_)_) let x be set ; ::_thesis: ( ( x in rng f implies x in succ t2 ) & ( x in succ t2 implies x in rng f ) ) thus ( x in rng f implies x in succ t2 ) ::_thesis: ( x in succ t2 implies x in rng f ) proof assume x in rng f ; ::_thesis: x in succ t2 then consider y being set such that A8: y in dom f and A9: x = f . y by FUNCT_1:def_3; y in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A7, A8, TREES_2:def_5; then consider n being Element of NAT such that A10: y = t ^ <*n*> and A11: t ^ <*n*> in Z1 ; A12: t2 ^ <*n*> in Z1 | p by A3, A11; x = t2 ^ <*n*> by A7, A8, A9, A10; then x in { (t2 ^ <*m*>) where m is Element of NAT : t2 ^ <*m*> in Z1 | p } by A12; hence x in succ t2 by TREES_2:def_5; ::_thesis: verum end; assume x in succ t2 ; ::_thesis: x in rng f then x in { (t2 ^ <*n*>) where n is Element of NAT : t2 ^ <*n*> in Z1 | p } by TREES_2:def_5; then consider n being Element of NAT such that A13: x = t2 ^ <*n*> and A14: t2 ^ <*n*> in Z1 | p ; t ^ <*n*> in Z1 by A3, A14; then t ^ <*n*> in { (t ^ <*m*>) where m is Element of NAT : 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; ::_thesis: verum end; then A16: rng f = succ t2 by TARSKI:1; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A17: x1 in dom f and A18: x2 in dom f and A19: f . x1 = f . x2 ; ::_thesis: x1 = x2 x2 in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A7, A18, TREES_2:def_5; then consider k being Element of NAT such that A20: x2 = t ^ <*k*> and t ^ <*k*> in Z1 ; x1 in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in Z1 } by A7, A17, TREES_2:def_5; then consider m being Element of NAT 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; ::_thesis: verum end; then f is one-to-one by FUNCT_1:def_4; hence succ t, succ t2 are_equipotent by A7, A16, WELLORD2:def_4; ::_thesis: verum end; theorem Th17: :: MODAL_1:17 for Z being finite Tree st branchdeg (Root Z) = 0 holds ( card Z = 1 & Z = {{}} ) proof let Z be finite Tree; ::_thesis: ( branchdeg (Root Z) = 0 implies ( card Z = 1 & Z = {{}} ) ) assume branchdeg (Root Z) = 0 ; ::_thesis: ( card Z = 1 & Z = {{}} ) then 0 = card (succ (Root Z)) by TREES_2:def_12; then A1: succ (Root Z) = {} ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Z_implies_x_in_{(Root_Z)}_)_&_(_x_in_{(Root_Z)}_implies_x_in_Z_)_) let x be set ; ::_thesis: ( ( x in Z implies x in {(Root Z)} ) & ( x in {(Root Z)} implies x in Z ) ) thus ( x in Z implies x in {(Root Z)} ) ::_thesis: ( x in {(Root Z)} implies x in Z ) proof assume x in Z ; ::_thesis: x in {(Root Z)} then reconsider z = x as Element of Z ; assume not x in {(Root Z)} ; ::_thesis: contradiction then z <> Root Z by TARSKI:def_1; then consider w being FinSequence of NAT , n being 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; ::_thesis: verum end; assume x in {(Root Z)} ; ::_thesis: x in Z then reconsider x9 = x as Element of Z ; x9 in Z ; hence x in Z ; ::_thesis: verum end; then Z = {(Root Z)} by TARSKI:1; hence ( card Z = 1 & Z = {{}} ) by CARD_2:42; ::_thesis: verum end; theorem Th18: :: MODAL_1:18 for Z being finite Tree st branchdeg (Root Z) = 1 holds succ (Root Z) = {<*0*>} proof let Z be finite Tree; ::_thesis: ( branchdeg (Root Z) = 1 implies succ (Root Z) = {<*0*>} ) assume branchdeg (Root Z) = 1 ; ::_thesis: succ (Root Z) = {<*0*>} then card (succ (Root Z)) = 1 by TREES_2:def_12; then consider x being set 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*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A2, TREES_2:def_5; then consider m being Element of NAT such that A3: x9 = (Root Z) ^ <*m*> and A4: (Root Z) ^ <*m*> in Z ; A5: x9 = <*m*> by A3, FINSEQ_1:34; now__::_thesis:_not_m_<>_0 A6: <*0*> = (Root Z) ^ <*0*> by FINSEQ_1:34; <*m*> in Z by A4, FINSEQ_1:34; then <*0*> in Z by Th8, 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 ; ::_thesis: contradiction hence contradiction by A5, A7, TREES_1:3; ::_thesis: verum end; hence succ (Root Z) = {<*0*>} by A1, A3, FINSEQ_1:34; ::_thesis: verum end; theorem Th19: :: MODAL_1:19 for Z being finite Tree st branchdeg (Root Z) = 2 holds succ (Root Z) = {<*0*>,<*1*>} proof let Z be finite Tree; ::_thesis: ( branchdeg (Root Z) = 2 implies succ (Root Z) = {<*0*>,<*1*>} ) assume branchdeg (Root Z) = 2 ; ::_thesis: succ (Root Z) = {<*0*>,<*1*>} then card (succ (Root Z)) = 2 by TREES_2:def_12; then consider x, y being set 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*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A3, TREES_2:def_5; then consider m being Element of NAT 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*>) where n is Element of NAT : (Root Z) ^ <*n*> in Z } by A6, TREES_2:def_5; then consider k being Element of NAT such that A7: y9 = (Root Z) ^ <*k*> and (Root Z) ^ <*k*> in Z ; A8: y9 = <*k*> by A7, FINSEQ_1:34; percases ( m = 0 or m <> 0 ) ; supposeA9: m = 0 ; ::_thesis: succ (Root Z) = {<*0*>,<*1*>} now__::_thesis:_not_k_<>_1 A10: <*1*> = (Root Z) ^ <*1*> by FINSEQ_1:34; assume A11: k <> 1 ; ::_thesis: contradiction then 2 <= k by A1, A5, A8, A9, NAT_1:26; then <*1*> in Z by A8, Th8, 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; ::_thesis: verum end; hence succ (Root Z) = {<*0*>,<*1*>} by A2, A4, A8, A9, FINSEQ_1:34; ::_thesis: verum end; supposeA12: m <> 0 ; ::_thesis: succ (Root Z) = {<*0*>,<*1*>} ( <*0*> in Z & <*0*> = (Root Z) ^ <*0*> ) by A5, Th8, 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__::_thesis:_not_m_<>_1 A14: <*1*> = (Root Z) ^ <*1*> by FINSEQ_1:34; assume A15: m <> 1 ; ::_thesis: contradiction then 2 <= m by A12, NAT_1:26; then <*1*> in Z by A5, Th8, 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; ::_thesis: verum end; hence succ (Root Z) = {<*0*>,<*1*>} by A2, A4, A8, A13, FINSEQ_1:34, TREES_1:3; ::_thesis: verum end; end; end; theorem Th20: :: MODAL_1:20 for Z being Tree for o being Element of Z st o <> Root Z holds ( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ) proof let Z be Tree; ::_thesis: for o being Element of Z st o <> Root Z holds ( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ) let o be Element of Z; ::_thesis: ( o <> Root Z implies ( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ) ) assume A1: o <> Root Z ; ::_thesis: ( Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent & not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ) set A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; thus Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent ::_thesis: not Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } proof defpred S1[ set , set ] means for s being FinSequence of NAT st $1 = s holds $2 = o ^ s; A2: for x being set st x in Z | o holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in Z | o implies ex y being set st S1[x,y] ) assume x in Z | o ; ::_thesis: ex y being set st S1[x,y] then reconsider s = x as FinSequence of NAT by TREES_1:19; take o ^ s ; ::_thesis: S1[x,o ^ s] let w be FinSequence of NAT ; ::_thesis: ( x = w implies o ^ s = o ^ w ) assume x = w ; ::_thesis: o ^ s = o ^ w hence o ^ s = o ^ w ; ::_thesis: verum end; ex f being Function st ( dom f = Z | o & ( for x being set st x in Z | o holds S1[x,f . x] ) ) from CLASSES1:sch_1(A2); then consider f being Function such that A3: dom f = Z | o and A4: for x being set st x in Z | o holds for s being FinSequence of NAT st x = s holds f . x = o ^ s ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_rng_f_implies_x_in__{__(o_^_s9)_where_s9_is_Element_of_NAT_*_:_o_^_s9_in_Z__}__)_&_(_x_in__{__(o_^_s9)_where_s9_is_Element_of_NAT_*_:_o_^_s9_in_Z__}__implies_x_in_rng_f_)_) let x be set ; ::_thesis: ( ( x in rng f implies x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ) & ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } implies x in rng f ) ) thus ( x in rng f implies x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ) ::_thesis: ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } implies x in rng f ) proof assume x in rng f ; ::_thesis: x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } then consider x1 being set such that A5: x1 in dom f and A6: x = f . x1 by FUNCT_1:def_3; reconsider x1 = x1 as FinSequence of NAT by A3, A5, TREES_1:19; reconsider x1 = 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 x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; ::_thesis: verum end; assume x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; ::_thesis: x in rng f then consider v9 being Element of NAT * 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; ::_thesis: verum end; then A10: rng f = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } by TARSKI:1; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A11: x1 in dom f and A12: x2 in dom f and A13: f . x1 = f . x2 ; ::_thesis: x1 = 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; ::_thesis: verum end; then f is one-to-one by FUNCT_1:def_4; hence Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent by A3, A10, WELLORD2:def_4; ::_thesis: verum end; assume Root Z in { (o ^ w9) where w9 is Element of NAT * : o ^ w9 in Z } ; ::_thesis: contradiction then ex v9 being Element of NAT * st ( Root Z = o ^ v9 & o ^ v9 in Z ) ; hence contradiction by A1; ::_thesis: verum end; theorem Th21: :: MODAL_1:21 for Z being finite Tree for o being Element of Z st o <> Root Z holds card (Z | o) < card Z proof let Z be finite Tree; ::_thesis: for o being Element of Z st o <> Root Z holds card (Z | o) < card Z let o be Element of Z; ::_thesis: ( o <> Root Z implies card (Z | o) < card Z ) assume A1: o <> Root Z ; ::_thesis: card (Z | o) < card Z set A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; A2: Z | o, { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } are_equipotent by A1, Th20; then reconsider A = { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } as finite set by CARD_1:38; reconsider B = A \/ {(Root Z)} as finite set ; now__::_thesis:_for_x_being_set_st_x_in_B_holds_ x_in_Z let x be set ; ::_thesis: ( x in B implies x in Z ) assume A3: x in B ; ::_thesis: x in Z now__::_thesis:_x_in_Z percases ( x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } or x in {(Root Z)} ) by A3, XBOOLE_0:def_3; suppose x in { (o ^ s9) where s9 is Element of NAT * : o ^ s9 in Z } ; ::_thesis: x in Z then ex v9 being Element of NAT * st ( x = o ^ v9 & o ^ v9 in Z ) ; hence x in Z ; ::_thesis: verum end; suppose x in {(Root Z)} ; ::_thesis: x in Z hence x in Z ; ::_thesis: verum end; end; end; hence x in Z ; ::_thesis: verum end; then A4: B c= Z by TARSKI:def_3; card B = (card A) + 1 by A1, Th20, 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 card (Z | o) < card Z by NAT_1:13; ::_thesis: verum end; theorem Th22: :: MODAL_1:22 for Z being finite Tree for z being Element of Z st succ (Root Z) = {z} holds Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) proof let Z be finite Tree; ::_thesis: for z being Element of Z st succ (Root Z) = {z} holds Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) let z be Element of Z; ::_thesis: ( succ (Root Z) = {z} implies Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) set e = elementary_tree 1; A1: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; A2: {} in Z by TREES_1:22; assume A3: succ (Root Z) = {z} ; ::_thesis: Z = (elementary_tree 1) with-replacement (<*0*>,(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, Th18; then z in {<*0*>} by TARSKI:def_1; then A4: z = <*0*> by TARSKI:def_1; then A5: <*0*> in Z ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Z_implies_x_in_(elementary_tree_1)_with-replacement_(<*0*>,(Z_|_z))_)_&_(_x_in_(elementary_tree_1)_with-replacement_(<*0*>,(Z_|_z))_implies_x_in_Z_)_) let x be set ; ::_thesis: ( ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) & ( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies b1 in Z ) ) thus ( x in Z implies x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ) ::_thesis: ( x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) implies b1 in Z ) proof assume x in Z ; ::_thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) then reconsider x9 = x as Element of Z ; percases ( x9 = {} or x9 <> {} ) ; suppose x9 = {} ; ::_thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) hence x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by TREES_1:22; ::_thesis: verum end; suppose x9 <> {} ; ::_thesis: x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) then consider w being FinSequence of NAT , n being 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 x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by A1, A6, A9, TREES_1:def_9; ::_thesis: verum end; end; end; assume x in (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ; ::_thesis: b1 in Z then reconsider x9 = x as Element of (elementary_tree 1) with-replacement (<*0*>,(Z | z)) ; percases ( ( x9 in elementary_tree 1 & not <*0*> is_a_proper_prefix_of x9 ) or ex s being FinSequence of NAT st ( s in Z | z & x9 = <*0*> ^ s ) ) by A1, TREES_1:def_9; suppose ( x9 in elementary_tree 1 & not <*0*> is_a_proper_prefix_of x9 ) ; ::_thesis: b1 in Z hence x in Z by A5, A2, TARSKI:def_2, TREES_1:51; ::_thesis: verum end; suppose ex s being FinSequence of NAT st ( s in Z | z & x9 = <*0*> ^ s ) ; ::_thesis: b1 in Z hence x in Z by A4, TREES_1:def_6; ::_thesis: verum end; end; end; hence Z = (elementary_tree 1) with-replacement (<*0*>,(Z | z)) by TARSKI:1; ::_thesis: verum end; Lm2: for f being Function st dom f is finite holds f is finite proof let f be Function; ::_thesis: ( dom f is finite implies f is finite ) assume A1: dom f is finite ; ::_thesis: f is finite then rng f is finite by FINSET_1:8; then [:(dom f),(rng f):] is finite by A1; hence f is finite by FINSET_1:1, RELAT_1:7; ::_thesis: verum end; theorem Th23: :: MODAL_1:23 for D being non empty set for Z being finite DecoratedTree of D for z being Element of dom Z st succ (Root (dom Z)) = {z} holds Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) proof let D be non empty set ; ::_thesis: for Z being finite DecoratedTree of D for z being Element of dom Z st succ (Root (dom Z)) = {z} holds Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) set e = elementary_tree 1; let Z be finite DecoratedTree of D; ::_thesis: for z being Element of dom Z st succ (Root (dom Z)) = {z} holds Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) let z be Element of dom Z; ::_thesis: ( succ (Root (dom Z)) = {z} implies Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) ) set E = (elementary_tree 1) --> (Root Z); A1: dom ((elementary_tree 1) --> (Root Z)) = elementary_tree 1 by FUNCOP_1:13; A2: dom (Z | z) = (dom Z) | z by TREES_2:def_10; A3: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; then A4: <*0*> in dom ((elementary_tree 1) --> (Root Z)) by FUNCOP_1:13; assume A5: succ (Root (dom Z)) = {z} ; ::_thesis: Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(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, Th18; then z in {<*0*>} by TARSKI:def_1; then A6: z = <*0*> by TARSKI:def_1; A7: for s being FinSequence of NAT st s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) holds (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s proof let s be FinSequence of NAT ; ::_thesis: ( s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) implies (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s ) assume A8: s in dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s A9: dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = (dom ((elementary_tree 1) --> (Root Z))) with-replacement (<*0*>,(dom (Z | z))) by A4, TREES_2:def_11; then A10: ( ( not <*0*> is_a_prefix_of s & (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = ((elementary_tree 1) --> (Root Z)) . s ) or ex w being FinSequence of NAT st ( w in dom (Z | z) & s = <*0*> ^ w & (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = (Z | z) . w ) ) by A4, A8, TREES_2:def_11; now__::_thesis:_(((elementary_tree_1)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_z)))_._s_=_Z_._s percases ( ( s in dom ((elementary_tree 1) --> (Root Z)) & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in dom (Z | z) & s = <*0*> ^ w ) ) by A4, A9, A8, TREES_1:def_9; supposeA11: ( s in dom ((elementary_tree 1) --> (Root Z)) & not <*0*> is_a_proper_prefix_of s ) ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s now__::_thesis:_(((elementary_tree_1)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_z)))_._s_=_Z_._s percases ( s = {} or s = <*0*> ) by A11, TARSKI:def_2, TREES_1:51; supposeA12: s = {} ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s then s in elementary_tree 1 by TREES_1:22; then A13: ((elementary_tree 1) --> (Root Z)) . s = Z . s by A12, FUNCOP_1:7; for w being FinSequence of NAT holds ( not w in dom (Z | z) or not s = <*0*> ^ w or not (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = (Z | z) . w ) by A12; hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A4, A9, A8, A13, TREES_2:def_11; ::_thesis: verum end; suppose s = <*0*> ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A6, A2, A10, TREES_2:def_10; ::_thesis: verum end; end; end; hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s ; ::_thesis: verum end; suppose ex w being FinSequence of NAT st ( w in dom (Z | z) & s = <*0*> ^ w ) ; ::_thesis: (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s by A6, A2, A10, TREES_1:1, TREES_2:def_10; ::_thesis: verum end; end; end; hence (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) . s = Z . s ; ::_thesis: verum end; dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = (elementary_tree 1) with-replacement (<*0*>,((dom Z) | z)) by A3, A1, A2, TREES_2:def_11; then dom (((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z))) = dom Z by A5, Th22; hence Z = ((elementary_tree 1) --> (Root Z)) with-replacement (<*0*>,(Z | z)) by A7, TREES_2:31; ::_thesis: verum end; theorem Th24: :: MODAL_1:24 for Z being Tree for x1, x2 being 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; ::_thesis: for x1, x2 being 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)) let x1, x2 be Element of Z; ::_thesis: ( x1 = <*0*> & x2 = <*1*> & succ (Root Z) = {x1,x2} implies Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) ) assume that A1: x1 = <*0*> and A2: x2 = <*1*> and A3: succ (Root Z) = {x1,x2} ; ::_thesis: Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) set T1 = (elementary_tree 2) with-replacement (<*0*>,(Z | x1)); A4: <*0*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53; A5: now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_not_s_in_Z_or_(_s_in_(elementary_tree_2)_with-replacement_(<*0*>,(Z_|_x1))_&_not_<*1*>_is_a_proper_prefix_of_s_)_or_ex_w_being_FinSequence_of_NAT_st_ (_w_in_Z_|_x2_&_s_=_<*1*>_^_w_)_)_&_(_(_(_s_in_(elementary_tree_2)_with-replacement_(<*0*>,(Z_|_x1))_&_not_<*1*>_is_a_proper_prefix_of_s_)_or_ex_w_being_FinSequence_of_NAT_st_ (_w_in_Z_|_x2_&_s_=_<*1*>_^_w_)_)_implies_s_in_Z_)_) let s be FinSequence of NAT ; ::_thesis: ( ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) & ( ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z ) ) thus ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) ::_thesis: ( ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) implies s in Z ) proof assume A6: s in Z ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) by TREES_1:12, TREES_1:15, TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) then consider w being FinSequence of NAT , n being 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__::_thesis:_(_(_s_in_(elementary_tree_2)_with-replacement_(<*0*>,(Z_|_x1))_&_not_<*1*>_is_a_proper_prefix_of_s_)_or_ex_w_being_FinSequence_of_NAT_st_ (_w_in_Z_|_x2_&_s_=_<*1*>_^_w_)_) percases ( <*n*> = <*0*> or <*n*> = <*1*> ) by A1, A2, A3, A9, TARSKI:def_2; supposeA10: <*n*> = <*0*> ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) then w in Z | x1 by A1, A6, A7, TREES_1:def_6; hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) by A4, A7, A10, Th3, TREES_1:def_9; ::_thesis: verum end; supposeA11: <*n*> = <*1*> ; ::_thesis: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) then w in Z | x2 by A2, A6, A7, TREES_1:def_6; hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) by A7, A11; ::_thesis: verum end; end; end; hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) ; ::_thesis: verum end; end; end; assume A12: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) ; ::_thesis: s in Z now__::_thesis:_s_in_Z percases ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ) by A12; supposeA13: ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) ; ::_thesis: s in Z now__::_thesis:_s_in_Z percases ( ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in Z | x1 & s = <*0*> ^ w ) ) by A4, A13, TREES_1:def_9; suppose ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) ; ::_thesis: s in Z then ( s = {} or s = <*0*> or s = <*1*> ) by ENUMSET1:def_1, TREES_1:53; hence s in Z by A1, A2, A3; ::_thesis: verum end; suppose ex w being FinSequence of NAT st ( w in Z | x1 & s = <*0*> ^ w ) ; ::_thesis: s in Z hence s in Z by A1, TREES_1:def_6; ::_thesis: verum end; end; end; hence s in Z ; ::_thesis: verum end; suppose ex w being FinSequence of NAT st ( w in Z | x2 & s = <*1*> ^ w ) ; ::_thesis: s in Z hence s in Z by A2, TREES_1:def_6; ::_thesis: verum end; end; end; hence s in Z ; ::_thesis: verum end; A14: now__::_thesis:_not_<*0*>_is_a_proper_prefix_of_<*1*> assume <*0*> is_a_proper_prefix_of <*1*> ; ::_thesis: contradiction then <*0*> is_a_prefix_of <*1*> by XBOOLE_0:def_8; hence contradiction by TREES_1:3; ::_thesis: verum end; <*1*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53; then <*1*> in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) by A4, A14, TREES_1:def_9; hence Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) by A5, TREES_1:def_9; ::_thesis: verum end; theorem Th25: :: MODAL_1:25 for D being non empty set for Z being DecoratedTree of D for x1, x2 being 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 let D be non empty set ; ::_thesis: for Z being DecoratedTree of D for x1, x2 being 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)) A1: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:52; set e = elementary_tree 2; let Z be DecoratedTree of D; ::_thesis: for x1, x2 being 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)) let x1, x2 be Element of dom Z; ::_thesis: ( x1 = <*0*> & x2 = <*1*> & succ (Root (dom Z)) = {x1,x2} implies Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) ) assume that A2: x1 = <*0*> and A3: x2 = <*1*> and A4: succ (Root (dom Z)) = {x1,x2} ; ::_thesis: Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | 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 = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)); A7: <*0*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53; then A8: <*0*> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:13; then A9: dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) = (dom ((elementary_tree 2) --> (Root Z))) with-replacement (<*0*>,(dom (Z | x1))) by TREES_2:def_11; <*1*> in elementary_tree 2 by ENUMSET1:def_1, TREES_1:53; then <*1*> in dom ((elementary_tree 2) --> (Root Z)) by FUNCOP_1:13; then A10: <*1*> in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) by A8, A9, A1, TREES_1:def_9; then A11: dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) = (dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1)))) with-replacement (<*1*>,(dom (Z | x2))) by TREES_2:def_11; A12: dom ((elementary_tree 2) --> (Root Z)) = elementary_tree 2 by FUNCOP_1:13; then A13: dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) = (elementary_tree 2) with-replacement (<*0*>,((dom Z) | x1)) by A7, A6, TREES_2:def_11; A14: for s being FinSequence of NAT st s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) holds ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s proof let s be FinSequence of NAT ; ::_thesis: ( s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) implies ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ) assume A15: s in dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s then A16: ( ( not <*1*> is_a_prefix_of s & ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s ) or ex u being FinSequence of NAT st ( u in dom (Z | x2) & s = <*1*> ^ u & ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (Z | x2) . u ) ) by A10, A11, TREES_2:def_11; now__::_thesis:_((((elementary_tree_2)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_x1)))_with-replacement_(<*1*>,(Z_|_x2)))_._s_=_Z_._s percases ( ( s in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in dom (Z | x2) & s = <*1*> ^ w ) ) by A10, A11, A15, TREES_1:def_9; supposeA17: ( s in dom (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) & not <*1*> is_a_proper_prefix_of s ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s then A18: ( ( not <*0*> is_a_prefix_of s & (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s = ((elementary_tree 2) --> (Root Z)) . s ) or ex u being FinSequence of NAT st ( u in dom (Z | x1) & s = <*0*> ^ u & (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) . s = (Z | x1) . u ) ) by A8, A9, TREES_2:def_11; now__::_thesis:_((((elementary_tree_2)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_x1)))_with-replacement_(<*1*>,(Z_|_x2)))_._s_=_Z_._s percases ( ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st ( w in (dom Z) | x1 & s = <*0*> ^ w ) ) by A7, A13, A17, TREES_1:def_9; supposeA19: ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s now__::_thesis:_((((elementary_tree_2)_-->_(Root_Z))_with-replacement_(<*0*>,(Z_|_x1)))_with-replacement_(<*1*>,(Z_|_x2)))_._s_=_Z_._s percases ( s = {} or s = <*0*> or s = <*1*> ) by A19, ENUMSET1:def_1, TREES_1:53; supposeA20: s = {} ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s then ( ( for u being FinSequence of NAT holds ( not u in dom (Z | x2) or not s = <*1*> ^ u or not ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = (Z | x2) . u ) ) & ((elementary_tree 2) --> (Root Z)) . s = Z . s ) by A19, FUNCOP_1:7; hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A10, A11, A15, A18, A20, TREES_2:def_11; ::_thesis: verum end; suppose s = <*0*> ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A2, A3, A6, A5, A16, A18, TREES_2:def_10; ::_thesis: verum end; suppose s = <*1*> ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A3, A5, A16, TREES_2:def_10; ::_thesis: verum end; end; end; hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; ::_thesis: verum end; suppose ex w being FinSequence of NAT st ( w in (dom Z) | x1 & s = <*0*> ^ w ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A2, A3, A6, A5, A16, A18, TREES_1:1, TREES_2:def_10; ::_thesis: verum end; end; end; hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; ::_thesis: verum end; suppose ex w being FinSequence of NAT st ( w in dom (Z | x2) & s = <*1*> ^ w ) ; ::_thesis: ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s by A3, A5, A16, TREES_1:1, TREES_2:def_10; ::_thesis: verum end; end; end; hence ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) . s = Z . s ; ::_thesis: verum end; dom Z = dom ((((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2))) by A2, A3, A4, A12, A6, A5, A9, A11, Th24; hence Z = (((elementary_tree 2) --> (Root Z)) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) by A14, TREES_2:31; ::_thesis: verum end; definition func MP-variables -> set equals :: MODAL_1:def 3 [:{3},NAT:]; coherence [:{3},NAT:] is set ; end; :: deftheorem defines MP-variables MODAL_1:def_3_:_ MP-variables = [:{3},NAT:]; registration cluster MP-variables -> non empty ; coherence not MP-variables is empty ; end; definition mode MP-variable is Element of MP-variables ; end; definition func MP-conectives -> set equals :: MODAL_1:def 4 [:{0,1,2},NAT:]; coherence [:{0,1,2},NAT:] is set ; end; :: deftheorem defines MP-conectives MODAL_1:def_4_:_ MP-conectives = [:{0,1,2},NAT:]; registration cluster MP-conectives -> non empty ; coherence not MP-conectives is empty ; end; definition mode MP-conective is Element of MP-conectives ; end; theorem Th26: :: MODAL_1:26 MP-conectives misses MP-variables proof assume not MP-conectives misses MP-variables ; ::_thesis: contradiction then consider x being set such that A1: x in [:{0,1,2},NAT:] and A2: x in [:{3},NAT:] by XBOOLE_0:3; consider x1, x2 being set 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; ::_thesis: verum end; definition let T be finite Tree; let v be Element of T; :: original: branchdeg redefine func branchdeg v -> Element of NAT ; coherence branchdeg v is Element of NAT proof branchdeg v = card (succ v) by TREES_2:def_12; hence branchdeg v is Element of NAT ; ::_thesis: verum end; end; definition func MP-WFF -> DTree-set of [:NAT,NAT:] means :Def5: :: MODAL_1:def 5 ( ( for x being DecoratedTree of [:NAT,NAT:] st x in it holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in it iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ); existence ex b1 being DTree-set of [:NAT,NAT:] st ( ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in b1 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) proof deffunc H1( set ) -> Element of [:NAT,NAT:] = [0,0]; set t = elementary_tree 0; set A = [:NAT,NAT:]; defpred S1[ set ] means ( $1 is finite DecoratedTree of [:NAT,NAT:] & ( for y being finite DecoratedTree of [:NAT,NAT:] st y = $1 holds ( dom y is finite & ( for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) ) ) ); consider Y being set such that A1: for x being set holds ( x in Y iff ( x in PFuncs ((NAT *),[:NAT,NAT:]) & S1[x] ) ) from XBOOLE_0:sch_1(); A2: for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in Y iff ( dom x is finite & ( for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) proof let x be finite DecoratedTree of [:NAT,NAT:]; ::_thesis: ( x in Y iff ( dom x is finite & ( for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) thus ( x in Y implies ( dom x is finite & ( for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) by A1; ::_thesis: ( dom x is finite & ( for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) implies x in Y ) assume that dom x is finite and A3: for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: x in Y A4: x in PFuncs ((NAT *),[:NAT,NAT:]) by Th10; for y being finite DecoratedTree of [:NAT,NAT:] st y = x holds ( dom y is finite & ( for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) ) by A3; hence x in Y by A1, A4; ::_thesis: verum end; consider T being DecoratedTree such that A5: ( dom T = elementary_tree 0 & ( for p being FinSequence of NAT st p in elementary_tree 0 holds T . p = H1(p) ) ) from TREES_2:sch_7(); rng T c= [:NAT,NAT:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng T or x in [:NAT,NAT:] ) assume x in rng T ; ::_thesis: x in [:NAT,NAT:] then consider z being set 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 = z as FinSequence of NAT ; T . z = [0,0] by A5, A6; hence x in [:NAT,NAT:] by A7; ::_thesis: verum end; then reconsider T = T as finite DecoratedTree of [:NAT,NAT:] by A5, Lm2, RELAT_1:def_19; A8: for y being finite DecoratedTree of [:NAT,NAT:] st y = T holds ( dom y is finite & ( for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) ) proof let y be finite DecoratedTree of [:NAT,NAT:]; ::_thesis: ( y = T implies ( dom y is finite & ( for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) ) ) assume A9: y = T ; ::_thesis: ( dom y is finite & ( for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) ) ) thus dom y is finite ; ::_thesis: for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) let v be Element of dom y; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) A10: succ v = {} proof set x = the Element of succ v; assume not succ v = {} ; ::_thesis: contradiction then A11: the Element of succ v in succ v ; succ v = { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in dom y } by TREES_2:def_5; then ex n being Element of NAT st ( the Element of succ v = v ^ <*n*> & v ^ <*n*> in dom y ) by A11; hence contradiction by A5, A9, TARSKI:def_1, TREES_1:29; ::_thesis: verum end; hence branchdeg v <= 2 by CARD_1:27, TREES_2:def_12; ::_thesis: ( ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) thus ( ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) by A5, A9, A10, CARD_1:27, TREES_2:def_12; ::_thesis: verum end; T in PFuncs ((NAT *),[:NAT,NAT:]) by Th10; then reconsider Y = Y as non empty set by A1, A8; for x being set st x in Y holds x is DecoratedTree of [:NAT,NAT:] by A1; then reconsider Y = Y as DTree-set of [:NAT,NAT:] by TREES_3:def_6; take Y ; ::_thesis: ( ( for x being DecoratedTree of [:NAT,NAT:] st x in Y holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in Y iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) thus ( ( for x being DecoratedTree of [:NAT,NAT:] st x in Y holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in Y iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being DTree-set of [:NAT,NAT:] st ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in b1 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) & ( for x being DecoratedTree of [:NAT,NAT:] st x in b2 holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in b2 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) holds b1 = b2 proof let D1, D2 be DTree-set of [:NAT,NAT:]; ::_thesis: ( ( for x being DecoratedTree of [:NAT,NAT:] st x in D1 holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in D1 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) & ( for x being DecoratedTree of [:NAT,NAT:] st x in D2 holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in D2 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) implies D1 = D2 ) assume that A12: for x being DecoratedTree of [:NAT,NAT:] st x in D1 holds x is finite and A13: for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in D1 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) and A14: for x being DecoratedTree of [:NAT,NAT:] st x in D2 holds x is finite and A15: for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in D2 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ; ::_thesis: D1 = D2 thus D1 c= D2 :: according to XBOOLE_0:def_10 ::_thesis: D2 c= D1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in D2 ) assume A16: x in D1 ; ::_thesis: x in D2 reconsider y = x as finite DecoratedTree of [:NAT,NAT:] by A12, A16; for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) by A13, A16; hence x in D2 by A15; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in D1 ) assume A17: x in D2 ; ::_thesis: x in D1 reconsider y = x as finite DecoratedTree of [:NAT,NAT:] by A14, A17; for v being Element of dom y holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0,0] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0] ) ) by A15, A17; hence x in D1 by A13; ::_thesis: verum end; end; :: deftheorem Def5 defines MP-WFF MODAL_1:def_5_:_ for b1 being DTree-set of [:NAT,NAT:] holds ( b1 = MP-WFF iff ( ( for x being DecoratedTree of [:NAT,NAT:] st x in b1 holds x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds ( x in b1 iff for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) ); definition mode MP-wff is Element of MP-WFF ; end; registration cluster -> finite for Element of MP-WFF ; coherence for b1 being MP-wff holds b1 is finite by Def5; end; definition let A be MP-wff; let a be Element of dom A; :: original: | redefine funcA | a -> MP-wff; coherence A | a is MP-wff proof set x = A | a; A1: dom (A | a) = (dom A) | a by TREES_2:def_10; then reconsider db = dom (A | a) as finite Tree ; reconsider x = A | a as finite DecoratedTree of [:NAT,NAT:] by A1, Lm2; now__::_thesis:_(_db_is_finite_&_(_for_v_being_Element_of_db_holds_ (_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_)_)_) thus db is finite ; ::_thesis: for v being Element of db holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) let v be Element of db; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) set da = dom A; reconsider v9 = v as Element of (dom A) | a by TREES_2:def_10; v in db ; then A2: v in (dom A) | a by TREES_2:def_10; then reconsider w = a ^ v as Element of dom A by TREES_1:def_6; ( succ v9, succ w are_equipotent & succ v9 = succ v ) by Th16, 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; ::_thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) thus ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) ::_thesis: ( ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) proof assume A4: branchdeg v = 0 ; ::_thesis: ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) percases ( A . w = [0,0] or ex k being Element of NAT st A . w = [3,k] ) by A3, A4, Def5; suppose A . w = [0,0] ; ::_thesis: ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) hence ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) by A2, TREES_2:def_10; ::_thesis: verum end; suppose ex k being Element of NAT st A . w = [3,k] ; ::_thesis: ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) then consider k being Element of NAT such that A5: A . w = [3,k] ; now__::_thesis:_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k] take k = k; ::_thesis: x . v = [3,k] thus x . v = [3,k] by A2, A5, TREES_2:def_10; ::_thesis: verum end; hence ( x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) ; ::_thesis: verum end; end; end; thus ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) ::_thesis: ( branchdeg v = 2 implies x . v = [2,0] ) proof assume A6: branchdeg v = 1 ; ::_thesis: ( x . v = [1,0] or x . v = [1,1] ) percases ( A . w = [1,0] or A . w = [1,1] ) by A3, A6, Def5; suppose A . w = [1,0] ; ::_thesis: ( x . v = [1,0] or x . v = [1,1] ) hence ( x . v = [1,0] or x . v = [1,1] ) by A2, TREES_2:def_10; ::_thesis: verum end; suppose A . w = [1,1] ; ::_thesis: ( x . v = [1,0] or x . v = [1,1] ) hence ( x . v = [1,0] or x . v = [1,1] ) by A2, TREES_2:def_10; ::_thesis: verum end; end; end; thus ( branchdeg v = 2 implies x . v = [2,0] ) ::_thesis: verum proof assume branchdeg v = 2 ; ::_thesis: x . v = [2,0] then A . w = [2,0] by A3, Def5; hence x . v = [2,0] by A2, TREES_2:def_10; ::_thesis: verum end; end; hence A | a is MP-wff by Def5; ::_thesis: verum end; end; definition let a be Element of MP-conectives ; func the_arity_of a -> Element of NAT equals :: MODAL_1:def 6 a `1 ; coherence a `1 is Element of NAT proof reconsider X = {0,1,2} as non empty set ; consider a1 being Element of X, k being 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 a `1 is Element of NAT by A1, MCART_1:7; ::_thesis: verum end; end; :: deftheorem defines the_arity_of MODAL_1:def_6_:_ for a being Element of MP-conectives holds the_arity_of a = a `1 ; definition let D be non empty set ; let T, T1 be DecoratedTree of D; let p be FinSequence of NAT ; assume A1: p in dom T ; func @ (T,p,T1) -> DecoratedTree of D equals :Def7: :: MODAL_1:def 7 T with-replacement (p,T1); coherence T with-replacement (p,T1) is DecoratedTree of D proof set X = T with-replacement (p,T1); rng (T with-replacement (p,T1)) c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (T with-replacement (p,T1)) or x in D ) assume x in rng (T with-replacement (p,T1)) ; ::_thesis: x in D then consider z being set such that A2: z in dom (T with-replacement (p,T1)) and A3: x = (T with-replacement (p,T1)) . z by FUNCT_1:def_3; reconsider z = z as FinSequence of NAT by A2, TREES_1:19; A4: dom (T with-replacement (p,T1)) = (dom T) with-replacement (p,(dom T1)) by A1, TREES_2:def_11; now__::_thesis:_x_in_D percases ( ( not p is_a_prefix_of z & (T with-replacement (p,T1)) . z = T . z ) or ex s being FinSequence of NAT st ( s in dom T1 & z = p ^ s & (T with-replacement (p,T1)) . z = T1 . s ) ) by A1, A2, A4, TREES_2:def_11; supposeA5: ( not p is_a_prefix_of z & (T with-replacement (p,T1)) . z = T . z ) ; ::_thesis: x in D then for s being FinSequence of NAT holds ( not s in dom T1 or not z = p ^ s ) by TREES_1:1; then reconsider z = z as Element of dom T by A1, A2, A4, TREES_1:def_9; T . z is Element of D ; hence x in D by A3, A5; ::_thesis: verum end; suppose ex s being FinSequence of NAT st ( s in dom T1 & z = p ^ s & (T with-replacement (p,T1)) . z = T1 . s ) ; ::_thesis: x in D then consider s being FinSequence of NAT such that A6: s in dom T1 and z = p ^ s and A7: (T with-replacement (p,T1)) . z = T1 . s ; reconsider s = s as Element of dom T1 by A6; T1 . s is Element of D ; hence x in D by A3, A7; ::_thesis: verum end; end; end; hence x in D ; ::_thesis: verum end; hence T with-replacement (p,T1) is DecoratedTree of D by RELAT_1:def_19; ::_thesis: verum end; end; :: deftheorem Def7 defines @ MODAL_1:def_7_:_ for D being non empty set for T, T1 being DecoratedTree of D for p being FinSequence of NAT st p in dom T holds @ (T,p,T1) = T with-replacement (p,T1); theorem Th27: :: MODAL_1:27 for A being MP-wff holds ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff proof let A be MP-wff; ::_thesis: ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff 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) = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) by Def7; dom (((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(dom A)) by A1, TREES_2:def_11; then dom (((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A)) = (elementary_tree 1) with-replacement (d,(dom A)) by FUNCOP_1:13; then reconsider x = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) 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 being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) now__::_thesis:_(_branchdeg_v_<=_2_&_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_) percases ( ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,0]) . v ) or ex s being FinSequence of NAT st ( s in dom A & v = <*0*> ^ s & x . v = A . s ) ) by A1, A3, TREES_2:def_11; supposeA4: ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,0]) . v ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A5: dom ((elementary_tree 1) --> [1,0]) = {{},<*0*>} by FUNCOP_1:13, TREES_1:51; A6: for s being FinSequence of NAT holds ( not s in dom A or not v = <*0*> ^ s ) by A4, TREES_1:1; then A7: v in dom ((elementary_tree 1) --> [1,0]) by A1, A3, TREES_1:def_9; then A8: v = {} by A4, A5, TARSKI:def_2; reconsider v9 = v as Element of dom ((elementary_tree 1) --> [1,0]) by A1, A3, A6, TREES_1:def_9; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_v9_implies_x_in_{<*0*>}_)_&_(_x_in_{<*0*>}_implies_x_in_succ_v9_)_) let x be set ; ::_thesis: ( ( x in succ v9 implies x in {<*0*>} ) & ( x in {<*0*>} implies x in succ v9 ) ) thus ( x in succ v9 implies x in {<*0*>} ) ::_thesis: ( x in {<*0*>} implies x in succ v9 ) proof assume x in succ v9 ; ::_thesis: x in {<*0*>} then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,0]) } by TREES_2:def_5; then consider n being Element of NAT such that A9: x = v9 ^ <*n*> and A10: v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,0]) ; <*n*> in dom ((elementary_tree 1) --> [1,0]) 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 x in {<*0*>} by A11, TARSKI:def_1; ::_thesis: verum end; assume x in {<*0*>} ; ::_thesis: x in succ v9 then A12: x = <*0*> by TARSKI:def_1; then A13: x = v9 ^ <*0*> by A8, FINSEQ_1:34; then v9 ^ <*0*> in dom ((elementary_tree 1) --> [1,0]) by A5, A12, TARSKI:def_2; then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,0]) } by A13; hence x in succ v9 by TREES_2:def_5; ::_thesis: verum end; then A14: succ v9 = {<*0*>} by TARSKI:1; succ v = succ v9 by A1, A3, A8, Lm1, Th13; then 1 = card (succ v) by A14, CARD_1:30; then A15: branchdeg v = 1 by TREES_2:def_12; hence branchdeg v <= 2 ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) v in elementary_tree 1 by A7; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A4, A15, FUNCOP_1:7; ::_thesis: verum end; suppose ex s being FinSequence of NAT st ( s in dom A & v = <*0*> ^ s & x . v = A . s ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) then consider s being FinSequence of NAT such that A16: s in dom A and A17: v = <*0*> ^ s and A18: x . v = A . s ; reconsider s = 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A21: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5; A22: ( branchdeg s = 2 implies A . s = [2,0] ) by Def5; ( not branchdeg s = 0 or A . s = [0,0] or ex m being Element of NAT st A . s = [3,m] ) by Def5; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A18, A20, A21, A22, A19, TREES_2:def_12; ::_thesis: verum end; end; end; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum end; hence ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff by Def5; ::_thesis: verum end; theorem Th28: :: MODAL_1:28 for A being MP-wff holds ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff proof let A be MP-wff; ::_thesis: ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff 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 (((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11; then A2: dom (((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A)) = (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 being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) now__::_thesis:_(_branchdeg_v_<=_2_&_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_) percases ( ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,1]) . v ) or ex s being FinSequence of NAT st ( s in dom A & v = <*0*> ^ s & x . v = A . s ) ) by A1, A3, TREES_2:def_11; supposeA4: ( not <*0*> is_a_prefix_of v & x . v = ((elementary_tree 1) --> [1,1]) . v ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A5: dom ((elementary_tree 1) --> [1,1]) = {{},<*0*>} by FUNCOP_1:13, TREES_1:51; A6: for s being FinSequence of NAT holds ( not s in dom A or not v = <*0*> ^ s ) by A4, TREES_1:1; then A7: v in dom ((elementary_tree 1) --> [1,1]) by A1, A3, TREES_1:def_9; then A8: v = {} by A4, A5, TARSKI:def_2; reconsider v9 = v as Element of dom ((elementary_tree 1) --> [1,1]) by A1, A3, A6, TREES_1:def_9; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_v9_implies_x_in_{<*0*>}_)_&_(_x_in_{<*0*>}_implies_x_in_succ_v9_)_) let x be set ; ::_thesis: ( ( x in succ v9 implies x in {<*0*>} ) & ( x in {<*0*>} implies x in succ v9 ) ) thus ( x in succ v9 implies x in {<*0*>} ) ::_thesis: ( x in {<*0*>} implies x in succ v9 ) proof assume x in succ v9 ; ::_thesis: x in {<*0*>} then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) } by TREES_2:def_5; then consider n being Element of NAT such that A9: x = v9 ^ <*n*> and A10: v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) ; <*n*> in dom ((elementary_tree 1) --> [1,1]) 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 x in {<*0*>} by A11, TARSKI:def_1; ::_thesis: verum end; assume x in {<*0*>} ; ::_thesis: x in succ v9 then A12: x = <*0*> by TARSKI:def_1; then A13: x = v9 ^ <*0*> by A8, FINSEQ_1:34; then v9 ^ <*0*> in dom ((elementary_tree 1) --> [1,1]) by A5, A12, TARSKI:def_2; then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 1) --> [1,1]) } by A13; hence x in succ v9 by TREES_2:def_5; ::_thesis: verum end; then A14: succ v9 = {<*0*>} by TARSKI:1; succ v = succ v9 by A1, A3, A8, Lm1, Th13; then 1 = card (succ v) by A14, CARD_1:30; then A15: branchdeg v = 1 by TREES_2:def_12; hence branchdeg v <= 2 ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) v in elementary_tree 1 by A7; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A4, A15, FUNCOP_1:7; ::_thesis: verum end; suppose ex s being FinSequence of NAT st ( s in dom A & v = <*0*> ^ s & x . v = A . s ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) then consider s being FinSequence of NAT such that A16: s in dom A and A17: v = <*0*> ^ s and A18: x . v = A . s ; reconsider s = 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A21: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5; A22: ( branchdeg s = 2 implies A . s = [2,0] ) by Def5; ( not branchdeg s = 0 or A . s = [0,0] or ex m being Element of NAT st A . s = [3,m] ) by Def5; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A18, A20, A21, A22, A19, TREES_2:def_12; ::_thesis: verum end; end; end; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum end; hence ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Def5; ::_thesis: verum end; theorem Th29: :: MODAL_1:29 for A, B being MP-wff holds (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff proof let A, B be MP-wff; ::_thesis: (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff 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 = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B); A1: not <*0*> is_a_proper_prefix_of <*1*> proof assume <*0*> is_a_proper_prefix_of <*1*> ; ::_thesis: contradiction then <*0*> is_a_prefix_of <*1*> by XBOOLE_0:def_8; hence contradiction by TREES_1:3; ::_thesis: verum end; 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) = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) by Def7; then reconsider y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A) 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 ((((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B)) = dy with-replacement (d1,db) & @ (y,<*1*>,B) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) ) by A5, Def7, TREES_2:def_11; then reconsider x = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) 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 being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) now__::_thesis:_(_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_) percases ( ( not <*1*> is_a_prefix_of v & x . v = y . v ) or ex s being FinSequence of NAT st ( s in dom B & v = <*1*> ^ s & x . v = B . s ) ) by A5, A6, TREES_2:def_11; supposeA7: ( not <*1*> is_a_prefix_of v & x . v = y . v ) ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) then A8: for s being FinSequence of NAT holds ( not s in dom B or not v = <*1*> ^ s ) by TREES_1:1; then A9: v in (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by A3, A5, A6, TREES_1:def_9; now__::_thesis:_(_branchdeg_v_<=_2_&_branchdeg_v_<=_2_&_(_not_branchdeg_v_=_0_or_x_._v_=_[0,0]_or_ex_k_being_Element_of_NAT_st_x_._v_=_[3,k]_)_&_(_not_branchdeg_v_=_1_or_x_._v_=_[1,0]_or_x_._v_=_[1,1]_)_&_(_branchdeg_v_=_2_implies_x_._v_=_[2,0]_)_) percases ( ( not <*0*> is_a_prefix_of v & y . v = ((elementary_tree 2) --> [2,0]) . v ) or ex s being FinSequence of NAT st ( s in dom A & v = <*0*> ^ s & y . v = A . s ) ) by A2, A9, TREES_2:def_11; supposeA10: ( not <*0*> is_a_prefix_of v & y . v = ((elementary_tree 2) --> [2,0]) . v ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A11: dom ((elementary_tree 2) --> [2,0]) = {{},<*0*>,<*1*>} by FUNCOP_1:13, TREES_1:53; A12: for s being FinSequence of NAT holds ( not s in dom A or not v = <*0*> ^ s ) by A10, TREES_1:1; then A13: v in dom ((elementary_tree 2) --> [2,0]) by A2, A9, TREES_1:def_9; then A14: v = {} by A7, A10, A11, ENUMSET1:def_1; reconsider v9 = v as Element of dom ((elementary_tree 2) --> [2,0]) 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, Th13; hence succ v = succ v9 by A5, A6, A14, Lm1, Th13; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_succ_v9_implies_x_in_{<*0*>,<*1*>}_)_&_(_x_in_{<*0*>,<*1*>}_implies_x_in_succ_v9_)_) let x be set ; ::_thesis: ( ( x in succ v9 implies x in {<*0*>,<*1*>} ) & ( x in {<*0*>,<*1*>} implies x in succ v9 ) ) thus ( x in succ v9 implies x in {<*0*>,<*1*>} ) ::_thesis: ( x in {<*0*>,<*1*>} implies x in succ v9 ) proof assume x in succ v9 ; ::_thesis: x in {<*0*>,<*1*>} then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by TREES_2:def_5; then consider n being Element of NAT such that A16: x = v9 ^ <*n*> and A17: v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) ; <*n*> in dom ((elementary_tree 2) --> [2,0]) 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 x in {<*0*>,<*1*>} by A18, TARSKI:def_2; ::_thesis: verum end; assume x in {<*0*>,<*1*>} ; ::_thesis: x in succ v9 then A19: ( x = <*0*> or x = <*1*> ) by TARSKI:def_2; now__::_thesis:_x_in_succ_v9 percases ( x = v9 ^ <*0*> or x = v9 ^ <*1*> ) by A14, A19, FINSEQ_1:34; supposeA20: x = v9 ^ <*0*> ; ::_thesis: x in succ v9 then v9 ^ <*0*> in dom ((elementary_tree 2) --> [2,0]) by A11, A19, ENUMSET1:def_1; then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by A20; hence x in succ v9 by TREES_2:def_5; ::_thesis: verum end; supposeA21: x = v9 ^ <*1*> ; ::_thesis: x in succ v9 then v9 ^ <*1*> in dom ((elementary_tree 2) --> [2,0]) by A11, A19, ENUMSET1:def_1; then x in { (v9 ^ <*n*>) where n is Element of NAT : v9 ^ <*n*> in dom ((elementary_tree 2) --> [2,0]) } by A21; hence x in succ v9 by TREES_2:def_5; ::_thesis: verum end; end; end; hence x in succ v9 ; ::_thesis: verum end; then A22: succ v9 = {<*0*>,<*1*>} by TARSKI:1; <*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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) v in elementary_tree 2 by A13; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A7, A10, A23, FUNCOP_1:7, TREES_2:def_12; ::_thesis: verum end; suppose ex s being FinSequence of NAT st ( s in dom A & v = <*0*> ^ s & y . v = A . s ) ; ::_thesis: ( branchdeg v <= 2 & branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) then consider s being FinSequence of NAT such that A24: s in dom A and A25: v = <*0*> ^ s and A26: y . v = A . s ; reconsider s = 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 succ v, succ s are_equipotent by A5, A6, A25, Th1, Th14; ::_thesis: verum 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A29: ( not branchdeg s = 1 or A . s = [1,0] or A . s = [1,1] ) by Def5; A30: ( branchdeg s = 2 implies A . s = [2,0] ) by Def5; ( not branchdeg s = 0 or A . s = [0,0] or ex m being Element of NAT st A . s = [3,m] ) by Def5; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A7, A26, A28, A29, A30, A27, TREES_2:def_12; ::_thesis: verum end; end; end; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum end; suppose ex s being FinSequence of NAT st ( s in dom B & v = <*1*> ^ s & x . v = B . s ) ; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) then consider s being FinSequence of NAT such that A31: s in dom B and A32: v = <*1*> ^ s and A33: x . v = B . s ; reconsider s = 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: ( not branchdeg s = 1 or B . s = [1,0] or B . s = [1,1] ) by Def5; A37: ( not branchdeg s = 0 or B . s = [0,0] or ex m being Element of NAT st B . s = [3,m] ) by Def5; branchdeg s <= 2 by Def5; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A33, A37, A36, A35, A34, TREES_2:def_12; ::_thesis: verum end; end; end; hence ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ; ::_thesis: verum end; hence (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Def5; ::_thesis: verum end; definition let A be MP-wff; func 'not' A -> MP-wff equals :: MODAL_1:def 8 ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A); coherence ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A) is MP-wff by Th27; func (#) A -> MP-wff equals :: MODAL_1:def 9 ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A); coherence ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A) is MP-wff by Th28; let B be MP-wff; funcA '&' B -> MP-wff equals :: MODAL_1:def 10 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B); coherence (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B) is MP-wff by Th29; end; :: deftheorem defines 'not' MODAL_1:def_8_:_ for A being MP-wff holds 'not' A = ((elementary_tree 1) --> [1,0]) with-replacement (<*0*>,A); :: deftheorem defines (#) MODAL_1:def_9_:_ for A being MP-wff holds (#) A = ((elementary_tree 1) --> [1,1]) with-replacement (<*0*>,A); :: deftheorem defines '&' MODAL_1:def_10_:_ for A, B being MP-wff holds A '&' B = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) with-replacement (<*1*>,B); definition let A be MP-wff; func ? A -> MP-wff equals :: MODAL_1:def 11 'not' ((#) ('not' A)); correctness coherence 'not' ((#) ('not' A)) is MP-wff; ; let B be MP-wff; funcA 'or' B -> MP-wff equals :: MODAL_1:def 12 'not' (('not' A) '&' ('not' B)); correctness coherence 'not' (('not' A) '&' ('not' B)) is MP-wff; ; funcA => B -> MP-wff equals :: MODAL_1:def 13 'not' (A '&' ('not' B)); correctness coherence 'not' (A '&' ('not' B)) is MP-wff; ; end; :: deftheorem defines ? MODAL_1:def_11_:_ for A being MP-wff holds ? A = 'not' ((#) ('not' A)); :: deftheorem defines 'or' MODAL_1:def_12_:_ for A, B being MP-wff holds A 'or' B = 'not' (('not' A) '&' ('not' B)); :: deftheorem defines => MODAL_1:def_13_:_ for A, B being MP-wff holds A => B = 'not' (A '&' ('not' B)); theorem Th30: :: MODAL_1:30 for n being Element of NAT holds (elementary_tree 0) --> [3,n] is MP-wff proof let n be Element of NAT ; ::_thesis: (elementary_tree 0) --> [3,n] is MP-wff set x = (elementary_tree 0) --> [3,n]; A1: dom ((elementary_tree 0) --> [3,n]) = {{}} by FUNCOP_1:13, TREES_1:29; reconsider x = (elementary_tree 0) --> [3,n] as finite DecoratedTree of [:NAT,NAT:] ; A2: dom x = elementary_tree 0 by FUNCOP_1:13; for v being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A3: succ v = {} proof set y = the Element of succ v; assume not succ v = {} ; ::_thesis: contradiction then the Element of succ v in succ v ; then the Element of succ v in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in dom x } by TREES_2:def_5; then ex m being Element of NAT st ( the Element of succ v = v ^ <*m*> & v ^ <*m*> in dom x ) ; hence contradiction by A1, TARSKI:def_1; ::_thesis: verum end; hence branchdeg v <= 2 by CARD_1:27, TREES_2:def_12; ::_thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) thus ( not branchdeg v = 0 or x . v = [0,0] or ex m being Element of NAT st x . v = [3,m] ) by A2, FUNCOP_1:7; ::_thesis: ( ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) thus ( ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A3, CARD_1:27, TREES_2:def_12; ::_thesis: verum end; hence (elementary_tree 0) --> [3,n] is MP-wff by Def5; ::_thesis: verum end; theorem Th31: :: MODAL_1:31 (elementary_tree 0) --> [0,0] is MP-wff proof set x = (elementary_tree 0) --> [0,0]; reconsider x = (elementary_tree 0) --> [0,0] 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 being Element of dom x holds ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or 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; ::_thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) A3: succ v = {} proof set y = the Element of succ v; assume not succ v = {} ; ::_thesis: contradiction then the Element of succ v in succ v ; then the Element of succ v in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in dom x } by TREES_2:def_5; then ex m being Element of NAT st ( the Element of succ v = v ^ <*m*> & v ^ <*m*> in dom x ) ; hence contradiction by A1, TARSKI:def_1; ::_thesis: verum end; hence branchdeg v <= 2 by CARD_1:27, TREES_2:def_12; ::_thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) thus ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) by A2, A3, CARD_1:27, FUNCOP_1:7, TREES_2:def_12; ::_thesis: verum end; hence (elementary_tree 0) --> [0,0] is MP-wff by Def5; ::_thesis: verum end; definition let p be MP-variable; func @ p -> MP-wff equals :: MODAL_1:def 14 (elementary_tree 0) --> p; coherence (elementary_tree 0) --> p is MP-wff proof consider x1, x2 being set 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 (elementary_tree 0) --> p is MP-wff by A2, Th30; ::_thesis: verum end; end; :: deftheorem defines @ MODAL_1:def_14_:_ for p being MP-variable holds @ p = (elementary_tree 0) --> p; theorem Th32: :: MODAL_1:32 for p, q being MP-variable st @ p = @ q holds p = q proof let p, q be MP-variable; ::_thesis: ( @ p = @ q implies p = q ) assume A1: @ p = @ q ; ::_thesis: 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 p = q ; ::_thesis: verum end; Lm3: for n, m being Element of NAT holds <*0*> in dom ((elementary_tree 1) --> [n,m]) proof let n, m be Element of NAT ; ::_thesis: <*0*> in dom ((elementary_tree 1) --> [n,m]) <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; hence <*0*> in dom ((elementary_tree 1) --> [n,m]) by FUNCOP_1:13; ::_thesis: verum end; theorem Th33: :: MODAL_1:33 for A, B being MP-wff st 'not' A = 'not' B holds A = B proof let A, B be MP-wff; ::_thesis: ( 'not' A = 'not' B implies A = B ) assume A1: 'not' A = 'not' B ; ::_thesis: A = B <*0*> in dom ((elementary_tree 1) --> [1,0]) by Lm3; hence A = B by A1, Th12; ::_thesis: verum end; theorem Th34: :: MODAL_1:34 for A, B being MP-wff st (#) A = (#) B holds A = B proof let A, B be MP-wff; ::_thesis: ( (#) A = (#) B implies A = B ) set AA = (elementary_tree 1) --> [1,1]; assume A1: (#) A = (#) B ; ::_thesis: A = B <*0*> in dom ((elementary_tree 1) --> [1,1]) by Lm3; hence A = B by A1, Th12; ::_thesis: verum end; theorem Th35: :: MODAL_1:35 for A, B, A1, B1 being MP-wff st A '&' B = A1 '&' B1 holds ( A = A1 & B = B1 ) proof let A, B, A1, B1 be MP-wff; ::_thesis: ( A '&' B = A1 '&' B1 implies ( A = A1 & B = B1 ) ) set e = elementary_tree 2; set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A); set y1 = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1); assume A1: A '&' B = A1 '&' B1 ; ::_thesis: ( A = A1 & B = B1 ) A2: <*1*> in elementary_tree 2 by TREES_1:28; A3: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28; then A4: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) = (dom ((elementary_tree 2) --> [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 ((elementary_tree 2) --> [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 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) by A2, A3, A4, TREES_1:def_9; A8: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by A3, TREES_2:def_11; then A9: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, A6, TREES_1:def_9; then A10: dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(dom B)) by TREES_2:def_11; A11: dom (A1 '&' B1) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1))) with-replacement (<*1*>,(dom B1)) by A7, TREES_2:def_11; now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_s_in_dom_B_implies_s_in_dom_B1_)_&_(_s_in_dom_B1_implies_s_in_dom_B_)_) let s be FinSequence of NAT ; ::_thesis: ( ( s in dom B implies s in dom B1 ) & ( s in dom B1 implies s in dom B ) ) thus ( s in dom B implies s in dom B1 ) ::_thesis: ( s in dom B1 implies s in dom B ) proof assume s in dom B ; ::_thesis: s in dom B1 then A12: <*1*> ^ s in dom (A1 '&' B1) by A1, A9, A10, TREES_1:def_9; now__::_thesis:_s_in_dom_B1 percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: s in dom B1 hence s in dom B1 by TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: s in dom B1 then <*1*> is_a_proper_prefix_of <*1*> ^ s by TREES_1:10; then ex w being FinSequence of NAT st ( w in dom B1 & <*1*> ^ s = <*1*> ^ w ) by A7, A11, A12, TREES_1:def_9; hence s in dom B1 by FINSEQ_1:33; ::_thesis: verum end; end; end; hence s in dom B1 ; ::_thesis: verum end; assume s in dom B1 ; ::_thesis: s in dom B then A13: <*1*> ^ s in dom (A '&' B) by A1, A7, A11, TREES_1:def_9; now__::_thesis:_s_in_dom_B percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: s in dom B hence s in dom B by TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: s in dom B then <*1*> is_a_proper_prefix_of <*1*> ^ s by TREES_1:10; then ex w being FinSequence of NAT 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; ::_thesis: verum end; end; end; hence s in dom B ; ::_thesis: verum end; then A14: dom B = dom B1 by TREES_2:def_1; A15: for s being FinSequence of NAT st s in dom B holds B . s = B1 . s proof let s be FinSequence of NAT ; ::_thesis: ( s in dom B implies B . s = B1 . s ) assume s in dom B ; ::_thesis: B . s = B1 . s 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 being FinSequence of NAT 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 being FinSequence of NAT 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 B . s = B1 . s by A1, A19, A20, FINSEQ_1:33; ::_thesis: verum 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 ((elementary_tree 2) --> [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 ((elementary_tree 2) --> [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, Th11; for s being FinSequence of NAT st s in dom A holds A . s = A1 . s proof let s be FinSequence of NAT ; ::_thesis: ( s in dom A implies A . s = A1 . s ) assume A26: s in dom A ; ::_thesis: A . s = A1 . s then A27: <*0*> ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A3, A8, TREES_1:def_9; A28: <*0*> is_a_prefix_of <*0*> ^ s by TREES_1:1; then A29: ex w being FinSequence of NAT st ( w in dom A & <*0*> ^ s = <*0*> ^ w & (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) . (<*0*> ^ s) = A . w ) by A3, A8, A27, TREES_2:def_11; <*0*> ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) by A3, A4, A25, A26, TREES_1:def_9; then A30: ex u being FinSequence of NAT st ( u in dom A1 & <*0*> ^ s = <*0*> ^ u & (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) . (<*0*> ^ s) = A1 . u ) by A3, A4, A28, TREES_2:def_11; not <*1*> is_a_proper_prefix_of <*0*> ^ s by Th3; then A31: <*0*> ^ s in dom (A '&' B) by A9, A10, A27, TREES_1:def_9; now__::_thesis:_for_w_being_FinSequence_of_NAT_holds_ (_not_w_in_dom_B_or_not_<*0*>_^_s_=_<*1*>_^_w_or_not_(A_'&'_B)_._(<*0*>_^_s)_=_B_._w_) given w being FinSequence of NAT such that w in dom B and A32: <*0*> ^ s = <*1*> ^ w and (A '&' B) . (<*0*> ^ s) = B . w ; ::_thesis: contradiction <*0*> is_a_prefix_of <*1*> ^ w by A32, TREES_1:1; hence contradiction by TREES_1:50; ::_thesis: verum end; then (A '&' B) . (<*0*> ^ s) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) . (<*0*> ^ s) by A9, A10, A31, TREES_2:def_11; then A33: A . s = (A1 '&' B) . (<*0*> ^ s) by A1, A21, A29, FINSEQ_1:33; now__::_thesis:_for_w_being_FinSequence_of_NAT_holds_ (_not_w_in_dom_B1_or_not_<*0*>_^_s_=_<*1*>_^_w_or_not_(A1_'&'_B1)_._(<*0*>_^_s)_=_B1_._w_) given w being FinSequence of NAT such that w in dom B1 and A34: <*0*> ^ s = <*1*> ^ w and (A1 '&' B1) . (<*0*> ^ s) = B1 . w ; ::_thesis: contradiction <*0*> is_a_prefix_of <*1*> ^ w by A34, TREES_1:1; hence contradiction by TREES_1:50; ::_thesis: verum end; then (A1 '&' B1) . (<*0*> ^ s) = (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A1)) . (<*0*> ^ s) by A1, A7, A11, A31, TREES_2:def_11; hence A . s = A1 . s by A21, A33, A30, FINSEQ_1:33; ::_thesis: verum end; hence ( A = A1 & B = B1 ) by A1, A5, A14, A23, A24, A15, Th11, TREES_2:31; ::_thesis: verum end; definition func VERUM -> MP-wff equals :: MODAL_1:def 15 (elementary_tree 0) --> [0,0]; coherence (elementary_tree 0) --> [0,0] is MP-wff by Th31; end; :: deftheorem defines VERUM MODAL_1:def_15_:_ VERUM = (elementary_tree 0) --> [0,0]; theorem Th36: :: MODAL_1:36 for A being MP-wff holds ( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p ) proof let A be MP-wff; ::_thesis: ( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p ) assume card (dom A) = 1 ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p ) then consider x being set such that A1: dom A = {x} by CARD_2:42; reconsider x = 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 succ x = {} ; ::_thesis: contradiction then A5: the Element of succ x in succ x ; succ x = { (x ^ <*n*>) where n is Element of NAT : x ^ <*n*> in dom A } by TREES_2:def_5; then ex n being Element of NAT st ( the Element of succ x = x ^ <*n*> & x ^ <*n*> in dom A ) by A5; hence contradiction by A4, TARSKI:def_1; ::_thesis: verum end; then A6: branchdeg x = 0 by CARD_1:27, TREES_2:def_12; now__::_thesis:_(_A_=_VERUM_or_ex_p_being_MP-variable_st_A_=_@_p_) percases ( A . x = [0,0] or ex n being Element of NAT st A . x = [3,n] ) by A6, Def5; suppose A . x = [0,0] ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p ) then for z being set st z in dom A holds A . z = [0,0] by A1, TARSKI:def_1; hence ( A = VERUM or ex p being MP-variable st A = @ p ) by A3, FUNCOP_1:11; ::_thesis: verum end; suppose ex n being Element of NAT st A . x = [3,n] ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p ) then consider n being Element of NAT such that A7: A . x = [3,n] ; reconsider p = [3,n] as MP-variable by ZFMISC_1:105; for z being set st z in dom A holds A . z = [3,n] by A1, A7, TARSKI:def_1; then A = @ p by A3, FUNCOP_1:11; hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; ::_thesis: verum end; end; end; hence ( A = VERUM or ex p being MP-variable st A = @ p ) ; ::_thesis: verum end; theorem Th37: :: MODAL_1:37 for A being MP-wff holds ( not card (dom A) >= 2 or ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) proof let A be MP-wff; ::_thesis: ( not card (dom A) >= 2 or ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) set b = branchdeg (Root (dom A)); set a = Root (dom A); assume A1: card (dom A) >= 2 ; ::_thesis: ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) A2: now__::_thesis:_not_branchdeg_(Root_(dom_A))_=_0 assume branchdeg (Root (dom A)) = 0 ; ::_thesis: contradiction then card (dom A) = 1 by Th17; hence contradiction by A1; ::_thesis: verum end; A3: branchdeg (Root (dom A)) <= 2 by Def5; now__::_thesis:_(_(_branchdeg_(Root_(dom_A))_=_1_&_ex_B_being_MP-wff_st_ (_ex_B_being_MP-wff_st_ (_A_=_'not'_B_or_A_=_(#)_B_)_or_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_)_)_or_(_branchdeg_(Root_(dom_A))_=_2_&_ex_B,_C_being_MP-wff_st_ (_ex_B_being_MP-wff_st_ (_A_=_'not'_B_or_A_=_(#)_B_)_or_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_)_)_) percases ( branchdeg (Root (dom A)) = 1 or branchdeg (Root (dom A)) = 2 ) by A3, A2, NAT_1:26; caseA4: branchdeg (Root (dom A)) = 1 ; ::_thesis: ex B being MP-wff st ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) then card (succ (Root (dom A))) = 1 by TREES_2:def_12; then consider x being set such that A5: succ (Root (dom A)) = {x} by CARD_2:42; x in succ (Root (dom A)) by A5, TARSKI:def_1; then reconsider x9 = x as Element of dom A ; take B = A | x9; ::_thesis: ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) now__::_thesis:_(_A_=_'not'_B_or_A_=_(#)_B_) percases ( A . (Root (dom A)) = [1,0] or A . (Root (dom A)) = [1,1] ) by A4, Def5; suppose A . (Root (dom A)) = [1,0] ; ::_thesis: ( A = 'not' B or A = (#) B ) then Root A = [1,0] ; hence ( A = 'not' B or A = (#) B ) by A5, Th23; ::_thesis: verum end; suppose A . (Root (dom A)) = [1,1] ; ::_thesis: ( A = 'not' B or A = (#) B ) then Root A = [1,1] ; hence ( A = 'not' B or A = (#) B ) by A5, Th23; ::_thesis: verum end; end; end; hence ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum end; caseA6: branchdeg (Root (dom A)) = 2 ; ::_thesis: ex B, C being MP-wff st ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) then A7: succ (Root (dom A)) = {<*0*>,<*1*>} by Th19; then ( <*0*> in succ (Root (dom A)) & <*1*> in succ (Root (dom A)) ) by TARSKI:def_2; then reconsider x = <*0*>, y = <*1*> as Element of dom A ; take B = A | x; ::_thesis: ex C being MP-wff st ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) take C = A | y; ::_thesis: ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) Root A = [2,0] by A6, Def5; then A = B '&' C by A7, Th25; hence ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum end; end; end; hence ( ex B being MP-wff st ( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum end; theorem Th38: :: MODAL_1:38 for A being MP-wff holds card (dom A) < card (dom ('not' A)) proof let A be MP-wff; ::_thesis: card (dom A) < card (dom ('not' A)) set e = elementary_tree 1; <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; then A1: <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13; then A2: dom ('not' A) = (dom ((elementary_tree 1) --> [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__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_s_in_dom_A_implies_o_^_s_in_dom_('not'_A)_)_&_(_o_^_s_in_dom_('not'_A)_implies_s_in_dom_A_)_) let s be FinSequence of NAT ; ::_thesis: ( ( s in dom A implies o ^ s in dom ('not' A) ) & ( o ^ s in dom ('not' A) implies s in dom A ) ) thus ( s in dom A implies o ^ s in dom ('not' A) ) by A1, A2, TREES_1:def_9; ::_thesis: ( o ^ s in dom ('not' A) implies s in dom A ) assume A3: o ^ s in dom ('not' A) ; ::_thesis: s in dom A now__::_thesis:_s_in_dom_A percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: s in dom A hence s in dom A by TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: s in dom A then o is_a_proper_prefix_of o ^ s by TREES_1:10; then ex w being FinSequence of NAT 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; ::_thesis: verum end; end; end; hence s in dom A ; ::_thesis: verum end; then A4: dom A = (dom ('not' A)) | o by TREES_1:def_6; o <> Root (dom ('not' A)) ; hence card (dom A) < card (dom ('not' A)) by A4, Th21; ::_thesis: verum end; theorem Th39: :: MODAL_1:39 for A being MP-wff holds card (dom A) < card (dom ((#) A)) proof let A be MP-wff; ::_thesis: card (dom A) < card (dom ((#) A)) set e = elementary_tree 1; <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; then A1: <*0*> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:13; then A2: dom ((#) A) = (dom ((elementary_tree 1) --> [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__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_s_in_dom_A_implies_o_^_s_in_dom_((#)_A)_)_&_(_o_^_s_in_dom_((#)_A)_implies_s_in_dom_A_)_) let s be FinSequence of NAT ; ::_thesis: ( ( s in dom A implies o ^ s in dom ((#) A) ) & ( o ^ s in dom ((#) A) implies s in dom A ) ) thus ( s in dom A implies o ^ s in dom ((#) A) ) by A1, A2, TREES_1:def_9; ::_thesis: ( o ^ s in dom ((#) A) implies s in dom A ) assume A3: o ^ s in dom ((#) A) ; ::_thesis: s in dom A now__::_thesis:_s_in_dom_A percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: s in dom A hence s in dom A by TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: s in dom A then o is_a_proper_prefix_of o ^ s by TREES_1:10; then ex w being FinSequence of NAT 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; ::_thesis: verum end; end; end; hence s in dom A ; ::_thesis: verum end; then A4: dom A = (dom ((#) A)) | o by TREES_1:def_6; o <> Root (dom ((#) A)) ; hence card (dom A) < card (dom ((#) A)) by A4, Th21; ::_thesis: verum end; theorem Th40: :: MODAL_1:40 for A, B being MP-wff holds ( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) ) proof let A, B be MP-wff; ::_thesis: ( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) ) set e = elementary_tree 2; set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A); A1: not <*1*> is_a_proper_prefix_of <*0*> by TREES_1:52; A2: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28; then A3: dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11; ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52; then A4: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, TREES_1:def_9; then A5: dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) 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 (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) 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__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_s_in_dom_A_implies_o_^_s_in_dom_(A_'&'_B)_)_&_(_o_^_s_in_dom_(A_'&'_B)_implies_s_in_dom_A_)_) let s be FinSequence of NAT ; ::_thesis: ( ( s in dom A implies o ^ s in dom (A '&' B) ) & ( o ^ s in dom (A '&' B) implies s in dom A ) ) thus ( s in dom A implies o ^ s in dom (A '&' B) ) ::_thesis: ( o ^ s in dom (A '&' B) implies s in dom A ) proof assume s in dom A ; ::_thesis: o ^ s in dom (A '&' B) then A6: o ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A2, A3, TREES_1:def_9; not <*1*> is_a_proper_prefix_of o ^ s by Th3; hence o ^ s in dom (A '&' B) by A4, A5, A6, TREES_1:def_9; ::_thesis: verum end; assume A7: o ^ s in dom (A '&' B) ; ::_thesis: s in dom A now__::_thesis:_s_in_dom_A percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: s in dom A hence s in dom A by TREES_1:22; ::_thesis: verum end; supposeA8: s <> {} ; ::_thesis: s in dom A now__::_thesis:_for_w_being_FinSequence_of_NAT_holds_ (_not_w_in_dom_B_or_not_o_^_s_=_<*1*>_^_w_) given w being FinSequence of NAT such that w in dom B and A9: o ^ s = <*1*> ^ w ; ::_thesis: contradiction o is_a_prefix_of <*1*> ^ w by A9, TREES_1:1; hence contradiction by TREES_1:50; ::_thesis: verum end; then A10: o ^ s in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A5, A7, TREES_1:def_9; o is_a_proper_prefix_of o ^ s by A8, TREES_1:10; then ex w being FinSequence of NAT st ( w in dom A & o ^ s = o ^ w ) by A2, A3, A10, TREES_1:def_9; hence s in dom A by FINSEQ_1:33; ::_thesis: verum end; end; end; hence s in dom A ; ::_thesis: verum end; then A11: dom A = (dom (A '&' B)) | o by TREES_1:def_6; now__::_thesis:_for_s_being_FinSequence_of_NAT_holds_ (_(_s_in_dom_B_implies_u_^_s_in_dom_(A_'&'_B)_)_&_(_u_^_s_in_dom_(A_'&'_B)_implies_s_in_dom_B_)_) let s be FinSequence of NAT ; ::_thesis: ( ( s in dom B implies u ^ s in dom (A '&' B) ) & ( u ^ s in dom (A '&' B) implies s in dom B ) ) thus ( s in dom B implies u ^ s in dom (A '&' B) ) by A4, A5, TREES_1:def_9; ::_thesis: ( u ^ s in dom (A '&' B) implies s in dom B ) assume A12: u ^ s in dom (A '&' B) ; ::_thesis: s in dom B now__::_thesis:_s_in_dom_B percases ( s = {} or s <> {} ) ; suppose s = {} ; ::_thesis: s in dom B hence s in dom B by TREES_1:22; ::_thesis: verum end; suppose s <> {} ; ::_thesis: s in dom B then <*1*> is_a_proper_prefix_of u ^ s by TREES_1:10; then ex w being FinSequence of NAT st ( w in dom B & u ^ s = <*1*> ^ w ) by A4, A5, A12, TREES_1:def_9; hence s in dom B by FINSEQ_1:33; ::_thesis: verum end; end; end; hence s in dom B ; ::_thesis: verum end; then A13: 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 A11, Th21; ::_thesis: card (dom B) < card (dom (A '&' B)) u <> Root (dom (A '&' B)) ; hence card (dom B) < card (dom (A '&' B)) by A13, Th21; ::_thesis: verum end; definition let IT be MP-wff; attrIT is atomic means :Def16: :: MODAL_1:def 16 ex p being MP-variable st IT = @ p; attrIT is negative means :Def17: :: MODAL_1:def 17 ex A being MP-wff st IT = 'not' A; attrIT is necessitive means :Def18: :: MODAL_1:def 18 ex A being MP-wff st IT = (#) A; attrIT is conjunctive means :Def19: :: MODAL_1:def 19 ex A, B being MP-wff st IT = A '&' B; end; :: deftheorem Def16 defines atomic MODAL_1:def_16_:_ for IT being MP-wff holds ( IT is atomic iff ex p being MP-variable st IT = @ p ); :: deftheorem Def17 defines negative MODAL_1:def_17_:_ for IT being MP-wff holds ( IT is negative iff ex A being MP-wff st IT = 'not' A ); :: deftheorem Def18 defines necessitive MODAL_1:def_18_:_ for IT being MP-wff holds ( IT is necessitive iff ex A being MP-wff st IT = (#) A ); :: deftheorem Def19 defines conjunctive MODAL_1:def_19_:_ for IT being MP-wff holds ( IT is conjunctive iff ex A, B being MP-wff st IT = A '&' B ); registration cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like atomic for Element of MP-WFF ; existence ex b1 being MP-wff st b1 is atomic proof reconsider p = [3,0] as MP-variable by ZFMISC_1:105; take @ p ; ::_thesis: @ p is atomic take p ; :: according to MODAL_1:def_16 ::_thesis: @ p = @ p thus @ p = @ p ; ::_thesis: verum end; cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like negative for Element of MP-WFF ; existence ex b1 being MP-wff st b1 is negative proof set A = VERUM ; take 'not' VERUM ; ::_thesis: 'not' VERUM is negative take VERUM ; :: according to MODAL_1:def_17 ::_thesis: 'not' VERUM = 'not' VERUM thus 'not' VERUM = 'not' VERUM ; ::_thesis: verum end; cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like necessitive for Element of MP-WFF ; existence ex b1 being MP-wff st b1 is necessitive proof set A = VERUM ; take (#) VERUM ; ::_thesis: (#) VERUM is necessitive take VERUM ; :: according to MODAL_1:def_18 ::_thesis: (#) VERUM = (#) VERUM thus (#) VERUM = (#) VERUM ; ::_thesis: verum end; cluster Relation-like [:NAT,NAT:] -valued Function-like finite DecoratedTree-like conjunctive for Element of MP-WFF ; existence ex b1 being MP-wff st b1 is conjunctive proof set B = VERUM ; set A = VERUM ; take VERUM '&' VERUM ; ::_thesis: VERUM '&' VERUM is conjunctive take VERUM ; :: according to MODAL_1:def_19 ::_thesis: ex B being MP-wff st VERUM '&' VERUM = VERUM '&' B take VERUM ; ::_thesis: VERUM '&' VERUM = VERUM '&' VERUM thus VERUM '&' VERUM = VERUM '&' VERUM ; ::_thesis: verum end; end; scheme :: MODAL_1:sch 1 MPInd{ P1[ Element of MP-WFF ] } : for A being Element of MP-WFF holds P1[A] provided A1: P1[ VERUM ] and A2: for p being MP-variable holds P1[ @ p] and A3: for A being Element of MP-WFF st P1[A] holds P1[ 'not' A] and A4: for A being Element of MP-WFF st P1[A] holds P1[ (#) A] and A5: for A, B being Element of MP-WFF st P1[A] & P1[B] holds P1[A '&' B] proof defpred S1[ Element of NAT ] means for A being MP-wff st card (dom A) <= $1 holds P1[A]; A6: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: for A being MP-wff st card (dom A) <= k holds P1[A] ; ::_thesis: S1[k + 1] let A be MP-wff; ::_thesis: ( card (dom A) <= k + 1 implies P1[A] ) assume A8: card (dom A) <= k + 1 ; ::_thesis: P1[A] set a = Root (dom A); set b = branchdeg (Root (dom A)); A9: branchdeg (Root (dom A)) <= 2 by Def5; now__::_thesis:_P1[A] percases ( branchdeg (Root (dom A)) = 0 or branchdeg (Root (dom A)) = 1 or branchdeg (Root (dom A)) = 2 ) by A9, NAT_1:26; suppose branchdeg (Root (dom A)) = 0 ; ::_thesis: P1[A] then A10: card (dom A) = 1 by Th17; now__::_thesis:_P1[A] percases ( A = VERUM or ex p being MP-variable st A = @ p ) by A10, Th36; suppose A = VERUM ; ::_thesis: P1[A] hence P1[A] by A1; ::_thesis: verum end; suppose ex p being MP-variable st A = @ p ; ::_thesis: P1[A] hence P1[A] by A2; ::_thesis: verum end; end; end; hence P1[A] ; ::_thesis: verum end; supposeA11: branchdeg (Root (dom A)) = 1 ; ::_thesis: P1[A] then A12: succ (Root (dom A)) = {<*0*>} by Th18; then <*0*> in succ (Root (dom 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, Th23; now__::_thesis:_P1[A] percases ( A . (Root (dom A)) = [1,0] or A . (Root (dom A)) = [1,1] ) by A11, Def5; supposeA14: A . (Root (dom A)) = [1,0] ; ::_thesis: P1[A] ( dom (A | o) = (dom A) | o & o <> Root (dom A) ) by TREES_2:def_10; then card (dom (A | o)) < k + 1 by A8, Th21, XXREAL_0:2; then A15: card (dom (A | o)) <= k by NAT_1:13; A = 'not' (A | o) by A13, A14; hence P1[A] by A3, A7, A15; ::_thesis: verum end; supposeA16: A . (Root (dom A)) = [1,1] ; ::_thesis: P1[A] ( dom (A | o) = (dom A) | o & o <> Root (dom A) ) by TREES_2:def_10; then card (dom (A | o)) < k + 1 by A8, Th21, XXREAL_0:2; then A17: card (dom (A | o)) <= k by NAT_1:13; A = (#) (A | o) by A13, A16; hence P1[A] by A4, A7, A17; ::_thesis: verum end; end; end; hence P1[A] ; ::_thesis: verum end; supposeA18: branchdeg (Root (dom A)) = 2 ; ::_thesis: P1[A] then A19: succ (Root (dom A)) = {<*0*>,<*1*>} by Th19; then ( <*0*> in succ (Root (dom A)) & <*1*> in succ (Root (dom 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, Th21, XXREAL_0:2; then card (dom (A | o1)) <= k by NAT_1:13; then A20: P1[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, Th21, XXREAL_0:2; then card (dom (A | o2)) <= k by NAT_1:13; then A21: P1[A | o2] by A7; A = (((elementary_tree 2) --> (Root A)) with-replacement (<*0*>,(A | o1))) with-replacement (<*1*>,(A | o2)) by A19, Th25; then A = (A | o1) '&' (A | o2) by A18, Def5; hence P1[A] by A5, A20, A21; ::_thesis: verum end; end; end; hence P1[A] ; ::_thesis: verum end; let A be MP-wff; ::_thesis: P1[A] A22: card (dom A) <= card (dom A) ; A23: S1[ 0 ] by NAT_1:2; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A23, A6); hence P1[A] by A22; ::_thesis: verum end; theorem :: MODAL_1:41 for A being 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 S1[ 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: S1[ VERUM ] ; A2: for A being Element of MP-WFF st S1[A] holds S1[ 'not' A] by Def17; A3: for A, B being Element of MP-WFF st S1[A] & S1[B] holds S1[A '&' B] by Def19; A4: for A being Element of MP-WFF st S1[A] holds S1[ (#) A] by Def18; A5: for p being MP-variable holds S1[ @ p] by Def16; thus for A being Element of MP-WFF holds S1[A] from MODAL_1:sch_1(A1, A5, A2, A4, A3); ::_thesis: verum end; theorem Th42: :: MODAL_1:42 for A being MP-wff holds ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) proof let A be MP-wff; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) now__::_thesis:_(_A_=_VERUM_or_ex_p_being_MP-variable_st_A_=_@_p_or_ex_B_being_MP-wff_st_A_=_'not'_B_or_ex_B_being_MP-wff_st_A_=_(#)_B_or_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_) percases ( card (dom A) = 1 or card (dom A) >= 2 ) by NAT_1:26; suppose card (dom A) = 1 ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) by Th36; ::_thesis: verum end; suppose card (dom A) >= 2 ; ::_thesis: ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) by Th37; ::_thesis: verum end; end; end; hence ( A = VERUM or ex p being MP-variable st A = @ p or ex B being MP-wff st A = 'not' B or ex B being MP-wff st A = (#) B or ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: verum end; theorem Th43: :: MODAL_1:43 for p being MP-variable for A, B being MP-wff holds ( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B ) proof let p be MP-variable; ::_thesis: for A, B being MP-wff holds ( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B ) let A, B be MP-wff; ::_thesis: ( @ p <> 'not' A & @ p <> (#) A & @ p <> A '&' B ) set e2 = elementary_tree 2; set e1 = elementary_tree 1; set e0 = elementary_tree 0; A1: dom (@ p) = elementary_tree 0 by FUNCOP_1:13; A2: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; dom ((elementary_tree 1) --> [1,0]) = elementary_tree 1 by FUNCOP_1:13; then dom ('not' A) = (elementary_tree 1) 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; ::_thesis: ( @ p <> (#) A & @ p <> A '&' B ) dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 by FUNCOP_1:13; then dom ((#) A) = (elementary_tree 1) 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; ::_thesis: @ p <> A '&' B set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A); A3: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52; A4: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28; then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11; then A5: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A3, TREES_1:def_9; then dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) with-replacement (<*1*>,(dom B)) by TREES_2:def_11; then <*1*> in dom (A '&' B) by A5, TREES_1:def_9; hence @ p <> A '&' B by A1, TARSKI:def_1, TREES_1:29; ::_thesis: verum end; theorem Th44: :: MODAL_1:44 for A, B, C being MP-wff holds ( 'not' A <> (#) B & 'not' A <> B '&' C ) proof let A, B, C be MP-wff; ::_thesis: ( 'not' A <> (#) B & 'not' A <> B '&' C ) set e2 = elementary_tree 2; set e1 = elementary_tree 1; set E = (elementary_tree 1) --> [1,0]; set F = (elementary_tree 1) --> [1,1]; reconsider e = {} as Element of dom ('not' A) by TREES_1:22; A1: ( {} in dom ((#) B) & ( for u being FinSequence of NAT holds ( not u in dom B or not e = <*0*> ^ u or not ((#) B) . e = B . u ) ) ) by TREES_1:22; A2: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; then A3: <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13; then A4: dom ('not' A) = (dom ((elementary_tree 1) --> [1,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11; A5: <*0*> in dom ((elementary_tree 1) --> [1,1]) by A2, FUNCOP_1:13; then dom ((#) B) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom B)) by TREES_2:def_11; then A6: ((#) B) . e = ((elementary_tree 1) --> [1,1]) . e by A5, A1, TREES_2:def_11; e in elementary_tree 1 by TREES_1:22; then A7: ( ((elementary_tree 1) --> [1,0]) . e = [1,0] & ((elementary_tree 1) --> [1,1]) . e = [1,1] ) by FUNCOP_1:7; ( ( for u being FinSequence of NAT holds ( not u in dom A or not e = <*0*> ^ u or not ('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; ::_thesis: 'not' A <> B '&' C set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B); A8: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52; A9: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28; then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom B)) by TREES_2:def_11; then A10: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) by A9, A8, TREES_1:def_9; then dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B))) 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__::_thesis:_not_<*1*>_in_dom_((elementary_tree_1)_-->_[1,0]) assume <*1*> in dom ((elementary_tree 1) --> [1,0]) ; ::_thesis: contradiction then ( <*1*> = {} or <*1*> = <*0*> ) by TARSKI:def_2, TREES_1:51; hence contradiction by TREES_1:3; ::_thesis: verum end; assume not 'not' A <> B '&' C ; ::_thesis: contradiction then ex s being FinSequence of NAT 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; ::_thesis: verum end; theorem Th45: :: MODAL_1:45 for A, B, C being MP-wff holds (#) A <> B '&' C proof let A, B, C be MP-wff; ::_thesis: (#) A <> B '&' C set e2 = elementary_tree 2; set e1 = elementary_tree 1; set F = (elementary_tree 1) --> [1,1]; set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B); A1: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52; A2: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28; then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom B)) by TREES_2:def_11; then A3: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B)) by A2, A1, TREES_1:def_9; then dom (B '&' C) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,B))) 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 (#) A <> B '&' C ; ::_thesis: contradiction A6: now__::_thesis:_not_<*1*>_in_dom_((elementary_tree_1)_-->_[1,1]) assume <*1*> in dom ((elementary_tree 1) --> [1,1]) ; ::_thesis: contradiction then ( <*1*> = {} or <*1*> = <*0*> ) by TARSKI:def_2, TREES_1:51; hence contradiction by TREES_1:3; ::_thesis: verum end; <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; then A7: <*0*> in dom ((elementary_tree 1) --> [1,1]) by FUNCOP_1:13; then dom ((#) A) = (dom ((elementary_tree 1) --> [1,1])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11; then ex s being FinSequence of NAT 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; ::_thesis: verum end; Lm4: for A, B being MP-wff holds ( VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B ) proof let A, B be MP-wff; ::_thesis: ( VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B ) set e2 = elementary_tree 2; set e1 = elementary_tree 1; A1: dom VERUM = elementary_tree 0 by FUNCOP_1:13; set F = (elementary_tree 1) --> [1,1]; set E = (elementary_tree 1) --> [1,0]; A2: <*0*> in elementary_tree 1 by TARSKI:def_2, TREES_1:51; then <*0*> in dom ((elementary_tree 1) --> [1,0]) by FUNCOP_1:13; then ( dom ((elementary_tree 1) --> [1,0]) = elementary_tree 1 & dom ('not' A) = (dom ((elementary_tree 1) --> [1,0])) 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; ::_thesis: ( VERUM <> (#) A & VERUM <> A '&' B ) <*0*> in dom ((elementary_tree 1) --> [1,1]) by A2, FUNCOP_1:13; then ( dom ((elementary_tree 1) --> [1,1]) = elementary_tree 1 & dom ((#) A) = (dom ((elementary_tree 1) --> [1,1])) 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; ::_thesis: VERUM <> A '&' B set y = ((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A); A3: ( <*1*> in elementary_tree 2 & not <*0*> is_a_proper_prefix_of <*1*> ) by TREES_1:28, TREES_1:52; A4: ( <*0*> in elementary_tree 2 & dom ((elementary_tree 2) --> [2,0]) = elementary_tree 2 ) by FUNCOP_1:13, TREES_1:28; then dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) = (dom ((elementary_tree 2) --> [2,0])) with-replacement (<*0*>,(dom A)) by TREES_2:def_11; then A5: <*1*> in dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A)) by A4, A3, TREES_1:def_9; then dom (A '&' B) = (dom (((elementary_tree 2) --> [2,0]) with-replacement (<*0*>,A))) 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 VERUM <> A '&' B ; ::_thesis: contradiction hence contradiction by A1, A6, TARSKI:def_1, TREES_1:29; ::_thesis: verum end; Lm5: [0,0] is MP-conective proof 0 in {0,1,2} by ENUMSET1:def_1; hence [0,0] is MP-conective by ZFMISC_1:87; ::_thesis: verum end; Lm6: for p being MP-variable holds VERUM <> @ p proof let p be MP-variable; ::_thesis: VERUM <> @ p assume A1: not VERUM <> @ p ; ::_thesis: contradiction ( 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, Th26, XBOOLE_0:3; ::_thesis: verum end; theorem :: MODAL_1:46 for p being MP-variable for A, B being MP-wff holds ( VERUM <> @ p & VERUM <> 'not' A & VERUM <> (#) A & VERUM <> A '&' B ) by Lm4, Lm6; scheme :: MODAL_1:sch 2 MPFuncEx{ F1() -> non empty set , F2() -> Element of F1(), F3( Element of MP-variables ) -> Element of F1(), F4( Element of F1()) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1() } : ex f being Function of MP-WFF,F1() st ( f . VERUM = F2() & ( for p being MP-variable holds f . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds f . ('not' A) = F4((f . A)) ) & ( for A being Element of MP-WFF holds f . ((#) A) = F5((f . A)) ) & ( for A, B being Element of MP-WFF holds f . (A '&' B) = F6((f . A),(f . B)) ) ) proof defpred S1[ Function of MP-WFF,F1(), Element of NAT ] means for A being MP-wff st card (dom A) <= $2 holds ( ( A = VERUM implies $1 . A = F2() ) & ( for p being MP-variable st A = @ p holds $1 . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds $1 . A = F4(($1 . B)) ) & ( for B being MP-wff st A = (#) B holds $1 . A = F5(($1 . B)) ) & ( for B, C being MP-wff st A = B '&' C holds $1 . A = F6(($1 . B),($1 . C)) ) ); defpred S2[ Element of F1(), Function of MP-WFF,F1(), Element of MP-WFF ] means ( ( $3 = VERUM implies $1 = F2() ) & ( for p being MP-variable st $3 = @ p holds $1 = F3(p) ) & ( for A being MP-wff st $3 = 'not' A holds $1 = F4(($2 . A)) ) & ( for A being MP-wff st $3 = (#) A holds $1 = F5(($2 . A)) ) & ( for A, B being MP-wff st $3 = A '&' B holds $1 = F6(($2 . A),($2 . B)) ) ); defpred S3[ Element of NAT ] means ex F being Function of MP-WFF,F1() st S1[F,$1]; defpred S4[ set , set ] means ex A being Element of MP-WFF st ( A = $1 & ( for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds $2 = g . A ) ); A1: for k being Element of NAT st S3[k] holds S3[k + 1] proof let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] ) given F being Function of MP-WFF,F1() such that A2: S1[F,k] ; ::_thesis: S3[k + 1] defpred S5[ Element of MP-WFF , Element of F1()] means ( ( card (dom $1) <> k + 1 implies $2 = F . $1 ) & ( card (dom $1) = k + 1 implies S2[$2,F,$1] ) ); A3: for x being Element of MP-WFF ex y being Element of F1() st S5[x,y] proof let A be Element of MP-WFF ; ::_thesis: ex y being Element of F1() st S5[A,y] now__::_thesis:_(_(_card_(dom_A)_<>_k_+_1_&_ex_y_being_Element_of_F1()_st_verum_)_or_(_card_(dom_A)_=_k_+_1_&_A_=_VERUM_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_p_being_MP-variable_st_A_=_@_p_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_B_being_MP-wff_st_A_=_'not'_B_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_B_being_MP-wff_st_A_=_(#)_B_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_or_(_card_(dom_A)_=_k_+_1_&_ex_B,_C_being_MP-wff_st_A_=_B_'&'_C_&_ex_y_being_Element_of_F1()_st_S2[y,F,A]_)_) percases ( card (dom A) <> k + 1 or ( card (dom A) = k + 1 & A = VERUM ) or ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) or ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ) by Th42; case card (dom A) <> k + 1 ; ::_thesis: ex y being Element of F1() st verum take y = F . A; ::_thesis: verum end; caseA4: ( card (dom A) = k + 1 & A = VERUM ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A] take y = F2(); ::_thesis: S2[y,F,A] thus S2[y,F,A] by A4, Lm4, Lm6; ::_thesis: verum end; case ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A] then consider p being MP-variable such that A5: A = @ p ; take y = F3(p); ::_thesis: S2[y,F,A] thus S2[y,F,A] by A5, Lm6, Th32, Th43; ::_thesis: verum end; case ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A] then consider B being MP-wff such that A6: A = 'not' B ; take y = F4((F . B)); ::_thesis: S2[y,F,A] thus S2[y,F,A] by A6, Lm4, Th33, Th43, Th44; ::_thesis: verum end; case ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A] then consider B being MP-wff such that A7: A = (#) B ; take y = F5((F . B)); ::_thesis: S2[y,F,A] thus S2[y,F,A] by A7, Lm4, Th34, Th43, Th44, Th45; ::_thesis: verum end; case ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ; ::_thesis: ex y being Element of F1() st S2[y,F,A] then consider B, C being MP-wff such that A8: A = B '&' C ; take y = F6((F . B),(F . C)); ::_thesis: S2[y,F,A] now__::_thesis:_for_B1,_C1_being_MP-wff_st_A_=_B1_'&'_C1_holds_ y_=_F6((F_._B1),(F_._C1)) let B1, C1 be MP-wff; ::_thesis: ( A = B1 '&' C1 implies y = F6((F . B1),(F . C1)) ) assume A9: A = B1 '&' C1 ; ::_thesis: y = F6((F . B1),(F . C1)) then B = B1 by A8, Th35; hence y = F6((F . B1),(F . C1)) by A8, A9, Th35; ::_thesis: verum end; hence S2[y,F,A] by A8, Lm4, Th43, Th44, Th45; ::_thesis: verum end; end; end; hence ex y being Element of F1() st S5[A,y] ; ::_thesis: verum end; consider G being Function of MP-WFF,F1() such that A10: for p being Element of MP-WFF holds S5[p,G . p] from FUNCT_2:sch_3(A3); take H = G; ::_thesis: S1[H,k + 1] thus S1[H,k + 1] ::_thesis: verum proof let A be Element of MP-WFF ; ::_thesis: ( card (dom A) <= k + 1 implies ( ( A = VERUM implies H . A = F2() ) & ( for p being MP-variable st A = @ p holds H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds H . A = F6((H . B),(H . C)) ) ) ) set p = card (dom A); assume A11: card (dom A) <= k + 1 ; ::_thesis: ( ( A = VERUM implies H . A = F2() ) & ( for p being MP-variable st A = @ p holds H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds H . A = F6((H . B),(H . C)) ) ) thus ( A = VERUM implies H . A = F2() ) ::_thesis: ( ( for p being MP-variable st A = @ p holds H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds H . A = F6((H . B),(H . C)) ) ) proof percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ; suppose card (dom A) <> k + 1 ; ::_thesis: ( A = VERUM implies H . A = F2() ) then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8; hence ( A = VERUM implies H . A = F2() ) by A2; ::_thesis: verum end; suppose card (dom A) = k + 1 ; ::_thesis: ( A = VERUM implies H . A = F2() ) hence ( A = VERUM implies H . A = F2() ) by A10; ::_thesis: verum end; end; end; thus for p being MP-variable st A = @ p holds H . A = F3(p) ::_thesis: ( ( for B being MP-wff st A = 'not' B holds H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds H . A = F6((H . B),(H . C)) ) ) proof let q be MP-variable; ::_thesis: ( A = @ q implies H . A = F3(q) ) assume A12: A = @ q ; ::_thesis: H . A = F3(q) percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ; suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F3(q) then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8; hence H . A = F3(q) by A2, A12; ::_thesis: verum end; suppose card (dom A) = k + 1 ; ::_thesis: H . A = F3(q) hence H . A = F3(q) by A10, A12; ::_thesis: verum end; end; end; thus for B being MP-wff st A = 'not' B holds H . A = F4((H . B)) ::_thesis: ( ( for B being MP-wff st A = (#) B holds H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds H . A = F6((H . B),(H . C)) ) ) proof let B be MP-wff; ::_thesis: ( A = 'not' B implies H . A = F4((H . B)) ) assume A13: A = 'not' B ; ::_thesis: H . A = F4((H . B)) then card (dom B) <> k + 1 by A11, Th38; then A14: H . B = F . B by A10; percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ; suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F4((H . B)) then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8; hence H . A = F4((H . B)) by A2, A13, A14; ::_thesis: verum end; suppose card (dom A) = k + 1 ; ::_thesis: H . A = F4((H . B)) hence H . A = F4((H . B)) by A10, A13, A14; ::_thesis: verum end; end; end; thus for B being MP-wff st A = (#) B holds H . A = F5((H . B)) ::_thesis: for B, C being MP-wff st A = B '&' C holds H . A = F6((H . B),(H . C)) proof let B be MP-wff; ::_thesis: ( A = (#) B implies H . A = F5((H . B)) ) assume A15: A = (#) B ; ::_thesis: H . A = F5((H . B)) then card (dom B) <> k + 1 by A11, Th39; then A16: H . B = F . B by A10; percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ; suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F5((H . B)) then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8; hence H . A = F5((H . B)) by A2, A15, A16; ::_thesis: verum end; suppose card (dom A) = k + 1 ; ::_thesis: H . A = F5((H . B)) hence H . A = F5((H . B)) by A10, A15, A16; ::_thesis: verum end; end; end; thus for B, C being MP-wff st A = B '&' C holds H . A = F6((H . B),(H . C)) ::_thesis: verum proof let B, C be MP-wff; ::_thesis: ( A = B '&' C implies H . A = F6((H . B),(H . C)) ) assume A17: A = B '&' C ; ::_thesis: H . A = F6((H . B),(H . C)) then card (dom B) <> k + 1 by A11, Th40; then A18: H . B = F . B by A10; card (dom C) <> k + 1 by A11, A17, Th40; then A19: H . C = F . C by A10; percases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ; suppose card (dom A) <> k + 1 ; ::_thesis: H . A = F6((H . B),(H . C)) then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8; hence H . A = F6((H . B),(H . C)) by A2, A17, A18, A19; ::_thesis: verum end; suppose card (dom A) = k + 1 ; ::_thesis: H . A = F6((H . B),(H . C)) hence H . A = F6((H . B),(H . C)) by A10, A17, A18, A19; ::_thesis: verum end; end; end; end; end; A20: S3[ 0 ] proof set F = the Function of MP-WFF,F1(); take the Function of MP-WFF,F1() ; ::_thesis: S1[ the Function of MP-WFF,F1(), 0 ] let A be MP-wff; ::_thesis: ( card (dom A) <= 0 implies ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) ) ) assume card (dom A) <= 0 ; ::_thesis: ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) ) hence ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) ) by NAT_1:2; ::_thesis: verum end; A21: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A20, A1); A22: for x being set st x in MP-WFF holds ex y being set st S4[x,y] proof let x be set ; ::_thesis: ( x in MP-WFF implies ex y being set st S4[x,y] ) assume x in MP-WFF ; ::_thesis: ex y being set st S4[x,y] then reconsider x9 = x as Element of MP-WFF ; consider F being Function of MP-WFF,F1() such that A23: S1[F, card (dom x9)] by A21; take F . x ; ::_thesis: S4[x,F . x] take x9 ; ::_thesis: ( x9 = x & ( for g being Function of MP-WFF,F1() st S1[g, card (dom x9)] holds F . x = g . x9 ) ) thus x = x9 ; ::_thesis: for g being Function of MP-WFF,F1() st S1[g, card (dom x9)] holds F . x = g . x9 let G be Function of MP-WFF,F1(); ::_thesis: ( S1[G, card (dom x9)] implies F . x = G . x9 ) defpred S5[ Element of MP-WFF ] means ( card (dom $1) <= card (dom x9) implies F . $1 = G . $1 ); assume A24: S1[G, card (dom x9)] ; ::_thesis: F . x = G . x9 A25: for p being MP-variable holds S5[ @ p] proof let p be MP-variable; ::_thesis: S5[ @ p] assume A26: card (dom (@ p)) <= card (dom x9) ; ::_thesis: F . (@ p) = G . (@ p) hence F . (@ p) = F3(p) by A23 .= G . (@ p) by A24, A26 ; ::_thesis: verum end; A27: for A, B being Element of MP-WFF st S5[A] & S5[B] holds S5[A '&' B] proof let A, B be MP-wff; ::_thesis: ( S5[A] & S5[B] implies S5[A '&' B] ) assume that A28: ( S5[A] & S5[B] ) and A29: card (dom (A '&' B)) <= card (dom x9) ; ::_thesis: F . (A '&' B) = G . (A '&' B) ( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) ) by Th40; hence F . (A '&' B) = F6((G . A),(G . B)) by A23, A28, A29, XXREAL_0:2 .= G . (A '&' B) by A24, A29 ; ::_thesis: verum end; A30: for A being Element of MP-WFF st S5[A] holds S5[ (#) A] proof let A be MP-wff; ::_thesis: ( S5[A] implies S5[ (#) A] ) assume A31: S5[A] ; ::_thesis: S5[ (#) A] assume A32: card (dom ((#) A)) <= card (dom x9) ; ::_thesis: F . ((#) A) = G . ((#) A) card (dom A) < card (dom ((#) A)) by Th39; hence F . ((#) A) = F5((G . A)) by A23, A31, A32, XXREAL_0:2 .= G . ((#) A) by A24, A32 ; ::_thesis: verum end; A33: for A being Element of MP-WFF st S5[A] holds S5[ 'not' A] proof let A be MP-wff; ::_thesis: ( S5[A] implies S5[ 'not' A] ) assume A34: S5[A] ; ::_thesis: S5[ 'not' A] assume A35: card (dom ('not' A)) <= card (dom x9) ; ::_thesis: F . ('not' A) = G . ('not' A) card (dom A) < card (dom ('not' A)) by Th38; hence F . ('not' A) = F4((G . A)) by A23, A34, A35, XXREAL_0:2 .= G . ('not' A) by A24, A35 ; ::_thesis: verum end; A36: S5[ VERUM ] proof assume A37: card (dom VERUM) <= card (dom x9) ; ::_thesis: F . VERUM = G . VERUM hence F . VERUM = F2() by A23 .= G . VERUM by A24, A37 ; ::_thesis: verum end; for p being Element of MP-WFF holds S5[p] from MODAL_1:sch_1(A36, A25, A33, A30, A27); hence F . x = G . x9 ; ::_thesis: verum end; consider F being Function such that A38: dom F = MP-WFF and A39: for x being set st x in MP-WFF holds S4[x,F . x] from CLASSES1:sch_1(A22); rng F c= F1() proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in F1() ) assume y in rng F ; ::_thesis: y in F1() then consider x being set such that A40: ( x in MP-WFF & y = F . x ) by A38, FUNCT_1:def_3; consider p being Element of MP-WFF such that p = x and A41: for g being Function of MP-WFF,F1() st S1[g, card (dom p)] holds y = g . p by A39, A40; consider G being Function of MP-WFF,F1() such that A42: S1[G, card (dom p)] by A21; y = G . p by A41, A42; hence y in F1() ; ::_thesis: verum end; then reconsider F = F as Function of MP-WFF,F1() by A38, FUNCT_2:def_1, RELSET_1:4; consider A being MP-wff such that A43: A = VERUM and A44: for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds F . VERUM = g . A by A39; take F ; ::_thesis: ( F . VERUM = F2() & ( for p being MP-variable holds F . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) ) consider G being Function of MP-WFF,F1() such that A45: S1[G, card (dom A)] by A21; F . VERUM = G . VERUM by A43, A44, A45; hence F . VERUM = F2() by A43, A45; ::_thesis: ( ( for p being MP-variable holds F . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) ) thus for p being MP-variable holds F . (@ p) = F3(p) ::_thesis: ( ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) ) proof let p be MP-variable; ::_thesis: F . (@ p) = F3(p) consider A being MP-wff such that A46: A = @ p and A47: for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds F . (@ p) = g . A by A39; consider G being Function of MP-WFF,F1() such that A48: S1[G, card (dom A)] by A21; F . (@ p) = G . (@ p) by A46, A47, A48; hence F . (@ p) = F3(p) by A46, A48; ::_thesis: verum end; thus for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ::_thesis: ( ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) ) proof let A be Element of MP-WFF ; ::_thesis: F . ('not' A) = F4((F . A)) consider A1 being MP-wff such that A49: A1 = 'not' A and A50: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds F . ('not' A) = g . A1 by A39; consider G being Function of MP-WFF,F1() such that A51: S1[G, card (dom A1)] by A21; A52: for k being Element of NAT st k < card (dom ('not' A)) holds S1[G,k] proof let k be Element of NAT ; ::_thesis: ( k < card (dom ('not' A)) implies S1[G,k] ) assume A53: k < card (dom ('not' A)) ; ::_thesis: S1[G,k] let a be Element of MP-WFF ; ::_thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) ) assume card (dom a) <= k ; ::_thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) then card (dom a) <= card (dom ('not' A)) by A53, XXREAL_0:2; hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) by A49, A51; ::_thesis: verum end; A54: ex B being MP-wff st ( B = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B)] holds F . A = g . B ) ) by A39; set k = card (dom A); card (dom A) < card (dom ('not' A)) by Th38; then S1[G, card (dom A)] by A52; then A55: F . A = G . A by A54; F . ('not' A) = G . ('not' A) by A49, A50, A51; hence F . ('not' A) = F4((F . A)) by A49, A51, A55; ::_thesis: verum end; thus for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ::_thesis: for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) proof let A be Element of MP-WFF ; ::_thesis: F . ((#) A) = F5((F . A)) consider A1 being MP-wff such that A56: A1 = (#) A and A57: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds F . ((#) A) = g . A1 by A39; consider G being Function of MP-WFF,F1() such that A58: S1[G, card (dom A1)] by A21; A59: for k being Element of NAT st k < card (dom ((#) A)) holds S1[G,k] proof let k be Element of NAT ; ::_thesis: ( k < card (dom ((#) A)) implies S1[G,k] ) assume A60: k < card (dom ((#) A)) ; ::_thesis: S1[G,k] let a be Element of MP-WFF ; ::_thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) ) assume card (dom a) <= k ; ::_thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) then card (dom a) <= card (dom ((#) A)) by A60, XXREAL_0:2; hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) by A56, A58; ::_thesis: verum end; A61: ex B being MP-wff st ( B = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B)] holds F . A = g . B ) ) by A39; set k = card (dom A); card (dom A) < card (dom ((#) A)) by Th39; then S1[G, card (dom A)] by A59; then A62: F . A = G . A by A61; F . ((#) A) = G . ((#) A) by A56, A57, A58; hence F . ((#) A) = F5((F . A)) by A56, A58, A62; ::_thesis: verum end; thus for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ::_thesis: verum proof let A, B be Element of MP-WFF ; ::_thesis: F . (A '&' B) = F6((F . A),(F . B)) set k1 = card (dom A); set k2 = card (dom B); consider A1 being MP-wff such that A63: A1 = A '&' B and A64: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds F . (A '&' B) = g . A1 by A39; consider G being Function of MP-WFF,F1() such that A65: S1[G, card (dom A1)] by A21; A66: for k being Element of NAT st k < card (dom (A '&' B)) holds S1[G,k] proof let k be Element of NAT ; ::_thesis: ( k < card (dom (A '&' B)) implies S1[G,k] ) assume A67: k < card (dom (A '&' B)) ; ::_thesis: S1[G,k] let a be Element of MP-WFF ; ::_thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) ) assume card (dom a) <= k ; ::_thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) then card (dom a) <= card (dom (A '&' B)) by A67, XXREAL_0:2; hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds G . a = F6((G . B),(G . C)) ) ) by A63, A65; ::_thesis: verum end; A68: ex B1 being MP-wff st ( B1 = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B1)] holds F . A = g . B1 ) ) by A39; card (dom A) < card (dom (A '&' B)) by Th40; then S1[G, card (dom A)] by A66; then A69: F . A = G . A by A68; A70: ex C being MP-wff st ( C = B & ( for g being Function of MP-WFF,F1() st S1[g, card (dom C)] holds F . B = g . C ) ) by A39; card (dom B) < card (dom (A '&' B)) by Th40; then S1[G, card (dom B)] by A66; then A71: F . B = G . B by A70; F . (A '&' B) = G . (A '&' B) by A63, A64, A65; hence F . (A '&' B) = F6((F . A),(F . B)) by A63, A65, A69, A71; ::_thesis: verum end; end;