• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    Some Results on Rewritability in Modal Logics over Tree Models*

    2020-08-01 10:20:58ShanshanDu
    邏輯學(xué)研究 2020年3期

    Shanshan Du

    Abstract.We have investigated locally equivalent and m-conservative rewritabilities in modal logics over tree models.The modal languages studied in this paper are ML,MLI,MLG and MLGI.

    1 Introduction

    Over the past 100 years,many artificial languages in distinct expressiveness powers and complexity degrees have been introduced.They range from classical first-order and higher-order predicate languages to a large variety of modal languages.

    Different types of languages may be“expressed”by other languages.For example,it is well known that each ML-formula is locally equivalently rewritable into a first-order formula over models.However,the converse does not hold:

    ? There are fisrt-order formulas that cannot be locally equivalently rewritable into an ML-formula.

    van Benthem Characterization Theorem in[2]characterizes when exactly a first-order formula is locally equivalently rewritable into an ML-formula.Following van Benthem Characterization Theorem,(locally)equivalent rewritability has become an important and active research problem in modal logic([4])and computer science([11,12])over the past 40 years.

    E.Rosen has proved characterization theorems on(locally)equivalent rewritability over finite Kripke models in [16].Characterization theorems over any class of Kripke models are proved by M.Otto in[14],where different versions of characterization theorems for MLI,ML plus a global modality and MLI plus a global modality are also proved.M.de Rijke proves characterization theorems for MLG in[15].Otto proves similar theorems forμML1The modal languageμML is ML plus a monadic least fixed point operator.in[13].A.Dawar and Otto proves several characterization theorems over kinds of classes of frames in[6].A model-theoretic characterization of MSO2MSO represents“monadic second-order”.toμML is proved by D.Janin and I.Walukiewicz in[9].G.Fontaine proves a model-theoretic characterization of MSO toμML over tree models in[7].Some theorems on globally equivalent rewritability of MLI to ML,MLG to ML,ML to EL3ML is the standard modal language;MLI is ML plus inverse modalities;MLG is ML plus graded modalities; MLGI is ML plus graded and inverse modalities; EL is a tractable modal language.For reference,see[17].over models are proved by F.Wolter in[17].

    Equivalent rewritability is an important notion,but it is rather strict for it cannot introduce additional non-logical symbols.So it is necessary to introduce a weaker notion admitting additional non-logical symbols,i.e.,“conservative rewritability”,which aims at a conservative extension rather than an equivalent one.Conservative rewritability is often studied in description logics([1]).Some important theorems in this area are proved by[10]and[12].[7]resolves the global case of m-conservative(i.e.,model conservative)rewritability of MSO toμML over tree models.The locally m-conservative rewritability of MLG to ML over tree models can be inferred from some results in [7].[17]characterizes the global cases of s-conservative4S-conservative rewritability is another notion of conservative rewritability,being different from m-conservative rewritability.However,it is not studied in this paper.For reference,see[10].and mconservative rewritability of MLI to ML,MLG to ML and ML to EL over models.

    Local equivalent and m-conservative rewritability over tree models are studied in this paper.Modal lauguages considered include ML,MLI,MLG and MLGI.Section 3 of this paper proves that each MLI-formula is equivalently rewritable into an MLformula at roots over tree models.Section 4 resolves whether each MLGI-formula is equivalently rewritable into an MLG-formula at roots over tree models.Section 5 characterizes the equivalent and m-conservative rewritability of“MLGI to MLI”over tree models.Section 6 resolves m-conservative rewritability of“MLGI to ML”over tree models.

    2 Preliminaries

    SyntaxML-formulas are formed according to the rule:

    φ::=5represents ≥1.

    wherepis a propositional variable.Other connectives are defined as follows:φ ∨ψ::=?(?φ ∧?ψ),::=p ∨?p,⊥::=,::=.

    MLI is ML plus,6?represents ?≥1.MLG is ML plusand MLGI is ML plusand.It should be noticed that

    ModelA(Kripke)frame Fis a pair(W,R)and a(Kripke)model Mis a triple(W,R,V),whereWis a non-empty set of states,Ris a binary relation onWandVis a valuation.A pointed model is a pair(M,d),whereMis a model andd ∈W.

    LetRrtbe the reflexive transitive closure ofR.If there is a uniqued?∈Wsuch thatd?Rrtdfor eachd ∈W,then the frame(W,R)is calledrootedandd?is its root.A rooted frame(W,R)withd?being its root is atreeif each stated ∈Wis reachable fromd?by a uniqueR-pathd?R···Rd.A model (W,R,V) is a tree model if its underlying frame(W,R)is a tree.

    The truth-relations for ML-formulas(MLI-formulas,MLG-formulas and MLGIformulas)are defined in the familiar way for the atomic and boolean cases.The other cases are as follows:

    ? (M,d)|=iff(M,d′)|=αfor at leastndifferent pointsd′ ∈Wsuch thatdRd′;

    ? (M,d)|=iff(M,d′)|=αfor at leastndifferent pointsd′ ∈Wsuch thatd′Rd;

    V(φ)is defined as{d ∈W:(M,d)|=φ}for each formulaφ.

    RewritabilityLetLi(i ∈{1,2}) be a modal language.AnL1-formulaφislocally equivalently rewritableinto anL2-formula(or a set ofL2-formulas ??)over a class of modelsCif there is anL2-formulaψ(or a set ofL2-formulas ??)such that

    ? for each modelM=(W,R,V)∈Candd ∈W,(M,d)|=φiff(M,d)|=ψ(or(M,d)|=??).

    AnL1-formulaφislocally m-conservatively rewritable7For reference,see[10].into anL2-formula(or a set ofL2-formulas ??)over a class of modelsCif there is anL2-formulaψ(or a set ofL2-formulas ??)such that

    ? for each modelM=(W,R,V)∈Candd ∈W,if(M,d)|=ψ(or(M,d)|=??),then(M,d)|=φ.

    ? for each modelM=(W,R,V)∈Candd ∈Wsuch that (M,d)|=φ,there is a modelM′ ∈Csuch thatM′=(W,R,V ′)andM=sig(φ)M′and(M′,d)|=ψ(or(M′,d)|=??).

    HereM=sig(φ)M′means thatV(p)=V ′(p) for each propositional variablep ∈sig(φ)andsig(φ)represents the set of propositional variables occurring inφ.

    According to the definition of locally m-conservative rewritability,the unique difference betweenMandM′is valuations of propositional variables,i.e.,M=M′iffV=V ′.Therefore,if anL1-formula is locally equivalently rewritable into anL2-formulaψ(or a set ofL2-formulas ??)over a class of modelsC,then it is locally m-conservatively rewritable into theL2-formulaψ(or the set ofL2-formulas ??)over the class of modelsC.

    WhenCis the set of all Kripke models,“over a class of modelsC” is omitted.WhenC={(M,d?) :Mis a tree model andd?is its root},anL1-formulaφis said to be equivalently (or m-conservatively) rewritable into anL2-formula (or a set ofL2-formulas)at roots over tree models.

    DegreeThe degree of an MLGI-formula is defined as follows:

    ?Deg(p)=0,

    ?Deg(⊥)=0,

    ?Deg(?φ)=Deg(φ),

    ?Deg(φ ∧ψ)=max{Deg(φ),Deg(ψ)},

    ?Deg()=Deg(φ)+1,

    ?Deg()=Deg(φ)+1.

    The degree of an MLI-formula(or an MLG-formula)is defined similarly.

    BisimulationLetM1=(W1,R1,V1)andM2=(W2,R2,V2)be two Kripke models.

    A non-empty relationS ?W1×W2isa bisimulation8For reference,see[5].between(M1,d1)and(M2,d2)if the following conditions are satisfied:

    ? (d1,d2)∈S;

    ? if(u,v)∈S,uandvsatisfy the same propositional variables;

    ? if(u,v)∈SanduR1x1,there is anx2such thatvR2x2such that(x1,x2)∈S(the forth condition);

    ? if(u,v)∈SandvR2x2,there is anx1such thatuR1x1such that(x1,x2)∈S(the back condition).

    A non-empty relationS ?W1× W2isan i-bisimulationbetween (M1,d1) and(M2,d2)ifSsatisfies all the conditions for bisimulation and the following conditions:

    ? if(u,v)∈Sandx1R1u,there is anx2such thatx2R2vsuch that(x1,x2)∈S(the inverse forth condition);

    ? if(u,v)∈Sandx2R2v,there is anx1such thatx1R1usuch that(x1,x2)∈S(the inverse back condition).

    A non-empty relationS ?W1×W2isan n-bisimulationbetween(M1,d1)and(M2,d2)9For reference,see[5].if there is a sequence of relationsSn ?···?S0such that:S=and for each 0≤i

    ? (d1,d2)∈Sn;

    ? if(u,v)∈S0,uandvsatisfy the same propositional variables;

    ? if (u,v)∈ Si+1anduR1x1,there isx2such thatvR2x2and (x1,x2)∈Si(the forth condition);

    ? if (u,v)∈ Si+1andvR2x2,there isx1such thatuR1x1and (x1,x2)∈Si(the back condition).

    A non-empty relationS ?W1×W2isan n-i-bisimulationbetween(M1,d1)and (M2,d2) if there is a sequence of binary relationsSn ?··· ?S0such thatS=and it satisfies all the conditions forn-bisimulation and the following conditions,i.e.,for each 0≤i

    ? if (u,v)∈ Si+1andx1R1u,there isx2such thatx2R2vand (x1,x2)∈Si(the inverse forth condition);

    ? if (u,v)∈ Si+1andx2R2v,there isx1such thatx1R1uand (x1,x2)∈Si(the inverse back condition).

    van Benthem Characterization Theorem equivalently rewrites a first-order formula into an ML-formula by bisimulation.(See[2]and[3].)

    Theorem 1(van Benthem Characterization Theorem).A first-order formula A(x)is invariant under bisimulations iff it is locally equivalently rewritable into the standard translation of an ML-formula.

    A non-empty binary relationS ?W1×W2isa counting bisimulationbetween(M1,d1)and(M2,d2)if the following conditions are satisfied:

    ? (d1,d2)∈S;

    ? if(u,v)∈S,uandvsatisfy the same propositional variables;

    ? if(u,v)∈SandX1?u↑is finite10x↑={y ∈W :xRy}.,there is anX2?v↑such thatScontains a bijection betweenX1andX2(the forth condition);

    ? if(u,v)∈SandX2?v↑is finite,there is anX1?u↑such thatScontains a bijection betweenX1andX2(the back condition).

    A non-empty binary relationS ?W1×W2isan nm-counting bisimulation11If“m”is changed into“finite”,it is an n-counting bisimulation.between(M1,d1)and(M2,d2)if there is a sequence of binary relationsSn ?···?S0such thatS=Siand it satisfies the following conditions,i.e.,for each 0≤i

    ? (d1,d2)∈Sn;

    ? if(u,v)∈S0,uandvsatisfy the same propositional variables;

    ? if(u,v)∈Si+1,| X1|≤mandX1?u↑,there is anX2?v↑such thatSicontains a bijection betweenX1andX2(the forth condition);

    ? if(u,v)∈Si+1,| X2|≤mandX2?v↑,there is anX1?u↑such thatSicontains a bijection betweenX1andX2(the back condition).

    A non-empty binary relationS ?W1× W2is annm-ik-counting bisimulation12If“k”is changed into“finite”,it is an nm-i-counting bisimulation.If“m”and“k”are both changed into“finite”,it is an n-i-counting bisimulation.between(M1,d1)and(M2,d2)if there is a sequence of binary relationsSn ?··· ?S0such thatS=Siand it satisfies the conditions fornm-counting bisimulation and the following conditions,i.e.,for each 0≤i

    ? if(u,v)∈Si+1,|Y1|≤kandY1?u↓13x↓={y ∈W :yRx}.,then there is aY2?v↓such thatSicontains a bijection betweenY1andY2(the inverse forth condition);

    ? if(u,v)∈Si+1,| Y2|≤kandY2?v↓,then there is aY1?u↓such thatSicontains a bijection betweenY1andY2(the inverse back condition).

    Let us discuss these different but resembled bisimulations.According to their definitions,it is known that

    ? each counting bisimulation is also a bisimulation.However,the inverse does not hold,i.e.,not each bisimulation is a counting one.

    ? each(n-)i-bisimulation is also an(n-)bisimulation sinceionly means the extra conditions for predecessors.However,it is obvious that the inverse does not hold.

    ? eachnm-ik-counting bisimulation is also annm-counting bisimulation.The inverse does not hold.

    ? whenm=1,thenm-counting bisimulation becomes ann-bisimulation.It means that ann-bisimulation is in fact a special case ofnm-counting bisimulations whenm=1.

    ? whenm=1 andk=1,thenm-ik-counting bisimulation becomes ann-ibisimulation.In fact,ann-i-bisimulation is a special case ofnm-ik-counting bisimulation whenm=1 andk=1.It should be noticed that eachnm-ikcounting bisimulation between two tree models is in fact annm-i1-counting bisimulation since any point,except the root14The root of a tree model has no predecessor.,in a tree model has only one predecessor.

    Figure 1 gives an example of 22-i1-counting bisimulationS.LetM1=(W1,R1,V1)andM2=(W2,R2,V2)be two(tree)models showed in Figure 1 withV1(p)=V2(p)for each propositional variablep.Define a sequence of binary relationsS2?S1?S0as follows:

    S2={(a0,b0)}

    S1={(a0,b0),(a1,b2),(a2,b1),(a3,b2)}

    S0={(a0,b0),(a1,b2),(a2,b1),(a3,b2),(a4,b3),(a5,b4),(a6,b4)}.

    LetS=Si.It is easy to prove thatSis a 22-i1-counting bisimulation betweenM1andM2.

    Figure 1

    Ap-morphismfrom(M1,d1)to(M2,d2)is a special bisimulationS15For reference,see[5].between(M1,d1)and(M2,d2)ifSis a surjective function fromW1toW2.

    Ani-p-morphismfrom (M1,d1) to (M2,d2) is a speciali-bisimulationSbetween(M1,d1)and(M2,d2)ifSis a surjective function fromW1toW2.

    Let Σ be a set of propositional variables.Each type of#-bisimulation is called a Σ-#-bisimulation,if no truth of propositional variables except those in Σ are considered.

    InvarianceAnL-formulaφisinvariant under#-bisimulations over a class of models C16#represents a type of bisimulation.,if

    (M1,d1)|=φiff(M2,d2)|=φ.17If it is substituted by“if(M1,d1) |= φ,then(M2,d2) |= φ”,then it means“preservation under#-bisimulations over a class of models C”.

    for each#-bisimulation between(M1,d1),(M2,d2)∈C.

    AnL-formulaφislocally preserved under inverse(i-)p-morphisms over a class of models Cif there is a(n)(i-)p-morphismffrom the pointed model(M1,d1)∈Cto the pointed model(M2,f(d1))∈Csuch that(M2,f(d1))|=φ,then(M1,d1)|=φ.WhenCis the class of all models,“over a class of modelsC”is omitted.

    This paper focuses on the class of all tree models.In some sections,the case thatC={(M,d?) :Mis a tree model andd?is its root}will be considered and it says to beinvariant(or preserved)under#-bisimulations at roots over tree models.

    Clearly invariance(or perservation)under bisimulations implies invariance(or perservation)undern-bisimulations for eachn ∈N.18For reference,see p.265 in[8].

    3 MLI to ML

    The following theorem is proved in this section:“each MLI-formula is equivalently rewritable into an ML-formula at roots over tree models”.However,Lemma 1 has to be proved first.

    Lemma 1From each bisimulation between tree models with their roots being mapped to each other,ani-bisimulation is constructed between the same two tree models with their roots being mapped to each other.

    ProofLetM1=(W1,R1,V1) andM2=(W2,R2,V2) be two tree models withbeing their roots respectively.Assume thatSis a bisimulation between(M1,) and (M2,) with ()∈S.NowSi ?S(i ∈N) is defined as follows:

    Since eachSi ?S,S??S.For constructingS?,those pairs having no predecessor pairs that belong toSare deleted fromS.

    Assume that (d,e)∈S?anddR1d′.Then (d,e)∈Sifor somei ∈N.So(d,e)∈S.By the assumption thatSis a bisimulation between(M1,)and(M2,)with()∈S,there is a pointe′ ∈W2such thateR2e′and(d′,e′)∈S.By the definition ofS?,(d′,e′)∈Si+1and then(d′,e′)∈S?.That is,S?satisfies the forth condition.The back condition can be proved similarly.Now consider the inverse forth and inverse back conditions.SinceM1andM2are both tree models,each point except their roots has only one predecessor.If a pair inS?is not the root pair(),the inverse forth and back conditions hold by the definition ofS?.If a pair inS?is the root pair(),the inverse forth and back conditions also hold because the roots have no predecessors at all. □

    Proposition 2 follows from Lemma 1 directly.

    Proposition 2From eachn-bisimulation between tree models with their roots being mapped to each other,ann-i-bisimulation is constructed between the same two tree models with their roots being mapped to each other.

    Proposition 3Each MLI-formulaφwithDeg(φ)≤nis invariant undern-i-bisimulations.

    ProofLetφbe an MLI-formula withDeg(φ)≤n.Assume that there is ann-ibisimulationS0with a sequenceSn ?··· ?S0between(M,w)and(M′,w′)and(w,w′)∈Sn.We should prove that

    We prove(1)by induction on the construction of MLI-formulas.The basis and boolean cases are trivial.

    Now consider the case thatφ=.Assume that (M,w)|=φ.Then there is a successorvofwinMsuch that (M,v)|=ψ.By the definition of ann-ibisimulation,there is a successorv′ofw′inM′such that(v,v′)∈Sn?1.So there is an(n ?1)-i-bisimulationS0withSn?1?···?S0between(M,v)and(M′,v′)and(v,v′)∈Sn?1.SinceDeg(ψ)≤n ?1,by induction hypothesis,

    (M,v)|=ψiff(M′,v′)|=ψ.

    By (M,v)|=ψ,we have that (M′,v′)|=ψ.Thus (M′,w′)|=φ.The inverse is proved similarly.

    Now consider the case thatφ=.Assume that(M,w)|=φ.Then there is a predecessorvofwinMsuch that (M,v)|=ψ.By the definition of ann-ibisimulation,there is a predecessorv′ofw′inM′such that (v,v′)∈Sn?1.Then there is an (n ?1)-i-bisimulationS0withSn?1?··· ?S0between (M,v) and(M′,v′)and(v,v′)∈Sn?1.SinceDeg(ψ)≤n ?1,by induction hypothesis,

    (M,v)|=ψiff(M′,v′)|=ψ.

    By (M,v)|=ψ,we have that (M′,v′)|=ψ.Thus (M′,w′)|=φ.The inverse is proved similarly. □

    We introduce characteristic ML-formulasin[8].

    Definition 4(Characteristic ML-Formula)Let Φ be a finite set of propositional variables and(M,d)be a pointed model withM=(W,R).The characteristic MLformula(n ∈N)is defined as follows:

    The main result of this section Theorem 5 is proved now.

    Theorem 5.Each MLI-formula is equivalently rewritable into an ML-formula at roots over tree models.

    ProofAssume thatφis an MLI-formula andDeg(φ)≤n.LetCbe the class of tree models(M,d?)withd?being its root such that(M,d?)|=φ.Assume that(M1,)∈Cand there is ann-bisimulationSbetween the tree model(M1,)and a tree model(M′,d′)withd′being its root such that(,d′)∈S.By Proposition 2,ann-i-bisimulationS?between(M1,)and(M′,d′)with(,d′)∈S?is constructed.Then by Proposition 3,(M1,)∈Cand(M1,)|=φ,we have that(M′,d′)|=φ.Therefore,(M′,d′)∈C.That is,Cis closed undern-bisimulations at roots over tree models.By Corollary 34 of[8]19Corollary 34 in[8]says that a class of pointed Kripke structures being closed under n-bisimulations is definable by an ML-formula in a finite vocabulary.,sinceCis closed undern-bisimulations,Cis definable by the ML-formula

    with Φ=sig(φ)20The ML-formula is finite as there are only finitely many suchof Definition 4.Therefore,the MLI-formulaφis equivalently rewritable into an ML-formula at roots over tree models. □

    Proposition 6 follows directly from Theorem 5.

    Proposition 6Each MLI-formula is m-conservatively rewritable into an ML-formula at roots over tree models.

    However,is each MLI-formula equivalently rewritable into an ML-formulaat any pointover tree models? The answer is“No”,answered by Example 7.up to logical equivalence in the vocabularysig(φ)ofφ.

    Example 7Assume thatis equivalently rewritable into an ML-formulaψat each point over tree models,i.e.,

    (M,d)|=iff(M,d)|=ψ

    for each tree model(M,d).Figure 2 says that(M1,a)and then(M1,a).The tree modelM1is a generated submodel ofM2in Figure 2.Sinceψis an MLformula,(M2,a).However,(M2,a)|=.Thusis not equivalently rewritable into an ML-formula at each point over tree models.

    Figure 2

    4 MLGI to MLG

    For an MLGI-formulaφ,let

    Proposition 8Each MLGI-formulaφwithDeg(φ)≤n,Ind(φ)≤mandInd?(φ)≤kis invariant undernm-ik-counting bisimulations.

    ProofThis proposition is proved by induction on the construction of MLGI-formulasφwithDeg(φ)≤n,Ind(φ)≤mandInd?(φ)≤k.Assume that there is annm-ikcounting bisimulationSbetween(M,d)and(M′,d′).The basis and boolean cases are trivial.

    Now consider the case thatφ=.Assume that(M,d)|=φ.Then there are at leastldifferent successorsd1,···,dlofdinMsuch that (M,di)|=ψfor each 1≤i ≤l.By the definition of annm-ik-counting bisimulation,n ≥1 andl ≤m,there are at leastldifferent successorsofd′inM′such that(d1,),···,(dl,)∈S.Then there is an(n?1)m-ik-counting bisimulation?Sbetween(M,di)and(M′,)for each 1≤i ≤l.SinceDeg(ψ)≤n ?1,Ind(ψ)≤mandInd?(ψ)≤k,by induction hypothesis,(M,di)|=ψiff (M′,)|=ψfor each 1≤i ≤l.By(M,di)|=ψfor each 1≤i ≤l,

    for each 1≤i ≤l.Thus(M′,d′)|=φ.The inverse can be proved similarly.

    Now consider the case thatφ=.Assume that (M,d)|=φ.Then there are at leastldifferent predecessorsd1,···,dlofdinMsuch that(M,di)|=ψfor each 1≤i ≤l.By the definition of annm-ik-counting bisimulation,n ≥1 andl ≤k,there are at leastldifferent predecessorsofd′inM′such that(d1,),···,(dl,)∈S.Then there is an(n?1)m-ik-counting bisimulation?Sbetween(M,di)and(M′,)for each 1≤i ≤l.SinceDeg(ψ)≤n ?1,Ind(ψ)≤mandInd?(ψ)≤k,by induction hypothesis,(M,di)|=ψiff (M′,)|=ψfor each 1≤i ≤l.By(M,di)|=ψfor each 1≤i ≤l,

    for each 1≤i ≤l.Thus(M′,d′)|=φ.The inverse can be proved similarly. □

    Proposition 9From eachnm-counting bisimulation between two tree models with their roots being mapped to each other,annm-ik-counting bisimulation (k ≥1) is constructed between these two tree models with their roots being mapped to each other.

    ProofLetM1=(W1,R1,V1)andM2=(W2,R2,V2)be two tree models withandbeing their roots respectively.Assume that

    Assume the contrary,i.e.,S′is not annm-i1-counting bisimulation.We can assume without loss of generality that there is a pair(1≤j ≤n)and a setD1?u′↑with|D1|≤m,but there is noD2?v′↑such thatS′contains a bijection betweenD1andD2.Sinceholds according to the definition ofS′.By the definition ofnm-counting bisimulation,there is a setD2?v′↑such thatScontains a bijection betweenD1andD2.According to the definition ofS′,S′contains a bijection betweenD1andD2,which is contrary to our assumption.So(1)holds.Since each point in a tree has only one predecessor,by the definition ofnm-ik-counting bisimulation,S′is anynm-ik-counting bisimulation for eachk ≥1 between(M1,)and(M2,)with their roots being mapped to each other. □

    In order to prove the main theorem of this section Theorem 11,Theorem 4.11 of[15]is introduced first:

    Theorem 10 (Theorem4.11in [15]).Assume that the language of MLG contains finitely many propositional variables.Let K be a class of pointed models.Then K is definable by a single MLG-formula iff K is closed under nm-counting bisimulations for some n,m ∈N.

    Theorem 11.Each MLGI-formula is equivalently rewritable into an MLG-formula at roots over tree models.

    ProofGive an MLGI-formulaφwithDeg(φ)≤n,Ind(φ)≤mandInd?(φ)≤kforn,m,k ≥1.By Theorem 10,it needs to prove that each MLGI-formula is invariant undernm-counting bisimulations at roots over tree models.By Proposition 9,from eachnm-counting bisimulation between two tree models with their roots being mapped to each other,annm-ik-counting bisimulation is constructed between these two tree models with their roots being mapped to each other.By Proposition 8,it can be easily proved that each MLGI-formulaφis invariant undernm-counting bisimulations at roots over tree models. □

    The following proposition follows directly from Theorem 11.

    Proposition 12Each MLGI-formula is m-conservatively rewritable into an MLGformula at roots over tree models.

    However,not each MLGI-formula is locally equivalently rewritable into an MLGformula at any point over tree models.Our example is stillin Example 7.is also an MLGI-formula.Since each MLG-formula is invariant under counting bisimulations at any point over tree models21For reference,see Proposition 3.3 in [15],which says that each MLG-formula is invariant under counting bisimulations.,ifcan be locally equivalently rewritable into an MLG-formula,it should be invariant under counting bisimulations at any point over tree models.Now Figure 2 shows that it is not the truth,for(M2,a)|=,(M1,a)and there is a counting bisimulationS={(a,a)}between the two tree models(M1,a)and(M2,a).

    Instead,the following theorem can be proved from Proposition 3.3 in[15],Theorem 10(i.e.,Theorem 4.11 in[15])and a similar proof of Theorem 17.22We should add“counting”before the word“bisimulations”in Theorem 17 and a quite similar theorem to Theorem 17 can be proved by a similar way of Theorem 17.

    Theorem 13.Let φ be an MLGI-formula with Deg(φ)≤n.Then the following conditions are equivalent:

    (i) φ is locally equivalently rewritable into an MLG-formula over tree models;

    (ii) φ is locally preserved(or invariant)under n-counting bisimulations over tree models;

    (iii) φ is locally preserved (or invariant) under counting bisimulations over tree models.

    5 MLGI to MLI

    5.1 Equivalent rewritability of MLGI to MLI

    Definition 14 (Height of States in Rooted Models)LetM=(W,R,V) be a rooted model with the rootd?.The heightH(d?) of the rootd?ofMis 0; if the heightH(d) ofdinMisn(n ∈N),then for each immediate successor23A successor y of x is an immediate successor of x ifx= y,?yRx and xRzRy implies z= x or z=y for each z ∈W.d′ofdinM,the heightH(d′)ofd′inMthat has not been assigned a height smaller thann+1 isn+1.The heightH(M)of a rooted modelMisnif the maximum height of points inMisn.Otherwise,H(M)is infinite.

    Definition 15 (Submodel of M Induced by X)The submodelM|Xof a modelM=(W,R,V) induced byX ?Wis defined asM|X=(X,R|X,V|X),whereR|X=R ∩(X ×X)andV|X=V(p)∩Xfor each propositional variablep.

    Proposition 16LetM=(W,R,V),d ∈WandX={e ∈W:H(e)≤max{H(d′) :d′ ∈Xd,n}},whereXd,n=d↑0∪··· ∪d↑n.Then there are ann-bisimulation and ann-i-bisimulation between(M|X,d)and(M,d).

    ProofA sequence of binary relationsSn ?···?S0is defined as follows(1≤i ≤n):

    It is easy to prove that(M|X,d)and(M,d)is bothn-bisimular andn-i-bisimular.□

    The following theorem holds for MLGI-formulas,also for MLG-formulas and MLI-formulas.

    Theorem 17.Let φ be an MLGI-formula with Deg(φ)≤n.The following two conditions are equivalent:

    (i) φ is locally preserved(or invariant)under n-bisimulations over tree models;

    (ii) φ is locally preserved(or invariant)under bisimulations over tree models.

    ProofWe only need to prove(?).Assume that an MLGI-formulaφwithDeg(φ)≤nis locally preserved24The“invariant”-case can be proved similarly.undern-bisimulations over tree models.LetM1=(W1,R1,V1)andM2=(W2,R2,V2)be two tree models,Sbe a bisimulation between(M1,d)and (M2,e) and (M1,d)|=φ.By Proposition 16,there is ann-bisimulation between (,d) and (M1,d),whereX1={d′′ ∈W1:H(d′′)≤max{H(d′) :d′ ∈}}and=d↑0∪···∪d↑n.Sinceφis locally preserved undernbisimulations over tree models,by (M1,d)|=φ,we have that (,d)|=φ.Similarly,there is ann-bisimulation between(,e)and(M2,e),whereX2={e′′ ∈W2:H(e′′)≤max{H(e′):e′ ∈}}and=e↑0∪···∪e↑n.Define a sequence of binary relationsSn ?Sn?1···?S0as follows(1≤i ≤n):

    Since(d,e)∈S,S??S.Then it is easy to prove thatS?is ann-bisimulation between(,d)and(,e).By our assumption thatφis locally preserved undern-bisimulations over tree models,from(,d)|=φwe have that(,e)|=φ.Since there is ann-bisimulation between(,e)and(M2,e),(M2,e)|=φ.Therefore,φis locally preserved under bisimulations over tree models. □

    Not each MLGI-formula is equivalently rewritable into an MLI-formula at roots over tree models.For example,2.Assume that2is equivalently rewritable into an MLI-formula at roots over tree models.Since each MLI-formula is invariant underi-bisimulations at roots over tree models,2should be invariant underibisimulations at roots over tree models.However,it is not the truth.We show it as follows.

    LetM1=(W1,R1,V1) andM2=(W2,R2,V2) be the two tree models in Figure 3 respectively.HereV1(p)=V2(p)=?for each propositional variablep.It is obvious that(M1,a0)|=2,(M2,b0)2,but there is ani-bisimulationS={(a0,b0),(a1,b1),(a2,b1)}between the two tree models(M1,a0)and(M2,b0).

    The following theorem is proved,instead.

    Figure 3

    Theorem 18.Let φ be an MLGI-formula with Deg(φ)≤n.Then the following conditions are equivalent:

    (i) φ is equivalently rewritable into an MLI-formula at roots over tree models;

    (ii) φ is preserved(or invariant)under bisimulations at roots over tree models;

    (iii) φ is preserved(or invariant)under n-bisimulations at roots over tree models;

    (iv) φ is preserved(or invariant)under n-i-bisimulations at roots over tree models;

    (v) φ is preserved(or invariant)under i-bisimulations at roots over tree models.

    Proof2?3 can be proved by a very similar proof of Theorem 17.

    3?4 is prove as follows:3?4 follows directly from the fact that eachn-i-bisimulation is also ann-bisimulation by the definitions ofn-bisimulation andn-i-bisimulation.4?3 follows from Proposition 2.

    2?5 is proved as follows:2?5 follows directly from the fact that eachibisimulation is also a bisimulation by the definitions of bisimulation andi-bisimulation.5?2 follows from Lemma 1.

    Now we prove that 1?5.(1?5)Assume that an MLGI-formulaφis equivalently rewritable into an MLI-formulaψat roots over tree models.Since each MLIformula is preserved(or invariant)underi-bisimulations at roots over tree models,φis preserved(or invariant)underi-bisimulations at roots over tree models.(5?1)Assume thatφis an MLGI-formula withDeg(φ)≤nand is preserved (or invariant) underi-bisimulations at roots over tree models.There are only finitely many non-equivalent MLI-formulasβwithDeg(β)≤mandsig(β)?sig(φ) for eachm ∈N.For each tree modelM=(W,R,V) andd ∈W,let the MLI-formulabe the conjunction of all these finitely many non-equivalent MLI-formulasβwithDeg(β)≤m,sig(β)?sig(φ)and(M,d)|=β.Now let

    whereMis a tree model withdbeing its root such that(M,d)|=φ.Being a disjunction of finitely many non-equivalent MLI-formulas,αis a proper MLI-formula.

    Now we prove thatφis equivalently rewritable into the MLI-formulaαat roots over tree models.LetM?be a tree model andd?be its root.Assume that(M?,d?)|=φ.By the definition ofαand,it is clear that(M?,d?)|=and then(M?,d?)|=α.

    Now assume thatM?=(W?,R?,V ?) is a tree model,d?is the root ofM?and(M?,d?)|=α.Then there is a tree modelM′=(W′,R′,V ′)withd′being its root and(M′,d′)|=φsuch that(M?,d?)|=.Now we prove the following claim:

    ? There is ann-i-bisimulationSbetween(M′,d′)and(M?,d?)with(d′,d?)∈S.

    Since(M?,d?)|=,it is easy to prove that(M?,d?)|=δiff(M′,d′)|=δfor each MLI-formulaδwithDeg(δ)≤nandsig(δ)?sig(φ).

    Assume thatd?R?v.By(M?,v)|=and then(M?,d?)|=.From (M?,d?)|=,we have that (M?,d?)|=δiff (M′,d′)|=δfor each MLI-formulaδwithDeg(δ)≤nandsig(δ)?sig(φ).So (M′,d′)|=.Thus there is a pointv′ ∈W′such thatd′R′v′and (M′,v′)|=.Then for each MLI-formulaδwithDeg(δ)≤n ?1 andsig(δ)?sig(φ),(M?,v)|=δiff(M′,v′)|=δ.By a similar argument,we can also prove that ifd′R′v′,there is a pointv ∈W?such thatd?R?vand for each MLI-formulaδwithDeg(δ)≤n ?1 andsig(δ)?sig(φ),(M?,v)|=δiff(M′,v′)|=δ.

    Now letSn?1be the union ofSn={(d′,d?)}and the set of all the above selected pairs(v′,v)such thatd′R′v′,d?R?vand(M?,v)|=δiff(M′,v′)|=δfor each MLIformulaδwithDeg(δ)≤n ?1 andsig(δ)?sig(φ).Similarly,a sequence of binary relationsSn ?Sn?1?···?S0is defined as follows:

    for each 1≤i ≤n,Si?1is the union ofSiand the set of all the selected pairs(v′,v) satisfying thatw′R′v′,wR?vfor some (w′,w)∈Siand (M?,v)|=δiff(M′,v′)|=δfor each MLI-formulaδwithDeg(δ)≤i ?1 andsig(δ)?sig(φ).It is easy to prove that

    is ann-i-bisimulation between(M′,d′)and(M?,d?)with(d′,d?)∈S0.

    Sinceφis preserved(or invariant)underi-bisimulations at roots over tree models,by 2?5,2?3 and 3?4,φis preserved(or invariant)undern-i-bisimulations at roots over tree models.Then by(M′,d′)|=φ,we have that(M?,d?)|=φ. □

    If being preserved(or invariant)at each point of a tree model is considered,we have the following theorem:

    Theorem 19.Let φ be an MLGI-formula with Deg(φ)≤n.Then the following conditions are equivalent:

    (i) φ is locally equivalently rewritable into an MLI-formula over tree models;

    (ii) φ is locally preserved(or invariant)under n-i-bisimulations over tree models;

    (iii) φ is locally preserved(or invariant)under i-bisimulations over tree models.

    Proof2?3 can be proved by a similar argument to the proof of Theorem 17.3?1 follows from a similar argument to the proof of 1?5 of Theorem 18. □

    5.2 m-Conservative rewritability of MLGI to MLI

    Lemma 2 follows from the fact that eachi-p-morphism is ani-bisimulation by their definitions and the fact that each MLI-formula is preserved(or invariant)underi-bisimulations.

    Lemma 2Let ?be a set of propositional variables,fbe a ?-i-p-morphism fromM1toM2.Then (M1,d)|=φiff (M2,f(d))|=φf(shuō)or each MLI-formulaφwithsig(φ)??.

    We prove Theorem 20 by Lemma 2.

    Theorem 20.Let φ be an MLGI-formula,??be a set of MLI-formulas and?be a set of propositional variables such that sig(φ)??and sig(α)??for each MLIformula α ∈??.If φ is locally m-conservatively rewritable into??,then it is locally preserved under inverse?-i-p-morphisms.

    ProofLetφbe an MLGI-formula,??be a set of MLI-formulas and ?be a set of propositional variables such thatsig(φ)??andsig(α)??for each MLI-formulaα ∈??.Assume thatφis locally m-conservatively rewritable into ??and there is a?-i-p-morphismffrom a modelM1=(W1,R1,V1)to a modelM2=(W2,R2,V2)withd1∈W1,d2∈W2,f(d1)=d2and (M2,d2)|=φ.We need to prove that(M1,d1)|=φ.According to our assumption that(M2,d2)|=φand the definition of locally m-conservative rewritability,there is a pointed model(,d2)with=(W2,R2,)such that(,d2)|=??andM2=sig(φ).ByM2=sig(φ),we have that

    By the definition of locally m-conservative rewritability,(M,d)|=??implies(M,d)|=φf(shuō)or each pointed model(M,d),then by(,d1)|=??we have that

    Give an MLGI-formulaφwithDeg(φ)≤?.Let Σ?(φ) be the set of all subformulas ofφ.Take new propositional variablesfor each subformla,and let Σ be the union ofsig(φ) and the set of all the new propositional variables.For eachχ ∈Σ?(φ),letχ?be the MLI-formula obtained fromχby replacing all the topmost subformulaswithpψand⊥respectively.is defined as the set of the MLI-formulaφ?and the following infinite many formulas for each:

    while eachψi(1≤i ≤n)is an MLI-formula withsig(ψi)?Σ and2irepresents a sequence ofioperators2(i ∈N).

    Now we can prove the main result Theorem 21 of this subsection.

    Theorem 21.Let φ be an MLGI-formula,??be a set of MLI-formulas and?be a set of propositional variables such that sig(φ)??and sig(α)??for each MLIformula α ∈??.Then the MLGI-formula φ is locally m-conservatively rewritable into??over tree models iff φ is locally preserved under inverse?-i-p-morphisms over tree models.

    Proof(?)It follows directly from Theorem 20.(?)Letφbe an MLGI-formula,Σ?(φ)be the set of all subformulas ofφ,Σ besig(φ)together with all the fresh propositional variablesbe the set of MLI-formulas being defined above.Assume that the MLGI-formulaφwithDeg(φ)≤?is locally preserved under inverse ?-i-p-morphisms over tree models withsig(φ)??andsig(α)??for each MLI-formulaα ∈.We prove thatφcan be locally m-conservatively rewritable into the setof MLI-formulas over tree models.We need to prove that

    Claim 1 for each tree modelM=(W,R,V)andd ∈Wsuch that(M,d)|=φ,there is a tree modelM′=(W,R,V ′)such thatM=sig(φ)M′and(M′,d)|=;

    Claim 2 for each tree modelM=(W,R,V) andd ∈W,if (M,d)|=,then(M,d)|=φ.

    To prove Claim 1,we should notice that each point in a tree model has only one predecessor,and then each MLGI-formula(n ≥2)is equivalent to⊥at each point of a tree model.Assume thatM=(W,R,V) is a tree model,d ∈Wand(M,d)|=φ.Let

    Then a new modelM′=(W,R,V ′) is constructed fromM.It is obvious thatM=sig(φ)M′and(M′,d)|=.

    Let’s consider Claim 2.Give a tree modelM=(W,R,V)withd ∈Wandd?being its root.Assume that(M,d)|=and(M,d)φ.LetS0={d′ ∈W:?k ∈N(d′ ∈d↓k)}.25d↓k= {d′ ∈W : ?d1···dk?1 ∈W(d′Rdk?1···d2Rd1Rd)} for k ∈N.When k=0,d↓0=j5i0abt0b.We should notice that the root of M belongs to S0,i.e.,d?∈S0.Assume thatS0?S1··· ?Snhave already been defined.Fix a pointe ∈Sn.

    Step(ii) For eachψ=∈Σ?(φ) (m ≥2) such that (M,e)|=pψ,selectmpointse1,···,em ∈Wsuch thateReiand

    for each 1≤i ≤m.

    Step(iii) For each subformulaofφ?such that(M,e)|=,select a pointe′ ∈Wsuch thateRe′and (M,e′)|=γ.For each subformulaofφ?such that(M,e)|=,select the only predecessore′ ∈Wofesuch that(M,e′)|=γ.

    Step(iv) For each subformulaofψ′?with∈Σ?(φ) (n ≥2) such that(M,e)|=,select a pointe′ ∈ Wsuch thateRe′and (M,e′)|=γ.For each subformulaofψ′?with∈Σ?(φ) (n ≥2) such that(M,e)|=,select the only predecessore′ ∈Wofesuch that(M,e′)|=γ.

    Repeat the above selection process for each pointe ∈Sn.LetSn+1contains all these pointseiore′selected by the above selection process(i)–(iv).Next,for each twod1,d2∈Snsuch thatd1is Σ-i-bisimilar tod2inM28Each point is Σ-i-bisimilar to itself in M.Therefore,if d1=d2,then d1 is definitely Σ-i-bisimilar to d2 in M.,ifand∈Sn+1,then each successor(or the only predecessor)ofd2being Σ-i-bisimilar toinMshould be added intoSn+1.LetSn+1be the smallest set of points satisfying all of the above conditions.Then the sequence of sets of pointsS0?S1···?Sn···is defined completely.

    The selection process (i)–(iv) may choose two successors of one point which are equivalent over MLI-formulasαwithsig(α)?Σ inMbut not Σ-i-bisimilar to each other inM.Assume that such a case occurs,i.e.,there are two successorsd1,d2∈Si+1ofd′ ∈Si(i ∈N)such thatd1,d2are equivalent over MLI-formulasαwithsig(α)?Σ inMbutd1is not Σ-i-bisimilar tod2inM.Let

    We delete the points of the setsfrom eachSi(i ∈N)for each two pointsd1,d2∈W.Let(i ∈N)be the remaining set of points after the above deletion process.Then a new sequenceis constructed from the sequenceS0?S1···?Sn···.

    Now a new modelM′=(W′,R′,V ′)can be defined as follows:

    According to the assumption thatMis a tree model withd?being its root,M′is also a tree model withd?being its root.29We should notice that d?∈S0 and d?won’t be deleted from each Si(i ∈N)since it is the root of M.So d?∈W′.Then by(M,d)φ,we have that(M′,d)φ.We need to prove that(M′,d)|=.Since we have Step(ii),the only cases inneeded to be considered are the formulas

    while eachψi(1≤i ≤nandn ≥2)is an MLI-formula withsig(ψi)?Σ.

    Assume the contrary,i.e.,there are a pointd′ ∈d↑m ?W′(0≤m ≤?)and MLI-formulasψ1,···,ψn(n ≥2) withsig(ψi)?Σ (1≤i ≤n) such that(M′,d′)pψfor someψ=∈Σ?(φ)and

    It means thatd′hasndifferentR′-successors that are not equivalent over MLIformulasαwithsig(α)?Σ inM′,and then not Σ-i-bisimilar to each other inM′.By the construction ofM′,ifd1∈W′is Σ-i-bisimilar tod2∈W′inM,thend1is Σi-bisimilar tod2inM′.Sod′hasndifferentR-successors that are not Σ-i-bisimilar to each other inM.We prove that thendifferentR-successors ofd′are also not equivalent over MLI-formulasαwithsig(α)?Σ inM.

    Assume the contrary,i.e.,there are two successors∈W′and∈W′ofd′ ∈W′satisfying thatare not equivalent over MLI-formulasαwithsig(α)?Σ inM′and not Σ-i-bisimilar to each other inM,but they are equivalent over MLI-formulasαwithsig(α)?Σ inM.Since Σ is finite30If Σ is finite,there are only finitely many non-equivalent MLI-formulas α with sig(α) ?Σ and Deg(α)≤2?.andare equivalent over MLI-formulasαwithsig(α)?Σ inM,is Σ-2?-i-bisimilar toinM.31The proof of this part is similar to Proposition 2.31 of[5].According to the construction of the sequenceis Σ-i-bisimilar toinM′.Therefore,is equivalent toover MLI-formulasαwithsig(α)?Σ inM′,which is contrary to our assumption thatare not equivalent over MLI-formulasαwithsig(α)?Σ inM′.Sod′ ∈d↑m(0≤m ≤?) hasndifferentR-successors that are not equivalent over MLI-formulasαwithsig(α)?Σ to each other inM.

    Since thesendifferentR-successors ofd′32These n points are also R′-successors of d′.satisfyψ′?inM′,according to the construction ofM′,each of them also satisfiesψ′?inM.Then there are MLI-formulaswithsig()?Σ(1≤i ≤n)such that

    Last,from(M,d)|=,d′ ∈d↑m(0≤m ≤?)?W′ ?Wand(0?),we have that(M,d′)|=pψ.It means that(M′,d′)|=pψby the construction ofM′,which is contrary to our assumption that(M′,d′)pψ.Therefore,(M′,d)|=is proved.

    Since“being Σ-i-bisimilar to”is an equivalence relation,let[e]={e′ ∈W′:(M′,e)is Σ-i-bisimilar to(M′,e′)}fore ∈W′.A new modelM′′=(W′′,R′′,V ′′)can be defined fromM′as follows:

    W′′={[e]:e ∈W′},

    [d1]R′′[d2]iff there aree1∈[d1]ande2∈[d2]such thate1R′e2.

    V ′′(p)={[e]∈W′′:e ∈V ′(p)}for each propositional variablep ∈Σ.

    According to the construction ofM′andM′′,M′′is of finite outdegrees,i.e.,each point inM′′has only finitely many successors.

    Now we show thatf:[e]fore ∈W′and[e]∈W′′is a Σ-i-p-morphism fromM′toM′′.The valuation and the forth conditions are obviously satisfied by the definition ofM′′.We prove the back condition as follows:

    The inverse forth condition follows from the definition ofR′′.Now we prove the inverse back condition as follows:

    Therefore,f:e[e]fore ∈W′and[e]∈W′′is a Σ-i-p-morphism fromM′toM′′.

    We prove thatM′′is a tree model.SinceM′is a tree model withd?being its root,there is anR′′-path from[d?]to[e]for each[e]∈W′′.If[d?]33[d?]={d?}.has a predecessor inM′′,d?has a predecessor inM′according to the definition ofR′′,which is contrary to our assumption thatd?is the root of the tree modelM′.Therefore,[d?]is the root ofM′′.Now we prove that there is a unique path from [d?]to [e]for each [e]inM′′.Assume the contrary,i.e.,there is a[e]inM′′such that[e]has two different predecessors[d1]and[d2]inM′′.Sincefis a Σ-i-p-morphism fromM′toM′′,there are two points∈[d1]and∈[d2]such that.Since[d1][d2],is also different from.It means that the pointehas two different predecessors in the tree modelM′,which is contrary to the definition of a tree model.So there is only one unique path from[d?]to[e]for each[e]inM′′.Therefore,M′′is a tree model with[d?]being its root.

    Next we prove the following claims:

    Claim(1) (M′′,[d])|=;

    Claim(2) Let[u]and[v]be successors of a point[w]∈W′′inM′′.For each MLI-formulaαwithsig(α)?Σ,if (M′′,[u])|=αiff (M′′,[v])|=α,then[u]=[v];

    Claim(1) (M′′,[d])|=φ.

    Claim(1)follows directly from Lemma 2 and(M′,d)|=.34We have proved that there is a Σ-i-p-morphism from M′ to M′′Claim(2)is proved as follows:

    Let[u]and[v]be successors of a point[w]∈W′′inM′′.Assume that

    for each MLI-formulaαwithsig(α)?Σ.SinceM′′is of finite outdegrees,[u]is Σ-i-bisimilar to[v]inM′′.35Since[u]and[v]has the same unique predecessor[w]in M′′,the proof of this part is similar to the proof of Theorem 2.24(i.e.,Hennessy-Milner Theorem)in[5].Since[u],[v]are successors of the point[w]inM′′and there is a Σ-i-p-morphism fromM′toM′′,there are pointsu1∈[u1]=[u]andv1∈[v1]=[v]such thatwR′u1andwR′v1.According to Lemma 2 and the fact thatf:e[e]fore ∈W′and[e]∈W′′is a Σ-i-p-morphism fromM′toM′′,

    for each MLI-formulaαwithsig(α)?Σ.Then by(1?),we have that

    for each MLI-formulaαwithsig(α)?Σ.

    Now we prove thatu1is Σ-i-bisimilar tov1inM′.Assume the contrary,i.e.,u1is not Σ-i-bisimilar tov1inM′.Sinceu1andv1has the same uniqueR′-predecessorwin the tree modelM′,we can assume without loss of generality that there is a point∈W′such thatand no successor ofv1is equivalent toover MLI-formulasαwithsig(α)?Σ inM′.Fromand the fact that there is a Σ-i-p-morphism fromM′toM′′,and thenby[u]=[u1].Since[u]is Σ-i-bisimilar to[v]inM′′,there is a point[v′]∈W′′such that[v]R′′[v′]andis Σ-i-bisimilar to[v′]inM′′.Then

    for each MLI-formulaαwithsig(α)?Σ.By Lemma 2 and the fact that there is a Σ-i-p-morphism fromM′toM′′,

    for each MLI-formulaαwithsig(α)?Σ.Thus,by(2?),we have that

    for each MLI-formulaαwithsig(α)?Σ.From[v]R′′[v′]and[v1]=[v],[v1]R′′[v′]holds.By the fact that there is a Σ-i-p-morphism fromM′toM′′,there is a point∈W′such thatand=[v′].Then from∈[v′]we get that

    for each MLI-formulaαwithsig(α)?Σ.Therefore,by(3?)and(4?),

    for each MLI-formulaαwithsig(α)?Σ.However,(5?)is contrary to our assumption that no successors ofv1is equivalent toover MLI-formulasαwithsig(α)?Σ inM′.Thusu1is Σ-i-bisimilar tov1inM′.

    Sinceu1is Σ-i-bisimilar tov1inM′,then [u1]=[v1].By [u1]=[u]and[v1]=[v],we finally get that[u]=[v].That is,Claim(2)is proved.

    We prove Claim(3)by showing that

    for eachψ=∈Σ?(φ) (n ≥2) and for each [d′]∈[d]↑0∪[d]↑1∪···∪[d]↑??Deg(ψ).

    SinceM′′is a tree model,we should notice that

    for each[e]∈W′′and for eachγ=∈Σ?(φ)(n ≥2).So we can assume without loss of generality that there are no such subformulasγ=(n ≥2) occurring in eachψ=∈Σ?(φ).36If such a subformula γ=?≥nγ′ (n ≥2)occurs in ψ,we can substitute γ with ⊥immediately.We prove (6?) by induction on the numbers of subformulas(t ≥2) occurring inψ′forψ=∈Σ?(φ)(n ≥2).Letψ=∈Σ?(φ) (n ≥2) andkbe the number of subformulas(t ≥2)occurring inψ′.

    Assume thatk=0.Thenψ′=ψ′?.Let[d′]∈[d]↑0∪[d]↑1∪···∪[d]↑??Deg(ψ).Assume that(M′′,[d′])|=pψ.By Claim(1)that(M′′,[d])|=and[d′]∈[d]↑0∪[d]↑1∪···∪[d]↑??Deg(ψ),we have that

    Assume that(M′′,[d′])|=ψ.Then[d′]hasndifferent successorssuch that(M′′,)|=ψ′(n ≥2)for each 1≤i ≤n.None ofis equivalent to another over MLI-formulasαwithsig(α)?Σ according to Claim(2).Therefore,there arendifferent MLI-formulasψ1,···,ψnwithsig(ψi)?Σ such that

    Fromψ′=ψ′?,we get that(M′′,[d′])|=pψ.That is,(6?)holds fork=0.

    Now assume that (6?) holds fork ≤m ∈N.Let’s consider the case thatk=m+1.Let[d′]∈[d]↑0∪[d]↑1∪···∪[d]↑??Deg(ψ).Let(q ∈N)be the topmost subformulas having the form(n ≥2)occurring inψ′.Letkibe the number of subformulas(n ≥2) occurring inδifor each 1≤i ≤q.By induction hypothesis that(6?)holds fork ≤mand the fact that eachki ≤k ≤mfor 1≤i ≤q,we have that

    Last,from (6?),Claim (1) andφ?∈,Claim (3) that (M′′,[d])|=φis proved.

    Sinceφis locally preserved under inverse ?-i-p-morphisms over tree models such thatsig(φ)??andsig(α)??for each MLI-formulaα ∈,from Claim(3)and the fact that there is a Σ-i-p-morphism fromM′toM′′,we have that(M′,d)|=φ,which is contrary to what we have prove that(M′,d)φ.Therefore,for each tree modelM=(W,R,V)withd ∈W,if(M,d)|=,then(M,d)|=φ,i.e.,Claim 2 is proved. □

    6 MLGI to ML

    Now we consider the problem of locally m-conservative rewritability of MLGI to ML over tree models.

    Theorem 22,the main result of this subsection,can be proved by Theorem 21.

    Theorem 22.Let φ be an MLGI-formula,??be a set of ML-formulas and?be a set of propositional variables such that sig(φ)??and sig(α)??for each MLformula α ∈??.Then the MLGI-formula φ is locally m-conservatively rewritable into??over tree models iff φ is locally preserved under inverse?-p-morphisms over tree models.

    Proof(?) This part can be proved by a similar one to the proof of Theorem 20.(?) Letφbe an MLGI-formula,??be a set of ML-formulas and ?be a set of propositional variables such thatsig(φ)??andsig(α)??for each ML-formulaα ∈??.Assume that an MLGI-formulaφis locally preserved under inverse ?-pmorphisms over tree models.Since eachi-p-morphism is also ap-morphism,φis locally preserved under inversei-p-morphisms over tree models.By Theorem 21 and the fact that each ML-formula is also an MLI-formula,φis locally m-conservatively rewritable into ??over tree models. □

    Lemma 3 says,ap-morphism between two tree modelsfitself is also ani-pmorphism.

    Lemma 3LetM1andM2be tree models.Then eachp-morphism fromM1toM2is also ani-p-morphism fromM1toM2.

    ProofAssume thatM1andM2are tree models withbeing their roots respectively.Letfbe ap-morphism fromM1toM2.We prove thatfis also ani-p-morphism fromM1andM2.Assume the contrary,i.e.,fis not ani-p-morphism fromM1toM2.It means thatf(x)R2f(y) withx,y ∈W1but there is no pointz ∈W1such thatzR1yandf(z)=f(x).SinceM1andM2are tree models andby the definition ofp-morphisms,.Then there is anR1-path···R1xnR1yfromtoyinM1.Thus,according to the definition ofp-morphisms,there is anR2-pathR2f(x1)R2f(x2)R2···R2f(xn)R2f(y) fromtof(y)inM2.Since there is no pointz ∈W1such thatzR1yandf(z)=f(x),we have thatf(xn)f(x).Then the pointf(y) inM2has two different predecessorsf(x) andf(xn).It is contrary to our assumption thatM2is a tree model.Therefore,fitself is also ani-p-morphism fromM1andM2. □

    From Theorem 22 and Lemma 3,the following theorem is got immediately,whose proof is omitted for its clearness.

    Theorem 23.Let φ be an MLGI-formula,??be a set of ML-formulas and?be a set of propositional variables such that sig(φ)??and sig(α)??for each MLformula α ∈??.The following conditions are equivalent for the MLGI-formula φ:

    (i) φ is locally m-conservatively rewritable into??over tree models;

    (ii) φ is locally preserved under inverse?-p-morphisms over tree models;

    (iii) φ is locally preserved under inverse?-i-p-morphisms over tree models.

    国产精品欧美亚洲77777| 久久 成人 亚洲| 亚洲欧美精品综合一区二区三区| 国产精品久久久av美女十八| 香蕉丝袜av| 国产极品粉嫩免费观看在线| 国产一区二区 视频在线| a 毛片基地| 18禁观看日本| 国产精品九九99| 国产成人影院久久av| 中文精品一卡2卡3卡4更新| 啦啦啦在线免费观看视频4| 日韩中文字幕欧美一区二区 | 亚洲av欧美aⅴ国产| 成人国产av品久久久| 极品人妻少妇av视频| 亚洲欧美一区二区三区国产| netflix在线观看网站| 国产精品一区二区精品视频观看| 嫩草影视91久久| 精品一品国产午夜福利视频| 亚洲精品日韩在线中文字幕| 久久久久国产一级毛片高清牌| av国产久精品久网站免费入址| 丝袜在线中文字幕| 久久久国产精品麻豆| 美女主播在线视频| 91精品伊人久久大香线蕉| 欧美成人精品欧美一级黄| 深夜精品福利| 女警被强在线播放| 天天躁日日躁夜夜躁夜夜| 自线自在国产av| 欧美激情极品国产一区二区三区| 日韩制服骚丝袜av| 2021少妇久久久久久久久久久| av天堂在线播放| av有码第一页| 亚洲免费av在线视频| 男男h啪啪无遮挡| 每晚都被弄得嗷嗷叫到高潮| 热99久久久久精品小说推荐| 纵有疾风起免费观看全集完整版| 777米奇影视久久| 超碰成人久久| 80岁老熟妇乱子伦牲交| 成人手机av| 在线观看国产h片| 亚洲精品第二区| 一区二区日韩欧美中文字幕| 一级片免费观看大全| 中文精品一卡2卡3卡4更新| 日本欧美国产在线视频| 午夜免费男女啪啪视频观看| 免费高清在线观看视频在线观看| 人人妻人人添人人爽欧美一区卜| 亚洲国产欧美日韩在线播放| 国产高清不卡午夜福利| 性少妇av在线| 欧美性长视频在线观看| 午夜福利一区二区在线看| 欧美精品人与动牲交sv欧美| 精品一区在线观看国产| 亚洲精品中文字幕在线视频| 性高湖久久久久久久久免费观看| 操美女的视频在线观看| 五月天丁香电影| 国产xxxxx性猛交| 久久人妻熟女aⅴ| 中文字幕色久视频| 国产精品一区二区精品视频观看| 亚洲,欧美,日韩| 亚洲熟女精品中文字幕| 国产成人a∨麻豆精品| 狠狠精品人妻久久久久久综合| 亚洲国产日韩一区二区| 日本vs欧美在线观看视频| 午夜日韩欧美国产| 亚洲成人免费av在线播放| 欧美日韩亚洲综合一区二区三区_| 亚洲av男天堂| 高清欧美精品videossex| 巨乳人妻的诱惑在线观看| 亚洲欧美一区二区三区黑人| 啦啦啦在线观看免费高清www| 欧美国产精品va在线观看不卡| 亚洲第一av免费看| 日韩大码丰满熟妇| 国产av国产精品国产| 999久久久国产精品视频| 久久久国产精品麻豆| 国产成人91sexporn| 亚洲欧美清纯卡通| 亚洲成人国产一区在线观看 | 日韩制服丝袜自拍偷拍| 美女脱内裤让男人舔精品视频| 爱豆传媒免费全集在线观看| 亚洲精品成人av观看孕妇| 人妻一区二区av| 亚洲一卡2卡3卡4卡5卡精品中文| 99国产精品99久久久久| 男人添女人高潮全过程视频| 国产色视频综合| 精品少妇久久久久久888优播| 在线亚洲精品国产二区图片欧美| 免费女性裸体啪啪无遮挡网站| 欧美日韩亚洲国产一区二区在线观看 | 一二三四在线观看免费中文在| 午夜福利一区二区在线看| 亚洲五月婷婷丁香| 欧美乱码精品一区二区三区| 亚洲人成网站在线观看播放| 99热国产这里只有精品6| 好男人视频免费观看在线| 波多野结衣av一区二区av| 永久免费av网站大全| 激情五月婷婷亚洲| 丝瓜视频免费看黄片| 久久女婷五月综合色啪小说| 午夜久久久在线观看| 一级黄片播放器| 亚洲精品美女久久久久99蜜臀 | 日本欧美视频一区| 成人手机av| 在线观看免费高清a一片| 精品人妻一区二区三区麻豆| 男女下面插进去视频免费观看| 中文字幕最新亚洲高清| 伊人久久大香线蕉亚洲五| 精品国产乱码久久久久久男人| 婷婷丁香在线五月| 久久精品久久久久久久性| 国产欧美日韩精品亚洲av| 日本wwww免费看| 最近手机中文字幕大全| h视频一区二区三区| 亚洲av国产av综合av卡| 亚洲中文日韩欧美视频| 日韩精品免费视频一区二区三区| 欧美人与性动交α欧美精品济南到| 美女福利国产在线| 亚洲成色77777| 爱豆传媒免费全集在线观看| 啦啦啦啦在线视频资源| 肉色欧美久久久久久久蜜桃| 欧美另类一区| 纯流量卡能插随身wifi吗| 丝袜美腿诱惑在线| 久久热在线av| av在线老鸭窝| 丝袜人妻中文字幕| 一级毛片我不卡| 日韩 欧美 亚洲 中文字幕| 最新的欧美精品一区二区| 国精品久久久久久国模美| videos熟女内射| 高清黄色对白视频在线免费看| 精品一区在线观看国产| 丁香六月天网| 青草久久国产| 99国产精品一区二区三区| 午夜免费男女啪啪视频观看| 七月丁香在线播放| 精品国产超薄肉色丝袜足j| 国产精品.久久久| 少妇的丰满在线观看| 亚洲专区国产一区二区| www.av在线官网国产| 成人国产av品久久久| av国产精品久久久久影院| 日本五十路高清| 电影成人av| 日日夜夜操网爽| 丝袜喷水一区| 久9热在线精品视频| 人妻人人澡人人爽人人| 中文字幕人妻丝袜一区二区| 777米奇影视久久| 天堂俺去俺来也www色官网| 成人免费观看视频高清| av天堂久久9| 人人妻,人人澡人人爽秒播 | 国产精品久久久久久精品电影小说| 国产91精品成人一区二区三区 | 国产精品一国产av| 老司机影院成人| 欧美人与善性xxx| 操美女的视频在线观看| 一级黄色大片毛片| 美女脱内裤让男人舔精品视频| 亚洲精品国产色婷婷电影| 亚洲精品国产av蜜桃| 叶爱在线成人免费视频播放| 高潮久久久久久久久久久不卡| 无遮挡黄片免费观看| 一级,二级,三级黄色视频| 亚洲,一卡二卡三卡| 一个人免费看片子| 观看av在线不卡| www日本在线高清视频| 久久亚洲国产成人精品v| 国产成人一区二区三区免费视频网站 | 在线观看一区二区三区激情| 欧美日韩成人在线一区二区| av不卡在线播放| a级片在线免费高清观看视频| 人人妻人人澡人人看| 亚洲欧美中文字幕日韩二区| 久久国产精品大桥未久av| 欧美另类一区| 亚洲欧美色中文字幕在线| 一级,二级,三级黄色视频| 中文字幕高清在线视频| 两个人免费观看高清视频| 国产欧美日韩综合在线一区二区| 一级黄片播放器| 国产av精品麻豆| 在线观看国产h片| 精品亚洲成国产av| 国产一区二区三区av在线| 亚洲欧美清纯卡通| 久久久国产精品麻豆| www.熟女人妻精品国产| 国产xxxxx性猛交| 日本午夜av视频| 国产精品熟女久久久久浪| 国产欧美日韩精品亚洲av| 色综合欧美亚洲国产小说| 纯流量卡能插随身wifi吗| 欧美精品人与动牲交sv欧美| 一本大道久久a久久精品| 18禁国产床啪视频网站| 亚洲成国产人片在线观看| 亚洲精品中文字幕在线视频| 视频在线观看一区二区三区| 亚洲自偷自拍图片 自拍| 精品少妇黑人巨大在线播放| svipshipincom国产片| 97在线人人人人妻| 国产欧美日韩综合在线一区二区| 在线观看www视频免费| 国产亚洲精品久久久久5区| 两个人看的免费小视频| 久久亚洲精品不卡| 日韩中文字幕视频在线看片| 亚洲av在线观看美女高潮| 欧美亚洲 丝袜 人妻 在线| 一本大道久久a久久精品| 欧美日本中文国产一区发布| 国产高清videossex| av线在线观看网站| 一区在线观看完整版| 下体分泌物呈黄色| 精品免费久久久久久久清纯 | 亚洲七黄色美女视频| 国精品久久久久久国模美| 国产精品久久久人人做人人爽| 最新在线观看一区二区三区 | 又大又爽又粗| 97人妻天天添夜夜摸| 夫妻性生交免费视频一级片| 国产av国产精品国产| 久久毛片免费看一区二区三区| 最新在线观看一区二区三区 | 婷婷色麻豆天堂久久| 午夜福利影视在线免费观看| 亚洲av电影在线进入| 国产一区二区 视频在线| 精品一区二区三卡| 国产精品亚洲av一区麻豆| 欧美成人精品欧美一级黄| 日韩av在线免费看完整版不卡| 一本综合久久免费| 18禁国产床啪视频网站| 欧美另类一区| 欧美黑人精品巨大| 一本色道久久久久久精品综合| 每晚都被弄得嗷嗷叫到高潮| 如日韩欧美国产精品一区二区三区| 9热在线视频观看99| 夫妻性生交免费视频一级片| 精品少妇久久久久久888优播| 亚洲激情在线av| 十分钟在线观看高清视频www| 欧美一区二区精品小视频在线| 在线观看午夜福利视频| 在线观看66精品国产| 精品免费久久久久久久清纯| 一本大道久久a久久精品| 亚洲中文av在线| 一本精品99久久精品77| 日韩欧美一区视频在线观看| 亚洲av电影不卡..在线观看| 18禁黄网站禁片免费观看直播| 午夜老司机福利片| 男人舔女人的私密视频| 久99久视频精品免费| 熟女电影av网| 日韩大码丰满熟妇| 国产亚洲av高清不卡| 国产成人精品无人区| 9191精品国产免费久久| 久久久久久大精品| 色综合婷婷激情| 长腿黑丝高跟| 日本一本二区三区精品| 国产一卡二卡三卡精品| 午夜久久久久精精品| 精品国产一区二区三区四区第35| 欧美一级毛片孕妇| 在线视频色国产色| 桃色一区二区三区在线观看| 亚洲精品一区av在线观看| 精品熟女少妇八av免费久了| 欧美一区二区精品小视频在线| 黄片大片在线免费观看| 一边摸一边做爽爽视频免费| a级毛片在线看网站| 亚洲国产精品合色在线| 亚洲一码二码三码区别大吗| 美女国产高潮福利片在线看| 制服丝袜大香蕉在线| 精品卡一卡二卡四卡免费| 久久久水蜜桃国产精品网| 观看免费一级毛片| 88av欧美| 精品第一国产精品| 88av欧美| 黄色a级毛片大全视频| 国产91精品成人一区二区三区| 欧洲精品卡2卡3卡4卡5卡区| 久久婷婷人人爽人人干人人爱| 特大巨黑吊av在线直播 | 国产高清videossex| 国产在线观看jvid| 婷婷丁香在线五月| 美女午夜性视频免费| 最新在线观看一区二区三区| 亚洲自拍偷在线| av片东京热男人的天堂| 天天躁狠狠躁夜夜躁狠狠躁| 精品欧美一区二区三区在线| 国产一区在线观看成人免费| 成人亚洲精品av一区二区| 亚洲国产精品sss在线观看| 99热6这里只有精品| 成人av一区二区三区在线看| 在线观看日韩欧美| www.自偷自拍.com| 国内精品久久久久久久电影| av中文乱码字幕在线| 亚洲人成电影免费在线| 国内少妇人妻偷人精品xxx网站 | 后天国语完整版免费观看| 亚洲三区欧美一区| 亚洲成av人片免费观看| 少妇粗大呻吟视频| 国产精品美女特级片免费视频播放器 | 黄片播放在线免费| 久久精品影院6| 我的亚洲天堂| 久久香蕉国产精品| 午夜日韩欧美国产| 中文字幕另类日韩欧美亚洲嫩草| 亚洲va日本ⅴa欧美va伊人久久| 精品国产乱码久久久久久男人| 搡老熟女国产l中国老女人| 黄色视频,在线免费观看| 人人妻人人看人人澡| a级毛片a级免费在线| 国产成人精品久久二区二区免费| 丝袜美腿诱惑在线| 又黄又爽又免费观看的视频| av超薄肉色丝袜交足视频| 精品福利观看| 这个男人来自地球电影免费观看| 成人特级黄色片久久久久久久| 99riav亚洲国产免费| 一边摸一边做爽爽视频免费| 一本一本综合久久| 大型黄色视频在线免费观看| aaaaa片日本免费| 婷婷精品国产亚洲av在线| xxxwww97欧美| 国产真人三级小视频在线观看| 精品久久蜜臀av无| 两个人免费观看高清视频| 欧洲精品卡2卡3卡4卡5卡区| 亚洲成人国产一区在线观看| 啦啦啦观看免费观看视频高清| АⅤ资源中文在线天堂| 成人精品一区二区免费| 精品国产乱码久久久久久男人| 熟妇人妻久久中文字幕3abv| 啪啪无遮挡十八禁网站| 黄网站色视频无遮挡免费观看| 在线观看免费日韩欧美大片| 久久久久久人人人人人| 99久久国产精品久久久| 日韩欧美国产一区二区入口| 首页视频小说图片口味搜索| 一级a爱片免费观看的视频| 99久久综合精品五月天人人| 久久亚洲精品不卡| 日本一本二区三区精品| av有码第一页| 欧美乱色亚洲激情| 免费人成视频x8x8入口观看| 黑人巨大精品欧美一区二区mp4| 老鸭窝网址在线观看| 亚洲自偷自拍图片 自拍| 午夜福利免费观看在线| 久9热在线精品视频| 视频在线观看一区二区三区| 免费一级毛片在线播放高清视频| 最近最新免费中文字幕在线| 亚洲av片天天在线观看| 在线观看一区二区三区| 成人三级做爰电影| 无遮挡黄片免费观看| 国产精华一区二区三区| 亚洲av五月六月丁香网| 久久久水蜜桃国产精品网| 少妇被粗大的猛进出69影院| 国产日本99.免费观看| 亚洲全国av大片| 性色av乱码一区二区三区2| 日韩大尺度精品在线看网址| 久久亚洲精品不卡| 国产视频内射| 91字幕亚洲| 一本一本综合久久| 日本成人三级电影网站| 一个人观看的视频www高清免费观看 | 成年免费大片在线观看| 色老头精品视频在线观看| 国产黄a三级三级三级人| www.精华液| 91字幕亚洲| 亚洲av中文字字幕乱码综合 | 久久午夜综合久久蜜桃| 99国产极品粉嫩在线观看| 视频在线观看一区二区三区| 成人欧美大片| 一区二区日韩欧美中文字幕| 午夜福利成人在线免费观看| 亚洲国产欧美日韩在线播放| 日韩高清综合在线| 女性被躁到高潮视频| АⅤ资源中文在线天堂| 久久国产精品人妻蜜桃| 男女下面进入的视频免费午夜 | 久久精品91蜜桃| 精品久久久久久久末码| 精品福利观看| 国产成人精品无人区| 亚洲一区中文字幕在线| 叶爱在线成人免费视频播放| 色播在线永久视频| 久久久久久国产a免费观看| 日日爽夜夜爽网站| 一二三四社区在线视频社区8| 级片在线观看| 一a级毛片在线观看| 色综合欧美亚洲国产小说| 韩国精品一区二区三区| 久久性视频一级片| 精品国产超薄肉色丝袜足j| 制服诱惑二区| 免费在线观看影片大全网站| 午夜免费激情av| 亚洲五月色婷婷综合| 欧美性猛交黑人性爽| 国产激情欧美一区二区| 久久天堂一区二区三区四区| 午夜成年电影在线免费观看| 亚洲av成人不卡在线观看播放网| 在线观看免费午夜福利视频| 久久香蕉精品热| av超薄肉色丝袜交足视频| 侵犯人妻中文字幕一二三四区| 欧美激情高清一区二区三区| 女人爽到高潮嗷嗷叫在线视频| 久久久久久久午夜电影| 丁香六月欧美| 老汉色av国产亚洲站长工具| 一级毛片精品| 色综合亚洲欧美另类图片| 一卡2卡三卡四卡精品乱码亚洲| 午夜福利高清视频| 午夜精品久久久久久毛片777| 黄色 视频免费看| 在线观看免费日韩欧美大片| 岛国在线观看网站| 国产黄色小视频在线观看| 无限看片的www在线观看| 性色av乱码一区二区三区2| 午夜日韩欧美国产| 久久中文字幕一级| 757午夜福利合集在线观看| 91成年电影在线观看| 亚洲国产日韩欧美精品在线观看 | 嫩草影院精品99| 国产av一区在线观看免费| 美女午夜性视频免费| 欧美一级毛片孕妇| 国产主播在线观看一区二区| 国产精品永久免费网站| 在线视频色国产色| 一卡2卡三卡四卡精品乱码亚洲| 国产主播在线观看一区二区| 欧美国产日韩亚洲一区| 久久中文看片网| 怎么达到女性高潮| 国产欧美日韩精品亚洲av| 国产99久久九九免费精品| 久久久水蜜桃国产精品网| 黄片播放在线免费| 在线天堂中文资源库| 成人18禁高潮啪啪吃奶动态图| 亚洲,欧美精品.| 看免费av毛片| 亚洲无线在线观看| 国产伦在线观看视频一区| 久久精品国产亚洲av高清一级| 美女国产高潮福利片在线看| 午夜福利在线观看吧| 欧美成人午夜精品| 欧美成狂野欧美在线观看| 久久久久久九九精品二区国产 | 日本三级黄在线观看| 亚洲激情在线av| 啦啦啦观看免费观看视频高清| 宅男免费午夜| 中文字幕最新亚洲高清| 日本精品一区二区三区蜜桃| 国产人伦9x9x在线观看| 欧美激情 高清一区二区三区| 欧美大码av| 久久精品影院6| 亚洲国产欧美网| 日日干狠狠操夜夜爽| 国语自产精品视频在线第100页| 欧美成人一区二区免费高清观看 | 成人18禁在线播放| 亚洲精品色激情综合| 国产1区2区3区精品| 天天添夜夜摸| 中文字幕精品免费在线观看视频| av视频在线观看入口| 亚洲五月色婷婷综合| 十八禁人妻一区二区| 一进一出抽搐gif免费好疼| 人人妻人人澡人人看| 亚洲第一av免费看| 国产av一区在线观看免费| 波多野结衣高清作品| 日日摸夜夜添夜夜添小说| 制服丝袜大香蕉在线| 亚洲专区国产一区二区| 久久性视频一级片| 神马国产精品三级电影在线观看 | 我的亚洲天堂| 一个人免费在线观看的高清视频| 久久久久国产精品人妻aⅴ院| 1024视频免费在线观看| 在线观看www视频免费| 免费在线观看亚洲国产| 搡老岳熟女国产| 日本在线视频免费播放| 亚洲久久久国产精品| netflix在线观看网站| 亚洲av第一区精品v没综合| 亚洲一区中文字幕在线| 亚洲五月婷婷丁香| 日韩欧美国产一区二区入口| 少妇的丰满在线观看| 欧美午夜高清在线| 国产亚洲精品久久久久5区| 搞女人的毛片| 一边摸一边抽搐一进一小说| 丝袜在线中文字幕| 国产97色在线日韩免费| 午夜福利一区二区在线看| 可以在线观看毛片的网站| 亚洲av电影在线进入| 好看av亚洲va欧美ⅴa在| av视频在线观看入口| 精品不卡国产一区二区三区| 给我免费播放毛片高清在线观看| 久久婷婷成人综合色麻豆| 可以在线观看的亚洲视频| 欧美+亚洲+日韩+国产| 日本三级黄在线观看| 国产一区二区在线av高清观看| 欧美性长视频在线观看| 嫁个100分男人电影在线观看| 国产亚洲精品久久久久久毛片| 久久香蕉激情| 国产精品影院久久| 午夜福利成人在线免费观看| 1024香蕉在线观看| 夜夜躁狠狠躁天天躁| 成人免费观看视频高清| 免费在线观看视频国产中文字幕亚洲| 日本 欧美在线| 亚洲精品中文字幕在线视频| 老司机午夜十八禁免费视频| 男女下面进入的视频免费午夜 | 亚洲精品国产区一区二| 99热6这里只有精品| 午夜福利欧美成人| 黑人欧美特级aaaaaa片| 国产精品日韩av在线免费观看|