The abstract of the Mizar article:

Introducing Spans

by

Andrzej Trybulec

Received May 27, 2002

MML identifier: JORDAN13

[ Mizar article, MML identifier index ]

environ

 vocabulary JORDAN13, JORDAN11, FINSEQ_1, TOPREAL1, GOBOARD1, BOOLE, JORDAN1H,
      FINSEQ_4, EUCLID, MATRIX_1, PRE_TOPC, SEQM_3, SPPOL_1, SPRECT_2,
      GOBOARD5, ABSVALUE, CONNSP_1, TOPREAL2, ARYTM_1, TOPS_1, RELAT_1,
      FUNCT_1, SUBSET_1, RELAT_2, RFINSEQ, GOBOARD9, TARSKI, TREES_1, CARD_1,
      JORDAN8, GOBRD13, FINSEQ_5, JORDAN2C, METRIC_1, PCOMPS_1, GROUP_1, ARYTM;
 notation TARSKI, GOBOARD5, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS,
      XREAL_0, REAL_1, NAT_1, BINARITH, ABSVALUE, RELAT_1, FUNCT_1, FUNCT_2,
      CARD_1, CARD_4, PARTFUN1, FINSEQ_1, FINSEQ_2, FINSEQ_4, RFINSEQ,
      MATRIX_1, METRIC_1, PRE_TOPC, TOPS_1, CONNSP_1, PCOMPS_1, EUCLID,
      TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, SPRECT_2, GOBOARD9, JORDAN8,
      GOBRD13, JORDAN2C, JORDAN1H, JORDAN11;
 constructors REAL_1, FINSEQ_4, CARD_4, RFINSEQ, BINARITH, TOPS_1, CONNSP_1,
      PSCOMP_1, REALSET1, SPRECT_2, GOBOARD9, JORDAN8, JORDAN2C, JORDAN11,
      GROUP_1, TOPREAL4, PARTFUN1, JORDAN1H, MEMBERED;
 clusters RELSET_1, FINSEQ_1, SPPOL_2, REVROT_1, SPRECT_2, XREAL_0, GOBOARD9,
      JORDAN8, GOBRD13, SUBSET_1, TOPREAL6, SPRECT_3, INT_1, EUCLID, JORDAN1A,
      MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;


begin :: Spans

 reserve i, j, k, l, m, n, i1, i2, j1, j2 for Nat;

definition let C be non vertical non horizontal non empty
                      being_simple_closed_curve Subset of TOP-REAL 2,
               n be Nat;
  assume
 n is_sufficiently_large_for C;
  func Span(C,n) -> clockwise_oriented
    (standard non constant special_circular_sequence) means
:: JORDAN13:def 1
      it is_sequence_on Gauge(C,n) &
    it/.1 = Gauge(C,n)*(X-SpanStart(C,n),Y-SpanStart(C,n)) &
    it/.2 = Gauge(C,n)*(X-SpanStart(C,n)-'1,Y-SpanStart(C,n)) &
    for k being Nat st 1 <= k & k+2 <= len it holds
      (front_right_cell(it,k,Gauge(C,n)) misses C &
        front_left_cell(it,k,Gauge(C,n)) misses C
          implies it turns_left k,Gauge(C,n)) &
      (front_right_cell(it,k,Gauge(C,n)) misses C &
        front_left_cell(it,k,Gauge(C,n)) meets C
          implies it goes_straight k,Gauge(C,n)) &
      (front_right_cell(it,k,Gauge(C,n)) meets C
        implies it turns_right k,Gauge(C,n));
end;