Nuprl Definition : mFOLeffect

The effect of a given rule r on a 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 L is the list of subgoal sequents.⋅
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 (∀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 x then a else b fi >];
        if concl ∈b hyps) then inl [] else inr ⋅  fi ;i.if i <z ||hyps||
        then let a,b = dest-"and"(hyps[i]) in
             inl [<[a; [b / hyps]], concl>]
        else inr ⋅ 
        fi ;
        i.if i <z ||hyps|| then let a,b = dest-"or"(hyps[i]) in inl [<[a / hyps], concl>; <[b / hyps], concl>] else inr \000C⋅  fi ;
        i.if i <z ||hyps|| then let a,b = dest-"imp"(hyps[i]) in inl [<hyps, a>; <[b / hyps], concl>] else inr ⋅  fi ;
        i,v.if i <z ||hyps|| then let x,b = dest-all(hyps[i]); in inl [<[b[v/x] / hyps], concl>] else inr ⋅  fi ;
        i,v.if i <z ||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 b then t else f fi ,  lt_int: i <z j,  bfalse: ff,  btrue: tt,  it: ⋅,  spread: spread def,  pair: <a, b>,  inr: inr x ,  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