/[mojave]/metaprl/theories/czf/czf_itt_equiv.ml
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_equiv.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3551 by xiny, Sun Mar 24 11:01:50 2002 UTC revision 3552 by xiny, Tue Apr 2 07:28:45 2002 UTC
# Line 118  Line 118 
118     sequent [squash] { 'H >- isset{'b} } -->     sequent [squash] { 'H >- isset{'b} } -->
119     sequent ['ext] { 'H >- "type"{equiv{'s; 'r; 'a; 'b}} }     sequent ['ext] { 'H >- "type"{equiv{'s; 'r; 'a; 'b}} }
120    
 interactive equiv_intro {| intro [] |} 'H :  
    [wf] sequent [squash] { 'H >- isset{'s} } -->  
    [wf] sequent [squash] { 'H >- isset{'r} } -->  
    [wf] sequent [squash] { 'H >- isset{'a} } -->  
    [wf] sequent [squash] { 'H >- isset{'b} } -->  
    sequent ['ext] { 'H >- mem{'a; 's} } -->  
    sequent ['ext] { 'H >- mem{'b; 's} } -->  
    sequent ['ext] { 'H >- mem{pair{'a; 'b}; 'r} } -->  
    sequent ['ext] { 'H >- equiv{'s; 'r; 'a; 'b} }  
   
121  (*  (*
122   * An equivalence relation on a set S is a relation   * An equivalence relation on a set S is a relation
123   * on S satisfying reflexivity, symmetry, and transitivity.   * on S satisfying reflexivity, symmetry, and transitivity.

Legend:
Removed from v.3551  
changed lines
  Added in v.3552

  ViewVC Help
Powered by ViewVC 1.1.26