:: On the Decomposition of Finite Sequences
:: by Andrzej Trybulec
::
:: Received May 24, 1995
:: Copyright (c) 1995 Association of Mizar Users
Lm1:
for x, y being set holds rng <*x,y*> = {x,y}
Lm2:
for x, y, z being set holds rng <*x,y,z*> = {x,y,z}
theorem :: FINSEQ_6:1
canceled;
theorem :: FINSEQ_6:2
canceled;
theorem Th3: :: FINSEQ_6:3
theorem Th4: :: FINSEQ_6:4
theorem Th5: :: FINSEQ_6:5
theorem Th6: :: FINSEQ_6:6
theorem Th7: :: FINSEQ_6:7
theorem Th8: :: FINSEQ_6:8
theorem Th9: :: FINSEQ_6:9
theorem Th10: :: FINSEQ_6:10
theorem Th11: :: FINSEQ_6:11
theorem Th12: :: FINSEQ_6:12
theorem :: FINSEQ_6:13
theorem Th14: :: FINSEQ_6:14
theorem Th15: :: FINSEQ_6:15
theorem Th16: :: FINSEQ_6:16
theorem Th17: :: FINSEQ_6:17
theorem :: FINSEQ_6:18
canceled;
theorem Th19: :: FINSEQ_6:19
theorem :: FINSEQ_6:20
theorem :: FINSEQ_6:21
canceled;
theorem Th22: :: FINSEQ_6:22
theorem Th23: :: FINSEQ_6:23
theorem Th24: :: FINSEQ_6:24
theorem Th25: :: FINSEQ_6:25
for
p1,
p2,
p3 being
set holds
p1 .. <*p1,p2,p3*> = 1
theorem Th26: :: FINSEQ_6:26
for
p1,
p2,
p3 being
set st
p1 <> p2 holds
p2 .. <*p1,p2,p3*> = 2
theorem Th27: :: FINSEQ_6:27
for
p1,
p3,
p2 being
set st
p1 <> p3 &
p2 <> p3 holds
p3 .. <*p1,p2,p3*> = 3
theorem Th28: :: FINSEQ_6:28
theorem Th29: :: FINSEQ_6:29
theorem Th30: :: FINSEQ_6:30
theorem Th31: :: FINSEQ_6:31
theorem Th32: :: FINSEQ_6:32
theorem :: FINSEQ_6:33
theorem Th34: :: FINSEQ_6:34
theorem :: FINSEQ_6:35
theorem Th36: :: FINSEQ_6:36
theorem Th37: :: FINSEQ_6:37
theorem Th38: :: FINSEQ_6:38
theorem Th39: :: FINSEQ_6:39
theorem Th40: :: FINSEQ_6:40
theorem Th41: :: FINSEQ_6:41
theorem Th42: :: FINSEQ_6:42
theorem :: FINSEQ_6:43
theorem Th44: :: FINSEQ_6:44
theorem Th45: :: FINSEQ_6:45
theorem Th46: :: FINSEQ_6:46
theorem Th47: :: FINSEQ_6:47
theorem Th48: :: FINSEQ_6:48
theorem Th49: :: FINSEQ_6:49
theorem Th50: :: FINSEQ_6:50
theorem Th51: :: FINSEQ_6:51
theorem Th52: :: FINSEQ_6:52
theorem Th53: :: FINSEQ_6:53
theorem Th54: :: FINSEQ_6:54
theorem Th55: :: FINSEQ_6:55
theorem :: FINSEQ_6:56
theorem Th57: :: FINSEQ_6:57
theorem Th58: :: FINSEQ_6:58
theorem Th59: :: FINSEQ_6:59
theorem :: FINSEQ_6:60
canceled;
theorem Th61: :: FINSEQ_6:61
theorem Th62: :: FINSEQ_6:62
theorem Th63: :: FINSEQ_6:63
theorem Th64: :: FINSEQ_6:64
theorem Th65: :: FINSEQ_6:65
theorem Th66: :: FINSEQ_6:66
theorem Th67: :: FINSEQ_6:67
theorem Th68: :: FINSEQ_6:68
theorem Th69: :: FINSEQ_6:69
theorem Th70: :: FINSEQ_6:70
theorem Th71: :: FINSEQ_6:71
theorem Th72: :: FINSEQ_6:72
theorem :: FINSEQ_6:73
theorem Th74: :: FINSEQ_6:74
theorem Th75: :: FINSEQ_6:75
theorem Th76: :: FINSEQ_6:76
theorem Th77: :: FINSEQ_6:77
theorem Th78: :: FINSEQ_6:78
theorem Th79: :: FINSEQ_6:79
theorem Th80: :: FINSEQ_6:80
theorem Th81: :: FINSEQ_6:81
theorem Th82: :: FINSEQ_6:82
theorem Th83: :: FINSEQ_6:83
theorem Th84: :: FINSEQ_6:84
Lm3:
for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > i holds
i + (p .. (f /^ i)) = p .. f
theorem :: FINSEQ_6:85
canceled;
theorem Th86: :: FINSEQ_6:86
theorem Th87: :: FINSEQ_6:87
theorem Th88: :: FINSEQ_6:88
theorem Th89: :: FINSEQ_6:89
theorem Th90: :: FINSEQ_6:90
theorem Th91: :: FINSEQ_6:91
theorem Th92: :: FINSEQ_6:92
theorem Th93: :: FINSEQ_6:93
theorem Th94: :: FINSEQ_6:94
:: deftheorem Def1 defines circular FINSEQ_6:def 1 :
:: deftheorem Def2 defines Rotate FINSEQ_6:def 2 :
theorem Th95: :: FINSEQ_6:95
theorem :: FINSEQ_6:96
theorem Th97: :: FINSEQ_6:97
theorem Th98: :: FINSEQ_6:98
theorem Th99: :: FINSEQ_6:99
theorem :: FINSEQ_6:100
theorem Th101: :: FINSEQ_6:101
theorem :: FINSEQ_6:102
theorem Th103: :: FINSEQ_6:103
theorem :: FINSEQ_6:104
theorem :: FINSEQ_6:105
theorem :: FINSEQ_6:106
theorem Th107: :: FINSEQ_6:107
theorem Th108: :: FINSEQ_6:108
theorem Th109: :: FINSEQ_6:109
theorem Th110: :: FINSEQ_6:110
theorem :: FINSEQ_6:111
theorem :: FINSEQ_6:112
theorem :: FINSEQ_6:113