Nuprl Definition : Form_ind

Form_ind(v;
         FormVar(name)⇒ Var[name];
         FormConst(value)⇒ Const[value];
         FormSet(var,phi)⇒ rec1.Set[var; phi; rec1];
         FormEqual(left,right)⇒ rec2,rec3.Equal[left; right; rec2; rec3];
         FormMember(element,set)⇒ rec4,rec5.Member[element; set; rec4; rec5];
         FormAnd(left,right)⇒ rec6,rec7.And[left; right; rec6; rec7];
         FormOr(left,right)⇒ rec8,rec9.Or[left; right; rec8; rec9];
         FormNot(body)⇒ rec10.Not[body; rec10];
         FormAll(var,body)⇒ rec11.All[var; body; rec11];
         FormExists(var,body)⇒ rec12.Exists[var; body; rec12])  ==
  fix((λForm_ind,v. let lbl,v1 = v 
                    in if lbl="Var" then Var[v1]
                       if lbl="Const" then Const[v1]
                       if lbl="Set" then let var,v2 = v1 in Set[var; v2; Form_ind v2]
                       if lbl="Equal" then let left,v2 = v1 in Equal[left; v2; Form_ind left; Form_ind v2]
                       if lbl="Member" then let element,v2 = v1 in Member[element; v2; Form_ind element; Form_ind v2]
                       if lbl="And" then let left,v2 = v1 in And[left; v2; Form_ind left; Form_ind v2]
                       if lbl="Or" then let left,v2 = v1 in Or[left; v2; Form_ind left; Form_ind v2]
                       if lbl="Not" then Not[v1; Form_ind v1]
                       if lbl="All" then let var,v2 = v1 in All[var; v2; Form_ind v2]
                       if lbl="Exists" then let var,v2 = v1 in Exists[var; v2; Form_ind v2]
                       else Ax
                       fi )) 
  v


Definitions occuring in Statement :  atom_eq: if a=b then c else d fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  token: "$token",  axiom: Ax
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  atom_eq: if a=b then c else d fi ,  token: "$token",  spread: spread def,  apply: f a,  axiom: Ax
FDL editor aliases :  Form_ind Form_ind
Latex:
Form\_ind(v;
                  FormVar(name){}\mRightarrow{}  Var[name];
                  FormConst(value){}\mRightarrow{}  Const[value];
                  FormSet(var,phi){}\mRightarrow{}  rec1.Set[var;  phi;  rec1];
                  FormEqual(left,right){}\mRightarrow{}  rec2,rec3.Equal[left;  right;  rec2;  rec3];
                  FormMember(element,set){}\mRightarrow{}  rec4,rec5.Member[element;  set;  rec4;  rec5];
                  FormAnd(left,right){}\mRightarrow{}  rec6,rec7.And[left;  right;  rec6;  rec7];
                  FormOr(left,right){}\mRightarrow{}  rec8,rec9.Or[left;  right;  rec8;  rec9];
                  FormNot(body){}\mRightarrow{}  rec10.Not[body;  rec10];
                  FormAll(var,body){}\mRightarrow{}  rec11.All[var;  body;  rec11];
                  FormExists(var,body){}\mRightarrow{}  rec12.Exists[var;  body;  rec12])    ==
    fix((\mlambda{}Form$_{ind}$,v.  let  lbl,v1  =  v 
                                      in  if  lbl="Var"  then  Var[v1]
                                            if  lbl="Const"  then  Const[v1]
                                            if  lbl="Set"  then  let  var,v2  =  v1  in  Set[var;  v2;  Form$_{ind}\mbackslash{}\000Cff24  v2]
                                            if  lbl="Equal"
                                                then  let  left,v2  =  v1 
                                                          in  Equal[left;  v2;  Form$_{ind}$  left;  Form$\mbackslash{}ff5\000Cf{ind}$  v2]
                                            if  lbl="Member"
                                                then  let  element,v2  =  v1 
                                                          in  Member[element;  v2;  Form$_{ind}$  element;  Form\mbackslash{}f\000Cf24_{ind}$  v2]
                                            if  lbl="And"  then  let  left,v2  =  v1  in  And[left;  v2;  Form$_{ind\mbackslash{}ff7\000Cd$  left;  Form$_{ind}$  v2]
                                            if  lbl="Or"  then  let  left,v2  =  v1  in  Or[left;  v2;  Form$_{ind}\mbackslash{}\000Cff24  left;  Form$_{ind}$  v2]
                                            if  lbl="Not"  then  Not[v1;  Form$_{ind}$  v1]
                                            if  lbl="All"  then  let  var,v2  =  v1  in  All[var;  v2;  Form$_{ind}\mbackslash{}\000Cff24  v2]
                                            if  lbl="Exists"  then  let  var,v2  =  v1  in  Exists[var;  v2;  Form$_{ind\000C}$  v2]
                                            else  Ax
                                            fi  )) 
    v


Date html generated: 2018_05_21-PM-11_25_49
Last ObjectModification: 2017_10_10-PM-04_36_03

Theory : PZF


Home Index