Nuprl Definition : mFOLeffect

The effect of given rule on given mFOL sequent s.
If the rule does not apply, then it `fails` by producing the effect ⌈inr ⋅ ⌉
otherwise it succeeds and produces ⌈inl L⌉where is the list of subgoal sequents.⋅

mFOLeffect(sr) ==
  let s,r sr 
  in let hyps,concl 
     in mFOLRule_ind(r;
        let a,b dest-"and"(concl) in
        inl [<hyps, a>; <hyps, b>];
        let a,b dest-"imp"(concl) in
        inl [<[a hyps], b>];
        v.if (∀h∈hyps.¬bv ∈b mFOL-freevars(h)))_b ∧b bv ∈b mFOL-freevars(concl)))
        then let x,b dest-all(concl); in
              inl [<hyps, b[v/x]>]
        else inr ⋅ 
        fi ;
        v.let x,b dest-exists(concl); in
           inl [<hyps, b[v/x]>];
        x.let a,b dest-"or"(concl) in
          inl [<hyps, if then else fi >];
        if concl ∈b hyps) then inl [] else inr ⋅  fi ;i.if i <||hyps||
        then let a,b dest-"and"(hyps[i]) in
             inl [<[a; [b hyps]], concl>]
        else inr ⋅ 
        fi ;
        i.if i <||hyps|| then let a,b dest-"or"(hyps[i]) in inl [<[a hyps], concl>; <[b hyps], concl>else inr \000C⋅  fi ;
        i.if i <||hyps|| then let a,b dest-"imp"(hyps[i]) in inl [<hyps, a>; <[b hyps], concl>else inr ⋅  fi ;
        i,v.if i <||hyps|| then let x,b dest-all(hyps[i]); in inl [<[b[v/x] hyps], concl>else inr ⋅  fi ;
        i,v.if i <||hyps|| ∧b (∀h∈hyps.¬bv ∈b mFOL-freevars(h)))_b ∧b bv ∈b mFOL-freevars(concl)))
        then let x,b dest-exists(hyps[i]); in
              inl [<[b[v/x] hyps], concl>]
        else inr ⋅ 
        fi )

Definitions occuring in Statement :  mFOLRule_ind: mFOLRule_ind mFOL-subst: fmla[nw/old] mFOL-freevars: mFOL-freevars(fmla) deq-mFO: deq-mFO() mFO-dest-quantifier: mFO-dest-quantifier mFO-dest-connective: mFO-dest-connective deq-member: x ∈b L) int-deq: IntDeq bl-all: (∀x∈L.P[x])_b select: L[n] length: ||as|| cons: [a b] nil: [] band: p ∧b q bnot: ¬bb ifthenelse: if then else fi  lt_int: i <j bfalse: ff btrue: tt it: spread: spread def pair: <a, b> inr: inr  inl: inl x token: "$token"
FDL editor aliases :  mFOLeffect
mFOLeffect(sr)  ==
    let  s,r  =  sr 
    in  let  hyps,concl  =  s 
          in  mFOLRule\_ind(r;
                let  a,b  =  dest-"and"(concl)  in
                inl  [<hyps,  a>  <hyps,  b>];
                let  a,b  =  dest-"imp"(concl)  in
                inl  [<[a  /  hyps],  b>];
                v.if  (\mforall{}h\mmember{}hyps.\mneg{}\msubb{}v  \mmember{}\msubb{}  mFOL-freevars(h)))\_b  \mwedge{}\msubb{}  (\mneg{}\msubb{}v  \mmember{}\msubb{}  mFOL-freevars(concl)))
                then  let  x,b  =  dest-all(concl);  in
                            inl  [<hyps,  b[v/x]>]
                else  inr  \mcdot{} 
                fi  ;
                v.let  x,b  =  dest-exists(concl);  in
                      inl  [<hyps,  b[v/x]>];
                x.let  a,b  =  dest-"or"(concl)  in
                    inl  [<hyps,  if  x  then  a  else  b  fi  >];
                if  concl  \mmember{}\msubb{}  hyps)  then  inl  []  else  inr  \mcdot{}    fi  ;i.if  i  <z  ||hyps||
                then  let  a,b  =  dest-"and"(hyps[i])  in
                          inl  [<[a;  [b  /  hyps]],  concl>]
                else  inr  \mcdot{} 
                fi  ;
                i.if  i  <z  ||hyps||
                then  let  a,b  =  dest-"or"(hyps[i])  in
                          inl  [<[a  /  hyps],  concl>  <[b  /  hyps],  concl>]
                else  inr  \mcdot{} 
                fi  ;
                i.if  i  <z  ||hyps||
                then  let  a,b  =  dest-"imp"(hyps[i])  in
                          inl  [<hyps,  a>  <[b  /  hyps],  concl>]
                else  inr  \mcdot{} 
                fi  ;
                i,v.if  i  <z  ||hyps||  then  let  x,b  =  dest-all(hyps[i]);  in  inl  [<[b[v/x]  /  hyps],  concl>]  els\000Ce  inr  \mcdot{}    fi  ;
                i,v.if  i  <z  ||hyps||
                              \mwedge{}\msubb{}  (\mforall{}h\mmember{}hyps.\mneg{}\msubb{}v  \mmember{}\msubb{}  mFOL-freevars(h)))\_b
                              \mwedge{}\msubb{}  (\mneg{}\msubb{}v  \mmember{}\msubb{}  mFOL-freevars(concl)))
                then  let  x,b  =  dest-exists(hyps[i]);  in
                            inl  [<[b[v/x]  /  hyps],  concl>]
                else  inr  \mcdot{} 
                fi  )

Date html generated: 2015_07_17-AM-07_56_42
Last ObjectModification: 2012_09_11-PM-05_46_30

Home Index